awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv :
  ∀ i ∈ p₁.vars,
    i ∈ p₂.vars →
      Eq.{v + 1} (α := S) ((f₁ : (a : MvPolynomial σ R) → S) (X i) : S) ((f₂ : (a : MvPolynomial σ R) → S) (X i) : S)
hp : p₁ = p₂
⊢ eval₂Hom (f₂.comp C) (comp (β := MvPolynomial σ R) (⇑f₂ : (a : MvPolynomial σ R) → S) X) = f₂
have hC₁ : ∀ (x : R),
  Eq.{v + 1} (α := S)
    ((RingHom.comp (β := MvPolynomial σ R)
            (eval₂Hom (f₂.comp C) (comp (β := MvPolynomial σ R) (⇑f₂ : (a : MvPolynomial σ R) → S) X)) C :
          (a : R) → S)
        x :
      S)
    ((f₂.comp C : (a : R) → S) x : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv :
  ∀ i ∈ p₁.vars,
    i ∈ p₂.vars →
      Eq.{v + 1} (α := S) ((f₁ : (a : MvPolynomial σ R) → S) (X i) : S) ((f₂ : (a : MvPolynomial σ R) → S) (X i) : S)
hp : p₁ = p₂
hC₁ :
  ∀ (x : R),
    Eq.{v + 1} (α := S)
      ((RingHom.comp (β := MvPolynomial σ R)
              (eval₂Hom (f₂.comp C) (comp (β := MvPolynomial σ R) (⇑f₂ : (a : MvPolynomial σ R) → S) X)) C :
            (a : R) → S)
          x :
        S)
      ((f₂.comp C : (a : R) → S) x : S)
⊢ eval₂Hom (f₂.comp C) (comp (β := MvPolynomial σ R) (⇑f₂ : (a : MvPolynomial σ R) → S) X) = f₂
have hX : ∀ (i : σ),
  Eq.{v + 1} (α := S)
    ((eval₂Hom (f₂.comp C) (comp (β := MvPolynomial σ R) (⇑f₂ : (a : MvPolynomial σ R) → S) X) :
          (a : MvPolynomial σ R) → S)
        (X i) :
      S)
    ((f₂ : (a : MvPolynomial σ R) → S) (X i) : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ (rename f : (a : MvPolynomial τ R) → MvPolynomial σ R)
      ((aeval fun (i : σ) ↦ Option.elim' 0 X (partialInv f i) : (a : MvPolynomial σ R) → MvPolynomial τ R) p) =
    p
have change : 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)
      p :
    MvPolynomial σ R)
  ((RingHom.id (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
Tactic: change (rename f).toRingHom.comp _ p = RingHom.id _ p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ 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)
        p :
      MvPolynomial σ R)
    ((RingHom.id (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
have refine_1 : Eq (α := R →+* 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)
  (RingHom.comp (RingHom.id (MvPolynomial σ R)) C)
Tactic: refine hom_congr_vars ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
refine_1 :
  Eq (α := R →+* 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)
    (RingHom.comp (RingHom.id (MvPolynomial σ R)) C)
⊢ 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)
        p :
      MvPolynomial σ R)
    ((RingHom.id (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
have refine_2 : ∀ i ∈ p.vars,
  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: refine hom_congr_vars ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
refine_1 :
  Eq (α := R →+* 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)
    (RingHom.comp (RingHom.id (MvPolynomial σ R)) C)
refine_2 :
  ∀ i ∈ p.vars,
    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)
⊢ 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)
        p :
      MvPolynomial σ R)
    ((RingHom.id (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
have refine_3 : p = p
Tactic: refine hom_congr_vars ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ Eq (α := R →+* 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)
    (RingHom.comp (RingHom.id (MvPolynomial σ R)) C)
have refine_1 : ∀ (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: ext1
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ 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)
have 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)
Tactic: rcases hf hip with ⟨i, rfl⟩
Cleared hypotheses: i, hip, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ i ∈ Finset.image f φ.vars
have simp : ∀
  (hi :
    Membership.mem (γ := Multiset τ)
      (degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) i),
  ∃ a ∈ φ.degrees, f a = i
Tactic: simp only [vars_def, Multiset.mem_toFinset, Finset.mem_image] at hi ⊢
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
⊢ vars.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) ⊆ Finset.image f φ.vars
have intro : ∀ ⦃i : τ⦄,
  Membership.mem (γ := Finset τ) (vars.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) i →
    i ∈ 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
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ vars.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) ⊆ Finset.image f φ.vars
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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)
⊢ (aeval fun (i : σ) ↦ if i ∈ s then X i else 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) q = q
have 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))
Tactic: rw [MvPolynomial.as_sum q, MvPolynomial.aeval_sum]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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))
have 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)
Tactic: refine Finset.sum_congr rfl fun u hu ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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)
    ((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)
have 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)
Tactic: rw [MvPolynomial.aeval_monomial, MvPolynomial.monomial_eq]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ 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)
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : LinearOrder σ
⊢ leadingCoeff (B := Lex (σ →₀ ℕ)) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p =
    coeff ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) p
have rw : (p : (a : σ →₀ ℕ) → R)
    (invFun (β := Lex (σ →₀ ℕ)) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
      (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) =
  coeff ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) p
Tactic: rw [leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : LinearOrder σ
⊢ (p : (a : σ →₀ ℕ) → R)
      (invFun (β := Lex (σ →₀ ℕ)) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
        (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) =
    coeff ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) p
have apply : Eq (α := σ →₀ ℕ)
  (invFun (β := Lex (σ →₀ ℕ)) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
      (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) :
    σ →₀ ℕ)
  ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ)
Tactic: apply congr_arg p.coeff
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : LinearOrder σ
⊢ Eq (α := σ →₀ ℕ)
    (invFun (β := Lex (σ →₀ ℕ)) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
        (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) :
      σ →₀ ℕ)
    ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ)
have 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 (σ →₀ ℕ))
Tactic: apply toLex.injective
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : LinearOrder σ
⊢ 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 (σ →₀ ℕ))
have a : Eq (α := 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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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 (σ →₀ ℕ))
⊢ 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 (σ →₀ ℕ))
have a₁ : Eq (α := Lex (σ →₀ ℕ)) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)
  (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)
Tactic: rw [Function.rightInverse_invFun toLex.surjective, toLex_ofLex]
-- Lean 4 proof step from Mathlib.Algebra.NoZeroSMulDivisors.Defs (goal)
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
⊢ x • f x_1 = 0
have rw : f (x • x_1) = 0
Tactic: rw [← hs, h, h0]
-- Lean 4 proof step from Mathlib.Algebra.NoZeroSMulDivisors.Defs (goal)
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
⊢ x • f x_1 = 0
have rw₂ : Eq.{u_6 + 1} (α := N) 0 0
Tactic: rw [← hs, h, h0]
-- Lean 4 proof step from Mathlib.Algebra.NoZeroSMulDivisors.Defs (hypothesis)
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₂
⊢ m₁ = m₂
have hm₁ : r • (m₁ - m₂) = 0
Tactic: rw [← sub_eq_zero, ← smul_sub] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.NoZeroSMulDivisors.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Zero R
inst_1 : Zero M
inst_2 : SMul R M
⊢ NoZeroSMulDivisors R M ↔ ∀ (r : R), r ≠ 0 → ∀ (m : M), r • m = 0 → m = 0
have simp_rw : (∀ {c : R} {x : M}, c • x = 0 → ¬c = 0 → x = 0) ↔ ∀ (r : R), r ≠ 0 → ∀ (m : M), r • m = 0 → m = 0
Tactic: simp_rw [noZeroSMulDivisors_iff, or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.Algebra.NoZeroSMulDivisors.Defs (goal)
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
⊢ n = 0 ∨ x = 0
have contrapose! : ∀ (hx : n ≠ 0 ∧ x ≠ 0), n • x ≠ 0
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.NoZeroSMulDivisors.Defs (goal)
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
⊢ n = 0 ∨ x = 0
have contrapose! : ∀ (hx : n ≠ 0 ∧ x ≠ 0), n • x ≠ 0
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.NonAssoc.LieAdmissible.Defs (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieAdmissibleRing L
x y z : L
⊢ ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆
have simp : x * z + y * z - (z * x + z * y) = x * z - z * x + (y * z - z * y)
Tactic: simp only [Ring.lie_def, mul_add, add_mul]
-- Lean 4 proof step from Mathlib.Algebra.NonAssoc.LieAdmissible.Defs (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieAdmissibleRing L
x y z : L
⊢ ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆
have simp : x * y + x * z - (y * x + z * x) = x * y - y * x + (x * z - z * x)
Tactic: simp only [Ring.lie_def, mul_add, add_mul]
-- Lean 4 proof step from Mathlib.Algebra.NonAssoc.LieAdmissible.Defs (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieAdmissibleRing L
x y z : L
⊢ ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆
have this : associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y
Tactic: have := LieAdmissibleRing.assoc_def x y z
-- Lean 4 proof step from Mathlib.Algebra.NonAssoc.LieAdmissible.Defs (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LeftPreLieRing L
x y z : L
⊢ associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y
have assoc_xyz : associator x y z = associator y x z
Tactic: have assoc_xyz := LeftPreLieRing.assoc_symm' x y z
-- Lean 4 proof step from Mathlib.Algebra.NonAssoc.LieAdmissible.Defs (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LeftPreLieRing L
x y z : L
assoc_xyz : associator x y z = associator y x z
⊢ associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y
have assoc_zxy : associator z x y = associator x z y
Tactic: have assoc_zxy := LeftPreLieRing.assoc_symm' z x y
-- Lean 4 proof step from Mathlib.Algebra.NonAssoc.LieAdmissible.Defs (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LeftPreLieRing L
x y z : L
assoc_xyz : associator x y z = associator y x z
assoc_zxy : associator z x y = associator x z y
⊢ associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y
have assoc_yzx : associator y z x = associator z y x
Tactic: have assoc_yzx := LeftPreLieRing.assoc_symm' y z x
-- Lean 4 proof step from Mathlib.Algebra.NonAssoc.LieAdmissible.Defs (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : RightPreLieRing L
x y z : L
⊢ associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y
have assoc_xyz : associator x y z = associator x z y
Tactic: have assoc_xyz := RightPreLieRing.assoc_symm' x y z
-- Lean 4 proof step from Mathlib.Algebra.NonAssoc.LieAdmissible.Defs (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : RightPreLieRing L
x y z : L
assoc_xyz : associator x y z = associator x z y
⊢ associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y
have assoc_zxy : associator z x y = associator z y x
Tactic: have assoc_zxy := RightPreLieRing.assoc_symm' z x y
-- Lean 4 proof step from Mathlib.Algebra.NonAssoc.LieAdmissible.Defs (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : RightPreLieRing L
x y z : L
assoc_xyz : associator x y z = associator x z y
assoc_zxy : associator z x y = associator z y x
⊢ associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y
have assoc_yzx : associator y z x = associator y x z
Tactic: have assoc_yzx := RightPreLieRing.assoc_symm' y z x