[GOAL]
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
z : A
⊢ ∃ a b, IsUnit (gcd a b) ∧ z * ↑(algebraMap R A) b = ↑(algebraMap R A) a
[PROOFSTEP]
obtain ⟨x, ⟨y, hy⟩, rfl⟩ := IsLocalization.mk'_surjective M z
[GOAL]
case intro.intro.mk
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
⊢ ∃ a b, IsUnit (gcd a b) ∧ mk' A x { val := y, property := hy } * ↑(algebraMap R A) b = ↑(algebraMap R A) a
[PROOFSTEP]
obtain ⟨x', y', hx', hy', hu⟩ := extract_gcd x y
[GOAL]
case intro.intro.mk.intro.intro.intro.intro
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
⊢ ∃ a b, IsUnit (gcd a b) ∧ mk' A x { val := y, property := hy } * ↑(algebraMap R A) b = ↑(algebraMap R A) a
[PROOFSTEP]
use x', y', hu
[GOAL]
case right
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
⊢ mk' A x { val := y, property := hy } * ↑(algebraMap R A) y' = ↑(algebraMap R A) x'
[PROOFSTEP]
rw [mul_comm, IsLocalization.mul_mk'_eq_mk'_of_mul]
[GOAL]
case right
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
⊢ mk' A (y' * x) { val := y, property := hy } = ↑(algebraMap R A) x'
[PROOFSTEP]
convert IsLocalization.mk'_mul_cancel_left (M := M) (S := A) _ _ using 2
[GOAL]
case h.e'_2.h.e'_8
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
⊢ y' * x = ↑{ val := y, property := hy } * x'
[PROOFSTEP]
rw [Subtype.coe_mk, hy', ← mul_comm y', mul_assoc]
[GOAL]
case h.e'_2.h.e'_8
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
⊢ y' * x = y' * (gcd x y * x')
[PROOFSTEP]
conv_lhs => rw [hx']
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
| y' * x
[PROOFSTEP]
rw [hx']
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
| y' * x
[PROOFSTEP]
rw [hx']
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : GCDMonoid R
inst✝² : CommRing A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
| y' * x
[PROOFSTEP]
rw [hx']
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
⊢ ∃ y, ↑(algebraMap R (FractionRing R)) y = X
[PROOFSTEP]
obtain ⟨x, y, hg, he⟩ := IsLocalization.surj_of_gcd_domain (nonZeroDivisors R) X
[GOAL]
case intro.intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
x y : R
hg : IsUnit (gcd x y)
he : X * ↑(algebraMap R (FractionRing R)) y = ↑(algebraMap R (FractionRing R)) x
⊢ ∃ y, ↑(algebraMap R (FractionRing R)) y = X
[PROOFSTEP]
have :=
  Polynomial.dvd_pow_natDegree_of_eval₂_eq_zero (IsFractionRing.injective R <| FractionRing R) hp₁ y x _ hp₂
    (by rw [mul_comm, he])
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
x y : R
hg : IsUnit (gcd x y)
he : X * ↑(algebraMap R (FractionRing R)) y = ↑(algebraMap R (FractionRing R)) x
⊢ ↑(algebraMap R (FractionRing R)) y * X = ↑(algebraMap R (FractionRing R)) x
[PROOFSTEP]
rw [mul_comm, he]
[GOAL]
case intro.intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
x y : R
hg : IsUnit (gcd x y)
he : X * ↑(algebraMap R (FractionRing R)) y = ↑(algebraMap R (FractionRing R)) x
this : y ∣ x ^ Polynomial.natDegree p
⊢ ∃ y, ↑(algebraMap R (FractionRing R)) y = X
[PROOFSTEP]
have : IsUnit y := by
  rw [isUnit_iff_dvd_one, ← one_pow]
  exact
    (dvd_gcd this <| dvd_refl y).trans
      (gcd_pow_left_dvd_pow_gcd.trans <| pow_dvd_pow_of_dvd (isUnit_iff_dvd_one.1 hg) _)
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
x y : R
hg : IsUnit (gcd x y)
he : X * ↑(algebraMap R (FractionRing R)) y = ↑(algebraMap R (FractionRing R)) x
this : y ∣ x ^ Polynomial.natDegree p
⊢ IsUnit y
[PROOFSTEP]
rw [isUnit_iff_dvd_one, ← one_pow]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
x y : R
hg : IsUnit (gcd x y)
he : X * ↑(algebraMap R (FractionRing R)) y = ↑(algebraMap R (FractionRing R)) x
this : y ∣ x ^ Polynomial.natDegree p
⊢ y ∣ 1 ^ ?m.56326
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
x y : R
hg : IsUnit (gcd x y)
he : X * ↑(algebraMap R (FractionRing R)) y = ↑(algebraMap R (FractionRing R)) x
this : y ∣ x ^ Polynomial.natDegree p
⊢ ℕ
[PROOFSTEP]
exact
  (dvd_gcd this <| dvd_refl y).trans (gcd_pow_left_dvd_pow_gcd.trans <| pow_dvd_pow_of_dvd (isUnit_iff_dvd_one.1 hg) _)
[GOAL]
case intro.intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
x y : R
hg : IsUnit (gcd x y)
he : X * ↑(algebraMap R (FractionRing R)) y = ↑(algebraMap R (FractionRing R)) x
this✝ : y ∣ x ^ Polynomial.natDegree p
this : IsUnit y
⊢ ∃ y, ↑(algebraMap R (FractionRing R)) y = X
[PROOFSTEP]
use x * (this.unit⁻¹ : _)
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
x y : R
hg : IsUnit (gcd x y)
he : X * ↑(algebraMap R (FractionRing R)) y = ↑(algebraMap R (FractionRing R)) x
this✝ : y ∣ x ^ Polynomial.natDegree p
this : IsUnit y
⊢ ↑(algebraMap R (FractionRing R)) (x * ↑(IsUnit.unit this)⁻¹) = X
[PROOFSTEP]
erw [map_mul, ← Units.coe_map_inv, eq_comm, Units.eq_mul_inv_iff_mul_eq]
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : GCDMonoid R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : Polynomial.Monic p
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
x y : R
hg : IsUnit (gcd x y)
he : X * ↑(algebraMap R (FractionRing R)) y = ↑(algebraMap R (FractionRing R)) x
this✝ : y ∣ x ^ Polynomial.natDegree p
this : IsUnit y
⊢ X * ↑(↑(Units.map ↑(algebraMap R (FractionRing R))) (IsUnit.unit this)) = ↑(algebraMap R (FractionRing R)) x
[PROOFSTEP]
exact he


[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
⊢ z • r ∈ zmultiples p ↔ ∃ k, r - ↑k • (p / ↑z) ∈ zmultiples p
[PROOFSTEP]
rw [AddSubgroup.mem_zmultiples_iff]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
⊢ (∃ k, k • p = z • r) ↔ ∃ k, r - ↑k • (p / ↑z) ∈ zmultiples p
[PROOFSTEP]
simp_rw [AddSubgroup.mem_zmultiples_iff, div_eq_mul_inv, ← smul_mul_assoc, eq_sub_iff_add_eq]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
⊢ (∃ k, k • p = z • r) ↔ ∃ k k_1, k_1 • p + ↑k • p * (↑z)⁻¹ = r
[PROOFSTEP]
have hz' : (z : R) ≠ 0 := Int.cast_ne_zero.mpr hz
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
⊢ (∃ k, k • p = z • r) ↔ ∃ k k_1, k_1 • p + ↑k • p * (↑z)⁻¹ = r
[PROOFSTEP]
conv_rhs => simp (config := { singlePass := true }) only [← (mul_right_injective₀ hz').eq_iff]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
| ∃ k k_1, k_1 • p + ↑k • p * (↑z)⁻¹ = r
[PROOFSTEP]
simp (config := { singlePass := true }) only [← (mul_right_injective₀ hz').eq_iff]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
| ∃ k k_1, k_1 • p + ↑k • p * (↑z)⁻¹ = r
[PROOFSTEP]
simp (config := { singlePass := true }) only [← (mul_right_injective₀ hz').eq_iff]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
| ∃ k k_1, k_1 • p + ↑k • p * (↑z)⁻¹ = r
[PROOFSTEP]
simp (config := { singlePass := true }) only [← (mul_right_injective₀ hz').eq_iff]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
⊢ (∃ k, k • p = z • r) ↔
    ∃ k k_1, (fun x x_1 => x * x_1) (↑z) (k_1 • p + ↑k • p * (↑z)⁻¹) = (fun x x_1 => x * x_1) (↑z) r
[PROOFSTEP]
simp_rw [← zsmul_eq_mul, smul_add, ← mul_smul_comm, zsmul_eq_mul (z : R)⁻¹, mul_inv_cancel hz', mul_one, ←
  coe_nat_zsmul, smul_smul, ← add_smul]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
⊢ (∃ k, k • p = z • r) ↔ ∃ k k_1, (z * k_1 + ↑↑k) • p = z • r
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
⊢ (∃ k, k • p = z • r) → ∃ k k_1, (z * k_1 + ↑↑k) • p = z • r
[PROOFSTEP]
rintro ⟨k, h⟩
[GOAL]
case mp.intro
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ ∃ k k_1, (z * k_1 + ↑↑k) • p = z • r
[PROOFSTEP]
simp_rw [← h]
[GOAL]
case mp.intro
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ ∃ k_1 k_2, (z * k_2 + ↑↑k_1) • p = k • p
[PROOFSTEP]
refine' ⟨⟨(k % z).toNat, _⟩, k / z, _⟩
[GOAL]
case mp.intro.refine'_1
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ Int.toNat (k % z) < Int.natAbs z
[PROOFSTEP]
rw [← Int.ofNat_lt, Int.toNat_of_nonneg (Int.emod_nonneg _ hz)]
[GOAL]
case mp.intro.refine'_1
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ k % z < ↑(Int.natAbs z)
[PROOFSTEP]
exact (Int.emod_lt _ hz).trans_eq (Int.abs_eq_natAbs _)
[GOAL]
case mp.intro.refine'_2
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ (z * (k / z) + ↑↑{ val := Int.toNat (k % z), isLt := (_ : Int.toNat (k % z) < Int.natAbs z) }) • p = k • p
[PROOFSTEP]
rw [Fin.val_mk, Int.toNat_of_nonneg (Int.emod_nonneg _ hz)]
[GOAL]
case mp.intro.refine'_2
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ (z * (k / z) + k % z) • p = k • p
[PROOFSTEP]
nth_rewrite 3 [← Int.div_add_mod k z]
[GOAL]
case mp.intro.refine'_2
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ (z * (k / z) + k % z) • p = (z * Int.div k z + Int.mod k z) • p
[PROOFSTEP]
rw [Int.mod_def, ← Int.div_def', Int.emod_def]
[GOAL]
case mp.intro.refine'_2
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ (z * (k / z) + (k - z * (k / z))) • p = (z * (k / z) + (k - z * (k / z))) • p
[PROOFSTEP]
simp only [add_sub_cancel'_right, zsmul_eq_mul, Int.div_def']
[GOAL]
case mpr
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
⊢ (∃ k k_1, (z * k_1 + ↑↑k) • p = z • r) → ∃ k, k • p = z • r
[PROOFSTEP]
rintro ⟨k, n, h⟩
[GOAL]
case mpr.intro.intro
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : Fin (Int.natAbs z)
n : ℤ
h : (z * n + ↑↑k) • p = z • r
⊢ ∃ k, k • p = z • r
[PROOFSTEP]
exact ⟨_, h⟩
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
n : ℕ
hn : n ≠ 0
⊢ n • r ∈ zmultiples p ↔ ∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p
[PROOFSTEP]
rw [← coe_nat_zsmul r, zsmul_mem_zmultiples_iff_exists_sub_div (Int.coe_nat_ne_zero.mpr hn), Int.cast_ofNat]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
n : ℕ
hn : n ≠ 0
⊢ (∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p) ↔ ∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
ψ θ : R ⧸ AddSubgroup.zmultiples p
z : ℤ
hz : z ≠ 0
⊢ z • ψ = z • θ ↔ ∃ k, ψ = θ + ↑(↑k • (p / ↑z))
[PROOFSTEP]
induction ψ using Quotient.inductionOn'
[GOAL]
case h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
θ : R ⧸ AddSubgroup.zmultiples p
z : ℤ
hz : z ≠ 0
a✝ : R
⊢ z • Quotient.mk'' a✝ = z • θ ↔ ∃ k, Quotient.mk'' a✝ = θ + ↑(↑k • (p / ↑z))
[PROOFSTEP]
induction θ using Quotient.inductionOn'
[GOAL]
case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
⊢ z • Quotient.mk'' a✝¹ = z • Quotient.mk'' a✝ ↔ ∃ k, Quotient.mk'' a✝¹ = Quotient.mk'' a✝ + ↑(↑k • (p / ↑z))
[PROOFSTEP]
let Zp := AddSubgroup.zmultiples p
[GOAL]
case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
Zp : AddSubgroup R := AddSubgroup.zmultiples p
⊢ z • Quotient.mk'' a✝¹ = z • Quotient.mk'' a✝ ↔ ∃ k, Quotient.mk'' a✝¹ = Quotient.mk'' a✝ + ↑(↑k • (p / ↑z))
[PROOFSTEP]
have : (Quotient.mk'' : R → R ⧸ Zp) = ((↑) : R → R ⧸ Zp) := rfl
[GOAL]
case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
Zp : AddSubgroup R := AddSubgroup.zmultiples p
this : Quotient.mk'' = mk
⊢ z • Quotient.mk'' a✝¹ = z • Quotient.mk'' a✝ ↔ ∃ k, Quotient.mk'' a✝¹ = Quotient.mk'' a✝ + ↑(↑k • (p / ↑z))
[PROOFSTEP]
simp only [this]
[GOAL]
case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
Zp : AddSubgroup R := AddSubgroup.zmultiples p
this : Quotient.mk'' = mk
⊢ z • ↑a✝¹ = z • ↑a✝ ↔ ∃ k, ↑a✝¹ = ↑a✝ + ↑(↑k • (p / ↑z))
[PROOFSTEP]
simp_rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_add, QuotientAddGroup.eq_iff_sub_mem, ← smul_sub, ← sub_sub]
[GOAL]
case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
Zp : AddSubgroup R := AddSubgroup.zmultiples p
this : Quotient.mk'' = mk
⊢ z • (a✝¹ - a✝) ∈ AddSubgroup.zmultiples p ↔ ∃ k, a✝¹ - a✝ - ↑k • (p / ↑z) ∈ AddSubgroup.zmultiples p
[PROOFSTEP]
exact AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div hz
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
ψ θ : R ⧸ AddSubgroup.zmultiples p
n : ℕ
hz : n ≠ 0
⊢ n • ψ = n • θ ↔ ∃ k, ψ = θ + ↑(↑k • (p / ↑n))
[PROOFSTEP]
rw [← coe_nat_zsmul ψ, ← coe_nat_zsmul θ, zmultiples_zsmul_eq_zsmul_iff (Int.coe_nat_ne_zero.mpr hz), Int.cast_ofNat]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
ψ θ : R ⧸ AddSubgroup.zmultiples p
n : ℕ
hz : n ≠ 0
⊢ (∃ k, ψ = θ + ↑(↑k • (p / ↑n))) ↔ ∃ k, ψ = θ + ↑(↑k • (p / ↑n))
[PROOFSTEP]
rfl


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ lcm s f ∣ a ↔ ∀ (b : β), b ∈ s → f b ∣ a
[PROOFSTEP]
apply Iff.trans Multiset.lcm_dvd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (∀ (b : α), b ∈ Multiset.map f s.val → b ∣ a) ↔ ∀ (b : β), b ∈ s → f b ∣ a
[PROOFSTEP]
simp only [Multiset.mem_map, and_imp, exists_imp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (∀ (b : α) (x : β), x ∈ s.val → f x = b → b ∣ a) ↔ ∀ (b : β), b ∈ s → f b ∣ a
[PROOFSTEP]
exact ⟨fun k b hb ↦ k _ _ hb rfl, fun k a' b hb h ↦ h ▸ k _ hb⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
⊢ lcm (insert b s) f = GCDMonoid.lcm (f b) (lcm s f)
[PROOFSTEP]
by_cases h : b ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∈ s
⊢ lcm (insert b s) f = GCDMonoid.lcm (f b) (lcm s f)
[PROOFSTEP]
rw [insert_eq_of_mem h, (lcm_eq_right_iff (f b) (s.lcm f) (Multiset.normalize_lcm (s.1.map f))).2 (dvd_lcm h)]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : ¬b ∈ s
⊢ lcm (insert b s) f = GCDMonoid.lcm (f b) (lcm s f)
[PROOFSTEP]
apply fold_insert h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
⊢ ↑normalize (lcm s f) = lcm s f
[PROOFSTEP]
simp [lcm_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ lcm (∅ ∪ s₂) f = GCDMonoid.lcm (lcm ∅ f) (lcm s₂ f)
[PROOFSTEP]
rw [empty_union, lcm_empty, lcm_one_left, normalize_lcm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : ¬a ∈ s
ih : lcm (s ∪ s₂) f = GCDMonoid.lcm (lcm s f) (lcm s₂ f)
⊢ lcm (insert a s ∪ s₂) f = GCDMonoid.lcm (lcm (insert a s) f) (lcm s₂ f)
[PROOFSTEP]
rw [insert_union, lcm_insert, lcm_insert, ih, lcm_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hs : s₁ = s₂
hfg : ∀ (a : β), a ∈ s₂ → f a = g a
⊢ lcm s₁ f = lcm s₂ g
[PROOFSTEP]
subst hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ : Finset β
f✝ f g : β → α
hfg : ∀ (a : β), a ∈ s₁ → f a = g a
⊢ lcm s₁ f = lcm s₁ g
[PROOFSTEP]
exact Finset.fold_congr hfg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
g : γ → β
s : Finset γ
⊢ lcm (image g s) f = lcm s (f ∘ g)
[PROOFSTEP]
classical induction' s using Finset.induction with c s _ ih <;> simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
g : γ → β
s : Finset γ
⊢ lcm (image g s) f = lcm s (f ∘ g)
[PROOFSTEP]
induction' s using Finset.induction with c s _ ih
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
g : γ → β
⊢ lcm (image g ∅) f = lcm ∅ (f ∘ g)
[PROOFSTEP]
simp [*]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
g : γ → β
c : γ
s : Finset γ
a✝ : ¬c ∈ s
ih : lcm (image g s) f = lcm s (f ∘ g)
⊢ lcm (image g (insert c s)) f = lcm (insert c s) (f ∘ g)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : Nontrivial α
⊢ lcm s f = 0 ↔ 0 ∈ f '' ↑s
[PROOFSTEP]
simp only [Multiset.mem_map, lcm_def, Multiset.lcm_eq_zero_iff, Set.mem_image, mem_coe, ← Finset.mem_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ a ∣ gcd s f ↔ ∀ (b : β), b ∈ s → a ∣ f b
[PROOFSTEP]
apply Iff.trans Multiset.dvd_gcd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (∀ (b : α), b ∈ Multiset.map f s.val → a ∣ b) ↔ ∀ (b : β), b ∈ s → a ∣ f b
[PROOFSTEP]
simp only [Multiset.mem_map, and_imp, exists_imp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (∀ (b : α) (x : β), x ∈ s.val → f x = b → a ∣ b) ↔ ∀ (b : β), b ∈ s → a ∣ f b
[PROOFSTEP]
exact ⟨fun k b hb ↦ k _ _ hb rfl, fun k a' b hb h ↦ h ▸ k _ hb⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
⊢ gcd (insert b s) f = GCDMonoid.gcd (f b) (gcd s f)
[PROOFSTEP]
by_cases h : b ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∈ s
⊢ gcd (insert b s) f = GCDMonoid.gcd (f b) (gcd s f)
[PROOFSTEP]
rw [insert_eq_of_mem h, (gcd_eq_right_iff (f b) (s.gcd f) (Multiset.normalize_gcd (s.1.map f))).2 (gcd_dvd h)]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : ¬b ∈ s
⊢ gcd (insert b s) f = GCDMonoid.gcd (f b) (gcd s f)
[PROOFSTEP]
apply fold_insert h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
⊢ ↑normalize (gcd s f) = gcd s f
[PROOFSTEP]
simp [gcd_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ gcd (∅ ∪ s₂) f = GCDMonoid.gcd (gcd ∅ f) (gcd s₂ f)
[PROOFSTEP]
rw [empty_union, gcd_empty, gcd_zero_left, normalize_gcd]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : ¬a ∈ s
ih : gcd (s ∪ s₂) f = GCDMonoid.gcd (gcd s f) (gcd s₂ f)
⊢ gcd (insert a s ∪ s₂) f = GCDMonoid.gcd (gcd (insert a s) f) (gcd s₂ f)
[PROOFSTEP]
rw [insert_union, gcd_insert, gcd_insert, ih, gcd_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hs : s₁ = s₂
hfg : ∀ (a : β), a ∈ s₂ → f a = g a
⊢ gcd s₁ f = gcd s₂ g
[PROOFSTEP]
subst hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ : Finset β
f✝ f g : β → α
hfg : ∀ (a : β), a ∈ s₁ → f a = g a
⊢ gcd s₁ f = gcd s₁ g
[PROOFSTEP]
exact Finset.fold_congr hfg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
g : γ → β
s : Finset γ
⊢ gcd (image g s) f = gcd s (f ∘ g)
[PROOFSTEP]
classical induction' s using Finset.induction with c s _ ih <;> simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
g : γ → β
s : Finset γ
⊢ gcd (image g s) f = gcd s (f ∘ g)
[PROOFSTEP]
induction' s using Finset.induction with c s _ ih
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
g : γ → β
⊢ gcd (image g ∅) f = gcd ∅ (f ∘ g)
[PROOFSTEP]
simp [*]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
g : γ → β
c : γ
s : Finset γ
a✝ : ¬c ∈ s
ih : gcd (image g s) f = gcd s (f ∘ g)
⊢ gcd (image g (insert c s)) f = gcd (insert c s) (f ∘ g)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
⊢ gcd s f = 0 ↔ ∀ (x : β), x ∈ s → f x = 0
[PROOFSTEP]
rw [gcd_def, Multiset.gcd_eq_zero_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
⊢ (∀ (x : α), x ∈ Multiset.map f s.val → x = 0) ↔ ∀ (x : β), x ∈ s → f x = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
⊢ (∀ (x : α), x ∈ Multiset.map f s.val → x = 0) → ∀ (x : β), x ∈ s → f x = 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
⊢ (∀ (x : β), x ∈ s → f x = 0) → ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
⊢ ∀ (x : β), x ∈ s → f x = 0
[PROOFSTEP]
intro b bs
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
b : β
bs : b ∈ s
⊢ f b = 0
[PROOFSTEP]
apply h (f b)
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
b : β
bs : b ∈ s
⊢ f b ∈ Multiset.map f s.val
[PROOFSTEP]
simp only [Multiset.mem_map, mem_def.1 bs]
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
b : β
bs : b ∈ s
⊢ ∃ a, a ∈ s.val ∧ f a = f b
[PROOFSTEP]
use b
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
b : β
bs : b ∈ s
⊢ b ∈ s.val ∧ f b = f b
[PROOFSTEP]
simp only [mem_def.1 bs, eq_self_iff_true, and_self]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : β), x ∈ s → f x = 0
⊢ ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
[PROOFSTEP]
intro a as
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : β), x ∈ s → f x = 0
a : α
as : a ∈ Multiset.map f s.val
⊢ a = 0
[PROOFSTEP]
rw [Multiset.mem_map] at as
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : β), x ∈ s → f x = 0
a : α
as : ∃ a_1, a_1 ∈ s.val ∧ f a_1 = a
⊢ a = 0
[PROOFSTEP]
rcases as with ⟨b, ⟨bs, rfl⟩⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : β), x ∈ s → f x = 0
b : β
bs : b ∈ s.val
⊢ f b = 0
[PROOFSTEP]
apply h b (mem_def.1 bs)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd s f = gcd (filter (fun x => f x ≠ 0) s) f
[PROOFSTEP]
classical
trans ((s.filter fun x ↦ f x = 0) ∪ s.filter fun x ↦ (f x ≠ 0)).gcd f
· rw [filter_union_filter_neg_eq]
rw [gcd_union]
refine' Eq.trans (_ : _ = GCDMonoid.gcd (0 : α) _) (_ : GCDMonoid.gcd (0 : α) _ = _)
· exact (gcd (filter (fun x => (f x ≠ 0)) s) f)
· refine' congr (congr rfl <| s.induction_on _ _) (by simp)
  · simp
  · intro a s _ h
    rw [filter_insert]
    split_ifs with h1 <;> simp [h, h1]
simp only [gcd_zero_left, normalize_gcd]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd s f = gcd (filter (fun x => f x ≠ 0) s) f
[PROOFSTEP]
trans ((s.filter fun x ↦ f x = 0) ∪ s.filter fun x ↦ (f x ≠ 0)).gcd f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd s f = gcd (filter (fun x => f x = 0) s ∪ filter (fun x => f x ≠ 0) s) f
[PROOFSTEP]
rw [filter_union_filter_neg_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd (filter (fun x => f x = 0) s ∪ filter (fun x => f x ≠ 0) s) f = gcd (filter (fun x => f x ≠ 0) s) f
[PROOFSTEP]
rw [gcd_union]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ GCDMonoid.gcd (gcd (filter (fun x => f x = 0) s) f) (gcd (filter (fun x => f x ≠ 0) s) f) =
    gcd (filter (fun x => f x ≠ 0) s) f
[PROOFSTEP]
refine' Eq.trans (_ : _ = GCDMonoid.gcd (0 : α) _) (_ : GCDMonoid.gcd (0 : α) _ = _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ α
[PROOFSTEP]
exact (gcd (filter (fun x => (f x ≠ 0)) s) f)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ GCDMonoid.gcd (gcd (filter (fun x => f x = 0) s) f) (gcd (filter (fun x => f x ≠ 0) s) f) =
    GCDMonoid.gcd 0 (gcd (filter (fun x => f x ≠ 0) s) f)
[PROOFSTEP]
refine' congr (congr rfl <| s.induction_on _ _) (by simp)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd (filter (fun x => f x ≠ 0) s) f = gcd (filter (fun x => f x ≠ 0) s) f
[PROOFSTEP]
simp
[GOAL]
case refine'_2.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd (filter (fun x => f x = 0) ∅) f = 0
[PROOFSTEP]
simp
[GOAL]
case refine'_2.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ ∀ ⦃a : β⦄ {s : Finset β},
    ¬a ∈ s → gcd (filter (fun x => f x = 0) s) f = 0 → gcd (filter (fun x => f x = 0) (insert a s)) f = 0
[PROOFSTEP]
intro a s _ h
[GOAL]
case refine'_2.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
a : β
s : Finset β
a✝ : ¬a ∈ s
h : gcd (filter (fun x => f x = 0) s) f = 0
⊢ gcd (filter (fun x => f x = 0) (insert a s)) f = 0
[PROOFSTEP]
rw [filter_insert]
[GOAL]
case refine'_2.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
a : β
s : Finset β
a✝ : ¬a ∈ s
h : gcd (filter (fun x => f x = 0) s) f = 0
⊢ gcd (if f a = 0 then insert a (filter (fun x => f x = 0) s) else filter (fun x => f x = 0) s) f = 0
[PROOFSTEP]
split_ifs with h1
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
a : β
s : Finset β
a✝ : ¬a ∈ s
h : gcd (filter (fun x => f x = 0) s) f = 0
h1 : f a = 0
⊢ gcd (insert a (filter (fun x => f x = 0) s)) f = 0
[PROOFSTEP]
simp [h, h1]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
a : β
s : Finset β
a✝ : ¬a ∈ s
h : gcd (filter (fun x => f x = 0) s) f = 0
h1 : ¬f a = 0
⊢ gcd (filter (fun x => f x = 0) s) f = 0
[PROOFSTEP]
simp [h, h1]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ GCDMonoid.gcd 0 (gcd (filter (fun x => f x ≠ 0) s) f) = gcd (filter (fun x => f x ≠ 0) s) f
[PROOFSTEP]
simp only [gcd_zero_left, normalize_gcd]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (gcd s fun x => a * f x) = ↑normalize a * gcd s f
[PROOFSTEP]
classical
refine' s.induction_on _ _
· simp
· intro b t _ h
  rw [gcd_insert, gcd_insert, h, ← gcd_mul_left]
  apply ((normalize_associated a).mul_right _).gcd_eq_right
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (gcd s fun x => a * f x) = ↑normalize a * gcd s f
[PROOFSTEP]
refine' s.induction_on _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (gcd ∅ fun x => a * f x) = ↑normalize a * gcd ∅ f
[PROOFSTEP]
simp
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ ∀ ⦃a_1 : β⦄ {s : Finset β},
    ¬a_1 ∈ s →
      (gcd s fun x => a * f x) = ↑normalize a * gcd s f →
        (gcd (insert a_1 s) fun x => a * f x) = ↑normalize a * gcd (insert a_1 s) f
[PROOFSTEP]
intro b t _ h
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : ¬b ∈ t
h : (gcd t fun x => a * f x) = ↑normalize a * gcd t f
⊢ (gcd (insert b t) fun x => a * f x) = ↑normalize a * gcd (insert b t) f
[PROOFSTEP]
rw [gcd_insert, gcd_insert, h, ← gcd_mul_left]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : ¬b ∈ t
h : (gcd t fun x => a * f x) = ↑normalize a * gcd t f
⊢ GCDMonoid.gcd (a * f b) (↑normalize a * gcd t f) = GCDMonoid.gcd (a * f b) (a * gcd t f)
[PROOFSTEP]
apply ((normalize_associated a).mul_right _).gcd_eq_right
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (gcd s fun x => f x * a) = gcd s f * ↑normalize a
[PROOFSTEP]
classical
refine' s.induction_on _ _
· simp
· intro b t _ h
  rw [gcd_insert, gcd_insert, h, ← gcd_mul_right]
  apply ((normalize_associated a).mul_left _).gcd_eq_right
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (gcd s fun x => f x * a) = gcd s f * ↑normalize a
[PROOFSTEP]
refine' s.induction_on _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (gcd ∅ fun x => f x * a) = gcd ∅ f * ↑normalize a
[PROOFSTEP]
simp
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ ∀ ⦃a_1 : β⦄ {s : Finset β},
    ¬a_1 ∈ s →
      (gcd s fun x => f x * a) = gcd s f * ↑normalize a →
        (gcd (insert a_1 s) fun x => f x * a) = gcd (insert a_1 s) f * ↑normalize a
[PROOFSTEP]
intro b t _ h
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : ¬b ∈ t
h : (gcd t fun x => f x * a) = gcd t f * ↑normalize a
⊢ (gcd (insert b t) fun x => f x * a) = gcd (insert b t) f * ↑normalize a
[PROOFSTEP]
rw [gcd_insert, gcd_insert, h, ← gcd_mul_right]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : ¬b ∈ t
h : (gcd t fun x => f x * a) = gcd t f * ↑normalize a
⊢ GCDMonoid.gcd (f b * a) (gcd t f * ↑normalize a) = GCDMonoid.gcd (f b * a) (gcd t f * a)
[PROOFSTEP]
apply ((normalize_associated a).mul_left _).gcd_eq_right
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hs : ∃ x, x ∈ s ∧ f x ≠ 0
hg : ∀ (b : β), b ∈ s → f b = gcd s f * g b
⊢ gcd s f * gcd s g = gcd s f
[PROOFSTEP]
conv_lhs => rw [← normalize_gcd, ← gcd_mul_left, ← gcd_congr rfl hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hs : ∃ x, x ∈ s ∧ f x ≠ 0
hg : ∀ (b : β), b ∈ s → f b = gcd s f * g b
| gcd s f * gcd s g
[PROOFSTEP]
rw [← normalize_gcd, ← gcd_mul_left, ← gcd_congr rfl hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hs : ∃ x, x ∈ s ∧ f x ≠ 0
hg : ∀ (b : β), b ∈ s → f b = gcd s f * g b
| gcd s f * gcd s g
[PROOFSTEP]
rw [← normalize_gcd, ← gcd_mul_left, ← gcd_congr rfl hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hs : ∃ x, x ∈ s ∧ f x ≠ 0
hg : ∀ (b : β), b ∈ s → f b = gcd s f * g b
| gcd s f * gcd s g
[PROOFSTEP]
rw [← normalize_gcd, ← gcd_mul_left, ← gcd_congr rfl hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hs : ∃ x, x ∈ s ∧ f x ≠ 0
hg : ∀ (b : β), b ∈ s → f b = gcd s f * g b
⊢ ¬gcd s f = 0
[PROOFSTEP]
contrapose! hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hg : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hs : gcd s f = 0
⊢ ∀ (x : β), x ∈ s → f x = 0
[PROOFSTEP]
exact gcd_eq_zero_iff.1 hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
⊢ ∃ g, (∀ (b : β), b ∈ s → f b = gcd s f * g b) ∧ gcd s g = 1
[PROOFSTEP]
classical
by_cases h : ∀ x ∈ s, f x = (0 : α)
· refine' ⟨fun _ ↦ 1, fun b hb ↦ by rw [h b hb, gcd_eq_zero_iff.2 h, mul_one], _⟩
  rw [gcd_eq_gcd_image, image_const hs, gcd_singleton, id, normalize_one]
· choose g' hg using @gcd_dvd _ _ _ _ s f
  push_neg at h
  refine' ⟨fun b ↦ if hb : b ∈ s then g' hb else 0, fun b hb ↦ _, extract_gcd' f _ h <| fun b hb ↦ _⟩
  simp only [hb, hg, dite_true]
  rw [dif_pos hb, hg hb]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
⊢ ∃ g, (∀ (b : β), b ∈ s → f b = gcd s f * g b) ∧ gcd s g = 1
[PROOFSTEP]
by_cases h : ∀ x ∈ s, f x = (0 : α)
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
h : ∀ (x : β), x ∈ s → f x = 0
⊢ ∃ g, (∀ (b : β), b ∈ s → f b = gcd s f * g b) ∧ gcd s g = 1
[PROOFSTEP]
refine' ⟨fun _ ↦ 1, fun b hb ↦ by rw [h b hb, gcd_eq_zero_iff.2 h, mul_one], _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
h : ∀ (x : β), x ∈ s → f x = 0
b : β
hb : b ∈ s
⊢ f b = gcd s f * (fun x => 1) b
[PROOFSTEP]
rw [h b hb, gcd_eq_zero_iff.2 h, mul_one]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
h : ∀ (x : β), x ∈ s → f x = 0
⊢ (gcd s fun x => 1) = 1
[PROOFSTEP]
rw [gcd_eq_gcd_image, image_const hs, gcd_singleton, id, normalize_one]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
h : ¬∀ (x : β), x ∈ s → f x = 0
⊢ ∃ g, (∀ (b : β), b ∈ s → f b = gcd s f * g b) ∧ gcd s g = 1
[PROOFSTEP]
choose g' hg using @gcd_dvd _ _ _ _ s f
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
h : ¬∀ (x : β), x ∈ s → f x = 0
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = gcd s f * g' hb
⊢ ∃ g, (∀ (b : β), b ∈ s → f b = gcd s f * g b) ∧ gcd s g = 1
[PROOFSTEP]
push_neg at h
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = gcd s f * g' hb
h : ∃ x, x ∈ s ∧ f x ≠ 0
⊢ ∃ g, (∀ (b : β), b ∈ s → f b = gcd s f * g b) ∧ gcd s g = 1
[PROOFSTEP]
refine' ⟨fun b ↦ if hb : b ∈ s then g' hb else 0, fun b hb ↦ _, extract_gcd' f _ h <| fun b hb ↦ _⟩
[GOAL]
case neg.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = gcd s f * g' hb
h : ∃ x, x ∈ s ∧ f x ≠ 0
b : β
hb : b ∈ s
⊢ f b = gcd s f * (fun b => if hb : b ∈ s then g' hb else 0) b
case neg.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = gcd s f * g' hb
h : ∃ x, x ∈ s ∧ f x ≠ 0
b : β
hb : b ∈ s
⊢ f b = gcd s f * if hb : b ∈ s then g' hb else 0
[PROOFSTEP]
simp only [hb, hg, dite_true]
[GOAL]
case neg.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = gcd s f * g' hb
h : ∃ x, x ∈ s ∧ f x ≠ 0
b : β
hb : b ∈ s
⊢ f b = gcd s f * if hb : b ∈ s then g' hb else 0
[PROOFSTEP]
rw [dif_pos hb, hg hb]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
h : ∀ (x : β), x ∈ s → a ∣ f x - g x
⊢ GCDMonoid.gcd a (gcd s f) = GCDMonoid.gcd a (gcd s g)
[PROOFSTEP]
classical
revert h
refine' s.induction_on _ _
· simp
intro b s _ hi h
rw [gcd_insert, gcd_insert, gcd_comm (f b), ← gcd_assoc, hi fun x hx ↦ h _ (mem_insert_of_mem hx), gcd_comm a,
  gcd_assoc, gcd_comm a (GCDMonoid.gcd _ _), gcd_comm (g b), gcd_assoc _ _ a, gcd_comm _ a]
exact congr_arg _ (gcd_eq_of_dvd_sub_right (h _ (mem_insert_self _ _)))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
h : ∀ (x : β), x ∈ s → a ∣ f x - g x
⊢ GCDMonoid.gcd a (gcd s f) = GCDMonoid.gcd a (gcd s g)
[PROOFSTEP]
revert h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
⊢ (∀ (x : β), x ∈ s → a ∣ f x - g x) → GCDMonoid.gcd a (gcd s f) = GCDMonoid.gcd a (gcd s g)
[PROOFSTEP]
refine' s.induction_on _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
⊢ (∀ (x : β), x ∈ ∅ → a ∣ f x - g x) → GCDMonoid.gcd a (gcd ∅ f) = GCDMonoid.gcd a (gcd ∅ g)
[PROOFSTEP]
simp
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
⊢ ∀ ⦃a_1 : β⦄ {s : Finset β},
    ¬a_1 ∈ s →
      ((∀ (x : β), x ∈ s → a ∣ f x - g x) → GCDMonoid.gcd a (gcd s f) = GCDMonoid.gcd a (gcd s g)) →
        (∀ (x : β), x ∈ insert a_1 s → a ∣ f x - g x) →
          GCDMonoid.gcd a (gcd (insert a_1 s) f) = GCDMonoid.gcd a (gcd (insert a_1 s) g)
[PROOFSTEP]
intro b s _ hi h
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s✝ : Finset β
f g : β → α
a : α
b : β
s : Finset β
a✝ : ¬b ∈ s
hi : (∀ (x : β), x ∈ s → a ∣ f x - g x) → GCDMonoid.gcd a (gcd s f) = GCDMonoid.gcd a (gcd s g)
h : ∀ (x : β), x ∈ insert b s → a ∣ f x - g x
⊢ GCDMonoid.gcd a (gcd (insert b s) f) = GCDMonoid.gcd a (gcd (insert b s) g)
[PROOFSTEP]
rw [gcd_insert, gcd_insert, gcd_comm (f b), ← gcd_assoc, hi fun x hx ↦ h _ (mem_insert_of_mem hx), gcd_comm a,
  gcd_assoc, gcd_comm a (GCDMonoid.gcd _ _), gcd_comm (g b), gcd_assoc _ _ a, gcd_comm _ a]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s✝ : Finset β
f g : β → α
a : α
b : β
s : Finset β
a✝ : ¬b ∈ s
hi : (∀ (x : β), x ∈ s → a ∣ f x - g x) → GCDMonoid.gcd a (gcd s f) = GCDMonoid.gcd a (gcd s g)
h : ∀ (x : β), x ∈ insert b s → a ∣ f x - g x
⊢ GCDMonoid.gcd (gcd s g) (GCDMonoid.gcd a (f b)) = GCDMonoid.gcd (gcd s g) (GCDMonoid.gcd a (g b))
[PROOFSTEP]
exact congr_arg _ (gcd_eq_of_dvd_sub_right (h _ (mem_insert_self _ _)))


[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : Add A
inst✝⁵ : Add B
inst✝⁴ : Add T
inst✝³ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degbm : ∀ {a b : A}, degb (a + b) ≤ degb a + degb b
f g : AddMonoidAlgebra R A
⊢ Finset.sup (f * g).support degb ≤ Finset.sup f.support degb + Finset.sup g.support degb
[PROOFSTEP]
refine' (Finset.sup_mono <| support_mul _ _).trans _
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : Add A
inst✝⁵ : Add B
inst✝⁴ : Add T
inst✝³ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degbm : ∀ {a b : A}, degb (a + b) ≤ degb a + degb b
f g : AddMonoidAlgebra R A
⊢ Finset.sup (Finset.biUnion f.support fun a₁ => Finset.biUnion g.support fun a₂ => {a₁ + a₂}) degb ≤
    Finset.sup f.support degb + Finset.sup g.support degb
[PROOFSTEP]
simp_rw [Finset.sup_biUnion, Finset.sup_singleton]
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : Add A
inst✝⁵ : Add B
inst✝⁴ : Add T
inst✝³ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degbm : ∀ {a b : A}, degb (a + b) ≤ degb a + degb b
f g : AddMonoidAlgebra R A
⊢ (Finset.sup f.support fun x => Finset.sup g.support fun x_1 => degb (x + x_1)) ≤
    Finset.sup f.support degb + Finset.sup g.support degb
[PROOFSTEP]
refine' Finset.sup_le fun fd fds => Finset.sup_le fun gd gds => degbm.trans <| add_le_add _ _
[GOAL]
case refine'_1
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : Add A
inst✝⁵ : Add B
inst✝⁴ : Add T
inst✝³ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degbm : ∀ {a b : A}, degb (a + b) ≤ degb a + degb b
f g : AddMonoidAlgebra R A
fd : A
fds : fd ∈ f.support
gd : A
gds : gd ∈ g.support
⊢ degb fd ≤ Finset.sup f.support degb
[PROOFSTEP]
exact Finset.le_sup ‹_›
[GOAL]
case refine'_2
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : Add A
inst✝⁵ : Add B
inst✝⁴ : Add T
inst✝³ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degbm : ∀ {a b : A}, degb (a + b) ≤ degb a + degb b
f g : AddMonoidAlgebra R A
fd : A
fds : fd ∈ f.support
gd : A
gds : gd ∈ g.support
⊢ degb gd ≤ Finset.sup g.support degb
[PROOFSTEP]
exact Finset.le_sup ‹_›
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : Add A
inst✝⁵ : Add B
inst✝⁴ : Add T
inst✝³ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degt : A → T
degtm : ∀ {a b : A}, degt a + degt b ≤ degt (a + b)
f g : AddMonoidAlgebra R A
⊢ Finset.inf f.support degt + Finset.inf g.support degt ≤ Finset.inf (f * g).support degt
[PROOFSTEP]
refine' OrderDual.ofDual_le_ofDual.mpr <| sup_support_mul_le (_) f g
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : Add A
inst✝⁵ : Add B
inst✝⁴ : Add T
inst✝³ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degt : A → T
degtm : ∀ {a b : A}, degt a + degt b ≤ degt (a + b)
f g : AddMonoidAlgebra R A
⊢ ∀ {a b : A}, degt (a + b) ≤ degt a + degt b
[PROOFSTEP]
intros a b
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : Add A
inst✝⁵ : Add B
inst✝⁴ : Add T
inst✝³ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degt : A → T
degtm : ∀ {a b : A}, degt a + degt b ≤ degt (a + b)
f g : AddMonoidAlgebra R A
a b : A
⊢ degt (a + b) ≤ degt a + degt b
[PROOFSTEP]
exact OrderDual.ofDual_le_ofDual.mp degtm
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
⊢ Finset.sup (List.prod []).support degb ≤ List.sum (List.map (fun f => Finset.sup f.support degb) [])
[PROOFSTEP]
rw [List.map_nil, Finset.sup_le_iff, List.prod_nil, List.sum_nil]
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
⊢ ∀ (b : A), b ∈ 1.support → degb b ≤ 0
[PROOFSTEP]
exact fun a ha => by rwa [Finset.mem_singleton.mp (Finsupp.support_single_subset ha)]
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
a : A
ha : a ∈ 1.support
⊢ degb a ≤ 0
[PROOFSTEP]
rwa [Finset.mem_singleton.mp (Finsupp.support_single_subset ha)]
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f : AddMonoidAlgebra R A
fs : List (AddMonoidAlgebra R A)
⊢ Finset.sup (List.prod (f :: fs)).support degb ≤ List.sum (List.map (fun f => Finset.sup f.support degb) (f :: fs))
[PROOFSTEP]
rw [List.prod_cons, List.map_cons, List.sum_cons]
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f : AddMonoidAlgebra R A
fs : List (AddMonoidAlgebra R A)
⊢ Finset.sup (f * List.prod fs).support degb ≤
    Finset.sup f.support degb + List.sum (List.map (fun f => Finset.sup f.support degb) fs)
[PROOFSTEP]
exact
  (sup_support_mul_le (@fun a b => degbm a b) _ _).trans (add_le_add_left (sup_support_list_prod_le degb0 degbm fs) _)
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List (AddMonoidAlgebra R A)
⊢ List.sum (List.map (fun f => Finset.inf f.support degt) l) ≤ Finset.inf (List.prod l).support degt
[PROOFSTEP]
refine' OrderDual.ofDual_le_ofDual.mpr _
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List (AddMonoidAlgebra R A)
⊢ Quot.lift (fun l => List.foldr (fun x x_1 => x ⊓ x_1) ⊤ l)
      (_ :
        ∀ (_l₁ _l₂ : List T),
          Setoid.r _l₁ _l₂ → List.foldr (fun x x_1 => x ⊓ x_1) ⊤ _l₁ = List.foldr (fun x x_1 => x ⊓ x_1) ⊤ _l₂)
      (Multiset.map degt (List.prod l).support.val) ≤
    List.foldl (fun x x_1 => x + x_1) 0 (List.map (fun f => Finset.inf f.support degt) l)
[PROOFSTEP]
refine' sup_support_list_prod_le _ _ l
[GOAL]
case refine'_1
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List (AddMonoidAlgebra R A)
⊢ degt 0 ≤ 0
[PROOFSTEP]
refine' (OrderDual.ofDual_le_ofDual.mp _)
[GOAL]
case refine'_1
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List (AddMonoidAlgebra R A)
⊢ ↑OrderDual.ofDual 0 ≤ ↑OrderDual.ofDual (degt 0)
[PROOFSTEP]
exact degt0
[GOAL]
case refine'_2
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List (AddMonoidAlgebra R A)
⊢ ∀ (a b : A), degt (a + b) ≤ degt a + degt b
[PROOFSTEP]
refine' (fun a b => OrderDual.ofDual_le_ofDual.mp _)
[GOAL]
case refine'_2
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List (AddMonoidAlgebra R A)
a b : A
⊢ ↑OrderDual.ofDual (degt a + degt b) ≤ ↑OrderDual.ofDual (degt (a + b))
[PROOFSTEP]
exact degtm a b
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : AddMonoidAlgebra R A
⊢ Finset.sup (f ^ n).support degb ≤ n • Finset.sup f.support degb
[PROOFSTEP]
rw [← List.prod_replicate, ← List.sum_replicate]
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : AddMonoidAlgebra R A
⊢ Finset.sup (List.prod (List.replicate n f)).support degb ≤ List.sum (List.replicate n (Finset.sup f.support degb))
[PROOFSTEP]
refine' (sup_support_list_prod_le degb0 degbm _).trans_eq _
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : AddMonoidAlgebra R A
⊢ List.sum (List.map (fun f => Finset.sup f.support degb) (List.replicate n f)) =
    List.sum (List.replicate n (Finset.sup f.support degb))
[PROOFSTEP]
rw [List.map_replicate]
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
n : ℕ
f : AddMonoidAlgebra R A
⊢ n • Finset.inf f.support degt ≤ Finset.inf (f ^ n).support degt
[PROOFSTEP]
refine'
  OrderDual.ofDual_le_ofDual.mpr <|
    sup_support_pow_le (OrderDual.ofDual_le_ofDual.mp _) (fun a b => OrderDual.ofDual_le_ofDual.mp _) n f
[GOAL]
case refine'_1
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
n : ℕ
f : AddMonoidAlgebra R A
⊢ ↑OrderDual.ofDual (degt 0) ≤ ↑OrderDual.ofDual 0
case refine'_2
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
n : ℕ
f : AddMonoidAlgebra R A
a b : A
⊢ ↑OrderDual.ofDual (degt (a + b)) ≤ ↑OrderDual.ofDual (degt a + degt b)
[PROOFSTEP]
exact degt0
[GOAL]
case refine'_2
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
n : ℕ
f : AddMonoidAlgebra R A
a b : A
⊢ ↑OrderDual.ofDual (degt (a + b)) ≤ ↑OrderDual.ofDual (degt a + degt b)
[PROOFSTEP]
exact degtm _ _
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : AddCommMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddCommMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
m : Multiset (AddMonoidAlgebra R A)
⊢ Finset.sup (Multiset.prod m).support degb ≤ Multiset.sum (Multiset.map (fun f => Finset.sup f.support degb) m)
[PROOFSTEP]
induction m using Quot.inductionOn
[GOAL]
case h
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : AddCommMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddCommMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
a✝ : List (AddMonoidAlgebra R A)
⊢ Finset.sup (Multiset.prod (Quot.mk Setoid.r a✝)).support degb ≤
    Multiset.sum (Multiset.map (fun f => Finset.sup f.support degb) (Quot.mk Setoid.r a✝))
[PROOFSTEP]
rw [Multiset.quot_mk_to_coe'', Multiset.coe_map, Multiset.coe_sum, Multiset.coe_prod]
[GOAL]
case h
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : AddCommMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddCommMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
a✝ : List (AddMonoidAlgebra R A)
⊢ Finset.sup (List.prod a✝).support degb ≤ List.sum (List.map (fun f => Finset.sup f.support degb) a✝)
[PROOFSTEP]
exact sup_support_list_prod_le degb0 degbm _
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : AddCommMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddCommMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset (AddMonoidAlgebra R A)
⊢ Multiset.sum (Multiset.map (fun f => Finset.inf f.support degt) m) ≤ Finset.inf (Multiset.prod m).support degt
[PROOFSTEP]
refine'
  OrderDual.ofDual_le_ofDual.mpr <|
    sup_support_multiset_prod_le (OrderDual.ofDual_le_ofDual.mp _) (fun a b => OrderDual.ofDual_le_ofDual.mp (_)) m
[GOAL]
case refine'_1
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : AddCommMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddCommMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset (AddMonoidAlgebra R A)
⊢ ↑OrderDual.ofDual (degt 0) ≤ ↑OrderDual.ofDual 0
case refine'_2
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : AddCommMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddCommMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset (AddMonoidAlgebra R A)
a b : A
⊢ ↑OrderDual.ofDual (degt (a + b)) ≤ ↑OrderDual.ofDual (degt a + degt b)
[PROOFSTEP]
exact degt0
[GOAL]
case refine'_2
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : AddCommMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddCommMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset (AddMonoidAlgebra R A)
a b : A
⊢ ↑OrderDual.ofDual (degt (a + b)) ≤ ↑OrderDual.ofDual (degt a + degt b)
[PROOFSTEP]
exact degtm _ _
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : AddCommMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddCommMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
s : Finset ι
f : ι → AddMonoidAlgebra R A
⊢ ∑ i in s, Finset.inf (f i).support degt =
    Multiset.sum (Multiset.map (fun f => Finset.inf f.support degt) (Multiset.map (fun i => f i) s.val))
[PROOFSTEP]
rw [Multiset.map_map]
[GOAL]
R : Type u_1
A : Type u_2
T : Type u_3
B : Type u_4
ι : Type u_5
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : AddCommMonoid B
inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : AddCommMonoid T
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degb : A → B
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
s : Finset ι
f : ι → AddMonoidAlgebra R A
⊢ ∑ i in s, Finset.inf (f i).support degt =
    Multiset.sum (Multiset.map ((fun f => Finset.inf f.support degt) ∘ fun i => f i) s.val)
[PROOFSTEP]
rfl


[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ Stream'.IsSeq (IntFractPair.stream v)
[PROOFSTEP]
intro _ hyp
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
hyp : IntFractPair.stream v n✝ = none
⊢ IntFractPair.stream v (n✝ + 1) = none
[PROOFSTEP]
simp [IntFractPair.stream, hyp]


[GOAL]
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
inst✝² : CharZero R✝
R : Type u_2
inst✝¹ : Semiring R
inst✝ : CharZero R
q n : ℕ
hn : n ≠ 0
⊢ ↑q ^ n = 1 ↔ q = 1
[PROOFSTEP]
rw [← cast_pow, cast_eq_one]
[GOAL]
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
inst✝² : CharZero R✝
R : Type u_2
inst✝¹ : Semiring R
inst✝ : CharZero R
q n : ℕ
hn : n ≠ 0
⊢ q ^ n = 1 ↔ q = 1
[PROOFSTEP]
exact pow_eq_one_iff hn
[GOAL]
R : Type u_1
inst✝³ : AddMonoidWithOne R
inst✝² : CharZero R
k : Type u_2
inst✝¹ : DivisionSemiring k
inst✝ : CharZero k
m n : ℕ
n_dvd : n ∣ m
⊢ ↑(m / n) = ↑m / ↑n
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
R : Type u_1
inst✝³ : AddMonoidWithOne R
inst✝² : CharZero R
k : Type u_2
inst✝¹ : DivisionSemiring k
inst✝ : CharZero k
m : ℕ
n_dvd : 0 ∣ m
⊢ ↑(m / 0) = ↑m / ↑0
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
inst✝³ : AddMonoidWithOne R
inst✝² : CharZero R
k : Type u_2
inst✝¹ : DivisionSemiring k
inst✝ : CharZero k
m n : ℕ
n_dvd : n ∣ m
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
[PROOFSTEP]
exact cast_div n_dvd (cast_ne_zero.2 hn)
[GOAL]
M : Type u_1
inst✝¹ : AddMonoidWithOne M
inst✝ : CharZero M
⊢ 2 ≠ 0
[PROOFSTEP]
have : ((2 : ℕ) : M) ≠ 0 := Nat.cast_ne_zero.2 (by decide)
[GOAL]
M : Type u_1
inst✝¹ : AddMonoidWithOne M
inst✝ : CharZero M
⊢ 2 ≠ 0
[PROOFSTEP]
decide
[GOAL]
M : Type u_1
inst✝¹ : AddMonoidWithOne M
inst✝ : CharZero M
this : ↑2 ≠ 0
⊢ 2 ≠ 0
[PROOFSTEP]
rwa [Nat.cast_two] at this
[GOAL]
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a✝ a : R
⊢ a + a = 0 ↔ a = 0
[PROOFSTEP]
simp only [(two_mul a).symm, mul_eq_zero, two_ne_zero, false_or_iff]
[GOAL]
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a✝ a : R
⊢ 0 = bit0 a ↔ a = 0
[PROOFSTEP]
rw [eq_comm]
[GOAL]
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a✝ a : R
⊢ bit0 a = 0 ↔ a = 0
[PROOFSTEP]
exact bit0_eq_zero
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h : ↑n * a = ↑n * b
⊢ n = 0 ∨ a = b
[PROOFSTEP]
rw [← sub_eq_zero, ← mul_sub, mul_eq_zero, sub_eq_zero] at h
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h✝ : ↑n * a = ↑n * b
h : ↑n = 0 ∨ a = b
⊢ n = 0 ∨ a = b
[PROOFSTEP]
exact_mod_cast h
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h : ↑n * a = ↑n * b
w : n ≠ 0
⊢ a = b
[PROOFSTEP]
simpa [w] using nat_mul_inj h
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a b : R
h : bit0 a = bit0 b
⊢ a = b
[PROOFSTEP]
dsimp [bit0] at h
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a b : R
h : a + a = b + b
⊢ a = b
[PROOFSTEP]
simp only [(two_mul a).symm, (two_mul b).symm] at h
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a b : R
h : 2 * a = 2 * b
⊢ a = b
[PROOFSTEP]
refine' nat_mul_inj' _ two_ne_zero
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a b : R
h : 2 * a = 2 * b
⊢ ↑2 * a = ↑2 * b
[PROOFSTEP]
exact_mod_cast h
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a b : R
h : bit1 a = bit1 b
⊢ a = b
[PROOFSTEP]
simp only [bit1, add_left_inj] at h
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a b : R
h : bit0 a = bit0 b
⊢ a = b
[PROOFSTEP]
exact bit0_injective h
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a : R
⊢ bit1 a = 1 ↔ a = 0
[PROOFSTEP]
rw [show (1 : R) = bit1 0 by simp, bit1_eq_bit1]
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a : R
⊢ 1 = bit1 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a : R
⊢ 1 = bit1 a ↔ a = 0
[PROOFSTEP]
rw [eq_comm]
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a : R
⊢ bit1 a = 1 ↔ a = 0
[PROOFSTEP]
exact bit1_eq_one
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
a : R
⊢ (a + a) / 2 = a
[PROOFSTEP]
rw [← mul_two, mul_div_cancel a two_ne_zero]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
a : R
⊢ a / 2 + a / 2 = a
[PROOFSTEP]
rw [← add_div, half_add_self]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
a : R
⊢ a - a / 2 = a / 2
[PROOFSTEP]
rw [sub_eq_iff_eq_add, add_halves']
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
a : R
⊢ a / 2 - a = -(a / 2)
[PROOFSTEP]
rw [← neg_sub, sub_half]
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
m n : ℕ
h : ↑m = ↑n
⊢ m = n
[PROOFSTEP]
rwa [← coe_nat, ← coe_nat n, coe_eq_coe, Nat.cast_inj] at h
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
m n : ℕ
h : ↑m = ↑n
⊢ m = n
[PROOFSTEP]
rwa [← coe_nat, ← coe_nat n, coe_eq_coe, Nat.cast_inj] at h
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hS : CharZero S
a b : ℕ
h : ↑a = ↑b
⊢ ↑a = ↑b
[PROOFSTEP]
rw [← map_natCast ϕ, ← map_natCast ϕ, h]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Function.Injective ↑ϕ
hR : CharZero R
⊢ Function.Injective Nat.cast
[PROOFSTEP]
intro a b h
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Function.Injective ↑ϕ
hR : CharZero R
a b : ℕ
h : ↑a = ↑b
⊢ a = b
[PROOFSTEP]
rwa [← @Nat.cast_inj R, ← hϕ.eq_iff, map_natCast ϕ, map_natCast ϕ]


[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
f g : AddMonoidAlgebra M ι
⊢ toDirectSum (f * g) = toDirectSum f * toDirectSum g
[PROOFSTEP]
let to_hom : AddMonoidAlgebra M ι →+ ⨁ _ : ι, M :=
  { toFun := toDirectSum
    map_zero' := toDirectSum_zero
    map_add' := toDirectSum_add }
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
f g : AddMonoidAlgebra M ι
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
⊢ toDirectSum (f * g) = toDirectSum f * toDirectSum g
[PROOFSTEP]
show to_hom (f * g) = to_hom f * to_hom g
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
f g : AddMonoidAlgebra M ι
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
⊢ ↑to_hom (f * g) = ↑to_hom f * ↑to_hom g
[PROOFSTEP]
let _ : NonUnitalNonAssocSemiring (ι →₀ M) := AddMonoidAlgebra.nonUnitalNonAssocSemiring
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
f g : AddMonoidAlgebra M ι
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring
⊢ ↑to_hom (f * g) = ↑to_hom f * ↑to_hom g
[PROOFSTEP]
revert f g
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring
⊢ ∀ (f g : AddMonoidAlgebra M ι), ↑to_hom (f * g) = ↑to_hom f * ↑to_hom g
[PROOFSTEP]
rw [AddMonoidHom.map_mul_iff]
  -- porting note: does not find `addHom_ext'`, was `ext (xi xv yi yv) : 4`
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring
⊢ AddMonoidHom.compr₂ AddMonoidHom.mul to_hom = AddMonoidHom.compl₂ (AddMonoidHom.comp AddMonoidHom.mul to_hom) to_hom
[PROOFSTEP]
refine Finsupp.addHom_ext' fun xi => AddMonoidHom.ext fun xv => ?_
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring
xi : ι
xv : M
⊢ ↑(AddMonoidHom.comp (AddMonoidHom.compr₂ AddMonoidHom.mul to_hom) (Finsupp.singleAddHom xi)) xv =
    ↑(AddMonoidHom.comp (AddMonoidHom.compl₂ (AddMonoidHom.comp AddMonoidHom.mul to_hom) to_hom)
          (Finsupp.singleAddHom xi))
      xv
[PROOFSTEP]
refine Finsupp.addHom_ext' fun yi => AddMonoidHom.ext fun yv => ?_
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring
xi : ι
xv : M
yi : ι
yv : M
⊢ ↑(AddMonoidHom.comp (↑(AddMonoidHom.comp (AddMonoidHom.compr₂ AddMonoidHom.mul to_hom) (Finsupp.singleAddHom xi)) xv)
          (Finsupp.singleAddHom yi))
      yv =
    ↑(AddMonoidHom.comp
          (↑(AddMonoidHom.comp (AddMonoidHom.compl₂ (AddMonoidHom.comp AddMonoidHom.mul to_hom) to_hom)
                (Finsupp.singleAddHom xi))
            xv)
          (Finsupp.singleAddHom yi))
      yv
[PROOFSTEP]
dsimp only [AddMonoidHom.comp_apply, AddMonoidHom.compl₂_apply, AddMonoidHom.compr₂_apply, AddMonoidHom.mul_apply,
  Finsupp.singleAddHom_apply]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring
xi : ι
xv : M
yi : ι
yv : M
⊢ ↑{ toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
          map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
      (Finsupp.single xi xv * Finsupp.single yi yv) =
    ↑{ toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
            map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
        (Finsupp.single xi xv) *
      ↑{ toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
            map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
        (Finsupp.single yi yv)
[PROOFSTEP]
simp only [AddMonoidHom.coe_mk, ZeroHom.coe_mk, toDirectSum_single]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring
xi : ι
xv : M
yi : ι
yv : M
⊢ toDirectSum (Finsupp.single xi xv * Finsupp.single yi yv) =
    ↑(DirectSum.of (fun i => M) xi) xv * ↑(DirectSum.of (fun i => M) yi) yv
[PROOFSTEP]
erw [AddMonoidAlgebra.single_mul_single, AddMonoidHom.coe_mk, ZeroHom.coe_mk, AddMonoidAlgebra.toDirectSum_single]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring
xi : ι
xv : M
yi : ι
yv : M
⊢ ↑(DirectSum.of (fun i => M) (xi + yi)) (xv * yv) = DFinsupp.single xi xv * ↑(DirectSum.of (fun i => M) yi) yv
[PROOFSTEP]
simp only [AddMonoidHom.coe_comp, AddMonoidHom.coe_mul, AddMonoidHom.coe_mk, ZeroHom.coe_mk, Function.comp_apply,
  toDirectSum_single, AddMonoidHom.id_apply, Finsupp.singleAddHom_apply, AddMonoidHom.coe_mulLeft]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring
xi : ι
xv : M
yi : ι
yv : M
⊢ ↑(DirectSum.of (fun i => M) (xi + yi)) (xv * yv) = DFinsupp.single xi xv * ↑(DirectSum.of (fun i => M) yi) yv
[PROOFSTEP]
erw [DirectSum.of_mul_of, Mul.gMul_mul]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ toAddMonoidAlgebra (f * g) = toAddMonoidAlgebra f * toAddMonoidAlgebra g
[PROOFSTEP]
apply_fun AddMonoidAlgebra.toDirectSum
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ AddMonoidAlgebra.toDirectSum (toAddMonoidAlgebra (f * g)) =
    AddMonoidAlgebra.toDirectSum (toAddMonoidAlgebra f * toAddMonoidAlgebra g)
[PROOFSTEP]
simp
[GOAL]
case inj
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ Function.Injective AddMonoidAlgebra.toDirectSum
[PROOFSTEP]
apply Function.LeftInverse.injective
[GOAL]
case inj.a
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ Function.LeftInverse ?inj.g AddMonoidAlgebra.toDirectSum
case inj.g
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (⨁ (x : ι), M) → AddMonoidAlgebra M ι
[PROOFSTEP]
apply AddMonoidAlgebra.toDirectSum_toAddMonoidAlgebra


[GOAL]
R : Type u_1
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
a : R
s : Set R
ha : a ∈ center R
⊢ star a ∈ center R
[PROOFSTEP]
simpa only [star_mul, star_star] using fun g => congr_arg star ((Set.mem_center_iff R).mp ha <| star g).symm
[GOAL]
R : Type u_1
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
a : R
s : Set R
h : ∀ (a : R), a ∈ s → star a ∈ s
ha : a ∈ centralizer s
y : R
hy : y ∈ s
⊢ y * star a = star a * y
[PROOFSTEP]
simpa using congr_arg star (ha _ (h _ hy)).symm


[GOAL]
I✝ : Type u
f : I✝ → Type v
I : Type u_1
J : Type u_2
α : Type u_3
x : I → α
y : J → α
inst✝ : Star α
⊢ star (Sum.elim x y) = Sum.elim (star x) (star y)
[PROOFSTEP]
ext x
[GOAL]
case h
I✝ : Type u
f : I✝ → Type v
I : Type u_1
J : Type u_2
α : Type u_3
x✝ : I → α
y : J → α
inst✝ : Star α
x : I ⊕ J
⊢ star (Sum.elim x✝ y) x = Sum.elim (star x✝) (star y) x
[PROOFSTEP]
cases x
[GOAL]
case h.inl
I✝ : Type u
f : I✝ → Type v
I : Type u_1
J : Type u_2
α : Type u_3
x : I → α
y : J → α
inst✝ : Star α
val✝ : I
⊢ star (Sum.elim x y) (Sum.inl val✝) = Sum.elim (star x) (star y) (Sum.inl val✝)
[PROOFSTEP]
simp only [Pi.star_apply, Sum.elim_inl, Sum.elim_inr]
[GOAL]
case h.inr
I✝ : Type u
f : I✝ → Type v
I : Type u_1
J : Type u_2
α : Type u_3
x : I → α
y : J → α
inst✝ : Star α
val✝ : J
⊢ star (Sum.elim x y) (Sum.inr val✝) = Sum.elim (star x) (star y) (Sum.inr val✝)
[PROOFSTEP]
simp only [Pi.star_apply, Sum.elim_inl, Sum.elim_inr]


[GOAL]
α : Type u_1
s t : Set α
a : α
inst✝ : InvolutiveStar α
⊢ a⋆ ∈ s⋆ ↔ a ∈ s
[PROOFSTEP]
simp only [mem_star, star_star]
[GOAL]
α : Type u_1
s t : Set α
a : α
inst✝ : InvolutiveStar α
⊢ star '' s = s⋆
[PROOFSTEP]
simp only [← star_preimage]
[GOAL]
α : Type u_1
s t : Set α
a : α
inst✝ : InvolutiveStar α
⊢ star '' s = star ⁻¹' s
[PROOFSTEP]
rw [image_eq_preimage_of_inverse]
[GOAL]
case h₁
α : Type u_1
s t : Set α
a : α
inst✝ : InvolutiveStar α
⊢ Function.LeftInverse star star
[PROOFSTEP]
intro
[GOAL]
case h₂
α : Type u_1
s t : Set α
a : α
inst✝ : InvolutiveStar α
⊢ Function.RightInverse star star
[PROOFSTEP]
intro
[GOAL]
case h₁
α : Type u_1
s t : Set α
a : α
inst✝ : InvolutiveStar α
x✝ : α
⊢ x✝⋆⋆ = x✝
[PROOFSTEP]
simp only [star_star]
[GOAL]
case h₂
α : Type u_1
s t : Set α
a : α
inst✝ : InvolutiveStar α
x✝ : α
⊢ x✝⋆⋆ = x✝
[PROOFSTEP]
simp only [star_star]
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
inst✝ : InvolutiveStar α
s : Set α
⊢ s⋆⋆ = s
[PROOFSTEP]
simp only [← star_preimage, preimage_preimage, star_star, preimage_id']
[GOAL]
α : Type u_1
s✝ t✝ : Set α
a : α
inst✝ : InvolutiveStar α
s t : Set α
⊢ s⋆ ⊆ t ↔ s ⊆ t⋆
[PROOFSTEP]
rw [← star_subset_star, star_star]
[GOAL]
α : Type u_1
s t : Set α
a : α
β : Type u_2
inst✝ : InvolutiveStar β
x : β
⊢ {x}⋆ = {x⋆}
[PROOFSTEP]
ext1 y
[GOAL]
case h
α : Type u_1
s t : Set α
a : α
β : Type u_2
inst✝ : InvolutiveStar β
x y : β
⊢ y ∈ {x}⋆ ↔ y ∈ {x⋆}
[PROOFSTEP]
rw [mem_star, mem_singleton_iff, mem_singleton_iff, star_eq_iff_star_eq, eq_comm]
[GOAL]
α : Type u_1
s✝ t✝ : Set α
a : α
inst✝¹ : Monoid α
inst✝ : StarSemigroup α
s t : Set α
⊢ (s * t)⋆ = t⋆ * s⋆
[PROOFSTEP]
simp_rw [← image_star, ← image2_mul, image_image2, image2_image_left, image2_image_right, star_mul, image2_swap _ s t]
[GOAL]
α : Type u_1
s✝ t✝ : Set α
a : α
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
s t : Set α
⊢ (s + t)⋆ = s⋆ + t⋆
[PROOFSTEP]
simp_rw [← image_star, ← image2_add, image_image2, image2_image_left, image2_image_right, star_add]
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Star α
inst✝ : TrivialStar α
s : Set α
⊢ s⋆ = s
[PROOFSTEP]
rw [← star_preimage]
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Star α
inst✝ : TrivialStar α
s : Set α
⊢ star ⁻¹' s = s
[PROOFSTEP]
ext1
[GOAL]
case h
α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Star α
inst✝ : TrivialStar α
s : Set α
x✝ : α
⊢ x✝ ∈ star ⁻¹' s ↔ x✝ ∈ s
[PROOFSTEP]
simp [star_trivial]
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Group α
inst✝ : StarSemigroup α
s : Set α
⊢ s⁻¹⋆ = s⋆⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Group α
inst✝ : StarSemigroup α
s : Set α
x✝ : α
⊢ x✝ ∈ s⁻¹⋆ ↔ x✝ ∈ s⋆⁻¹
[PROOFSTEP]
simp only [mem_star, mem_inv, star_inv]
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : DivisionSemiring α
inst✝ : StarRing α
s : Set α
⊢ s⁻¹⋆ = s⋆⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : DivisionSemiring α
inst✝ : StarRing α
s : Set α
x✝ : α
⊢ x✝ ∈ s⁻¹⋆ ↔ x✝ ∈ s⋆⁻¹
[PROOFSTEP]
simp only [mem_star, mem_inv, star_inv']
[GOAL]
S : Type u_1
α : Type u_2
inst✝² : InvolutiveStar α
inst✝¹ : SetLike S α
inst✝ : StarMemClass S α
s : S
⊢ star ↑s = ↑s
[PROOFSTEP]
ext x
[GOAL]
case h
S : Type u_1
α : Type u_2
inst✝² : InvolutiveStar α
inst✝¹ : SetLike S α
inst✝ : StarMemClass S α
s : S
x : α
⊢ x ∈ star ↑s ↔ x ∈ ↑s
[PROOFSTEP]
simp only [Set.mem_star, SetLike.mem_coe]
[GOAL]
case h
S : Type u_1
α : Type u_2
inst✝² : InvolutiveStar α
inst✝¹ : SetLike S α
inst✝ : StarMemClass S α
s : S
x : α
⊢ star x ∈ s ↔ x ∈ s
[PROOFSTEP]
exact ⟨by simpa only [star_star] using star_mem (s := s) (r := star x), star_mem⟩
[GOAL]
S : Type u_1
α : Type u_2
inst✝² : InvolutiveStar α
inst✝¹ : SetLike S α
inst✝ : StarMemClass S α
s : S
x : α
⊢ star x ∈ s → x ∈ s
[PROOFSTEP]
simpa only [star_star] using star_mem (s := s) (r := star x)