awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : (↑p.vars : Set σ) ⊆ range f
x : R
⊢ Eq (α := MvPolynomial σ R)
    ((RingHom.comp (β := MvPolynomial σ R)
            (RingHom.comp (AlgHom.toRingHom (rename f))
              (AlgHom.toRingHom (aeval fun (i : σ) ↦ Option.elim' 0 X (partialInv f i))))
            C :
          (a : R) → MvPolynomial σ R)
        x :
      MvPolynomial σ R)
    ((RingHom.comp (RingHom.id (MvPolynomial σ R)) C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)

Tactic:
simp [algebraMap_eq]

Premises used: MvPolynomial.algebraMap_eq
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : (↑p.vars : Set σ) ⊆ range f
i : σ
hip : i ∈ p.vars
refine_2 :
  i ∈ p.vars →
    Eq (α := MvPolynomial σ R)
      ((RingHom.comp (AlgHom.toRingHom (rename f))
              (AlgHom.toRingHom (aeval fun (i : σ) ↦ Option.elim' 0 X (partialInv f i))) :
            (a : MvPolynomial σ R) → MvPolynomial σ R)
          (X i) :
        MvPolynomial σ R)
      ((RingHom.id (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
⊢ i ∈ p.vars →
    Eq (α := MvPolynomial σ R)
      ((RingHom.comp (AlgHom.toRingHom (rename f))
              (AlgHom.toRingHom (aeval fun (i : σ) ↦ Option.elim' 0 X (partialInv f i))) :
            (a : MvPolynomial σ R) → MvPolynomial σ R)
          (X i) :
        MvPolynomial σ R)
      ((RingHom.id (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)

Tactic:
_
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : (↑p.vars : Set σ) ⊆ range f
i : σ
hip h : i ∈ p.vars
refine_2 :
  ∀ (i : τ) (hip : f i ∈ p.vars),
    f i ∈ p.vars →
      Eq (α := MvPolynomial σ R)
        ((RingHom.comp (AlgHom.toRingHom (rename f))
                (AlgHom.toRingHom (aeval fun (i : σ) ↦ Option.elim' 0 X (partialInv f i))) :
              (a : MvPolynomial σ R) → MvPolynomial σ R)
            (X (f i)) :
          MvPolynomial σ R)
        ((RingHom.id (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X (f i)) : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((RingHom.comp (AlgHom.toRingHom (rename f))
            (AlgHom.toRingHom (aeval fun (i : σ) ↦ Option.elim' 0 X (partialInv f i))) :
          (a : MvPolynomial σ R) → MvPolynomial σ R)
        (X i) :
      MvPolynomial σ R)
    ((RingHom.id (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)

Tactic:
rcases hf hip with ⟨i, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : (↑p.vars : Set σ) ⊆ range f
i : τ
hip h : f i ∈ p.vars
⊢ Eq (α := MvPolynomial σ R)
    ((RingHom.comp (AlgHom.toRingHom (rename f))
            (AlgHom.toRingHom (aeval fun (i : σ) ↦ Option.elim' 0 X (partialInv f i))) :
          (a : MvPolynomial σ R) → MvPolynomial σ R)
        (X (f i)) :
      MvPolynomial σ R)
    ((RingHom.id (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X (f i)) : MvPolynomial σ R)

Tactic:
simp [partialInv_left hfi]

Premises used: Function.partialInv_left
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : (↑p.vars : Set σ) ⊆ range f
⊢ p = p

Tactic:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
i : τ
hi :
  Membership.mem (γ := Finset τ) (vars.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) i
simp :
  ∀
    (hi :
      Membership.mem (γ := Multiset τ)
        (degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) i),
    ∃ a ∈ φ.degrees, f a = i
⊢ i ∈ Finset.image f φ.vars

Tactic:
simp only [vars_def, Multiset.mem_toFinset, Finset.mem_image] at hi ⊢

Premises used: Finset.mem_image, MvPolynomial.vars_def, Multiset.mem_toFinset
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
i : τ
hi :
  Membership.mem (γ := Multiset τ)
    (degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) i
⊢ ∃ a ∈ φ.degrees, f a = i

Tactic:
simpa only [Multiset.mem_map] using degrees_rename _ _ hi

Premises used: Multiset.mem_map, MvPolynomial.degrees_rename
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
intro intro₁ :
  ∀ ⦃i : τ⦄
    (hi :
      Membership.mem (γ := Finset τ) (vars.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ))
        i),
    i ∈ Finset.image f φ.vars
intro₂ :
  ∀ ⦃i : τ⦄
    (hi :
      Membership.mem (γ := Multiset τ)
        (degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) i),
    ∃ a ∈ φ.degrees, f a = i
⊢ vars.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) ⊆ Finset.image f φ.vars

Tactic:
classical
  intro i hi
  simp only [vars_def, Multiset.mem_toFinset, Finset.mem_image] at hi ⊢
  simpa only [Multiset.mem_map] using degrees_rename _ _ hi

Premises used: Finset.mem_image, Multiset.mem_map, MvPolynomial.vars_def, Multiset.mem_toFinset
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
j : τ
h : Membership.mem (γ := Finset τ) (vars.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) j
⊢ ∃ i ∈ φ.vars, f i = j

Tactic:
simpa only [exists_prop, Finset.mem_image] using vars_rename f φ h

Premises used: Finset.mem_image, exists_prop, MvPolynomial.vars_rename
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
j : τ
h : Membership.mem (γ := Finset τ) (vars.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) j
⊢ ∃ i ∈ φ.vars, f i = j

Tactic:
classical
  simpa only [exists_prop, Finset.mem_image] using vars_rename f φ h

Premises used: Finset.mem_image, exists_prop
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : (↑q.vars : Set σ) ⊆ s
inst_1 : (i : σ) → Decidable (i ∈ s)
rw :
  Eq (α := MvPolynomial σ R)
    (∑ i ∈ q.support,
      (aeval fun (i : σ) ↦ if i ∈ s then X i else 0 : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((monomial i : (a : R) → MvPolynomial σ R) (coeff i q)))
    (∑ v ∈ q.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v q))
⊢ (aeval fun (i : σ) ↦ if i ∈ s then X i else 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) q = q

Tactic:
rw [MvPolynomial.as_sum q, MvPolynomial.aeval_sum]

Premises used: MvPolynomial.aeval_sum, MvPolynomial.as_sum
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : (↑q.vars : Set σ) ⊆ s
inst_1 : (i : σ) → Decidable (i ∈ s)
⊢ Eq (α := MvPolynomial σ R)
    (∑ i ∈ q.support,
      (aeval fun (i : σ) ↦ if i ∈ s then X i else 0 : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((monomial i : (a : R) → MvPolynomial σ R) (coeff i q)))
    (∑ v ∈ q.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v q))

Tactic:
Finset.sum_congr rfl fun u hu ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : (↑q.vars : Set σ) ⊆ s
inst_1 : (i : σ) → Decidable (i ∈ s)
refine :
  ∀ (u : σ →₀ ℕ) (hu : u ∈ q.support),
    Eq (α := MvPolynomial σ R)
      ((aeval fun (i : σ) ↦ if i ∈ s then X i else 0 : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((monomial u : (a : R) → MvPolynomial σ R) (coeff u q)) :
        MvPolynomial σ R)
      ((monomial u : (a : R) → MvPolynomial σ R) (coeff u q) : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    (∑ i ∈ q.support,
      (aeval fun (i : σ) ↦ if i ∈ s then X i else 0 : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((monomial i : (a : R) → MvPolynomial σ R) (coeff i q)))
    (∑ v ∈ q.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v q))

Tactic:
refine Finset.sum_congr rfl fun u hu ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : (↑q.vars : Set σ) ⊆ s
inst_1 : (i : σ) → Decidable (i ∈ s)
u : σ →₀ ℕ
hu : u ∈ q.support
rw :
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) (coeff u q) : MvPolynomial σ R)
      (u.prod fun (i : σ) (k : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (if i ∈ s then X i else 0) k : MvPolynomial σ R) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (coeff u q) : MvPolynomial σ R)
      (u.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (X n) e : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((aeval fun (i : σ) ↦ if i ∈ s then X i else 0 : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((monomial u : (a : R) → MvPolynomial σ R) (coeff u q)) :
      MvPolynomial σ R)
    ((monomial u : (a : R) → MvPolynomial σ R) (coeff u q) : MvPolynomial σ R)

Tactic:
rw [MvPolynomial.aeval_monomial, MvPolynomial.monomial_eq]

Premises used: MvPolynomial.monomial_eq, MvPolynomial.aeval_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : (↑q.vars : Set σ) ⊆ s
inst_1 : (i : σ) → Decidable (i ∈ s)
u : σ →₀ ℕ
hu : u ∈ q.support
e_a :
  Eq (α := MvPolynomial σ R)
    (u.prod fun (i : σ) (k : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (if i ∈ s then X i else 0) k)
    (u.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (X n) e)
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) (coeff u q) : MvPolynomial σ R)
      (u.prod fun (i : σ) (k : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (if i ∈ s then X i else 0) k : MvPolynomial σ R) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (coeff u q) : MvPolynomial σ R)
      (u.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (X n) e : MvPolynomial σ R)

Tactic:
congr 1
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : (↑q.vars : Set σ) ⊆ s
inst_1 : (i : σ) → Decidable (i ∈ s)
u : σ →₀ ℕ
hu : u ∈ q.support
i : σ
hi : i ∈ u.support
⊢ HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (if i ∈ s then X i else 0) ((u : (a : σ) → ℕ) i : ℕ) =
    HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) ((u : (a : σ) → ℕ) i : ℕ)

Tactic:
simp [hs ((mem_vars_iff_mem_support _).mpr ⟨u, hu, hi⟩)]

Premises used: Iff.mpr, And.intro, Exists.intro, MvPolynomial.mem_vars_iff_mem_support
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : (↑q.vars : Set σ) ⊆ s
inst_1 : (i : σ) → Decidable (i ∈ s)
u : σ →₀ ℕ
hu : u ∈ q.support
⊢ Eq (α := MvPolynomial σ R)
    (u.prod fun (i : σ) (k : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (if i ∈ s then X i else 0) k)
    (u.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (X n) e)

Tactic:
exact Finsupp.prod_congr (fun i hi ↦ by simp [hs ((mem_vars_iff_mem_support _).mpr ⟨u, hu, hi⟩)])

Premises used: Finsupp.prod_congr
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : LinearOrder σ
rw :
  (p : (a : σ →₀ ℕ) → R)
      (invFun (β := Lex (σ →₀ ℕ)) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
        (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) =
    coeff ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) p
⊢ leadingCoeff (B := Lex (σ →₀ ℕ)) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p =
    coeff ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) p

Tactic:
rw [leadingCoeff]

Premises used: AddMonoidAlgebra.leadingCoeff
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : LinearOrder σ
apply :
  Eq (α := σ →₀ ℕ)
    (invFun (β := Lex (σ →₀ ℕ)) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
        (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) :
      σ →₀ ℕ)
    ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ)
⊢ (p : (a : σ →₀ ℕ) → R)
      (invFun (β := Lex (σ →₀ ℕ)) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
        (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) =
    coeff ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) p

Tactic:
apply congr_arg p.coeff

Premises used: MvPolynomial.coeff, congr_arg
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : LinearOrder σ
a :
  Eq (α := Lex (σ →₀ ℕ))
    ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
        (invFun (β := Lex (σ →₀ ℕ)) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
          (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) :
      Lex (σ →₀ ℕ))
    ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
        ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) :
      Lex (σ →₀ ℕ))
⊢ Eq (α := σ →₀ ℕ)
    (invFun (β := Lex (σ →₀ ℕ)) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
        (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) :
      σ →₀ ℕ)
    ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ)

Tactic:
apply toLex.injective

Premises used: Equiv.injective, toLex
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : LinearOrder σ
a :
  Eq (α := Lex (σ →₀ ℕ)) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p : Lex (σ →₀ ℕ))
    ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
        ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) :
      Lex (σ →₀ ℕ))
a₁ a₂ :
  Eq (α := Lex (σ →₀ ℕ)) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)
    (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)
⊢ Eq (α := Lex (σ →₀ ℕ))
    ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
        (invFun (β := Lex (σ →₀ ℕ)) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
          (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) :
      Lex (σ →₀ ℕ))
    ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
        ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) :
      Lex (σ →₀ ℕ))

Tactic:
rw [Function.rightInverse_invFun toLex.surjective, toLex_ofLex]

Premises used: Function.rightInverse_invFun, toLex_ofLex, Equiv.surjective, toLex
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : LinearOrder σ
r : R
⊢ Eq.{u_1 + 1} (α := Lex (σ →₀ ℕ))
    (supDegree.{u, u_1, u_1} (R := R) (A := σ →₀ ℕ) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
      ((C : (a : R) → MvPolynomial σ R) r))
    0

Tactic:
(supDegree_single _ r).trans (ite_eq_iff'.mpr ⟨fun _ => rfl, fun _ => rfl⟩)

Premises used: Iff.mpr, AddMonoidAlgebra.supDegree_single, And.intro, ite_eq_iff', rfl, Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : LinearOrder σ
r : R
⊢ Eq.{u_1 + 1} (α := Lex (σ →₀ ℕ))
    (supDegree.{u, u_1, u_1} (R := R) (A := σ →₀ ℕ) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
      ((C : (a : R) → MvPolynomial σ R) r))
    0

Tactic:
exact (supDegree_single _ r).trans (ite_eq_iff'.mpr ⟨fun _ => rfl, fun _ => rfl⟩)

Premises used: Iff.mpr, AddMonoidAlgebra.supDegree_single, And.intro, ite_eq_iff', rfl, Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : LinearOrder σ
r : R
⊢ Eq.{u_1 + 1} (α := Lex (σ →₀ ℕ))
    (supDegree.{u, u_1, u_1} (R := R) (A := σ →₀ ℕ) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
      ((C : (a : R) → MvPolynomial σ R) r))
    0

Tactic:
classical
    exact (supDegree_single _ r).trans (ite_eq_iff'.mpr ⟨fun _ => rfl, fun _ => rfl⟩)

Premises used: Iff.mpr, AddMonoidAlgebra.supDegree_single, And.intro, ite_eq_iff', rfl, Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : LinearOrder σ
r : R
⊢ leadingCoeff.{u, u_1, u_1} (A := σ →₀ ℕ) (B := Lex (σ →₀ ℕ)) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
      ((C : (a : R) → MvPolynomial σ R) r) =
    r

Tactic:
leadingCoeff_single toLex.injective _ r

Premises used: AddMonoidAlgebra.leadingCoeff_single, Equiv.injective, Finsupp.single, toLex
-- Module: Mathlib.Algebra.NeZero
Goal:
R : Type u_1
inst : Zero R
n : R
⊢ ¬NeZero n ↔ n = 0

Tactic:
simp [neZero_iff]

Premises used: neZero_iff
-- Module: Mathlib.Algebra.NeZero
Goal:
R : Type u_1
inst : Zero R
a : R
⊢ a = 0 ∨ NeZero a

Tactic:
(eq_or_ne a 0).imp_right NeZero.mk

Premises used: NeZero.mk, eq_or_ne, OfNat.ofNat, Or.imp_right
-- Module: Mathlib.Algebra.NeZero
Goal:
α : Type u_2
inst : Zero α
inst_1 : One α
inst_2 : NeZero.{u_2} (R := α) 1
⊢ Ne.{u_2 + 1} (α := α) 0 1

Tactic:
NeZero.ne' (1 : α)

Premises used: NeZero.ne', OfNat.ofNat
-- Module: Mathlib.Algebra.NeZero
Goal:
α : Type u_2
inst : Zero α
inst_1 : One α
inst_2 : NeZero.{u_2} (R := α) 1
⊢ Ne.{u_2 + 1} (α := α) 1 0

Tactic:
NeZero.ne (1 : α)

Premises used: OfNat.ofNat, NeZero.ne
-- Module: Mathlib.Algebra.NeZero
Goal:
α : Type u_2
inst : Zero α
inst_1 : One α
inst_2 : NeZero.{u_2} (R := α) 1
a : α
h : a = 1
⊢ a ≠ 0

Tactic:
h ▸ one_ne_zero

Premises used: Eq.rec, one_ne_zero, Eq.symm
-- Module: Mathlib.Algebra.NeZero
Goal:
α : Type u_2
inst : Zero α
inst_1 : OfNat α 2
inst_2 : NeZero.{u_2} (R := α) 2
⊢ Ne.{u_2 + 1} (α := α) 2 0

Tactic:
NeZero.ne (2 : α)

Premises used: OfNat.ofNat, NeZero.ne
-- Module: Mathlib.Algebra.NeZero
Goal:
α : Type u_2
inst : Zero α
inst_1 : OfNat α 3
inst_2 : NeZero.{u_2} (R := α) 3
⊢ Ne.{u_2 + 1} (α := α) 3 0

Tactic:
NeZero.ne (3 : α)

Premises used: OfNat.ofNat, NeZero.ne
-- Module: Mathlib.Algebra.NeZero
Goal:
α : Type u_2
inst : Zero α
inst_1 : OfNat α 4
inst_2 : NeZero.{u_2} (R := α) 4
⊢ Ne.{u_2 + 1} (α := α) 4 0

Tactic:
NeZero.ne (4 : α)

Premises used: OfNat.ofNat, NeZero.ne
-- Module: Mathlib.Algebra.NeZero
Goal:
α : Type u_2
inst : Zero α
inst_1 : One α
inst_2 : NeZero.{u_2} (R := α) 1
⊢ Ne.{u_2 + 1} (α := α) 0 1

Tactic:
zero_ne_one

Premises used: zero_ne_one
-- Module: Mathlib.Algebra.NeZero
Goal:
α : Type u_2
inst : Zero α
inst_1 : One α
inst_2 : NeZero.{u_2} (R := α) 1
⊢ Ne.{u_2 + 1} (α := α) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.NeZero
Goal:
α : Type u_2
inst : Zero α
inst_1 : OfNat α 2
inst_2 : NeZero.{u_2} (R := α) 2
⊢ Ne.{u_2 + 1} (α := α) 2 0

Tactic:
two_ne_zero

Premises used: two_ne_zero
-- Module: Mathlib.Algebra.NeZero
Goal:
α : Type u_2
inst : Zero α
inst_1 : OfNat α 3
inst_2 : NeZero.{u_2} (R := α) 3
⊢ Ne.{u_2 + 1} (α := α) 3 0

Tactic:
three_ne_zero

Premises used: three_ne_zero
-- Module: Mathlib.Algebra.NeZero
Goal:
α : Type u_2
inst : Zero α
inst_1 : OfNat α 4
inst_2 : NeZero.{u_2} (R := α) 4
⊢ Ne.{u_2 + 1} (α := α) 4 0

Tactic:
four_ne_zero

Premises used: four_ne_zero
-- Module: Mathlib.Algebra.NeZero
Goal:
M : Type u_2
x : M
inst : Preorder M
inst_1 : Zero M
h : 0 < x
⊢ NeZero x

Tactic:
⟨ne_of_gt h⟩

Premises used: NeZero.mk, ne_of_gt
-- Module: Mathlib.Algebra.NoZeroSMulDivisors.Basic
Goal:
R : Type u_1
M : Type u_2
inst : GroupWithZero R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
⊢ NoZeroSMulDivisors R M

Tactic:
⟨fun {a _} h ↦ or_iff_not_imp_left.2 fun ha ↦ (smul_eq_zero_iff_eq <| Units.mk0 a ha).1 h⟩

Premises used: Iff.mpr, smul_eq_zero_iff_eq, NoZeroSMulDivisors.mk, Units.mk0, Classical.or_iff_not_imp_left, Iff.mp
-- Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs
Goal:
R : Type u_4
M : Type u_5
N : Type u_6
inst : Zero R
inst_1 : Zero M
inst_2 : Zero N
inst_3 : SMul R M
inst_4 : SMul R N
inst_5 : NoZeroSMulDivisors R N
f : M → N
hf : Injective f
h0 : f 0 = 0
hs : ∀ (c : R) (x : M), f (c • x) = c • f x
x : R
x_1 : M
h : x • x_1 = 0
rw : f (x • x_1) = 0
rw₁ : f 0 = 0
rw₂ rw₃ : Eq.{u_6 + 1} (α := N) 0 0
⊢ x • f x_1 = 0

Tactic:
rw [← hs, h, h0]
-- Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs
Goal:
R : Type u_1
M : Type u_2
G : Type u_3
inst : Zero R
inst_1 : Mul R
inst_2 : NoZeroDivisors R
⊢ NoZeroSMulDivisors R R

Tactic:
⟨fun {_ _} => eq_zero_or_eq_zero_of_mul_eq_zero⟩

Premises used: NoZeroSMulDivisors.mk, NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
-- Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs
Goal:
R : Type u_1
M : Type u_2
G : Type u_3
inst : Semiring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : NoZeroSMulDivisors R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : r • m₁ = r • m₂
⊢ r • (m₁ - m₂) = 0

Tactic:
rw [← sub_eq_zero, ← smul_sub] at hm

Premises used: sub_eq_zero, smul_sub
-- Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs
Goal:
R : Type u_1
M : Type u_2
G : Type u_3
inst : Semiring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : NoZeroSMulDivisors R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : r • (m₁ - m₂) = 0
⊢ m₁ = m₂

Tactic:
simpa [hr.ne_zero, sub_eq_zero] using eq_zero_or_eq_zero_of_smul_eq_zero hm

Premises used: sub_eq_zero, NoZeroSMulDivisors.eq_zero_or_eq_zero_of_smul_eq_zero, IsRegular.ne_zero
-- Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Zero R
inst_1 : Zero M
inst_2 : SMul R M
simp_rw : (∀ {c : R} {x : M}, c • x = 0 → ¬c = 0 → x = 0) ↔ ∀ (r : R), r ≠ 0 → ∀ (m : M), r • m = 0 → m = 0
⊢ NoZeroSMulDivisors R M ↔ ∀ (r : R), r ≠ 0 → ∀ (m : M), r • m = 0 → m = 0

Tactic:
simp_rw [noZeroSMulDivisors_iff, or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left, noZeroSMulDivisors_iff
-- Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Zero R
inst_1 : Zero M
inst_2 : SMul R M
⊢ (∀ {c : R} {x : M}, c • x = 0 → ¬c = 0 → x = 0) ↔ ∀ (r : R), r ≠ 0 → ∀ (m : M), r • m = 0 → m = 0

Tactic:
⟨fun h r hr m eq ↦ h eq hr, fun h r m eq hr ↦ h r hr m eq⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Zero R
inst_1 : Zero M
inst_2 : SMul R M
⊢ (∀ {c : R} {x : M}, c • x = 0 → ¬c = 0 → x = 0) ↔ ∀ (r : R), r ≠ 0 → ∀ (m : M), r • m = 0 → m = 0

Tactic:
exact ⟨fun h r hr m eq ↦ h eq hr, fun h r m eq hr ↦ h r hr m eq⟩
-- Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs
Goal:
R : Type u_1
M : Type u_2
G : Type u_3
inst : AddMonoid M
inst_1 : IsAddTorsionFree M
n : ℕ
x : M
hx : n • x = 0
contrapose! : ∀ (hx : n ≠ 0 ∧ x ≠ 0), n • x ≠ 0
⊢ n = 0 ∨ x = 0

Tactic:
contrapose! hx
-- Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs
Goal:
R : Type u_1
M : Type u_2
G : Type u_3
inst : AddMonoid M
inst_1 : IsAddTorsionFree M
n : ℕ
x : M
hx : n ≠ 0 ∧ x ≠ 0
⊢ n • x ≠ 0

Tactic:
simpa using (nsmul_right_injective hx.1).ne hx.2

Premises used: Function.Injective.ne, And.right, And.left, nsmul_right_injective
-- Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs
Goal:
R : Type u_1
M : Type u_2
G : Type u_3
inst : AddGroup G
inst_1 : IsAddTorsionFree G
n : ℤ
x : G
hx : n • x = 0
contrapose! : ∀ (hx : n ≠ 0 ∧ x ≠ 0), n • x ≠ 0
⊢ n = 0 ∨ x = 0

Tactic:
contrapose! hx