awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g
⊢ f = g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁)
have mpr : ∀ (x : M₂),
  Eq.{u_10 + 1} (α := M₃) ((f : (a : M₂) → M₃) x : M₃) ((g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) : (a : M₂) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
⊢ g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) = f ↔ g = f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)
have mp : g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) = f → g = f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
mp : g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) = f → g = f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)
⊢ g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) = f ↔ g = f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)
have mpr : g = f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) → g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) = f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) = f
⊢ g = f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)
have mp : ∀ (x : M₁),
  Eq.{u_10 + 1} (α := M₃) ((g : (a : M₁) → M₃) x : M₃) ((f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : g = f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)
⊢ g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) = f
have mpr : ∀ (x : M₂),
  Eq.{u_10 + 1} (α := M₃) ((g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) : (a : M₂) → M₃) x : M₃) ((f : (a : M₂) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
⊢ f = (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g ↔ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = g
have mp : f = (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g → (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
mp : f = (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g → (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = g
⊢ f = (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g ↔ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = g
have mpr : (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = g → f = (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
H : f = (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g
⊢ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = g
have mp : ∀ (x : M₃), Eq.{u_9 + 1} (α := M₂) (((↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f : (a : M₃) → M₂) x : M₂) ((g : (a : M₃) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
H : (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = g
⊢ f = (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g
have mpr : ∀ (x : M₃),
  Eq.{u_8 + 1} (α := M₁) ((f : (a : M₃) → M₁) x : M₁) (((↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g : (a : M₃) → M₁) x : M₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
⊢ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g = f ↔ g = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f
have mp : (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g = f → g = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
mp : (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g = f → g = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f
⊢ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g = f ↔ g = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f
have mpr : g = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f → (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g = f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
H : (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g = f
⊢ g = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f
have mp : ∀ (x : M₃), Eq.{u_9 + 1} (α := M₂) ((g : (a : M₃) → M₂) x : M₂) (((↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f : (a : M₃) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
H : g = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f
⊢ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g = f
have mpr : ∀ (x : M₃),
  Eq.{u_8 + 1} (α := M₁) (((↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g : (a : M₃) → M₁) x : M₁) ((f : (a : M₃) → M₁) x : M₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f g : M₃ →ₛₗ[σ₃₁] M₁
⊢ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ g ↔ f = g
have refine : ∀ (h : (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ g), f = g
Tactic: refine ⟨fun h => ?_, congrArg e₁₂.comp⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f g : M₃ →ₛₗ[σ₃₁] M₁
h : (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ g
⊢ f = g
have rw : f = (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f
Tactic: rw [← (toLinearMap_symm_comp_eq g (e₁₂.toLinearMap.comp f)).mpr h, eq_toLinearMap_symm_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f g : M₃ →ₛₗ[σ₃₁] M₁
h : (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ g
rw : f = (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f
⊢ f = g
have rw₁ : (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f
Tactic: rw [← (toLinearMap_symm_comp_eq g (e₁₂.toLinearMap.comp f)).mpr h, eq_toLinearMap_symm_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f g : M₂ →ₛₗ[σ₂₃] M₃
⊢ f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ↔ f = g
have refine : ∀ (h : f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)), f = g
Tactic: refine ⟨fun h => ?_, fun a ↦ congrFun (congrArg LinearMap.comp a) e₁₂.toLinearMap⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f g : M₂ →ₛₗ[σ₂₃] M₃
h : f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)
⊢ f = g
have rw : f = (f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)) ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁)
Tactic: rw [(eq_comp_toLinearMap_symm g (f.comp e₁₂.toLinearMap)).mpr h.symm, eq_comp_toLinearMap_symm]
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f g : M₂ →ₛₗ[σ₂₃] M₃
h : f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)
rw : f = (f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)) ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁)
⊢ f = g
have rw₁ : f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)
Tactic: rw [(eq_comp_toLinearMap_symm g (f.comp e₁₂.toLinearMap)).mpr h.symm, eq_comp_toLinearMap_symm]
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₂] M₂
⊢ (↑e : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ (↑e.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ f = f
have h : ∀ (x : M₃),
  Eq.{u_9 + 1} (α := M₂) (((↑e : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ (↑e.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ f : (a : M₃) → M₂) x : M₂)
    ((f : (a : M₃) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₁] M₁
⊢ (↑e.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ (↑e : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = f
have h : ∀ (x : M₃),
  Eq.{u_8 + 1} (α := M₁) (((↑e.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ (↑e : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f : (a : M₃) → M₁) x : M₁)
    ((f : (a : M₃) → M₁) x : M₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₂ →ₛₗ[σ₂₃] M₃
⊢ (f ∘ₛₗ (↑e : M₁ →ₛₗ[σ₁₂] M₂)) ∘ₛₗ (↑e.symm : M₂ →ₛₗ[σ₂₁] M₁) = f
have h : ∀ (x : M₂),
  Eq.{u_10 + 1} (α := M₃) (((f ∘ₛₗ (↑e : M₁ →ₛₗ[σ₁₂] M₂)) ∘ₛₗ (↑e.symm : M₂ →ₛₗ[σ₂₁] M₁) : (a : M₂) → M₃) x : M₃)
    ((f : (a : M₂) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₁ →ₛₗ[σ₁₃] M₃
⊢ (f ∘ₛₗ (↑e.symm : M₂ →ₛₗ[σ₂₁] M₁)) ∘ₛₗ (↑e : M₁ →ₛₗ[σ₁₂] M₂) = f
have h : ∀ (x : M₁),
  Eq.{u_10 + 1} (α := M₃) (((f ∘ₛₗ (↑e.symm : M₂ →ₛₗ[σ₂₁] M₁)) ∘ₛₗ (↑e : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₃) x : M₃)
    ((f : (a : M₁) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_6 : RingHomInvPair σ₁₃ σ₃₁
inst_7 : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_10 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst_11 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₁ ≃ₛₗ[σ₁₃] M₃
⊢ e.trans (re₂₃ := re₂₃) (re₃₂ := re₃₂) (e.symm.trans f) = f
have h : ∀ (x : M₁),
  Eq.{u_10 + 1} (α := M₃) ((e.trans (re₂₃ := re₂₃) (re₃₂ := re₃₂) (e.symm.trans f) : (a : M₁) → M₃) x : M₃)
    ((f : (a : M₁) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_6 : RingHomInvPair σ₁₃ σ₃₁
inst_7 : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_10 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst_11 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₂ ≃ₛₗ[σ₂₃] M₃
⊢ e.symm.trans (re₂₃ := inst_6) (re₃₂ := inst_7) (e.trans f) = f
have h : ∀ (x : M₂),
  Eq.{u_10 + 1} (α := M₃) ((e.symm.trans (re₂₃ := inst_6) (re₃₂ := inst_7) (e.trans f) : (a : M₂) → M₃) x : M₃)
    ((f : (a : M₂) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_6 : RingHomInvPair σ₁₃ σ₃₁
inst_7 : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_10 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst_11 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ ≃ₛₗ[σ₃₁] M₁
⊢ trans (re₁₂ := re₃₂) (re₂₁ := re₂₃) (f.trans e) e.symm = f
have h : ∀ (x : M₃),
  Eq.{u_8 + 1} (α := M₁) ((trans (re₁₂ := re₃₂) (re₂₁ := re₂₃) (f.trans e) e.symm : (a : M₃) → M₁) x : M₁)
    ((f : (a : M₃) → M₁) x : M₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_6 : RingHomInvPair σ₁₃ σ₃₁
inst_7 : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_10 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst_11 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ ≃ₛₗ[σ₃₂] M₂
⊢ trans (re₁₂ := inst_7) (re₂₁ := inst_6) (f.trans e.symm) e = f
have h : ∀ (x : M₃),
  Eq.{u_9 + 1} (α := M₂) ((trans (re₁₂ := inst_7) (re₂₁ := inst_6) (f.trans e.symm) e : (a : M₃) → M₂) x : M₂)
    ((f : (a : M₃) → M₂) x : M₂)
Tactic: ext