awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
φ : A →ₐ[R] A
n : ℕ
h : ∀ (x : A), (φ ^ Nat.zero : (a : A) → A) x = (⇑φ : (a : A) → A)^[Nat.zero] x
⊢ Eq (α := (a : A) → A) (⇑(φ ^ Nat.zero) : (a : A) → A) (⇑φ : (a : A) → A)^[Nat.zero]

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
φ : A →ₐ[R] A
n : ℕ
x : A
⊢ (φ ^ Nat.zero : (a : A) → A) x = (⇑φ : (a : A) → A)^[Nat.zero] x

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Hom
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]
h : ∀ (x_1 : A), (φ ^ x.succ : (a : A) → A) x_1 = (⇑φ : (a : A) → A)^[x.succ] x_1
⊢ Eq (α := (a : A) → A) (⇑(φ ^ x.succ) : (a : A) → A) (⇑φ : (a : A) → A)^[x.succ]

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Hom
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]
x_1 : A
⊢ (φ ^ x.succ : (a : A) → A) x_1 = (⇑φ : (a : A) → A)^[x.succ] x_1

Tactic:
simp [pow_succ, ih]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
y : R
x : A
h : (algebraMap R A : (a : R) → A) y = x
⊢ Eq.{w + 1} (α := B) ((algebraMap R B : (a : R) → B) y : B) ((f : (a : A) → B) x : B)

Tactic:
h ▸ (f.commutes _).symm

Premises used: Eq.rec, AlgHom.commutes, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
g₁ g₂ : B →ₐ[R] C
f : A →ₐ[R] B
hf : Function.Surjective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => AlgHom.ext <| hf.forall.2 (AlgHom.ext_iff.1 h), fun h => h ▸ rfl⟩

Premises used: Iff.mpr, Function.Surjective.forall, AlgHom.ext_iff, Eq.rec, AlgHom.ext, Iff.intro, Iff.mp, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
g₁ g₂ : A →ₐ[R] B
f : B →ₐ[R] C
hf : Function.Injective.{w + 1, u₁ + 1} (α := B) (β := C) (⇑f : (a : B) → C)
⊢ f.comp g₁ = f.comp g₂ ↔ g₁ = g₂

Tactic:
⟨fun h => AlgHom.ext <| fun _ ↦ hf.eq_iff.mp <| AlgHom.ext_iff.mp h _, fun h => h ▸ rfl⟩

Premises used: AlgHom.ext_iff, Function.Injective.eq_iff, Eq.rec, AlgHom.ext, Iff.intro, Iff.mp, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
r : R
⊢ OneHom.toFun (↑(↑(algebraMap S A) : S →* A) : OneHom S A) ((algebraMap R S : (a : R) → S) r) =
    (algebraMap R A : (a : R) → A) r

Tactic:
simpa [Algebra.smul_def] using smul_assoc r (1 : S) (1 : A)

Premises used: Algebra.smul_def, OfNat.ofNat, IsScalarTower.smul_assoc
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
y : S
⊢ Eq.{u_3 + 1} (α := A) ((toAlgHom R S A : (a : S) → A) y : A) ((algebraMap S A : (a : S) → A) y : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
⊢ Eq (α := S →+* A) (↑(toAlgHom R S A) : S →+* A) (algebraMap S A)

Tactic:
RingHom.ext fun _ => rfl

Premises used: RingHom.ext, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
⊢ Eq (α := (a : S) → A) (⇑(toAlgHom R S A) : (a : S) → A) (⇑(algebraMap S A) : (a : S) → A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
F : Type u_4
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
f : F
⊢ Eq (α := A →+* B) (↑(↑f : A →ₐ[R] B) : A →+* B) (↑f : A →+* B)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, AlgHomClass.toAlgHom, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
n : ℕ
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) ((algebraMap ℕ R : (a : ℕ) → R) n : R) : S)
    ((algebraMap ℕ S : (a : ℕ) → S) n : S)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
⊢ Eq (α := (a : R) → S) (⇑f.toNatAlgHom : (a : R) → S) (⇑f : (a : R) → S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : R
⊢ Eq.{u_2 + 1} (α := S) ((f.toNatAlgHom : (a : R) → S) x : S) ((f : (a : R) → S) x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
n : ℤ
⊢ (↑(↑f : R →* S) : OneHom R S).toFun ((algebraMap ℤ R : (a : ℤ) → R) n) = (algebraMap ℤ S : (a : ℤ) → S) n

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
⊢ Eq (α := (a : R) → S) (⇑f.toIntAlgHom : (a : R) → S) (⇑f : (a : R) → S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
x : R
⊢ Eq.{u_2 + 1} (α := S) ((f.toIntAlgHom : (a : R) → S) x : S) ((f : (a : R) → S) x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
⊢ Function.Injective (α := R →+* S) toIntAlgHom

Tactic:
fun _ _ e ↦ DFunLike.ext _ _ (fun x ↦ DFunLike.congr_fun e x)

Premises used: DFunLike.congr_fun, DFunLike.ext, Function.Injective
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := R →ₐ[R] R) (ofId R R) (AlgHom.id R R)

Tactic:
rfl

Premises used: AlgHom.id, Algebra.ofId, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := R →+* A) (↑(ofId R A) : R →+* A) (algebraMap R A)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
⊢ Eq.{v + 1} (α := A) ((ofId R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) r : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
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
⊢ Subsingleton (R →ₐ[R] A)

Tactic:
⟨fun f g => AlgHom.ext fun _ => (f.commutes _).trans (g.commutes _).symm⟩

Premises used: AlgHom.ext, Subsingleton.intro, AlgHom.commutes, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
f g : R →ₐ[R] A
⊢ f = g

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.Algebra.Hom
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
φ : A →ₐ[R] B
⊢ φ.comp (ofId R A) = ofId R B

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Hom
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ˣ
huv : (↑((x * x_1) • x_2) : A) = (↑(x • x_1 • x_2) : A)
⊢ (x * x_1) • x_2 = x • x_1 • x_2

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Hom
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) : A) = (↑(x • x_1 • x_2) : A)

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Hom
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ˣ
huv : (↑(HSMul.hSMul (α := A →ₐ[R] A) 1 x) : A) = (↑x : A)
⊢ HSMul.hSMul (α := A →ₐ[R] A) 1 x = x

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Hom
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) : A) = (↑x : A)

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Hom
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
huv : (↑(HSMul.hSMul (β := Aˣ) x 1) : A) = (↑1 : A)
⊢ HSMul.hSMul (β := Aˣ) x 1 = 1

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Hom
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) : A) = (↑1 : A)

Tactic:
map_one _

Premises used: map_one
-- Module: Mathlib.Algebra.Algebra.Hom
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) : A) = (↑1 : A)

Tactic:
exact map_one _

Premises used: map_one
-- Module: Mathlib.Algebra.Algebra.Hom
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ˣ
huv : (↑(x • (x_1 * x_2)) : A) = (↑(x • x_1 * x • x_2) : A)
⊢ x • (x_1 * x_2) = x • x_1 * x • x_2

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Hom
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)) : A) = (↑(x • x_1 * x • x_2) : A)

Tactic:
map_mul _ _ _

Premises used: map_mul
-- Module: Mathlib.Algebra.Algebra.Hom
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)) : A) = (↑(x • x_1 * x • x_2) : A)

Tactic:
exact map_mul _ _ _

Premises used: map_mul
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
f : A →ₐ[R] A
x : Aˣ
⊢ f • x = (Units.map (↑f : A →* A) : (a : Aˣ) → Aˣ) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom
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
h :
  ∀ (x : B),
    Membership.mem (γ := Submonoid B) (Submonoid.map f (algebraMapSubmonoid A M)) x ↔
      Membership.mem (γ := Submonoid B) (algebraMapSubmonoid B M) x
⊢ Eq (α := Submonoid B) (Submonoid.map f (algebraMapSubmonoid A M)) (algebraMapSubmonoid B M)

Tactic:
ext x
-- Module: Mathlib.Algebra.Algebra.Hom
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
h₁ :
  Membership.mem (γ := Submonoid B) (algebraMapSubmonoid B M) x →
    Membership.mem (γ := Submonoid B) (Submonoid.map f (algebraMapSubmonoid A M)) x
⊢ Membership.mem (γ := Submonoid B) (Submonoid.map f (algebraMapSubmonoid A M)) x ↔
    Membership.mem (γ := Submonoid B) (algebraMapSubmonoid B M) x

Tactic:
constructor
-- Module: Mathlib.Algebra.Algebra.Hom
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)
h : Membership.mem (α := B) (γ := Submonoid B) (algebraMapSubmonoid B M) ((algebraMap R B : (a : R) → B) r : B)
⊢ Membership.mem (α := B) (γ := Submonoid B) (algebraMapSubmonoid B M)
    ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)

Tactic:
simp only [AlgHom.commutes]

Premises used: AlgHom.commutes
-- Module: Mathlib.Algebra.Algebra.Hom
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
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)
⊢ Membership.mem (α := B) (γ := Submonoid B) (algebraMapSubmonoid B M) ((algebraMap R B : (a : R) → B) r : B)

Tactic:
use r
-- Module: Mathlib.Algebra.Algebra.Hom
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)
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)
⊢ ∃ (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)

Tactic:
use (algebraMap R A r)

Premises used: Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Hom
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)
h : Membership.mem (α := A) (γ := Submonoid A) (algebraMapSubmonoid A M) ((algebraMap R A : (a : R) → A) r : A)
⊢ 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:
simp only [AlgHom.commutes, and_true]

Premises used: and_true, AlgHom.commutes
-- Module: Mathlib.Algebra.Algebra.Hom
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
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)
⊢ Membership.mem (α := A) (γ := Submonoid A) (algebraMapSubmonoid A M) ((algebraMap R A : (a : R) → A) r : A)

Tactic:
use r
-- Module: Mathlib.Algebra.Algebra.Hom
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
rw :
  LE.le (α := Submonoid A) (algebraMapSubmonoid A M)
    (Submonoid.comap f.toRingHom (Submonoid.map f (algebraMapSubmonoid A M)))
⊢ LE.le (α := Submonoid A) (algebraMapSubmonoid A M) (Submonoid.comap f.toRingHom (algebraMapSubmonoid B M))

Tactic:
rw [← algebraMapSubmonoid_map_eq M f]

Premises used: Algebra.algebraMapSubmonoid_map_eq
-- Module: Mathlib.Algebra.Algebra.Hom
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 (Submonoid.map f (algebraMapSubmonoid A M)))

Tactic:
Submonoid.le_comap_map (Algebra.algebraMapSubmonoid A M)

Premises used: Submonoid.le_comap_map, Set.Mem, Algebra.algebraMapSubmonoid
-- Module: Mathlib.Algebra.Algebra.Hom
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 (Submonoid.map f (algebraMapSubmonoid A M)))

Tactic:
exact Submonoid.le_comap_map (Algebra.algebraMapSubmonoid A M)

Premises used: Submonoid.le_comap_map, Algebra.algebraMapSubmonoid
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
M : Type u_1
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : MulSemiringAction M A
inst_5 : SMulCommClass M R A
inst_6 : FaithfulSMul M A
⊢ Function.Injective.{u_1 + 1, u_4 + 1} (α := M) (β := A →ₐ[R] A) (toAlgHom R A)

Tactic:
fun _m₁ _m₂ h =>
  eq_of_smul_eq_smul fun r => AlgHom.ext_iff.1 h r

Premises used: FaithfulSMul.eq_of_smul_eq_smul, AlgHom.ext_iff, Iff.mp, Function.Injective
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Subsingleton T
x : S
⊢ Eq.{u_3 + 1} (α := T) ((default : (a : S) → T) x : T) (0 : T)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.IsSimpleRing
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : IsSimpleRing R
inst_4 : Nontrivial A
⊢ FaithfulSMul R A

Tactic:
faithfulSMul_iff_algebraMap_injective R A |>.2 <| RingHom.injective _

Premises used: Iff.mpr, faithfulSMul_iff_algebraMap_injective, RingHom.injective
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R_1 : Type u
S_1 : Type u₁
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
x : Monoid R
x_1 : Monoid S
φ : R →* S
x_2 : NonUnitalNonAssocSemiring A
inst : DistribMulAction R A
x_3 : NonUnitalNonAssocSemiring B
inst_1 : DistribMulAction S B
inst_2 : FunLike F A B
inst_3 : NonUnitalAlgSemiHomClass F φ A B
⊢ NonUnitalRingHomClass F A B

Tactic:
{ ‹NonUnitalAlgSemiHomClass F φ A B› with }

Premises used: NonUnitalRingHomClass.mk
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R_1 : Type u
S_1 : Type u₁
inst : Semiring R_1
inst_1 : Semiring S_1
φ_1 : R_1 →+* S_1
A_1 : Type u_1
B_1 : Type u_2
inst_2 : NonUnitalNonAssocSemiring A_1
inst_3 : Module R_1 A_1
inst_4 : NonUnitalNonAssocSemiring B_1
inst_5 : Module S_1 B_1
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
x : Semiring R
x_1 : Semiring S
φ : R →+* S
x_2 : NonUnitalSemiring A
x_3 : NonUnitalSemiring B
inst_6 : Module R A
inst_7 : Module S B
inst_8 : FunLike F A B
inst_9 : NonUnitalAlgSemiHomClass F (↑φ : R →* S) A B
⊢ SemilinearMapClass F φ A B

Tactic:
{ ‹NonUnitalAlgSemiHomClass F φ A B› with map_smulₛₗ := map_smulₛₗ }

Premises used: SemilinearMapClass.mk
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
inst : Semiring R
inst_1 : Semiring S
φ : R →+* S
A : Type u_1
B : Type u_2
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module S B
F : Type u_3
inst_6 : FunLike F A B
inst_7 : Module R B
inst_8 : NonUnitalAlgHomClass F R A B
⊢ LinearMapClass F R A B

Tactic:
{ ‹NonUnitalAlgHomClass F R A B› with map_smulₛₗ := map_smulₛₗ }

Premises used: SemilinearMapClass.mk
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
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 : A →ₛₙₐ[φ] B
⊢ f.toFun = (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
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 : Type u_2
inst_6 : FunLike F A B
inst_7 : NonUnitalAlgSemiHomClass F φ A B
f : F
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →ₛₙₐ[φ] B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
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 : A → B
map_smul' : ∀ (m : R) (x : A), f (m • x) = HSMul.hSMul.{u₁, w, w} (α := S) ((φ : (a : R) → S) m : S) (f x)
map_zero' :
  { toFun := f, map_smul' := map_smul' : MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun 0 =
    0
map_add' :
  ∀ (x y : A),
    { toFun := f, map_smul' := map_smul' : MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
        (x + y) =
      { toFun := f, map_smul' := map_smul' : MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
          x +
        { toFun := f, map_smul' := map_smul' :
              MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
          y
map_mul' :
  ∀ (x y : A),
    { toFun := f, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add' : A →ₑ+[φ] B }.toFun (x * y) =
      { toFun := f, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add' : A →ₑ+[φ] B }.toFun x *
        { toFun := f, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add' : A →ₑ+[φ] B }.toFun y
g : A → B
map_smul'_1 : ∀ (m : R) (x : A), g (m • x) = HSMul.hSMul.{u₁, w, w} (α := S) ((φ : (a : R) → S) m : S) (g x)
map_zero'_1 :
  { toFun := g, map_smul' := map_smul'_1 : MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
      0 =
    0
map_add'_1 :
  ∀ (x y : A),
    { toFun := g, map_smul' := map_smul'_1 : MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
        (x + y) =
      { toFun := g, map_smul' := map_smul'_1 :
              MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
          x +
        { toFun := g, map_smul' := map_smul'_1 :
              MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
          y
map_mul'_1 :
  ∀ (x y : A),
    { toFun := g, map_smul' := map_smul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1 : A →ₑ+[φ] B }.toFun
        (x * y) =
      { toFun := g, map_smul' := map_smul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1 : A →ₑ+[φ] B }.toFun x *
        { toFun := g, map_smul' := map_smul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1 : A →ₑ+[φ] B }.toFun y
h :
  Eq (α := A → B)
    (⇑{ toFun := f, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add', map_mul' := map_mul' :
          A →ₛₙₐ[φ] B } :
      (a : A) → B)
    (⇑{ toFun := g, map_smul' := map_smul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1, map_mul' := map_mul'_1 :
          A →ₛₙₐ[φ] B } :
      (a : A) → B)
⊢ { toFun := f, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add', map_mul' := map_mul' :
      A →ₛₙₐ[φ] B } =
    { toFun := g, map_smul' := map_smul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1, map_mul' := map_mul'_1 }

Tactic:
congr