-- Mathlib/Algebra/Algebra/Defs.lean
theorem algebra_ext {R : Type*} [CommSemiring R] {A : Type*} [Semiring A] (P Q : Algebra R A)
    (h : ∀ r : R, (haveI := P; algebraMap R A r) = haveI := Q; algebraMap R A r) :
    P = Q

Proof state:
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : ∀ (r : R), (algebraMap R A) r = (algebraMap R A) r
⊢ P = Q

Tactic:
replace h : P.algebraMap = Q.algebraMap := DFunLike.ext _ _ h

Result:
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : Algebra.algebraMap = Algebra.algebraMap
⊢ P = Q

Proof state:
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : Algebra.algebraMap = Algebra.algebraMap
h' : (fun x1 x2 => x1 • x2) = fun x1 x2 => x1 • x2
⊢ P = Q

Tactic:
rcases P with @⟨⟨P⟩⟩

Result:
case mk.mk
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
Q : Algebra R A
algebraMap✝ : R →+* A
commutes'✝ : ∀ (r : R) (x : A), algebraMap✝ r * x = x * algebraMap✝ r
P : R → A → A
smul_def'✝ : ∀ (r : R) (x : A), r • x = algebraMap✝ r * x
h : Algebra.algebraMap = Algebra.algebraMap
h' : (fun x1 x2 => x1 • x2) = fun x1 x2 => x1 • x2
⊢ mk algebraMap✝ commutes'✝ smul_def'✝ = Q

Proof state:
case h.h
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : Algebra.algebraMap = Algebra.algebraMap
r : R
a : A
⊢ r • a = r • a

Tactic:
rw [P.smul_def', Q.smul_def', h]

Result:
no goals

Proof state:
case mk.mk
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
Q : Algebra R A
algebraMap✝ : R →+* A
commutes'✝ : ∀ (r : R) (x : A), algebraMap✝ r * x = x * algebraMap✝ r
P : R → A → A
smul_def'✝ : ∀ (r : R) (x : A), r • x = algebraMap✝ r * x
h : Algebra.algebraMap = Algebra.algebraMap
h' : (fun x1 x2 => x1 • x2) = fun x1 x2 => x1 • x2
⊢ mk algebraMap✝ commutes'✝ smul_def'✝ = Q

Tactic:
rcases Q with @⟨⟨Q⟩⟩

Result:
case mk.mk.mk.mk
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
algebraMap✝¹ : R →+* A
commutes'✝¹ : ∀ (r : R) (x : A), algebraMap✝¹ r * x = x * algebraMap✝¹ r
P : R → A → A
smul_def'✝¹ : ∀ (r : R) (x : A), r • x = algebraMap✝¹ r * x
algebraMap✝ : R →+* A
commutes'✝ : ∀ (r : R) (x : A), algebraMap✝ r * x = x * algebraMap✝ r
Q : R → A → A
smul_def'✝ : ∀ (r : R) (x : A), r • x = algebraMap✝ r * x
h : Algebra.algebraMap = Algebra.algebraMap
h' : (fun x1 x2 => x1 • x2) = fun x1 x2 => x1 • x2
⊢ mk algebraMap✝¹ commutes'✝¹ smul_def'✝¹ = mk algebraMap✝ commutes'✝ smul_def'✝

Proof state:
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : Algebra.algebraMap = Algebra.algebraMap
⊢ (fun x1 x2 => x1 • x2) = fun x1 x2 => x1 • x2

Tactic:
funext r a

Result:
case h.h
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : Algebra.algebraMap = Algebra.algebraMap
r : R
a : A
⊢ r • a = r • a

Proof state:
case mk.mk.mk.mk
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
algebraMap✝¹ : R →+* A
commutes'✝¹ : ∀ (r : R) (x : A), algebraMap✝¹ r * x = x * algebraMap✝¹ r
P : R → A → A
smul_def'✝¹ : ∀ (r : R) (x : A), r • x = algebraMap✝¹ r * x
algebraMap✝ : R →+* A
commutes'✝ : ∀ (r : R) (x : A), algebraMap✝ r * x = x * algebraMap✝ r
Q : R → A → A
smul_def'✝ : ∀ (r : R) (x : A), r • x = algebraMap✝ r * x
h : Algebra.algebraMap = Algebra.algebraMap
h' : (fun x1 x2 => x1 • x2) = fun x1 x2 => x1 • x2
⊢ mk algebraMap✝¹ commutes'✝¹ smul_def'✝¹ = mk algebraMap✝ commutes'✝ smul_def'✝

Tactic:
congr

Result:
no goals