[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s₁ s₂ : Multiset α
⊢ lcm (s₁ + s₂) = fold GCDMonoid.lcm (GCDMonoid.lcm 1 1) (s₁ + s₂)
[PROOFSTEP]
simp [lcm]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ lcm 0 ∣ a ↔ ∀ (b : α), b ∈ 0 → b ∣ a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ ∀ ⦃a_1 : α⦄ {s : Multiset α},
    (lcm s ∣ a ↔ ∀ (b : α), b ∈ s → b ∣ a) → (lcm (a_1 ::ₘ s) ∣ a ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → b ∣ a)
[PROOFSTEP]
simp (config := { contextual := true }) [or_imp, forall_and, lcm_dvd_iff]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ ↑normalize (lcm 0) = lcm 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s✝ : Multiset α
a : α
s : Multiset α
x✝ : ↑normalize (lcm s) = lcm s
⊢ ↑normalize (lcm (a ::ₘ s)) = lcm (a ::ₘ s)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : Nontrivial α
s : Multiset α
⊢ lcm s = 0 ↔ 0 ∈ s
[PROOFSTEP]
induction' s using Multiset.induction_on with a s ihs
[GOAL]
case empty
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : Nontrivial α
⊢ lcm 0 = 0 ↔ 0 ∈ 0
[PROOFSTEP]
simp only [lcm_zero, one_ne_zero, not_mem_zero]
[GOAL]
case cons
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : Nontrivial α
a : α
s : Multiset α
ihs : lcm s = 0 ↔ 0 ∈ s
⊢ lcm (a ::ₘ s) = 0 ↔ 0 ∈ a ::ₘ s
[PROOFSTEP]
simp only [mem_cons, lcm_cons, lcm_eq_zero_iff, ihs, @eq_comm _ a]
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s : Multiset α
⊢ lcm (dedup 0) = lcm 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : lcm (dedup s) = lcm s
⊢ lcm (dedup (a ::ₘ s)) = lcm (a ::ₘ s)
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : lcm (dedup s) = lcm s
h : a ∈ s
⊢ lcm (dedup (a ::ₘ s)) = lcm (a ::ₘ s)
[PROOFSTEP]
simp [IH, h]
[GOAL]
case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : lcm (dedup s) = lcm s
h : ¬a ∈ s
⊢ lcm (dedup (a ::ₘ s)) = lcm (a ::ₘ s)
[PROOFSTEP]
simp [IH, h]
[GOAL]
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : lcm (dedup s) = lcm s
h : a ∈ s
⊢ lcm s = GCDMonoid.lcm a (lcm s)
[PROOFSTEP]
unfold lcm
[GOAL]
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : lcm (dedup s) = lcm s
h : a ∈ s
⊢ fold GCDMonoid.lcm 1 s = GCDMonoid.lcm a (fold GCDMonoid.lcm 1 s)
[PROOFSTEP]
rw [← cons_erase h, fold_cons_left, ← lcm_assoc, lcm_same]
[GOAL]
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : lcm (dedup s) = lcm s
h : a ∈ s
⊢ GCDMonoid.lcm a (fold GCDMonoid.lcm 1 (erase s a)) = GCDMonoid.lcm (↑normalize a) (fold GCDMonoid.lcm 1 (erase s a))
[PROOFSTEP]
apply lcm_eq_of_associated_left (associated_normalize _)
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ lcm (ndunion s₁ s₂) = GCDMonoid.lcm (lcm s₁) (lcm s₂)
[PROOFSTEP]
rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_add]
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ ndunion s₁ s₂ ↔ a ∈ s₁ + s₂
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ lcm (s₁ ∪ s₂) = GCDMonoid.lcm (lcm s₁) (lcm s₂)
[PROOFSTEP]
rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_add]
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ lcm (ndinsert a s) = GCDMonoid.lcm a (lcm s)
[PROOFSTEP]
rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_cons]
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s₁ s₂ : Multiset α
⊢ gcd (s₁ + s₂) = fold GCDMonoid.gcd (GCDMonoid.gcd 0 0) (s₁ + s₂)
[PROOFSTEP]
simp [gcd]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ a ∣ gcd 0 ↔ ∀ (b : α), b ∈ 0 → a ∣ b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ ∀ ⦃a_1 : α⦄ {s : Multiset α},
    (a ∣ gcd s ↔ ∀ (b : α), b ∈ s → a ∣ b) → (a ∣ gcd (a_1 ::ₘ s) ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → a ∣ b)
[PROOFSTEP]
simp (config := { contextual := true }) [or_imp, forall_and, dvd_gcd_iff]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ ↑normalize (gcd 0) = gcd 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s✝ : Multiset α
a : α
s : Multiset α
x✝ : ↑normalize (gcd s) = gcd s
⊢ ↑normalize (gcd (a ::ₘ s)) = gcd (a ::ₘ s)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ gcd s = 0 ↔ ∀ (x : α), x ∈ s → x = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ gcd s = 0 → ∀ (x : α), x ∈ s → x = 0
[PROOFSTEP]
intro h x hx
[GOAL]
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : gcd s = 0
x : α
hx : x ∈ s
⊢ x = 0
[PROOFSTEP]
apply eq_zero_of_zero_dvd
[GOAL]
case mp.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : gcd s = 0
x : α
hx : x ∈ s
⊢ 0 ∣ x
[PROOFSTEP]
rw [← h]
[GOAL]
case mp.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : gcd s = 0
x : α
hx : x ∈ s
⊢ gcd s ∣ x
[PROOFSTEP]
apply gcd_dvd hx
[GOAL]
case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ s → x = 0) → gcd s = 0
[PROOFSTEP]
refine' s.induction_on _ _
[GOAL]
case mpr.refine'_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ 0 → x = 0) → gcd 0 = 0
[PROOFSTEP]
simp
[GOAL]
case mpr.refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((∀ (x : α), x ∈ s → x = 0) → gcd s = 0) → (∀ (x : α), x ∈ a ::ₘ s → x = 0) → gcd (a ::ₘ s) = 0
[PROOFSTEP]
intro a s sgcd h
[GOAL]
case mpr.refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s✝ : Multiset α
a : α
s : Multiset α
sgcd : (∀ (x : α), x ∈ s → x = 0) → gcd s = 0
h : ∀ (x : α), x ∈ a ::ₘ s → x = 0
⊢ gcd (a ::ₘ s) = 0
[PROOFSTEP]
simp [h a (mem_cons_self a s), sgcd fun x hx ↦ h x (mem_cons_of_mem hx)]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ gcd (map ((fun x x_1 => x * x_1) a) s) = ↑normalize a * gcd s
[PROOFSTEP]
refine' s.induction_on _ fun b s ih ↦ _
[GOAL]
case refine'_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ gcd (map ((fun x x_1 => x * x_1) a) 0) = ↑normalize a * gcd 0
[PROOFSTEP]
simp_rw [map_zero, gcd_zero, mul_zero]
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : gcd (map ((fun x x_1 => x * x_1) a) s) = ↑normalize a * gcd s
⊢ gcd (map ((fun x x_1 => x * x_1) a) (b ::ₘ s)) = ↑normalize a * gcd (b ::ₘ s)
[PROOFSTEP]
simp_rw [map_cons, gcd_cons, ← gcd_mul_left]
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : gcd (map ((fun x x_1 => x * x_1) a) s) = ↑normalize a * gcd s
⊢ GCDMonoid.gcd (a * b) (gcd (map (fun x => a * x) s)) = GCDMonoid.gcd (a * b) (a * gcd s)
[PROOFSTEP]
rw [ih]
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : gcd (map ((fun x x_1 => x * x_1) a) s) = ↑normalize a * gcd s
⊢ GCDMonoid.gcd (a * b) (↑normalize a * gcd s) = GCDMonoid.gcd (a * b) (a * gcd s)
[PROOFSTEP]
apply ((normalize_associated a).mul_right _).gcd_eq_right
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s : Multiset α
⊢ gcd (dedup 0) = gcd 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
⊢ gcd (dedup (a ::ₘ s)) = gcd (a ::ₘ s)
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
h : a ∈ s
⊢ gcd (dedup (a ::ₘ s)) = gcd (a ::ₘ s)
[PROOFSTEP]
simp [IH, h]
[GOAL]
case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
h : ¬a ∈ s
⊢ gcd (dedup (a ::ₘ s)) = gcd (a ::ₘ s)
[PROOFSTEP]
simp [IH, h]
[GOAL]
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
h : a ∈ s
⊢ gcd s = GCDMonoid.gcd a (gcd s)
[PROOFSTEP]
unfold gcd
[GOAL]
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
h : a ∈ s
⊢ fold GCDMonoid.gcd 0 s = GCDMonoid.gcd a (fold GCDMonoid.gcd 0 s)
[PROOFSTEP]
rw [← cons_erase h, fold_cons_left, ← gcd_assoc, gcd_same]
[GOAL]
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
h : a ∈ s
⊢ GCDMonoid.gcd a (fold GCDMonoid.gcd 0 (erase s a)) = GCDMonoid.gcd (↑normalize a) (fold GCDMonoid.gcd 0 (erase s a))
[PROOFSTEP]
apply (associated_normalize _).gcd_eq_left
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ gcd (ndunion s₁ s₂) = GCDMonoid.gcd (gcd s₁) (gcd s₂)
[PROOFSTEP]
rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add]
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ ndunion s₁ s₂ ↔ a ∈ s₁ + s₂
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ gcd (s₁ ∪ s₂) = GCDMonoid.gcd (gcd s₁) (gcd s₂)
[PROOFSTEP]
rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add]
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ gcd (ndinsert a s) = GCDMonoid.gcd a (gcd s)
[PROOFSTEP]
rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_cons]
[GOAL]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x, x ∈ s ∧ x ≠ 0
ht : s = map ((fun x x_1 => x * x_1) (gcd s)) t
⊢ gcd s * gcd t = gcd s
[PROOFSTEP]
conv_lhs => rw [← normalize_gcd, ← gcd_map_mul, ← ht]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x, x ∈ s ∧ x ≠ 0
ht : s = map ((fun x x_1 => x * x_1) (gcd s)) t
| gcd s * gcd t
[PROOFSTEP]
rw [← normalize_gcd, ← gcd_map_mul, ← ht]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x, x ∈ s ∧ x ≠ 0
ht : s = map ((fun x x_1 => x * x_1) (gcd s)) t
| gcd s * gcd t
[PROOFSTEP]
rw [← normalize_gcd, ← gcd_map_mul, ← ht]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x, x ∈ s ∧ x ≠ 0
ht : s = map ((fun x x_1 => x * x_1) (gcd s)) t
| gcd s * gcd t
[PROOFSTEP]
rw [← normalize_gcd, ← gcd_map_mul, ← ht]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x, x ∈ s ∧ x ≠ 0
ht : s = map ((fun x x_1 => x * x_1) (gcd s)) t
⊢ ¬gcd s = 0
[PROOFSTEP]
contrapose! hs
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
ht : s = map ((fun x x_1 => x * x_1) (gcd s)) t
hs : gcd s = 0
⊢ ∀ (x : α), x ∈ s → x = 0
[PROOFSTEP]
exact s.gcd_eq_zero_iff.1 hs
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
⊢ ∃ t, s = map ((fun x x_1 => x * x_1) (gcd s)) t ∧ gcd t = 1
[PROOFSTEP]
classical
by_cases h : ∀ x ∈ s, x = (0 : α)
· use replicate (card s) 1
  simp only
  rw [map_replicate, eq_replicate, mul_one, s.gcd_eq_zero_iff.2 h, ← nsmul_singleton, ← gcd_dedup,
    dedup_nsmul (card_pos.2 hs).ne', dedup_singleton, gcd_singleton]
  exact ⟨⟨rfl, h⟩, normalize_one⟩
· choose f hf using @gcd_dvd _ _ _ s
  push_neg at h
  refine' ⟨s.pmap @f fun _ ↦ id, _, extract_gcd' s _ h _⟩ <;>
    · rw [map_pmap]
      conv_lhs => rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
      congr with (x hx)
      simp only
      rw [id]
      rw [← hf hx]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
⊢ ∃ t, s = map ((fun x x_1 => x * x_1) (gcd s)) t ∧ gcd t = 1
[PROOFSTEP]
by_cases h : ∀ x ∈ s, x = (0 : α)
[GOAL]
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ ∃ t, s = map ((fun x x_1 => x * x_1) (gcd s)) t ∧ gcd t = 1
[PROOFSTEP]
use replicate (card s) 1
[GOAL]
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ s = map ((fun x x_1 => x * x_1) (gcd s)) (replicate (↑card s) 1) ∧ gcd (replicate (↑card s) 1) = 1
[PROOFSTEP]
simp only
[GOAL]
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ s = map (fun x => gcd s * x) (replicate (↑card s) 1) ∧ gcd (replicate (↑card s) 1) = 1
[PROOFSTEP]
rw [map_replicate, eq_replicate, mul_one, s.gcd_eq_zero_iff.2 h, ← nsmul_singleton, ← gcd_dedup,
  dedup_nsmul (card_pos.2 hs).ne', dedup_singleton, gcd_singleton]
[GOAL]
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ (↑card s = ↑card s ∧ ∀ (b : α), b ∈ s → b = 0) ∧ ↑normalize 1 = 1
[PROOFSTEP]
exact ⟨⟨rfl, h⟩, normalize_one⟩
[GOAL]
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ¬∀ (x : α), x ∈ s → x = 0
⊢ ∃ t, s = map ((fun x x_1 => x * x_1) (gcd s)) t ∧ gcd t = 1
[PROOFSTEP]
choose f hf using @gcd_dvd _ _ _ s
[GOAL]
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ¬∀ (x : α), x ∈ s → x = 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
⊢ ∃ t, s = map ((fun x x_1 => x * x_1) (gcd s)) t ∧ gcd t = 1
[PROOFSTEP]
push_neg at h
[GOAL]
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ ∃ t, s = map ((fun x x_1 => x * x_1) (gcd s)) t ∧ gcd t = 1
[PROOFSTEP]
refine' ⟨s.pmap @f fun _ ↦ id, _, extract_gcd' s _ h _⟩
[GOAL]
case neg.refine'_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ s = map ((fun x x_1 => x * x_1) (gcd s)) (pmap f s (_ : ∀ (x : α), x ∈ s → x ∈ s))
[PROOFSTEP]
rw [map_pmap]
[GOAL]
case neg.refine'_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ s = pmap (fun a h => (fun x x_1 => x * x_1) (gcd s) (f h)) s (_ : ∀ (x : α), x ∈ s → x ∈ s)
[PROOFSTEP]
conv_lhs => rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
| s
[PROOFSTEP]
rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
| s
[PROOFSTEP]
rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
| s
[PROOFSTEP]
rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
[GOAL]
case neg.refine'_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ pmap (fun a x => id a) s (_ : ∀ (x : α), x ∈ s → x ∈ s) =
    pmap (fun a h => (fun x x_1 => x * x_1) (gcd s) (f h)) s (_ : ∀ (x : α), x ∈ s → x ∈ s)
[PROOFSTEP]
congr with (x hx)
[GOAL]
case neg.refine'_1.e_f.h.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
x : α
hx : x ∈ s
⊢ id x = (fun x x_1 => x * x_1) (gcd s) (f hx)
[PROOFSTEP]
simp only
[GOAL]
case neg.refine'_1.e_f.h.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
x : α
hx : x ∈ s
⊢ id x = gcd s * f hx
[PROOFSTEP]
rw [id]
[GOAL]
case neg.refine'_1.e_f.h.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
x : α
hx : x ∈ s
⊢ x = gcd s * f hx
[PROOFSTEP]
rw [← hf hx]
[GOAL]
case neg.refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ s = map ((fun x x_1 => x * x_1) (gcd s)) (pmap f s (_ : ∀ (x : α), x ∈ s → x ∈ s))
[PROOFSTEP]
rw [map_pmap]
[GOAL]
case neg.refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ s = pmap (fun a h => (fun x x_1 => x * x_1) (gcd s) (f h)) s (_ : ∀ (x : α), x ∈ s → x ∈ s)
[PROOFSTEP]
conv_lhs => rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
| s
[PROOFSTEP]
rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
| s
[PROOFSTEP]
rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
| s
[PROOFSTEP]
rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
[GOAL]
case neg.refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ pmap (fun a x => id a) s (_ : ∀ (x : α), x ∈ s → x ∈ s) =
    pmap (fun a h => (fun x x_1 => x * x_1) (gcd s) (f h)) s (_ : ∀ (x : α), x ∈ s → x ∈ s)
[PROOFSTEP]
congr with (x hx)
[GOAL]
case neg.refine'_2.e_f.h.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
x : α
hx : x ∈ s
⊢ id x = (fun x x_1 => x * x_1) (gcd s) (f hx)
[PROOFSTEP]
simp only
[GOAL]
case neg.refine'_2.e_f.h.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
x : α
hx : x ∈ s
⊢ id x = gcd s * f hx
[PROOFSTEP]
rw [id]
[GOAL]
case neg.refine'_2.e_f.h.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = gcd s * f h
h : ∃ x, x ∈ s ∧ x ≠ 0
x : α
hx : x ∈ s
⊢ x = gcd s * f hx
[PROOFSTEP]
rw [← hf hx]


[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedSemiring α
a : α
inst✝ : Invertible a
⊢ 0 < a * ⅟a
[PROOFSTEP]
simp only [mul_invOf_self, zero_lt_one]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedSemiring α
a : α
inst✝ : Invertible a
⊢ ⅟a ≤ 0 ↔ a ≤ 0
[PROOFSTEP]
simp only [← not_lt, invOf_pos]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedSemiring α
a : α
inst✝ : Invertible a
⊢ 0 < a * ⅟a
[PROOFSTEP]
simp only [mul_invOf_self, zero_lt_one]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedSemiring α
a : α
inst✝ : Invertible a
⊢ ⅟a < 0 ↔ a < 0
[PROOFSTEP]
simp only [← not_le, invOf_nonneg]


[GOAL]
R : Type u_1
A : Type u_2
inst✝ : InvolutiveStar R
x : R
⊢ IsSelfAdjoint (star x) ↔ IsSelfAdjoint x
[PROOFSTEP]
simpa only [IsSelfAdjoint, star_star] using eq_comm
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x : R
⊢ IsSelfAdjoint (star x * x)
[PROOFSTEP]
simp only [IsSelfAdjoint, star_mul, star_star]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x : R
⊢ IsSelfAdjoint (x * star x)
[PROOFSTEP]
simpa only [star_star] using star_mul_self (star x)
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddMonoid R
inst✝ : StarAddMonoid R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x + y)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_add, hx.star_eq, hy.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddMonoid R
inst✝ : StarAddMonoid R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint (_root_.bit0 x)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_bit0, hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint (-x)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_neg, hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x - y)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_sub, hx.star_eq, hy.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddCommMonoid R
inst✝ : StarAddMonoid R
x : R
⊢ IsSelfAdjoint (x + star x)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, add_comm, star_add, star_star]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddCommMonoid R
inst✝ : StarAddMonoid R
x : R
⊢ IsSelfAdjoint (star x + x)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, add_comm, star_add, star_star]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x : R
hx : IsSelfAdjoint x
z : R
⊢ IsSelfAdjoint (z * x * star z)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_mul, star_star, mul_assoc, hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x : R
hx : IsSelfAdjoint x
z : R
⊢ IsSelfAdjoint (star z * x * z)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_mul, star_star, mul_assoc, hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x : R
hx : IsSelfAdjoint x
⊢ Commute (star x) x
[PROOFSTEP]
simp only [Commute, SemiconjBy, hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
x : R
hx : IsSelfAdjoint x
n : ℕ
⊢ IsSelfAdjoint (x ^ n)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_pow, hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : StarRing R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint (_root_.bit1 x)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_bit1, hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : CommSemigroup R
inst✝ : StarSemigroup R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x * y)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_mul', hx.star_eq, hy.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : DivisionSemiring R
inst✝ : StarRing R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint x⁻¹
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_inv', hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : DivisionSemiring R
inst✝ : StarRing R
x : R
hx : IsSelfAdjoint x
n : ℤ
⊢ IsSelfAdjoint (x ^ n)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_zpow₀, hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semifield R
inst✝ : StarRing R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x / y)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_div', hx.star_eq, hy.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : Star R
inst✝³ : AddMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : SMul R A
inst✝ : StarModule R A
r : R
hr : IsSelfAdjoint r
x : A
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint (r • x)
[PROOFSTEP]
simp only [isSelfAdjoint_iff, star_smul, hr.star_eq, hx.star_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x y : R
hx : star x = -x
hy : star y = -y
⊢ star (x + y) = -(x + y)
[PROOFSTEP]
rw [star_add x y, hx, hy, neg_add]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
⊢ star 0 = -0
[PROOFSTEP]
simp only [star_zero, neg_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x : R
hx : star x = -x
⊢ star (-x) = - -x
[PROOFSTEP]
simp only [hx, star_neg]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ selfAdjoint R ↔ star x = x
[PROOFSTEP]
rw [← AddSubgroup.mem_carrier]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ (selfAdjoint R).toAddSubmonoid.toAddSubsemigroup.carrier ↔ star x = x
[PROOFSTEP]
exact Iff.rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
a : ℚ
x : { x // x ∈ selfAdjoint R }
⊢ a • ↑x ∈ selfAdjoint R
[PROOFSTEP]
rw [Rat.smul_def]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
a : ℚ
x : { x // x ∈ selfAdjoint R }
⊢ ↑a * ↑x ∈ selfAdjoint R
[PROOFSTEP]
exact IsSelfAdjoint.mul (isSelfAdjoint_ratCast a) x.prop
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ skewAdjoint R ↔ star x = -x
[PROOFSTEP]
rw [← AddSubgroup.mem_carrier]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ (skewAdjoint R).toAddSubmonoid.toAddSubsemigroup.carrier ↔ star x = -x
[PROOFSTEP]
exact Iff.rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x : R
hx : x ∈ skewAdjoint R
⊢ bit0 x ∈ skewAdjoint R
[PROOFSTEP]
rw [mem_iff, star_bit0, mem_iff.mp hx, bit0, bit0, neg_add]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : x ∈ skewAdjoint R
z : R
⊢ z * x * star z ∈ skewAdjoint R
[PROOFSTEP]
simp only [mem_iff, star_mul, star_star, mem_iff.mp hx, neg_mul, mul_neg, mul_assoc]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : x ∈ skewAdjoint R
z : R
⊢ star z * x * z ∈ skewAdjoint R
[PROOFSTEP]
simp only [mem_iff, star_mul, star_star, mem_iff.mp hx, neg_mul, mul_neg, mul_assoc]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : x ∈ skewAdjoint R
⊢ Commute (star x) x
[PROOFSTEP]
simp only [mem_iff] at hx
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : star x = -x
⊢ Commute (star x) x
[PROOFSTEP]
simp only [hx, Commute.neg_left, Commute.refl]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁶ : Star R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : Monoid R
inst✝¹ : DistribMulAction R A
inst✝ : StarModule R A
r : R
x : A
h : x ∈ skewAdjoint A
⊢ r • x ∈ skewAdjoint A
[PROOFSTEP]
rw [mem_iff, star_smul, star_trivial, mem_iff.mp h, smul_neg r]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : StarRing R
⊢ Commute (star 0) 0
[PROOFSTEP]
simp only [Commute.refl, star_comm_self, star_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
⊢ Commute (star 1) 1
[PROOFSTEP]
simp only [Commute.refl, star_comm_self, star_one]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Monoid R
inst✝¹ : StarSemigroup R
x : R
inst✝ : IsStarNormal x
⊢ star (star x) * star x = star x * star (star x)
[PROOFSTEP]
rw [star_star, star_comm_self']
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Monoid R
inst✝¹ : StarSemigroup R
inst✝ : TrivialStar R
x : R
⊢ Commute (star x) x
[PROOFSTEP]
rw [star_trivial]


[GOAL]
R : Type u_1
A : Type u_2
a✝ b✝ : A
r : R
inst✝³ : OrderedCommRing R
inst✝² : OrderedRing A
inst✝¹ : Algebra R A
inst✝ : OrderedSMul R A
a b : R
h : a ≤ b
⊢ ↑(algebraMap R A) a ≤ ↑(algebraMap R A) b
[PROOFSTEP]
rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, ← sub_nonneg, ← sub_smul]
[GOAL]
R : Type u_1
A : Type u_2
a✝ b✝ : A
r : R
inst✝³ : OrderedCommRing R
inst✝² : OrderedRing A
inst✝¹ : Algebra R A
inst✝ : OrderedSMul R A
a b : R
h : a ≤ b
⊢ 0 ≤ (b - a) • 1
[PROOFSTEP]
trans (b - a) • (0 : A)
[GOAL]
R : Type u_1
A : Type u_2
a✝ b✝ : A
r : R
inst✝³ : OrderedCommRing R
inst✝² : OrderedRing A
inst✝¹ : Algebra R A
inst✝ : OrderedSMul R A
a b : R
h : a ≤ b
⊢ 0 ≤ (b - a) • 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
a✝ b✝ : A
r : R
inst✝³ : OrderedCommRing R
inst✝² : OrderedRing A
inst✝¹ : Algebra R A
inst✝ : OrderedSMul R A
a b : R
h : a ≤ b
⊢ (b - a) • 0 ≤ (b - a) • 1
[PROOFSTEP]
exact smul_le_smul_of_nonneg zero_le_one (sub_nonneg.mpr h)