awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
B : Type u_2
F : Type u_3
inst_2 : Ring B
inst_3 : FunLike F A B
inst_4 : RingHomClass F A B
inst_5 : Module ℚ B
a : A
f : F
k : ℕ
hk : a ^ k = 0
⊢ HPow.hPow (α := B) ((f : (a : A) → B) a : B) k = 0

Tactic:
have hk' : (f a) ^ k = 0 := by simp [← map_pow, hk]
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
B : Type u_2
F : Type u_3
inst_2 : Ring B
inst_3 : FunLike F A B
inst_4 : RingHomClass F A B
inst_5 : Module ℚ B
a : A
f : F
k : ℕ
hk : a ^ k = 0
hk' : HPow.hPow (α := B) ((f : (a : A) → B) a : B) k = 0
⊢ Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (exp a) : B) (exp ((f : (a : A) → B) a) : B)

Tactic:
simp [exp_eq_sum hk, exp_eq_sum hk', map_rat_smul]

Premises used: IsNilpotent.exp_eq_sum, map_rat_smul
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
G : Type u_2
inst_2 : Monoid G
inst_3 : MulSemiringAction G A
g : G
a : A
ha : IsNilpotent a
⊢ exp (g • a) = g • exp a

Tactic:
(map_exp ha (MulSemiringAction.toRingHom G A g)).symm

Premises used: IsNilpotent.map_exp, MulSemiringAction.toRingHom, Eq.symm
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a : A
ha : IsNilpotent a
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a : A
ha : IsNilpotent a
h : Nontrivial A
rw :
  IsNilpotent
    (∑ k ∈ range (nilpotencyClass a - Nat.succ 0), HSMul.hSMul (α := ℚ) (↑(k + 1)! : ℚ)⁻¹ (a ^ (k + 1)) +
        HSMul.hSMul (α := ℚ) (↑0! : ℚ)⁻¹ (HPow.hPow (β := ℕ) a 0) -
      1)
⊢ IsNilpotent (exp a - 1)

Tactic:
rw [exp, ← Nat.sub_add_cancel (pos_nilpotencyClass_iff.2 ha), Finset.sum_range_succ']

Premises used: Iff.mpr, pos_nilpotencyClass_iff, IsNilpotent.exp, Nat.sub_add_cancel, Finset.sum_range_succ'
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a : A
ha : IsNilpotent a
h : Nontrivial A
simp :
  IsNilpotent.{u_1} (R := A) (∑ x ∈ range (nilpotencyClass a - 1), HSMul.hSMul (α := ℚ) (↑(x + 1)! : ℚ)⁻¹ (a ^ (x + 1)))
⊢ IsNilpotent
    (∑ k ∈ range (nilpotencyClass a - Nat.succ 0), HSMul.hSMul (α := ℚ) (↑(k + 1)! : ℚ)⁻¹ (a ^ (k + 1)) +
        HSMul.hSMul (α := ℚ) (↑0! : ℚ)⁻¹ (HPow.hPow (β := ℕ) a 0) -
      1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a : A
ha : IsNilpotent a
h : Nontrivial A
x : ℕ
h_1 : x ∈ range (nilpotencyClass a - 1)
⊢ x + 1 ≠ 0

Tactic:
positivity
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a : A
ha : IsNilpotent a
h : Nontrivial A
apply :
  ∀ (i j : ℕ),
    i ∈ range (nilpotencyClass a - 1) →
      j ∈ range (nilpotencyClass a - 1) →
        Commute (HSMul.hSMul (α := ℚ) (↑(i + 1)! : ℚ)⁻¹ (a ^ (i + 1)))
          (HSMul.hSMul (α := ℚ) (↑(j + 1)! : ℚ)⁻¹ (a ^ (j + 1)))
⊢ IsNilpotent.{u_1} (R := A) (∑ x ∈ range (nilpotencyClass a - 1), HSMul.hSMul (α := ℚ) (↑(x + 1)! : ℚ)⁻¹ (a ^ (x + 1)))

Tactic:
apply Commute.isNilpotent_sum fun _ _ ↦ smul (pow_of_pos ha <| by positivity) _

Premises used: Commute.isNilpotent_sum, IsNilpotent.smul, IsNilpotent.pow_of_pos
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a : A
ha : IsNilpotent a
h : Nontrivial A
⊢ ∀ (i j : ℕ),
    i ∈ range (nilpotencyClass a - 1) →
      j ∈ range (nilpotencyClass a - 1) →
        Commute (HSMul.hSMul (α := ℚ) (↑(i + 1)! : ℚ)⁻¹ (a ^ (i + 1)))
          (HSMul.hSMul (α := ℚ) (↑(j + 1)! : ℚ)⁻¹ (a ^ (j + 1)))

Tactic:
simp [Nat.factorial_ne_zero]

Premises used: Nat.factorial_ne_zero
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module ℚ M
inst_6 : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
hfM : IsNilpotent fM
hfN : IsNilpotent fN
h : fN ∘ₗ g = g ∘ₗ fM
h₁ : ∀ (m : M), Eq.{u_3 + 1} (α := N) ((exp fN ∘ₗ g : (a : M) → N) m : N) ((g ∘ₗ exp fM : (a : M) → N) m : N)
⊢ exp fN ∘ₗ g = g ∘ₗ exp fM

Tactic:
ext m
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module ℚ M
inst_6 : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
hfM : IsNilpotent fM
hfN : IsNilpotent fN
h : fN ∘ₗ g = g ∘ₗ fM
m : M
h₁ :
  ∀ (k : ℕ) (hfM : fM ^ k = 0),
    Eq.{u_3 + 1} (α := N) ((exp fN ∘ₗ g : (a : M) → N) m : N) ((g ∘ₗ exp fM : (a : M) → N) m : N)
⊢ Eq.{u_3 + 1} (α := N) ((exp fN ∘ₗ g : (a : M) → N) m : N) ((g ∘ₗ exp fM : (a : M) → N) m : N)

Tactic:
obtain ⟨k, hfM⟩ := hfM
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module ℚ M
inst_6 : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
hfN : IsNilpotent fN
h : fN ∘ₗ g = g ∘ₗ fM
m : M
k : ℕ
hfM : fM ^ k = 0
h₁ :
  ∀ (l : ℕ) (hfN : fN ^ l = 0),
    Eq.{u_3 + 1} (α := N) ((exp fN ∘ₗ g : (a : M) → N) m : N) ((g ∘ₗ exp fM : (a : M) → N) m : N)
⊢ Eq.{u_3 + 1} (α := N) ((exp fN ∘ₗ g : (a : M) → N) m : N) ((g ∘ₗ exp fM : (a : M) → N) m : N)

Tactic:
obtain ⟨l, hfN⟩ := hfN
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module ℚ M
inst_6 : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
h : fN ∘ₗ g = g ∘ₗ fM
m : M
k : ℕ
hfM : fM ^ k = 0
l : ℕ
hfN : fN ^ l = 0
kl : ℕ := max k l
⊢ k ≤ kl

Tactic:
omega
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module ℚ M
inst_6 : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
h : fN ∘ₗ g = g ∘ₗ fM
m : M
k : ℕ
hfM : fM ^ k = 0
l : ℕ
hfN : fN ^ l = 0
kl : ℕ := max k l
⊢ fM ^ kl = 0

Tactic:
replace hfM : fM ^ kl = 0 := pow_eq_zero_of_le (by omega) hfM
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module ℚ M
inst_6 : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
h : fN ∘ₗ g = g ∘ₗ fM
m : M
k l : ℕ
hfN : fN ^ l = 0
kl : ℕ := max k l
hfM : fM ^ kl = 0
⊢ l ≤ kl

Tactic:
omega
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module ℚ M
inst_6 : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
h : fN ∘ₗ g = g ∘ₗ fM
m : M
k l : ℕ
hfN : fN ^ l = 0
kl : ℕ := max k l
hfM : fM ^ kl = 0
⊢ fN ^ kl = 0

Tactic:
replace hfN : fN ^ kl = 0 := pow_eq_zero_of_le (by omega) hfN
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module ℚ M
inst_6 : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
h : fN ∘ₗ g = g ∘ₗ fM
m : M
k l : ℕ
kl : ℕ := max k l
hfM : fM ^ kl = 0
hfN : fN ^ kl = 0
i : ℕ
⊢ Eq (α := N) ((fN ^ i : (a : N) → N) ((g : (a : M) → N) m : N) : N)
    ((g : (a : M) → N) ((fM ^ i : (a : M) → M) m : M) : N)

Tactic:
simpa using LinearMap.congr_fun (Module.End.commute_pow_left_of_commute h i) m

Premises used: LinearMap.congr_fun, Module.End.commute_pow_left_of_commute
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module ℚ M
inst_6 : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
h : fN ∘ₗ g = g ∘ₗ fM
m : M
k l : ℕ
kl : ℕ := max k l
hfM : fM ^ kl = 0
hfN : fN ^ kl = 0
⊢ ∀ (i : ℕ),
    Eq (α := N) ((fN ^ i : (a : N) → N) ((g : (a : M) → N) m : N) : N)
      ((g : (a : M) → N) ((fM ^ i : (a : M) → M) m : M) : N)

Tactic:
have (i : ℕ) : (fN ^ i) (g m) = g ((fM ^ i) m) := by
    simpa using LinearMap.congr_fun (Module.End.commute_pow_left_of_commute h i) m
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module ℚ M
inst_6 : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
h : fN ∘ₗ g = g ∘ₗ fM
m : M
k l : ℕ
kl : ℕ := max k l
hfM : fM ^ kl = 0
hfN : fN ^ kl = 0
this :
  ∀ (i : ℕ),
    Eq (α := N) ((fN ^ i : (a : N) → N) ((g : (a : M) → N) m : N) : N)
      ((g : (a : M) → N) ((fM ^ i : (a : M) → M) m : M) : N)
⊢ Eq.{u_3 + 1} (α := N) ((exp fN ∘ₗ g : (a : M) → N) m : N) ((g ∘ₗ exp fM : (a : M) → N) m : N)

Tactic:
simp [exp_eq_sum hfM, exp_eq_sum hfN, this, map_rat_smul]

Premises used: IsNilpotent.exp_eq_sum, map_rat_smul
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
⊢ IsNilpotent DL

Tactic:
have h_nilL : IsNilpotent DL := h_nil.map <| lTensorAlgHom R B B
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
⊢ IsNilpotent DR

Tactic:
have h_nilR : IsNilpotent DR := h_nil.map <| rTensorAlgHom R B B
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
a :
  ∀ (x x_1 : B),
    Eq (α := B ⊗[R] B)
      (((((AlgebraTensorModule.curry (DL * DR) : B →ₗ[R] B →ₗ[R] B ⊗[R] B) : (a : B) → B →ₗ[R] B ⊗[R] B) x :
              B →ₗ[R] B ⊗[R] B) :
            (a : B) → B ⊗[R] B)
          x_1 :
        B ⊗[R] B)
      (((((AlgebraTensorModule.curry (DR * DL) : B →ₗ[R] B →ₗ[R] B ⊗[R] B) : (a : B) → B →ₗ[R] B ⊗[R] B) x :
              B →ₗ[R] B ⊗[R] B) :
            (a : B) → B ⊗[R] B)
          x_1 :
        B ⊗[R] B)
⊢ Commute DL DR

Tactic:
ext
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
x_1 x_2 : B
⊢ Eq (α := B ⊗[R] B)
    (((((AlgebraTensorModule.curry (DL * DR) : B →ₗ[R] B →ₗ[R] B ⊗[R] B) : (a : B) → B →ₗ[R] B ⊗[R] B) x_1 :
            B →ₗ[R] B ⊗[R] B) :
          (a : B) → B ⊗[R] B)
        x_2 :
      B ⊗[R] B)
    (((((AlgebraTensorModule.curry (DR * DL) : B →ₗ[R] B →ₗ[R] B ⊗[R] B) : (a : B) → B →ₗ[R] B ⊗[R] B) x_1 :
            B →ₗ[R] B ⊗[R] B) :
          (a : B) → B ⊗[R] B)
        x_2 :
      B ⊗[R] B)

Tactic:
simp [DL, DR]
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
⊢ Commute DL DR

Tactic:
have h_comm : Commute DL DR := by ext; simp [DL, DR]
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
⊢ let m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B;
  m = LinearMap.mul' R B

Tactic:
set m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B with hm

Premises used: LinearMap.mul'
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
this : exp D ∘ₗ m = m ∘ₗ exp (DL + DR)
⊢ Eq (α := B) ((exp D : (a : B) → B) (x * y) : B)
    ((m : (a : B ⊗[R] B) → B) ((exp (DL + DR) : (a : B ⊗[R] B) → B ⊗[R] B) (x ⊗ₜ[R] y) : B ⊗[R] B) : B)

Tactic:
simpa using LinearMap.congr_fun this (x ⊗ₜ[R] y)

Premises used: LinearMap.congr_fun, TensorProduct.tmul
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
suffices : exp D ∘ₗ m = m ∘ₗ exp (DL + DR)
⊢ Eq (α := B) ((exp D : (a : B) → B) (x * y) : B)
    ((m : (a : B ⊗[R] B) → B) ((exp (DL + DR) : (a : B ⊗[R] B) → B ⊗[R] B) (x ⊗ₜ[R] y) : B ⊗[R] B) : B)

Tactic:
suffices exp D ∘ₗ m = m ∘ₗ exp (DL + DR) by simpa using LinearMap.congr_fun this (x ⊗ₜ[R] y)
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
apply : D ∘ₗ m = m ∘ₗ (DL + DR)
⊢ exp D ∘ₗ m = m ∘ₗ exp (DL + DR)

Tactic:
apply commute_exp_left_of_commute (h_comm.isNilpotent_add h_nilL h_nilR) h_nil

Premises used: Module.End.commute_exp_left_of_commute, Commute.isNilpotent_add
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
a :
  ∀ (x x_1 : B),
    Eq (α := B)
      (((((AlgebraTensorModule.curry (D ∘ₗ m) : B →ₗ[R] B →ₗ[R] B) : (a : B) → B →ₗ[R] B) x : B →ₗ[R] B) : (a : B) → B)
          x_1 :
        B)
      (((((AlgebraTensorModule.curry (m ∘ₗ (DL + DR)) : B →ₗ[R] B →ₗ[R] B) : (a : B) → B →ₗ[R] B) x : B →ₗ[R] B) :
            (a : B) → B)
          x_1 :
        B)
⊢ D ∘ₗ m = m ∘ₗ (DL + DR)

Tactic:
ext
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
x_1 x_2 : B
⊢ Eq (α := B)
    (((((AlgebraTensorModule.curry (D ∘ₗ m) : B →ₗ[R] B →ₗ[R] B) : (a : B) → B →ₗ[R] B) x_1 : B →ₗ[R] B) : (a : B) → B)
        x_2 :
      B)
    (((((AlgebraTensorModule.curry (m ∘ₗ (DL + DR)) : B →ₗ[R] B →ₗ[R] B) : (a : B) → B →ₗ[R] B) x_1 : B →ₗ[R] B) :
          (a : B) → B)
        x_2 :
      B)

Tactic:
simp [DL, DR, hm, h_der]
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
⊢ Eq (α := B) ((exp D : (a : B) → B) (x * y) : B)
    ((m : (a : B ⊗[R] B) → B) ((exp (DL + DR) : (a : B ⊗[R] B) → B ⊗[R] B) (x ⊗ₜ[R] y) : B ⊗[R] B) : B)

Tactic:
have h₁ : exp D (x * y) = m (exp (DL + DR) (x ⊗ₜ[R] y)) := by
    suffices exp D ∘ₗ m = m ∘ₗ exp (DL + DR) by simpa using LinearMap.congr_fun this (x ⊗ₜ[R] y)
    apply commute_exp_left_of_commute (h_comm.isNilpotent_add h_nilL h_nilR) h_nil
    ext
    simp [DL, DR, hm, h_der]
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
h₁ :
  Eq (α := B) ((exp D : (a : B) → B) (x * y) : B)
    ((m : (a : B ⊗[R] B) → B) ((exp (DL + DR) : (a : B ⊗[R] B) → B ⊗[R] B) (x ⊗ₜ[R] y) : B ⊗[R] B) : B)
⊢ exp DL = LinearMap.lTensor B (exp D)

Tactic:
have h₂ : exp DL = (exp D).lTensor B := (h_nil.map_exp (lTensorAlgHom R B B)).symm
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
h₁ :
  Eq (α := B) ((exp D : (a : B) → B) (x * y) : B)
    ((m : (a : B ⊗[R] B) → B) ((exp (DL + DR) : (a : B ⊗[R] B) → B ⊗[R] B) (x ⊗ₜ[R] y) : B ⊗[R] B) : B)
h₂ : exp DL = LinearMap.lTensor B (exp D)
⊢ exp DR = LinearMap.rTensor B (exp D)

Tactic:
have h₃ : exp DR = (exp D).rTensor B := (h_nil.map_exp (rTensorAlgHom R B B)).symm
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
h₁ :
  Eq (α := B) ((exp D : (a : B) → B) (x * y) : B)
    ((m : (a : B ⊗[R] B) → B) ((exp (DL + DR) : (a : B ⊗[R] B) → B ⊗[R] B) (x ⊗ₜ[R] y) : B ⊗[R] B) : B)
h₂ : exp DL = LinearMap.lTensor B (exp D)
h₃ : exp DR = LinearMap.rTensor B (exp D)
⊢ (exp D : (a : B) → B) (x * y) =
    HMul.hMul (α := B) (β := B) ((exp D : (a : B) → B) x : B) ((exp D : (a : B) → B) y : B)

Tactic:
simp [h₁, exp_add_of_commute h_comm h_nilL h_nilR, h₂, h₃, hm]

Premises used: IsNilpotent.exp_add_of_commute
-- Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced
Goal:
k : Type u_3
A : Type u_4
inst : Field k
inst_1 : Ring A
inst_2 : Algebra k A
e : (p : Ideal k) → [inst_3 : p.IsPrime] → AlgebraicClosure k ≃ₐ[k] AlgebraicClosure p.ResidueField :=
  fun (p : Ideal k) [p.IsPrime] ↦
    have this : Algebra.IsAlgebraic k p.ResidueField := ⋯;
    IsAlgClosure.equiv k (AlgebraicClosure k) (AlgebraicClosure p.ResidueField)
⊢ IsGeometricallyReduced k A ↔ IsReduced (AlgebraicClosure k ⊗[k] A)

Tactic:
⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨fun p hp ↦ ?_⟩⟩

Premises used: _private.0.Algebra.isGeometricallyReduced_field_iff.match_1, Iff.intro, Algebra.IsGeometricallyReduced.mk, TensorProduct, AlgebraicClosure, IsReduced