awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
g : Γ'
hg : (embDomain f x * embDomain f y).coeff g ≠ 0
neg :
  ∀ (w : Γ') (hi : w ∈ (embDomain f x).support) (w_1 : Γ') (hj : w_1 ∈ (embDomain f y).support)
    (hg : (embDomain f x * embDomain f y).coeff ((fun (x1 x2 : Γ') ↦ x1 + x2) w w_1) ≠ 0),
    Membership.mem (γ := Set Γ') (Set.range.{u_6, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ'))
      ((fun (x1 x2 : Γ') ↦ x1 + x2) w w_1)
⊢ Membership.mem (γ := Set Γ') (Set.range.{u_6, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) g

Tactic:
obtain ⟨_, hi, _, hj, rfl⟩ := support_mul_subset ((mem_support _ _).2 hg)

Premises used: Iff.mpr, HahnSeries.support_mul_subset, rfl, HahnSeries.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
w : Γ'
hi : w ∈ (embDomain f x).support
w_1 : Γ'
hj : w_1 ∈ (embDomain f y).support
hg : (embDomain f x * embDomain f y).coeff ((fun (x1 x2 : Γ') ↦ x1 + x2) w w_1) ≠ 0
neg :
  ∀ i ∈ x.support,
    ∀ (hi : Membership.mem (α := Γ') (embDomain f x).support ((f : (a : Γ) → Γ') i : Γ'))
      (hg : (embDomain f x * embDomain f y).coeff ((fun (x1 x2 : Γ') ↦ x1 + x2) ((f : (a : Γ) → Γ') i) w_1) ≠ 0),
      Membership.mem (γ := Set Γ') (Set.range.{u_6, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ'))
        ((fun (x1 x2 : Γ') ↦ x1 + x2) ((f : (a : Γ) → Γ') i) w_1)
⊢ Membership.mem (γ := Set Γ') (Set.range.{u_6, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ'))
    ((fun (x1 x2 : Γ') ↦ x1 + x2) w w_1)

Tactic:
obtain ⟨i, _, rfl⟩ := support_embDomain_subset hi

Premises used: HahnSeries.support_embDomain_subset, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
w : Γ'
hj : w ∈ (embDomain f y).support
i : Γ
left : i ∈ x.support
hi : Membership.mem (α := Γ') (embDomain f x).support ((f : (a : Γ) → Γ') i : Γ')
hg : (embDomain f x * embDomain f y).coeff ((fun (x1 x2 : Γ') ↦ x1 + x2) ((f : (a : Γ) → Γ') i) w) ≠ 0
neg :
  ∀ j ∈ y.support,
    ∀ (hj : Membership.mem (α := Γ') (embDomain f y).support ((f : (a : Γ) → Γ') j : Γ'))
      (hg :
        (embDomain f x * embDomain f y).coeff
            ((fun (x1 x2 : Γ') ↦ x1 + x2) ((f : (a : Γ) → Γ') i) ((f : (a : Γ) → Γ') j)) ≠
          0),
      Membership.mem (γ := Set Γ') (Set.range.{u_6, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ'))
        ((fun (x1 x2 : Γ') ↦ x1 + x2) ((f : (a : Γ) → Γ') i) ((f : (a : Γ) → Γ') j))
⊢ Membership.mem (γ := Set Γ') (Set.range.{u_6, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ'))
    ((fun (x1 x2 : Γ') ↦ x1 + x2) ((f : (a : Γ) → Γ') i) w)

Tactic:
obtain ⟨j, _, rfl⟩ := support_embDomain_subset hj

Premises used: HahnSeries.support_embDomain_subset, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
i : Γ
left : i ∈ x.support
hi : Membership.mem (α := Γ') (embDomain f x).support ((f : (a : Γ) → Γ') i : Γ')
j : Γ
left_1 : j ∈ y.support
hj : Membership.mem (α := Γ') (embDomain f y).support ((f : (a : Γ) → Γ') j : Γ')
hg :
  (embDomain f x * embDomain f y).coeff ((fun (x1 x2 : Γ') ↦ x1 + x2) ((f : (a : Γ) → Γ') i) ((f : (a : Γ) → Γ') j)) ≠ 0
⊢ Membership.mem (γ := Set Γ') (Set.range.{u_6, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ'))
    ((fun (x1 x2 : Γ') ↦ x1 + x2) ((f : (a : Γ) → Γ') i) ((f : (a : Γ) → Γ') j))

Tactic:
⟨i + j, hf i j⟩

Premises used: Set.Mem, setOf, HAdd.hAdd, Exists.intro, Set.range
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
i : Γ
left : i ∈ x.support
hi : Membership.mem (α := Γ') (embDomain f x).support ((f : (a : Γ) → Γ') i : Γ')
j : Γ
left_1 : j ∈ y.support
hj : Membership.mem (α := Γ') (embDomain f y).support ((f : (a : Γ) → Γ') j : Γ')
hg :
  (embDomain f x * embDomain f y).coeff ((fun (x1 x2 : Γ') ↦ x1 + x2) ((f : (a : Γ) → Γ') i) ((f : (a : Γ) → Γ') j)) ≠ 0
⊢ Membership.mem (γ := Set Γ') (Set.range.{u_6, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ'))
    ((fun (x1 x2 : Γ') ↦ x1 + x2) ((f : (a : Γ) → Γ') i) ((f : (a : Γ) → Γ') j))

Tactic:
exact ⟨i + j, hf i j⟩
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
Γ' : Type u_6
inst_2 : AddCommMonoid Γ'
inst_3 : PartialOrder Γ'
inst_4 : NonAssocSemiring R
f : Γ ↪o Γ'
hf : Eq.{u_6 + 1} (α := Γ') ((f : (a : Γ) → Γ') 0 : Γ') (0 : Γ')
⊢ Eq (α := R⟦Γ'⟧) (embDomain f 1) 1

Tactic:
embDomain_single.trans <| hf.symm ▸ rfl

Premises used: Eq.rec, HahnSeries.embDomain_single, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonAssocSemiring R
f : Γ →+ Γ'
hfi : Injective.{u_1 + 1, u_6 + 1} (α := Γ) (β := Γ') (⇑f : (a : Γ) → Γ')
hf : ∀ (g g' : Γ), LE.le.{u_6} (α := Γ') ((f : (a : Γ) → Γ') g : Γ') ((f : (a : Γ) → Γ') g' : Γ') ↔ g ≤ g'
r : R
⊢ Eq (α := R⟦Γ'⟧)
    (((single
              ((RelEmbedding.mk (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)
                    { toFun := (⇑f : (a : Γ) → Γ'), inj' := hfi } ⋯ :
                  (a : Γ) → Γ')
                0) :
            ZeroHom R R⟦Γ'⟧) :
          (a : R) → R⟦Γ'⟧)
        r :
      R⟦Γ'⟧)
    ((C : (a : R) → R⟦Γ'⟧) r : R⟦Γ'⟧)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommSemiring R
A : Type u_6
inst_4 : Semiring A
inst_5 : Algebra R A
r : R
x : A⟦Γ⟧
coeff :
  ∀ (x_1 : Γ),
    (HMul.hMul (α := A⟦Γ⟧) ((RingHom.comp C (algebraMap R A) : (a : R) → A⟦Γ⟧) r : A⟦Γ⟧) x).coeff x_1 =
      (HMul.hMul (β := A⟦Γ⟧) x ((RingHom.comp C (algebraMap R A) : (a : R) → A⟦Γ⟧) r : A⟦Γ⟧)).coeff x_1
⊢ HMul.hMul (α := A⟦Γ⟧) ((RingHom.comp C (algebraMap R A) : (a : R) → A⟦Γ⟧) r : A⟦Γ⟧) x =
    HMul.hMul (β := A⟦Γ⟧) x ((RingHom.comp C (algebraMap R A) : (a : R) → A⟦Γ⟧) r : A⟦Γ⟧)

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommSemiring R
A : Type u_6
inst_4 : Semiring A
inst_5 : Algebra R A
r : R
x : A⟦Γ⟧
x_1 : Γ
coeff : r • x.coeff x_1 = HMul.hMul (β := A) (x.coeff x_1) ((algebraMap R A : (a : R) → A) r : A)
⊢ (HMul.hMul (α := A⟦Γ⟧) ((RingHom.comp C (algebraMap R A) : (a : R) → A⟦Γ⟧) r : A⟦Γ⟧) x).coeff x_1 =
    (HMul.hMul (β := A⟦Γ⟧) x ((RingHom.comp C (algebraMap R A) : (a : R) → A⟦Γ⟧) r : A⟦Γ⟧)).coeff x_1

Tactic:
simp only [coeff_smul, single_zero_mul_eq_smul, RingHom.coe_comp, C_apply,
      Function.comp_apply, algebraMap_smul, coeff_mul_single_zero]

Premises used: HahnSeries.single_zero_mul_eq_smul, HahnSeries.coeff_smul, algebraMap_smul, RingHom.coe_comp, Function.comp_apply, HahnSeries.coeff_mul_single_zero, HahnSeries.C_apply
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommSemiring R
A : Type u_6
inst_4 : Semiring A
inst_5 : Algebra R A
r : R
x : A⟦Γ⟧
x_1 : Γ
coeff : r • x.coeff x_1 = HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x.coeff x_1)
coeff₁ coeff₂ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x.coeff x_1) =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x.coeff x_1)
⊢ r • x.coeff x_1 = HMul.hMul (β := A) (x.coeff x_1) ((algebraMap R A : (a : R) → A) r : A)

Tactic:
rw [← Algebra.commutes, Algebra.smul_def]

Premises used: Algebra.smul_def, Algebra.commutes
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommSemiring R
A : Type u_6
inst_4 : Semiring A
inst_5 : Algebra R A
r : R
x : A⟦Γ⟧
coeff :
  ∀ (x_1 : Γ),
    (r • x).coeff x_1 =
      (HMul.hMul (α := A⟦Γ⟧) ((RingHom.comp C (algebraMap R A) : (a : R) → A⟦Γ⟧) r : A⟦Γ⟧) x).coeff x_1
⊢ r • x = HMul.hMul (α := A⟦Γ⟧) ((RingHom.comp C (algebraMap R A) : (a : R) → A⟦Γ⟧) r : A⟦Γ⟧) x

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommSemiring R
A : Type u_6
inst_4 : Semiring A
inst_5 : Algebra R A
r : R
x : A⟦Γ⟧
x_1 : Γ
⊢ (r • x).coeff x_1 = (HMul.hMul (α := A⟦Γ⟧) ((RingHom.comp C (algebraMap R A) : (a : R) → A⟦Γ⟧) r : A⟦Γ⟧) x).coeff x_1

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommSemiring R
⊢ Eq (α := R →+* R⟦Γ⟧) C (algebraMap R R⟦Γ⟧)

Tactic:
rfl

Premises used: HahnSeries.C, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommSemiring R
A : Type u_6
inst_4 : Semiring A
inst_5 : Algebra R A
r : R
⊢ Eq (α := A⟦Γ⟧) ((algebraMap R A⟦Γ⟧ : (a : R) → A⟦Γ⟧) r : A⟦Γ⟧)
    ((C : (a : A) → A⟦Γ⟧) ((algebraMap R A : (a : R) → A) r) : A⟦Γ⟧)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
hyz : Eq (α := R⟦Γ⟧) ((fun (x_1 : R⟦Γ⟧) ↦ x * x_1) y) ((fun (x_1 : R⟦Γ⟧) ↦ x * x_1) z)
this : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
contrapose! : ∀ (hyz : y ≠ z), x * y ≠ x * z
⊢ y = z

Tactic:
contrapose! hyz
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : y ≠ z
simp : ∀ (hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x), ∃ (x_1 : Γ), ¬(x * y).coeff x_1 = (x * z).coeff x_1
⊢ x * y ≠ x * z

Tactic:
simp only [ne_eq, ← coeff_inj, funext_iff, not_forall] at ⊢ hyz

Premises used: funext_iff, ne_eq, HahnSeries.coeff_inj, Classical.not_forall
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
a : Γ
⊢ ¬y.coeff a = z.coeff a → ¬y.coeff a = 0 ∨ ¬z.coeff a = 0

Tactic:
grind
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
⊢ Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}

Tactic:
have : Set.IsWF {a | y.coeff a ≠ z.coeff a} :=
      .mono (y.isWF_support.union z.isWF_support) (by intro; simp; grind)
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
⊢ y.coeff a ≠ z.coeff a

Tactic:
have ha : y.coeff a ≠ z.coeff a := this.min_mem hyz
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
⊢ ∃ (x_1 : Γ), ¬(x * y).coeff x_1 = (x * z).coeff x_1

Tactic:
⟨x.order + a, ?_⟩

Premises used: HahnSeries.order, HAdd.hAdd, Exists.intro
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
refine : ¬(x * y).coeff (x.order + a) = (x * z).coeff (x.order + a)
⊢ ∃ (x_1 : Γ), ¬(x * y).coeff x_1 = (x * z).coeff x_1

Tactic:
refine ⟨x.order + a, ?_⟩
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
hi :
  (x.order, a) ∈
    addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ (x.order + a) ∪
      addAntidiagonal (s := x.support) (t := z.support) ⋯ ⋯ (x.order + a)
hfg :
  ∀
    j ∈
      addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ (x.order + a) ∪
        addAntidiagonal (s := x.support) (t := z.support) ⋯ ⋯ (x.order + a),
    j ≠ (x.order, a) → x.coeff j.1 * y.coeff j.2 = x.coeff j.1 * z.coeff j.2
rwa :
  ∀
    x_1 ∈
      addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ (x.order + a) ∪
        addAntidiagonal (s := x.support) (t := z.support) ⋯ ⋯ (x.order + a),
    x_1 ∉ addAntidiagonal (s := x.support) (t := z.support) ⋯ ⋯ (x.order + a) → x.coeff x_1.1 * z.coeff x_1.2 = 0
rwa₁ :
  ∀
    x_1 ∈
      addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ (x.order + a) ∪
        addAntidiagonal (s := x.support) (t := z.support) ⋯ ⋯ (x.order + a),
    x_1 ∉ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ (x.order + a) → x.coeff x_1.1 * y.coeff x_1.2 = 0
⊢ ¬(x * y).coeff (x.order + a) = (x * z).coeff (x.order + a)

Tactic:
rwa [coeff_mul, coeff_mul, sum_subset subset_union_left,
      sum_subset (s₁ := addAntidiagonal _ _ _) subset_union_right,
      sum_eq_sum_iff_single (i := (x.order, a)), mul_right_inj' (coeff_order_eq_zero.not.2 hx)]

Premises used: Iff.mpr, HahnSeries.coeff_mul, Iff.not, Finset.subset_union_left, HahnSeries.coeff_order_eq_zero, Finset.sum_subset, Finset.sum_eq_sum_iff_single, mul_right_inj', Finset.subset_union_right
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
hi : ¬y.coeff a = 0 ∨ ¬z.coeff a = 0
⊢ (x.order, a) ∈
    addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ (x.order + a) ∪
      addAntidiagonal (s := x.support) (t := z.support) ⋯ ⋯ (x.order + a)

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
⊢ ¬y.coeff a = 0 ∨ ¬z.coeff a = 0

Tactic:
grind
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
hfg :
  ∀ (a_1 b : Γ),
    ¬x.coeff a_1 = 0 →
      ¬y.coeff b = 0 ∨ ¬z.coeff b = 0 → a_1 + b = x.order + a → (a_1 = x.order → ¬b = a) → y.coeff b = z.coeff b
⊢ ∀
    j ∈
      addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ (x.order + a) ∪
        addAntidiagonal (s := x.support) (t := z.support) ⋯ ⋯ (x.order + a),
    j ≠ (x.order, a) → x.coeff j.1 * y.coeff j.2 = x.coeff j.1 * z.coeff j.2

Tactic:
simp +contextual only [mem_union, mem_addAntidiagonal, mul_eq_mul_left_iff, Prod.mk.injEq,
        ne_eq, ← and_or_left, ← or_and_right, or_false, and_imp, Prod.forall, mem_support, not_and]

Premises used: and_or_left, and_imp, mul_eq_mul_left_iff, ne_eq, Prod.mk.injEq, Prod.forall, Finset.mem_union, or_false, not_and, or_and_right, HahnSeries.mem_support, Finset.mem_addAntidiagonal
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
b c : Γ
hxb : ¬x.coeff b = 0
hbc : b + c = x.order + a
hbc' : b = x.order → ¬c = a
hfg : ∀ (hbc' : y.coeff c ≠ z.coeff c), b = x.order ∧ c = a
⊢ y.coeff c = z.coeff c

Tactic:
contrapose! hbc'
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
b c : Γ
hxb : ¬x.coeff b = 0
hbc : b + c = x.order + a
hbc' : y.coeff c ≠ z.coeff c
hfg : x.order = b ∧ c = a
hfg₁ : x.order = b ∧ a = c
hfg₂ : x.order + this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz = b + c
hfg₃ hfg₄ hfg₅ hfg₆ : b + c = x.order + this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
⊢ b = x.order ∧ c = a

Tactic:
rwa [eq_comm, eq_comm (a := c), ← add_eq_add_iff_eq_and_eq (order_le_of_coeff_ne_zero hxb)
        (Set.IsWF.min_le _ _ hbc'), eq_comm]

Premises used: add_eq_add_iff_eq_and_eq, HahnSeries.order_le_of_coeff_ne_zero, eq_comm, Set.IsWF.min_le
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
⊢ ∀
    x_1 ∈
      addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ (x.order + a) ∪
        addAntidiagonal (s := x.support) (t := z.support) ⋯ ⋯ (x.order + a),
    x_1 ∉ addAntidiagonal (s := x.support) (t := z.support) ⋯ ⋯ (x.order + a) → x.coeff x_1.1 * z.coeff x_1.2 = 0

Tactic:
simp +contextual [← and_or_left, ← or_and_right]

Premises used: and_or_left, or_and_right