awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
e : R ≃ₗ[R] A
x : A
rw :
  HMul.hMul (α := A)
      ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A) ((e.symm : (a : A) → R) 1 : R) ((e : (a : R) → A) 1 : A)) =
    x
rw₁ :
  HMul.hMul (α := A)
      ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
      (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
        ((e : (a : R) → A) 1 : A)) =
    x
rw₂ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
      (HMul.hMul (α := A) (β := A)
        ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) :
          A)
        ((e : (a : R) → A) 1 : A)) =
    x
rw₃ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A)
        ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) ((e : (a : R) → A) 1 : A)) =
    x
rw₄ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
      ((e : (a : R) → A)
          (HSMul.hSMul (α := R) (β := R) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R)
            1) :
        A) =
    x
rw₅ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
      ((e : (a : R) → A)
          (HMul.hMul (α := R) (β := R) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R)
            (1 : R)) :
        A) =
    x
rw₆ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
      ((e : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A) =
    x
rw₇ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
      (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) =
    x
rw₈ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
        ((e : (a : R) → A) 1 : A) *
      x =
    x
⊢ HMul.hMul (α := A) (β := A)
      ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
      ((e : (a : R) → A) (HSMul.hSMul (α := R) (β := R) ((e.symm : (a : A) → R) 1 : R) 1) : A) =
    x
have rw₉ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A) ((e.symm : (a : A) → R) 1 : R) ((e : (a : R) → A) 1 : A) * x = x
Tactic: rw [map_smul, Algebra.smul_def, mul_left_comm, ← Algebra.smul_def _ (e 1),
          ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply, ← mul_assoc, ← Algebra.smul_def,
          ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
e : R ≃ₗ[R] A
x : A
rw :
  HMul.hMul (α := A)
      ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A) ((e.symm : (a : A) → R) 1 : R) ((e : (a : R) → A) 1 : A)) =
    x
rw₁ :
  HMul.hMul (α := A)
      ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
      (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
        ((e : (a : R) → A) 1 : A)) =
    x
rw₂ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
      (HMul.hMul (α := A) (β := A)
        ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) :
          A)
        ((e : (a : R) → A) 1 : A)) =
    x
rw₃ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A)
        ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) ((e : (a : R) → A) 1 : A)) =
    x
rw₄ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
      ((e : (a : R) → A)
          (HSMul.hSMul (α := R) (β := R) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R)
            1) :
        A) =
    x
rw₅ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
      ((e : (a : R) → A)
          (HMul.hMul (α := R) (β := R) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R)
            (1 : R)) :
        A) =
    x
rw₆ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
      ((e : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A) =
    x
rw₇ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
      (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) =
    x
rw₈ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
        ((e : (a : R) → A) 1 : A) *
      x =
    x
rw₉ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A) ((e.symm : (a : A) → R) 1 : R) ((e : (a : R) → A) 1 : A) * x = x
⊢ HMul.hMul (α := A) (β := A)
      ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
      ((e : (a : R) → A) (HSMul.hSMul (α := R) (β := R) ((e.symm : (a : A) → R) 1 : R) 1) : A) =
    x
have rw₁₀ : HMul.hMul (α := A) ((e : (a : R) → A) (HSMul.hSMul (α := R) (β := R) ((e.symm : (a : A) → R) 1 : R) 1) : A) x = x
Tactic: rw [map_smul, Algebra.smul_def, mul_left_comm, ← Algebra.smul_def _ (e 1),
          ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply, ← mul_assoc, ← Algebra.smul_def,
          ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₁
inst_7 : Module S M₂
inst_8 : SMulCommClass S R M₁
inst_9 : SMulCommClass S R M₂
inst_10 : SMul R S
inst_11 : IsScalarTower R S M₁
inst_12 : IsScalarTower R S M₂
e : M₁ ≃ₗ[S] M₂
x : R
⊢ e.conjRingEquiv.toFun ((algebraMap R (Module.End S M₁) : (a : R) → Module.End S M₁) x) =
    (algebraMap R (Module.End S M₂) : (a : R) → Module.End S M₂) x
have h : ∀ (x_1 : M₂),
  Eq (α := M₂)
    ((e.conjRingEquiv.toFun ((algebraMap R (Module.End S M₁) : (a : R) → Module.End S M₁) x) : (a : M₂) → M₂) x_1 : M₂)
    ((((algebraMap R (Module.End S M₂) : (a : R) → Module.End S M₂) x : Module.End S M₂) : (a : M₂) → M₂) x_1 : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₁
inst_7 : Module S M₂
inst_8 : SMulCommClass S R M₁
inst_9 : SMulCommClass S R M₂
inst_10 : SMul R S
inst_11 : IsScalarTower R S M₁
inst_12 : IsScalarTower R S M₂
e : M₁ ≃ₗ[S] M₂
x : R
x_1 : M₂
⊢ Eq (α := M₂)
    ((e.conjRingEquiv.toFun ((algebraMap R (Module.End S M₁) : (a : R) → Module.End S M₁) x) : (a : M₂) → M₂) x_1 : M₂)
    ((((algebraMap R (Module.End S M₂) : (a : R) → Module.End S M₂) x : Module.End S M₂) : (a : M₂) → M₂) x_1 : M₂)
have h : Eq.{u_4 + 1} (α := M₂)
  ((restrictScalars R e : (a : M₁) → M₂)
      ((((algebraMap R (Module.End S M₁) : (a : R) → Module.End S M₁) x : Module.End S M₁) : (a : M₁) → M₁)
          (((↑e.symm : M₂ →ₗ[S] M₁) : (a : M₂) → M₁) x_1 : M₁) :
        M₁) :
    M₂)
  ((((algebraMap R (Module.End S M₂) : (a : R) → Module.End S M₂) x : Module.End S M₂) : (a : M₂) → M₂) x_1 : M₂)
Tactic: change e.restrictScalars R _ = _
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Hom (goal)
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
f g : A →ₐ[R] B
h :
  Eq (α := (a : A) → B) ((fun (f : A →ₐ[R] B) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) f)
    ((fun (f : A →ₐ[R] B) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) g)
⊢ f = g
have rcases : ∀ (toFun : A → B) (map_one' : toFun 1 = 1)
  (map_mul' :
    ∀ (x y : A),
      { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun (x * y) =
        { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun x *
          { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun y)
  (map_zero' : (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun 0 = 0)
  (map_add' :
    ∀ (x y : A),
      (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun (x + y) =
        (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun x +
          (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun y)
  (commutes' :
    ∀ (r : R),
      (↑(↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add' :
                      A →+* B } :
                  A →* B) :
              OneHom A B).toFun
          ((algebraMap R A : (a : R) → A) r) =
        (algebraMap R B : (a : R) → B) r)
  (h :
    Eq (α := (a : A) → B)
      ((fun (f : A →ₐ[R] B) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
        { toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
          commutes' := commutes' })
      ((fun (f : A →ₐ[R] B) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) g)),
  { toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
      commutes' := commutes' : A →ₐ[R] B } =
    g
Tactic: rcases f with ⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Hom (goal)
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
φ : A →ₐ[R] B
φ₁ : B →ₐ[R] C
φ₂ : A →ₐ[R] B
r : R
⊢ OneHom.toFun (↑(↑(φ₁.comp (↑φ₂ : A →+* B)) : A →* C) : OneHom A C) ((algebraMap R A : (a : R) → A) r) =
    (algebraMap R C : (a : R) → C) r
have rw : OneHom.toFun (↑(↑(φ₁.comp (↑φ₂ : A →+* B)) : A →* C) : OneHom A C) ((algebraMap R A : (a : R) → A) r) =
  (φ₁ : (a : B) → C) ((φ₂ : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
Tactic: rw [← φ₁.commutes, ← φ₂.commutes]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Hom (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
φ : A →ₐ[R] A
n : ℕ
⊢ Eq (α := (a : A) → A) (⇑(φ ^ Nat.zero) : (a : A) → A) (⇑φ : (a : A) → A)^[Nat.zero]
have h : ∀ (x : A), (φ ^ Nat.zero : (a : A) → A) x = (⇑φ : (a : A) → A)^[Nat.zero] x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Hom (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
φ : A →ₐ[R] A
n x : ℕ
ih : Eq (α := (a : A) → A) (⇑(φ ^ x) : (a : A) → A) (⇑φ : (a : A) → A)^[x]
⊢ Eq (α := (a : A) → A) (⇑(φ ^ x.succ) : (a : A) → A) (⇑φ : (a : A) → A)^[x.succ]
have h : ∀ (x_1 : A), (φ ^ x.succ : (a : A) → A) x_1 = (⇑φ : (a : A) → A)^[x.succ] x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Hom (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
x x_1 : A →ₐ[R] A
x_2 : Aˣ
⊢ (x * x_1) • x_2 = x • x_1 • x_2
have huv : (↑((x * x_1) • x_2) : A) = (↑(x • x_1 • x_2) : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Hom (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
x : Aˣ
⊢ HSMul.hSMul (α := A →ₐ[R] A) 1 x = x
have huv : (↑(HSMul.hSMul (α := A →ₐ[R] A) 1 x) : A) = (↑x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Hom (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
x : A →ₐ[R] A
⊢ HSMul.hSMul (β := Aˣ) x 1 = 1
have huv : (↑(HSMul.hSMul (β := Aˣ) x 1) : A) = (↑1 : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Hom (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
x : A →ₐ[R] A
x_1 x_2 : Aˣ
⊢ x • (x_1 * x_2) = x • x_1 * x • x_2
have huv : (↑(x • (x_1 * x_2)) : A) = (↑(x • x_1 * x • x_2) : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Hom (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
M : Submonoid R
B : Type w
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ Eq (α := Submonoid B) (Submonoid.map f (algebraMapSubmonoid A M)) (algebraMapSubmonoid B M)
have h : ∀ (x : B),
  Membership.mem (γ := Submonoid B) (Submonoid.map f (algebraMapSubmonoid A M)) x ↔
    Membership.mem (γ := Submonoid B) (algebraMapSubmonoid B M) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Hom (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
M : Submonoid R
B : Type w
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
x : B
⊢ Membership.mem (γ := Submonoid B) (Submonoid.map f (algebraMapSubmonoid A M)) x ↔
    Membership.mem (γ := Submonoid B) (algebraMapSubmonoid B M) x
have h : Membership.mem (γ := Submonoid B) (Submonoid.map f (algebraMapSubmonoid A M)) x →
  Membership.mem (γ := Submonoid B) (algebraMapSubmonoid B M) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Hom (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
M : Submonoid R
B : Type w
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
x : B
h :
  Membership.mem (γ := Submonoid B) (Submonoid.map f (algebraMapSubmonoid A M)) x →
    Membership.mem (γ := Submonoid B) (algebraMapSubmonoid B M) x
⊢ Membership.mem (γ := Submonoid B) (Submonoid.map f (algebraMapSubmonoid A M)) x ↔
    Membership.mem (γ := Submonoid B) (algebraMapSubmonoid B M) x
have h₁ : Membership.mem (γ := Submonoid B) (algebraMapSubmonoid B M) x →
  Membership.mem (γ := Submonoid B) (Submonoid.map f (algebraMapSubmonoid A M)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Hom (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
M : Submonoid R
B : Type w
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ (↑M : Set R)
⊢ Membership.mem (α := B) (γ := Submonoid B) (algebraMapSubmonoid B M)
    ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
have h : Membership.mem (α := B) (γ := Submonoid B) (algebraMapSubmonoid B M) ((algebraMap R B : (a : R) → B) r : B)
Tactic: simp only [AlgHom.commutes]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Hom (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
M : Submonoid R
B : Type w
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ (↑M : Set R)
w : R
⊢ Membership.mem (α := B) (γ := Submonoid B) (algebraMapSubmonoid B M) ((algebraMap R B : (a : R) → B) r : B)
have h : r ∈ (↑M : Set R) ∧ Eq.{w + 1} (α := B) ((algebraMap R B : (a : R) → B) r : B) ((algebraMap R B : (a : R) → B) r : B)
Tactic: use r
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Hom (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
M : Submonoid R
B : Type w
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ (↑M : Set R)
⊢ ∃ (x : A),
    Membership.mem (γ := Submonoid A) (algebraMapSubmonoid A M) x ∧
      Eq.{w + 1} (α := B) ((f : (a : A) → B) x : B) ((algebraMap R B : (a : R) → B) r : B)
have h : Membership.mem (α := A) (γ := Submonoid A) (algebraMapSubmonoid A M) ((algebraMap R A : (a : R) → A) r : A) ∧
  Eq.{w + 1} (α := B) ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
    ((algebraMap R B : (a : R) → B) r : B)
Tactic: use (algebraMap R A r)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Hom (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
M : Submonoid R
B : Type w
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ (↑M : Set R)
⊢ Membership.mem (α := A) (γ := Submonoid A) (algebraMapSubmonoid A M) ((algebraMap R A : (a : R) → A) r : A) ∧
    Eq.{w + 1} (α := B) ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
      ((algebraMap R B : (a : R) → B) r : B)
have h : Membership.mem (α := A) (γ := Submonoid A) (algebraMapSubmonoid A M) ((algebraMap R A : (a : R) → A) r : A)
Tactic: simp only [AlgHom.commutes, and_true]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Hom (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
M : Submonoid R
B : Type w
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ (↑M : Set R)
w : R
⊢ Membership.mem (α := A) (γ := Submonoid A) (algebraMapSubmonoid A M) ((algebraMap R A : (a : R) → A) r : A)
have h : r ∈ (↑M : Set R) ∧ Eq.{v + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) r : A)
Tactic: use r
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Hom (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
M : Submonoid R
B : Type w
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ LE.le (α := Submonoid A) (algebraMapSubmonoid A M) (Submonoid.comap f.toRingHom (algebraMapSubmonoid B M))
have rw : LE.le (α := Submonoid A) (algebraMapSubmonoid A M)
  (Submonoid.comap f.toRingHom (Submonoid.map f (algebraMapSubmonoid A M)))
Tactic: rw [← algebraMapSubmonoid_map_eq M f]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalHom (goal)
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : Eq (α := A →ₑ+[φ] B) (↑f : A →ₑ+[φ] B) (↑g : A →ₑ+[φ] B)
⊢ f = g
have h₁ : ∀ (a : A), Eq.{w + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalHom (goal)
Goal:
R : Type u
S : Type u₁
inst : Monoid R
inst_1 : Monoid S
φ : R →* S
A : Type v
B : Type w
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : Eq (α := A →ₙ* B) (↑f : A →ₙ* B) (↑g : A →ₙ* B)
⊢ f = g
have h₁ : ∀ (a : A), Eq.{w + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalHom (goal)
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst_9 : NonUnitalNonAssocSemiring B₁
inst_10 : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse.{u + 1, u₁ + 1} (α := R) (β := S) (⇑φ' : (a : S) → R) (⇑φ : (a : R) → S)
h₁ : Function.LeftInverse g (⇑f : (a : A) → B)
h₂ : Function.RightInverse g (⇑f : (a : A) → B)
⊢ MulHom.toFun (MulHom.inverse (↑f : A →ₙ* B) g h₁ h₂) 0 = 0
have simp : g 0 = 0
Tactic: simp only [MulHom.toFun_eq_coe, MulHom.inverse_apply]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalHom (goal)
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst_9 : NonUnitalNonAssocSemiring B₁
inst_10 : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse.{u + 1, u₁ + 1} (α := R) (β := S) (⇑φ' : (a : S) → R) (⇑φ : (a : R) → S)
h₁ : Function.LeftInverse g (⇑f : (a : A) → B)
h₂ : Function.RightInverse g (⇑f : (a : A) → B)
⊢ g 0 = 0
have rw : g ((f : (a : A) → B) 0) = 0
Tactic: rw [← f.map_zero, h₁]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalHom (goal)
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst_9 : NonUnitalNonAssocSemiring B₁
inst_10 : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse.{u + 1, u₁ + 1} (α := R) (β := S) (⇑φ' : (a : S) → R) (⇑φ : (a : R) → S)
h₁ : Function.LeftInverse g (⇑f : (a : A) → B)
h₂ : Function.RightInverse g (⇑f : (a : A) → B)
rw : g ((f : (a : A) → B) 0) = 0
⊢ g 0 = 0
have rw₁ : Eq.{v + 1} (α := A) 0 0
Tactic: rw [← f.map_zero, h₁]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalHom (goal)
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst_9 : NonUnitalNonAssocSemiring B₁
inst_10 : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse.{u + 1, u₁ + 1} (α := R) (β := S) (⇑φ' : (a : S) → R) (⇑φ : (a : R) → S)
h₁ : Function.LeftInverse g (⇑f : (a : A) → B)
h₂ : Function.RightInverse g (⇑f : (a : A) → B)
x y : B
⊢ MulHom.toFun (MulHom.inverse (↑f : A →ₙ* B) g h₁ h₂) (x + y) =
    MulHom.toFun (MulHom.inverse (↑f : A →ₙ* B) g h₁ h₂) x + MulHom.toFun (MulHom.inverse (↑f : A →ₙ* B) g h₁ h₂) y
have simp : g (x + y) = g x + g y
Tactic: simp only [MulHom.toFun_eq_coe, MulHom.inverse_apply]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalHom (goal)
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst_9 : NonUnitalNonAssocSemiring B₁
inst_10 : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse.{u + 1, u₁ + 1} (α := R) (β := S) (⇑φ' : (a : S) → R) (⇑φ : (a : R) → S)
h₁ : Function.LeftInverse g (⇑f : (a : A) → B)
h₂ : Function.RightInverse g (⇑f : (a : A) → B)
x y : B
⊢ g (x + y) = g x + g y
have rw : g (HAdd.hAdd (α := B) ((f : (a : A) → B) (g x) : B) y) = g ((f : (a : A) → B) (g x)) + g y
Tactic: rw [← h₂ x, ← h₂ y, ← map_add, h₁, h₂, h₂]