awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h_1 : Nontrivial.{u_2} (A ⧸ R')
x y s : A
hs : Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] s) (x ⊗ₜ[R] y)
this : Eq.{u_2 + 1} (α := A ⧸ R') ((R'.mkQ : (a : A) → A ⧸ R') 1) 0
tmul :
  Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    (((map.{u_1, u_1, u_2, u_2, u_2, u_2} (R := R) (R₂ := R) (σ₁₂ := RingHom.id R) (M := A) (N := A) (M₂ := A ⧸ R')
              (N₂ := A ⧸ R') R'.mkQ R'.mkQ :
            A ⊗[R] A →ₗ[R] (A ⧸ R') ⊗[R] (A ⧸ R')) :
          (a : A ⊗[R] A) → (A ⧸ R') ⊗[R] (A ⧸ R'))
        (x ⊗ₜ[R] y) :
      (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
⊢ Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    ((R'.mkQ : (a : A) → A ⧸ R') x ⊗ₜ[R] (R'.mkQ : (a : A) → A ⧸ R') y : (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
have tmul₁ : Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
  (((map.{u_1, u_1, u_2, u_2, u_2, u_2} (R := R) (R₂ := R) (σ₁₂ := RingHom.id R) (M := A) (N := A) (M₂ := A ⧸ R') (N₂ :=
            A ⧸ R') R'.mkQ R'.mkQ :
          A ⊗[R] A →ₗ[R] (A ⧸ R') ⊗[R] (A ⧸ R')) :
        (a : A ⊗[R] A) → (A ⧸ R') ⊗[R] (A ⧸ R'))
      (1 ⊗ₜ[R] s) :
    (A ⧸ R') ⊗[R] (A ⧸ R'))
  (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
Tactic: rw [← map_tmul R'.mkQ R'.mkQ, ← hs, map_tmul, this, zero_tmul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h_1 : Nontrivial.{u_2} (A ⧸ R')
x y s : A
hs : Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] s) (x ⊗ₜ[R] y)
this : Eq.{u_2 + 1} (α := A ⧸ R') ((R'.mkQ : (a : A) → A ⧸ R') 1) 0
tmul :
  Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    (((map.{u_1, u_1, u_2, u_2, u_2, u_2} (R := R) (R₂ := R) (σ₁₂ := RingHom.id R) (M := A) (N := A) (M₂ := A ⧸ R')
              (N₂ := A ⧸ R') R'.mkQ R'.mkQ :
            A ⊗[R] A →ₗ[R] (A ⧸ R') ⊗[R] (A ⧸ R')) :
          (a : A ⊗[R] A) → (A ⧸ R') ⊗[R] (A ⧸ R'))
        (x ⊗ₜ[R] y) :
      (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
tmul₁ :
  Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    (((map.{u_1, u_1, u_2, u_2, u_2, u_2} (R := R) (R₂ := R) (σ₁₂ := RingHom.id R) (M := A) (N := A) (M₂ := A ⧸ R')
              (N₂ := A ⧸ R') R'.mkQ R'.mkQ :
            A ⊗[R] A →ₗ[R] (A ⧸ R') ⊗[R] (A ⧸ R')) :
          (a : A ⊗[R] A) → (A ⧸ R') ⊗[R] (A ⧸ R'))
        (1 ⊗ₜ[R] s) :
      (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
⊢ Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    ((R'.mkQ : (a : A) → A ⧸ R') x ⊗ₜ[R] (R'.mkQ : (a : A) → A ⧸ R') y : (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
have tmul₂ : Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
  ((R'.mkQ : (a : A) → A ⧸ R') 1 ⊗ₜ[R] (R'.mkQ : (a : A) → A ⧸ R') s : (A ⧸ R') ⊗[R] (A ⧸ R'))
  (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
Tactic: rw [← map_tmul R'.mkQ R'.mkQ, ← hs, map_tmul, this, zero_tmul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h_1 : Nontrivial.{u_2} (A ⧸ R')
x y s : A
hs : Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] s) (x ⊗ₜ[R] y)
this : Eq.{u_2 + 1} (α := A ⧸ R') ((R'.mkQ : (a : A) → A ⧸ R') 1) 0
tmul :
  Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    (((map.{u_1, u_1, u_2, u_2, u_2, u_2} (R := R) (R₂ := R) (σ₁₂ := RingHom.id R) (M := A) (N := A) (M₂ := A ⧸ R')
              (N₂ := A ⧸ R') R'.mkQ R'.mkQ :
            A ⊗[R] A →ₗ[R] (A ⧸ R') ⊗[R] (A ⧸ R')) :
          (a : A ⊗[R] A) → (A ⧸ R') ⊗[R] (A ⧸ R'))
        (x ⊗ₜ[R] y) :
      (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
tmul₁ :
  Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    (((map.{u_1, u_1, u_2, u_2, u_2, u_2} (R := R) (R₂ := R) (σ₁₂ := RingHom.id R) (M := A) (N := A) (M₂ := A ⧸ R')
              (N₂ := A ⧸ R') R'.mkQ R'.mkQ :
            A ⊗[R] A →ₗ[R] (A ⧸ R') ⊗[R] (A ⧸ R')) :
          (a : A ⊗[R] A) → (A ⧸ R') ⊗[R] (A ⧸ R'))
        (1 ⊗ₜ[R] s) :
      (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
tmul₂ :
  Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    ((R'.mkQ : (a : A) → A ⧸ R') 1 ⊗ₜ[R] (R'.mkQ : (a : A) → A ⧸ R') s : (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
⊢ Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    ((R'.mkQ : (a : A) → A ⧸ R') x ⊗ₜ[R] (R'.mkQ : (a : A) → A ⧸ R') y : (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
have tmul₃ : Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R')) (0 ⊗ₜ[R] (R'.mkQ : (a : A) → A ⧸ R') s : (A ⧸ R') ⊗[R] (A ⧸ R'))
  (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
Tactic: rw [← map_tmul R'.mkQ R'.mkQ, ← hs, map_tmul, this, zero_tmul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h_1 : Nontrivial.{u_2} (A ⧸ R')
x y s : A
hs : Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] s) (x ⊗ₜ[R] y)
this : Eq.{u_2 + 1} (α := A ⧸ R') ((R'.mkQ : (a : A) → A ⧸ R') 1) 0
tmul :
  Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    (((map.{u_1, u_1, u_2, u_2, u_2, u_2} (R := R) (R₂ := R) (σ₁₂ := RingHom.id R) (M := A) (N := A) (M₂ := A ⧸ R')
              (N₂ := A ⧸ R') R'.mkQ R'.mkQ :
            A ⊗[R] A →ₗ[R] (A ⧸ R') ⊗[R] (A ⧸ R')) :
          (a : A ⊗[R] A) → (A ⧸ R') ⊗[R] (A ⧸ R'))
        (x ⊗ₜ[R] y) :
      (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
tmul₁ :
  Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    (((map.{u_1, u_1, u_2, u_2, u_2, u_2} (R := R) (R₂ := R) (σ₁₂ := RingHom.id R) (M := A) (N := A) (M₂ := A ⧸ R')
              (N₂ := A ⧸ R') R'.mkQ R'.mkQ :
            A ⊗[R] A →ₗ[R] (A ⧸ R') ⊗[R] (A ⧸ R')) :
          (a : A ⊗[R] A) → (A ⧸ R') ⊗[R] (A ⧸ R'))
        (1 ⊗ₜ[R] s) :
      (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
tmul₂ :
  Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    ((R'.mkQ : (a : A) → A ⧸ R') 1 ⊗ₜ[R] (R'.mkQ : (a : A) → A ⧸ R') s : (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
tmul₃ :
  Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R')) (0 ⊗ₜ[R] (R'.mkQ : (a : A) → A ⧸ R') s : (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
⊢ Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R'))
    ((R'.mkQ : (a : A) → A ⧸ R') x ⊗ₜ[R] (R'.mkQ : (a : A) → A ⧸ R') y : (A ⧸ R') ⊗[R] (A ⧸ R'))
    (0 : (A ⧸ R') ⊗[R] (A ⧸ R'))
have tmul₄ : Eq.{u_2 + 1} (α := (A ⧸ R') ⊗[R] (A ⧸ R')) 0 0
Tactic: rw [← map_tmul R'.mkQ R'.mkQ, ← hs, map_tmul, this, zero_tmul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h_1 : Nontrivial.{u_2} (A ⧸ R')
y : (A ⧸ R') ⊗[R] (A ⧸ R')
⊢ y = 0
have zero : Eq.{u_2 + 1} (α := (A ⧸ R') ⊗[R] (A ⧸ R')) 0 0
Tactic: induction y with
    | zero => rfl
    | add a b e₁ e₂ => rwa [e₁, zero_add]
    | tmul x y =>
      obtain ⟨x, rfl⟩ := R'.mkQ_surjective x
      obtain ⟨y, rfl⟩ := R'.mkQ_surjective y
      obtain ⟨s, hs⟩ : ∃ s, 1 ⊗ₜ[R] s = x ⊗ₜ[R] y := by
        use x * y
        trans x ⊗ₜ 1 * 1 ⊗ₜ y
        · simp [(isEpi_iff_forall_one_tmul_eq R A).mp]
        · simp
      have : R'.mkQ 1 = 0 := (Submodule.Quotient.mk_eq_zero R').mpr ⟨1, map_one (algebraMap R A)⟩
      rw [← map_tmul R'.mkQ R'.mkQ, ← hs, map_tmul, this, zero_tmul]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h_1 : Nontrivial.{u_2} (A ⧸ R')
y : (A ⧸ R') ⊗[R] (A ⧸ R')
zero : Eq.{u_2 + 1} (α := (A ⧸ R') ⊗[R] (A ⧸ R')) 0 0
⊢ y = 0
have add : ∀ (a b : (A ⧸ R') ⊗[R] (A ⧸ R')) (e₁ : a = 0) (e₂ : b = 0), a + b = 0
Tactic: induction y with
    | zero => rfl
    | add a b e₁ e₂ => rwa [e₁, zero_add]
    | tmul x y =>
      obtain ⟨x, rfl⟩ := R'.mkQ_surjective x
      obtain ⟨y, rfl⟩ := R'.mkQ_surjective y
      obtain ⟨s, hs⟩ : ∃ s, 1 ⊗ₜ[R] s = x ⊗ₜ[R] y := by
        use x * y
        trans x ⊗ₜ 1 * 1 ⊗ₜ y
        · simp [(isEpi_iff_forall_one_tmul_eq R A).mp]
        · simp
      have : R'.mkQ 1 = 0 := (Submodule.Quotient.mk_eq_zero R').mpr ⟨1, map_one (algebraMap R A)⟩
      rw [← map_tmul R'.mkQ R'.mkQ, ← hs, map_tmul, this, zero_tmul]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h_1 : Nontrivial.{u_2} (A ⧸ R')
y : (A ⧸ R') ⊗[R] (A ⧸ R')
zero : Eq.{u_2 + 1} (α := (A ⧸ R') ⊗[R] (A ⧸ R')) 0 0
add : ∀ (a b : (A ⧸ R') ⊗[R] (A ⧸ R')) (e₁ : a = 0) (e₂ : b = 0), a + b = 0
⊢ y = 0
have tmul : ∀ (x y : A ⧸ R'), Eq (α := (A ⧸ R') ⊗[R] (A ⧸ R')) (x ⊗ₜ[R] y) 0
Tactic: induction y with
    | zero => rfl
    | add a b e₁ e₂ => rwa [e₁, zero_add]
    | tmul x y =>
      obtain ⟨x, rfl⟩ := R'.mkQ_surjective x
      obtain ⟨y, rfl⟩ := R'.mkQ_surjective y
      obtain ⟨s, hs⟩ : ∃ s, 1 ⊗ₜ[R] s = x ⊗ₜ[R] y := by
        use x * y
        trans x ⊗ₜ 1 * 1 ⊗ₜ y
        · simp [(isEpi_iff_forall_one_tmul_eq R A).mp]
        · simp
      have : R'.mkQ 1 = 0 := (Submodule.Quotient.mk_eq_zero R').mpr ⟨1, map_one (algebraMap R A)⟩
      rw [← map_tmul R'.mkQ R'.mkQ, ← hs, map_tmul, this, zero_tmul]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := LinearMap.range (Algebra.linearMap R A)
h_1 : Nontrivial.{u_2} (A ⧸ R')
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
have this : Subsingleton.{u_2 + 1} ((A ⧸ R') ⊗[R] (A ⧸ R'))
Tactic: have : Subsingleton ((A ⧸ R') ⊗[R] (A ⧸ R')) := by
    refine subsingleton_of_forall_eq 0 fun y ↦ ?_
    induction y with
    | zero => rfl
    | add a b e₁ e₂ => rwa [e₁, zero_add]
    | tmul x y =>
      obtain ⟨x, rfl⟩ := R'.mkQ_surjective x
      obtain ⟨y, rfl⟩ := R'.mkQ_surjective y
      obtain ⟨s, hs⟩ : ∃ s, 1 ⊗ₜ[R] s = x ⊗ₜ[R] y := by
        use x * y
        trans x ⊗ₜ 1 * 1 ⊗ₜ y
        · simp [(isEpi_iff_forall_one_tmul_eq R A).mp]
        · simp
      have : R'.mkQ 1 = 0 := (Submodule.Quotient.mk_eq_zero R').mpr ⟨1, map_one (algebraMap R A)⟩
      rw [← map_tmul R'.mkQ R'.mkQ, ← hs, map_tmul, this, zero_tmul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
a_1 b_1 a b : A
⊢ a ⊗ₜ[R] b = HSMul.hSMul (β := A ⊗[R] A) a (1 ⊗ₜ[R] b)
have rw : HSMul.hSMul (β := A ⊗[R] A) a (1 ⊗ₜ[R] b) = HSMul.hSMul (β := A ⊗[R] A) a (1 ⊗ₜ[R] b)
Tactic: rw [tmul_eq_smul_one_tmul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
a_1 b_1 a b : A
⊢ HSMul.hSMul (β := A ⊗[R] A) a (1 ⊗ₜ[R] b) = HSMul.hSMul (β := A ⊗[R] A) a (b ⊗ₜ[R] 1)
have rw : HSMul.hSMul (β := A ⊗[R] A) a (b ⊗ₜ[R] 1) = HSMul.hSMul (β := A ⊗[R] A) a (b ⊗ₜ[R] 1)
Tactic: rw [(isEpi_iff_forall_one_tmul_eq R A).mp inferInstance b]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
a_1 b_1 a b : A
⊢ HSMul.hSMul (β := A ⊗[R] A) a (b ⊗ₜ[R] 1) = a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1)
have rw : a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1) = a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1)
Tactic: rw [tmul_eq_smul_one_tmul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
a b : A
⊢ Eq (α := A ⊗[R] A) (a ⊗ₜ[R] b) (b ⊗ₜ[R] a)
have this : ∀ (a b : A), a ⊗ₜ[R] b = a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1)
Tactic: have (a b : A) := calc a ⊗ₜ[R] b
      = a • (1 ⊗ₜ[R] b) := by rw [tmul_eq_smul_one_tmul]
    _ = a • (b ⊗ₜ[R] 1) := by rw [(isEpi_iff_forall_one_tmul_eq R A).mp inferInstance b]
    _ = a • (b • (1 ⊗ₜ[R] 1)) := by rw [tmul_eq_smul_one_tmul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
a b : A
this : ∀ (a b : A), a ⊗ₜ[R] b = a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1)
⊢ Eq (α := A ⊗[R] A) (a ⊗ₜ[R] b) (b ⊗ₜ[R] a)
have rw : a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1) = b ⊗ₜ[R] a
Tactic: rw [this a b, this b a, smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
a b : A
this : ∀ (a b : A), a ⊗ₜ[R] b = a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1)
rw : a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1) = b ⊗ₜ[R] a
⊢ Eq (α := A ⊗[R] A) (a ⊗ₜ[R] b) (b ⊗ₜ[R] a)
have rw₁ : a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1) = b • HSMul.hSMul (β := A ⊗[R] A) a (1 ⊗ₜ[R] 1)
Tactic: rw [this a b, this b a, smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
a b : A
this : ∀ (a b : A), a ⊗ₜ[R] b = a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1)
rw : a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1) = b ⊗ₜ[R] a
rw₁ : a • HSMul.hSMul (β := A ⊗[R] A) b (1 ⊗ₜ[R] 1) = b • HSMul.hSMul (β := A ⊗[R] A) a (1 ⊗ₜ[R] 1)
⊢ Eq (α := A ⊗[R] A) (a ⊗ₜ[R] b) (b ⊗ₜ[R] a)
have rw₂ : b • HSMul.hSMul (β := A ⊗[R] A) a (1 ⊗ₜ[R] 1) = b • HSMul.hSMul (β := A ⊗[R] A) a (1 ⊗ₜ[R] 1)
Tactic: rw [this a b, this b a, smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
this : ∀ (a : A) (m : M), Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] (a • m)) (a ⊗ₜ[R] m)
f : M →ₗ[R] A ⊗[R] M := { toFun := fun (m : M) ↦ 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
⊢ f ∘ₗ lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)) = LinearMap.id
have a : ∀ (a : A) (m : M),
  Eq (α := A ⊗[R] M)
    (((((AlgebraTensorModule.curry (f ∘ₗ lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M))) :
                  A →ₗ[R] M →ₗ[R] A ⊗[R] M) :
                (a : A) → M →ₗ[R] A ⊗[R] M)
              a :
            M →ₗ[R] A ⊗[R] M) :
          (a : M) → A ⊗[R] M)
        m :
      A ⊗[R] M)
    (((((AlgebraTensorModule.curry LinearMap.id : A →ₗ[R] M →ₗ[R] A ⊗[R] M) : (a : A) → M →ₗ[R] A ⊗[R] M) a :
            M →ₗ[R] A ⊗[R] M) :
          (a : M) → A ⊗[R] M)
        m :
      A ⊗[R] M)
Tactic: ext a m
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
this : ∀ (a : A) (m : M), Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] (a • m)) (a ⊗ₜ[R] m)
f : M →ₗ[R] A ⊗[R] M := { toFun := fun (m : M) ↦ 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
⊢ Injective (α := A ⊗[R] M) (β := M)
    (⇑(lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M))) : (a : A ⊗[R] M) → M)
have aux : f ∘ₗ lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)) = LinearMap.id
Tactic: have aux : f ∘ₗ (lift <| LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)) = .id := by
      ext a m; simpa using this a m
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
⊢ Injective (α := A ⊗[R] M) (β := M)
    (⇑(lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M))) : (a : A ⊗[R] M) → M)
have suffices : ∀ (a : A) (m : M), Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] (a • m)) (a ⊗ₜ[R] m)
Tactic: suffices ∀ (a : A) (m : M), 1 ⊗ₜ[R] (a • m) = a ⊗ₜ[R] m by
    let f : M →ₗ[R] A ⊗[R] M :=
      { toFun m := 1 ⊗ₜ m
        map_add' m n := tmul_add _ _ _
        map_smul' r m := tmul_smul _ _ _ }
    have aux : f ∘ₗ (lift <| LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)) = .id := by
      ext a m; simpa using this a m
    exact HasLeftInverse.injective ⟨f, fun x ↦ congr($aux x)⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
a : A
m : M
x y : A
⊢ { toFun := fun (y_1 : A) ↦ (x + y) ⊗ₜ[R] (y_1 • m), map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := A →ₗ[R] A ⊗[R] M)
      { toFun := fun (y : A) ↦ x ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] A ⊗[R] M }
      { toFun := fun (y_1 : A) ↦ y ⊗ₜ[R] (y_1 • m), map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] A ⊗[R] M }
have h : ∀ (x_1 : A),
  Eq (α := A ⊗[R] M)
    (({ toFun := fun (y_1 : A) ↦ (x + y) ⊗ₜ[R] (y_1 • m), map_add' := sorry, map_smul' := sorry } : (a : A) → A ⊗[R] M) x_1 :
      A ⊗[R] M)
    ((HAdd.hAdd (α := A →ₗ[R] A ⊗[R] M)
            { toFun := fun (y : A) ↦ x ⊗ₜ[R] (y • m), map_add' := sorry, map_smul' := sorry : A →ₗ[R] A ⊗[R] M }
            { toFun := fun (y_1 : A) ↦ y ⊗ₜ[R] (y_1 • m), map_add' := sorry, map_smul' := sorry : A →ₗ[R] A ⊗[R] M } :
          (a : A) → A ⊗[R] M)
        x_1 :
      A ⊗[R] M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Epi (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
a : A
m : M
m_1 : R
x : A
⊢ { toFun := fun (y : A) ↦ (m_1 • x) ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := R) (β := A →ₗ[R] A ⊗[R] M) ((RingHom.id R : (a : R) → R) m_1 : R)
      { toFun := fun (y : A) ↦ x ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] A ⊗[R] M }
have h : ∀ (x_1 : A),
  Eq (α := A ⊗[R] M)
    (({ toFun := fun (y : A) ↦ (m_1 • x) ⊗ₜ[R] (y • m), map_add' := sorry, map_smul' := sorry } : (a : A) → A ⊗[R] M) x_1 :
      A ⊗[R] M)
    ((HSMul.hSMul (α := R) (β := A →ₗ[R] A ⊗[R] M) ((RingHom.id R : (a : R) → R) m_1 : R)
            { toFun := fun (y : A) ↦ x ⊗ₜ[R] (y • m), map_add' := sorry, map_smul' := sorry : A →ₗ[R] A ⊗[R] M } :
          (a : A) → A ⊗[R] M)
        x_1 :
      A ⊗[R] M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e f g : A₁ ≃ₐ[R] A₂
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g
have obtain : ∀ (f : A₁ → A₂) (invFun : A₂ → A₁) (left_inv : Function.LeftInverse invFun f)
  (right_inv : Function.RightInverse invFun f)
  (map_mul' :
    ∀ (x y : A₁),
      { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun (x * y) =
        { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun x *
          { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun y)
  (map_add' :
    ∀ (x y : A₁),
      { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun (x + y) =
        { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun x +
          { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun y)
  (commutes' :
    ∀ (r : R),
      { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun
          ((algebraMap R A₁ : (a : R) → A₁) r) =
        (algebraMap R A₂ : (a : R) → A₂) r)
  (h₁ :
    { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
          map_add' := map_add', commutes' := commutes' : A₁ ≃ₐ[R] A₂ }.toFun =
      g.toFun)
  (h₂ :
    { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
          map_add' := map_add', commutes' := commutes' : A₁ ≃ₐ[R] A₂ }.invFun =
      g.invFun),
  { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
      map_add' := map_add', commutes' := commutes' : A₁ ≃ₐ[R] A₂ } =
    g
Tactic: obtain ⟨⟨f, _⟩, _⟩ := f
Cleared hypotheses: f, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e_1 e : A₁ ≃ₐ[R] A₂
r : R
⊢ e.toRingEquiv.symm.toFun ((algebraMap R A₂ : (a : R) → A₂) r) = (algebraMap R A₁ : (a : R) → A₁) r
have rw : e.toRingEquiv.symm.toFun ((algebraMap R A₂ : (a : R) → A₂) r) =
  (e.toRingEquiv.symm : (a : A₂) → A₁) ((e.toRingEquiv : (a : A₁) → A₂) ((algebraMap R A₁ : (a : R) → A₁) r : A₁) : A₂)
Tactic: rw [← e.toRingEquiv.symm_apply_apply (algebraMap R A₁ r)]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e_1 e : A₁ ≃ₐ[R] A₂
r : R
⊢ e.toRingEquiv.symm.toFun ((algebraMap R A₂ : (a : R) → A₂) r) =
    (e.toRingEquiv.symm : (a : A₂) → A₁)
      ((e.toRingEquiv : (a : A₁) → A₂) ((algebraMap R A₁ : (a : R) → A₁) r : A₁) : A₂)
have e_a : Eq.{uA₂ + 1} (α := A₂) ((algebraMap R A₂ : (a : R) → A₂) r : A₂)
  ((e.toRingEquiv : (a : A₁) → A₂) ((algebraMap R A₁ : (a : R) → A₁) r : A₁) : A₂)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ (↑e : A₁ →ₐ[R] A₂).comp (↑e.symm : A₂ →ₐ[R] A₁) = AlgHom.id R A₂
have H : ∀ (x : A₂),
  Eq (α := A₂) (((↑e : A₁ →ₐ[R] A₂).comp (↑e.symm : A₂ →ₐ[R] A₁) : (a : A₂) → A₂) x : A₂)
    ((AlgHom.id R A₂ : (a : A₂) → A₂) x : A₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ (↑e.symm : A₂ →ₐ[R] A₁).comp (↑e : A₁ →ₐ[R] A₂) = AlgHom.id R A₁
have H : ∀ (x : A₁),
  Eq (α := A₁) (((↑e.symm : A₂ →ₐ[R] A₁).comp (↑e : A₁ →ₐ[R] A₂) : (a : A₁) → A₁) x : A₁)
    ((AlgHom.id R A₁ : (a : A₁) → A₁) x : A₁)
Tactic: ext