awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Central.Basic (goal)
Goal:
k : Type u_1
K : Type u_2
D : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Ring D
inst_3 : Nontrivial D
inst_4 : Algebra k K
inst_5 : Algebra K D
inst_6 : Algebra k D
inst_7 : IsScalarTower k K D
inst_8 : IsCentral k D
this : IsCentral K D
x : K
H : ∃ (y : k), Eq.{u_3 + 1} (α := D) ((algebraMap k D : (a : k) → D) y : D) ((algebraMap K D : (a : K) → D) x : D)
⊢ ∃ (a : k), (algebraMap k K : (a : k) → K) a = x
have obtain : ∀ (x' : k) (H : Eq.{u_3 + 1} (α := D) ((algebraMap k D : (a : k) → D) x' : D) ((algebraMap K D : (a : K) → D) x : D)),
  ∃ (a : k), (algebraMap k K : (a : k) → K) a = x
Tactic: obtain ⟨x', H⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.Central.End (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : CommSemiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
inst_7 : Algebra S R
inst_8 : IsScalarTower S R M
M₂ : Type u_4
inst_9 : AddCommMonoid M₂
inst_10 : Module R M₂
inst_11 : Module S M₂
inst_12 : SMulCommClass R S M₂
inst_13 : IsScalarTower S R M₂
inst_14 : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
| Eq (α := AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) (conjAlgEquiv S f) (conjAlgEquiv S g)
have rw : Eq (α := AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) (conjAlgEquiv S g) (conjAlgEquiv S f)
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Central.End (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : CommSemiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
inst_7 : Algebra S R
inst_8 : IsScalarTower S R M
M₂ : Type u_4
inst_9 : AddCommMonoid M₂
inst_10 : Module R M₂
inst_11 : Module S M₂
inst_12 : SMulCommClass R S M₂
inst_13 : IsScalarTower S R M₂
inst_14 : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ Eq (α := AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) (conjAlgEquiv S f) (conjAlgEquiv S g) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
have conv_lhs : Eq (α := AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) (conjAlgEquiv S g) (conjAlgEquiv S f) ↔
  ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
Tactic: conv_lhs => rw [eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Central.End (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : CommSemiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
inst_7 : Algebra S R
inst_8 : IsScalarTower S R M
M₂ : Type u_4
inst_9 : AddCommMonoid M₂
inst_10 : Module R M₂
inst_11 : Module S M₂
inst_12 : SMulCommClass R S M₂
inst_13 : IsScalarTower S R M₂
inst_14 : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ Eq (α := AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) (conjAlgEquiv S g) (conjAlgEquiv S f) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
have simp_rw : (∀ (a : End R M),
    Eq.{u_4 + 1} (α := End R M₂)
      (((conjAlgEquiv S g : AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) : (a : End R M) → End R M₂) a : End R M₂)
      (((conjAlgEquiv S f : AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) : (a : End R M) → End R M₂) a :
        End R M₂)) ↔
  ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
Tactic: simp_rw [AlgEquiv.ext_iff, conjAlgEquiv_apply, ← eq_toLinearMap_symm_comp, ← comp_assoc,
    eq_comp_toLinearMap_symm, comp_assoc, ← comp_assoc _ _ g.symm.toLinearMap, comp_coe,
    ← End.mul_eq_comp, ← Subalgebra.mem_center_iff (R := S), Algebra.IsCentral.center_eq_bot,
    ← comp_coe, Algebra.mem_bot, Set.mem_range, Algebra.algebraMap_eq_smul_one,
    eq_toLinearMap_symm_comp, eq_comm, LinearMap.ext_iff, funext_iff, comp_apply, coe_coe,
    LinearMap.smul_apply, End.one_apply, Pi.smul_apply, LinearMapClass.map_smul_of_tower g]
-- Lean 4 proof step from Mathlib.Algebra.Central.End (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : CommSemiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
inst_7 : Algebra S R
inst_8 : IsScalarTower S R M
M₂ : Type u_4
inst_9 : AddCommMonoid M₂
inst_10 : Module R M₂
inst_11 : Module S M₂
inst_12 : SMulCommClass R S M₂
inst_13 : IsScalarTower S R M₂
inst_14 : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
simp_rw :
  (∀ (a : End R M),
      Eq.{u_4 + 1} (α := End R M₂)
        (((conjAlgEquiv S g : AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) : (a : End R M) → End R M₂) a : End R M₂)
        (((conjAlgEquiv S f : AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) : (a : End R M) → End R M₂) a :
          End R M₂)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
⊢ Eq (α := AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) (conjAlgEquiv S g) (conjAlgEquiv S f) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
have simp_rw₁ : (∀ (a : End R M), (↑g : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) = (↑f : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑f.symm : M₂ →ₗ[R] M)) ↔
  ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
Tactic: simp_rw [AlgEquiv.ext_iff, conjAlgEquiv_apply, ← eq_toLinearMap_symm_comp, ← comp_assoc,
    eq_comp_toLinearMap_symm, comp_assoc, ← comp_assoc _ _ g.symm.toLinearMap, comp_coe,
    ← End.mul_eq_comp, ← Subalgebra.mem_center_iff (R := S), Algebra.IsCentral.center_eq_bot,
    ← comp_coe, Algebra.mem_bot, Set.mem_range, Algebra.algebraMap_eq_smul_one,
    eq_toLinearMap_symm_comp, eq_comm, LinearMap.ext_iff, funext_iff, comp_apply, coe_coe,
    LinearMap.smul_apply, End.one_apply, Pi.smul_apply, LinearMapClass.map_smul_of_tower g]
-- Lean 4 proof step from Mathlib.Algebra.Central.End (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : CommSemiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
inst_7 : Algebra S R
inst_8 : IsScalarTower S R M
M₂ : Type u_4
inst_9 : AddCommMonoid M₂
inst_10 : Module R M₂
inst_11 : Module S M₂
inst_12 : SMulCommClass R S M₂
inst_13 : IsScalarTower S R M₂
inst_14 : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
simp_rw :
  (∀ (a : End R M),
      Eq.{u_4 + 1} (α := End R M₂)
        (((conjAlgEquiv S g : AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) : (a : End R M) → End R M₂) a : End R M₂)
        (((conjAlgEquiv S f : AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) : (a : End R M) → End R M₂) a :
          End R M₂)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₁ :
  (∀ (a : End R M),
      (↑g : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) = (↑f : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑f.symm : M₂ →ₗ[R] M)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
⊢ Eq (α := AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) (conjAlgEquiv S g) (conjAlgEquiv S f) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
have simp_rw₂ : (∀ (a : End R M),
    a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) = (↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑f.symm : M₂ →ₗ[R] M)) ↔
  ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
Tactic: simp_rw [AlgEquiv.ext_iff, conjAlgEquiv_apply, ← eq_toLinearMap_symm_comp, ← comp_assoc,
    eq_comp_toLinearMap_symm, comp_assoc, ← comp_assoc _ _ g.symm.toLinearMap, comp_coe,
    ← End.mul_eq_comp, ← Subalgebra.mem_center_iff (R := S), Algebra.IsCentral.center_eq_bot,
    ← comp_coe, Algebra.mem_bot, Set.mem_range, Algebra.algebraMap_eq_smul_one,
    eq_toLinearMap_symm_comp, eq_comm, LinearMap.ext_iff, funext_iff, comp_apply, coe_coe,
    LinearMap.smul_apply, End.one_apply, Pi.smul_apply, LinearMapClass.map_smul_of_tower g]
-- Lean 4 proof step from Mathlib.Algebra.Central.End (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : CommSemiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
inst_7 : Algebra S R
inst_8 : IsScalarTower S R M
M₂ : Type u_4
inst_9 : AddCommMonoid M₂
inst_10 : Module R M₂
inst_11 : Module S M₂
inst_12 : SMulCommClass R S M₂
inst_13 : IsScalarTower S R M₂
inst_14 : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
simp_rw :
  (∀ (a : End R M),
      Eq.{u_4 + 1} (α := End R M₂)
        (((conjAlgEquiv S g : AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) : (a : End R M) → End R M₂) a : End R M₂)
        (((conjAlgEquiv S f : AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) : (a : End R M) → End R M₂) a :
          End R M₂)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₁ :
  (∀ (a : End R M),
      (↑g : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) = (↑f : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑f.symm : M₂ →ₗ[R] M)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₂ :
  (∀ (a : End R M),
      a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) = (↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑f.symm : M₂ →ₗ[R] M)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
⊢ Eq (α := AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) (conjAlgEquiv S g) (conjAlgEquiv S f) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
have simp_rw₃ : (∀ (a : End R M),
    a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) = (((↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂)) ∘ₗ a) ∘ₗ (↑f.symm : M₂ →ₗ[R] M)) ↔
  ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
Tactic: simp_rw [AlgEquiv.ext_iff, conjAlgEquiv_apply, ← eq_toLinearMap_symm_comp, ← comp_assoc,
    eq_comp_toLinearMap_symm, comp_assoc, ← comp_assoc _ _ g.symm.toLinearMap, comp_coe,
    ← End.mul_eq_comp, ← Subalgebra.mem_center_iff (R := S), Algebra.IsCentral.center_eq_bot,
    ← comp_coe, Algebra.mem_bot, Set.mem_range, Algebra.algebraMap_eq_smul_one,
    eq_toLinearMap_symm_comp, eq_comm, LinearMap.ext_iff, funext_iff, comp_apply, coe_coe,
    LinearMap.smul_apply, End.one_apply, Pi.smul_apply, LinearMapClass.map_smul_of_tower g]
-- Lean 4 proof step from Mathlib.Algebra.Central.End (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : CommSemiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
inst_7 : Algebra S R
inst_8 : IsScalarTower S R M
M₂ : Type u_4
inst_9 : AddCommMonoid M₂
inst_10 : Module R M₂
inst_11 : Module S M₂
inst_12 : SMulCommClass R S M₂
inst_13 : IsScalarTower S R M₂
inst_14 : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
simp_rw :
  (∀ (a : End R M),
      Eq.{u_4 + 1} (α := End R M₂)
        (((conjAlgEquiv S g : AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) : (a : End R M) → End R M₂) a : End R M₂)
        (((conjAlgEquiv S f : AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) : (a : End R M) → End R M₂) a :
          End R M₂)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₁ :
  (∀ (a : End R M),
      (↑g : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) = (↑f : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑f.symm : M₂ →ₗ[R] M)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₂ :
  (∀ (a : End R M),
      a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) = (↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑f.symm : M₂ →ₗ[R] M)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₃ :
  (∀ (a : End R M),
      a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) = (((↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂)) ∘ₗ a) ∘ₗ (↑f.symm : M₂ →ₗ[R] M)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
⊢ Eq (α := AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) (conjAlgEquiv S g) (conjAlgEquiv S f) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
have simp_rw₄ : (∀ (a : End R M),
    (a ∘ₗ (↑g.symm : M₂ →ₗ[R] M)) ∘ₗ (↑f : M →ₗ[R] M₂) = ((↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂)) ∘ₗ a) ↔
  ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
Tactic: simp_rw [AlgEquiv.ext_iff, conjAlgEquiv_apply, ← eq_toLinearMap_symm_comp, ← comp_assoc,
    eq_comp_toLinearMap_symm, comp_assoc, ← comp_assoc _ _ g.symm.toLinearMap, comp_coe,
    ← End.mul_eq_comp, ← Subalgebra.mem_center_iff (R := S), Algebra.IsCentral.center_eq_bot,
    ← comp_coe, Algebra.mem_bot, Set.mem_range, Algebra.algebraMap_eq_smul_one,
    eq_toLinearMap_symm_comp, eq_comm, LinearMap.ext_iff, funext_iff, comp_apply, coe_coe,
    LinearMap.smul_apply, End.one_apply, Pi.smul_apply, LinearMapClass.map_smul_of_tower g]
-- Lean 4 proof step from Mathlib.Algebra.Central.End (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : CommSemiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
inst_7 : Algebra S R
inst_8 : IsScalarTower S R M
M₂ : Type u_4
inst_9 : AddCommMonoid M₂
inst_10 : Module R M₂
inst_11 : Module S M₂
inst_12 : SMulCommClass R S M₂
inst_13 : IsScalarTower S R M₂
inst_14 : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
simp_rw :
  (∀ (a : End R M),
      Eq.{u_4 + 1} (α := End R M₂)
        (((conjAlgEquiv S g : AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) : (a : End R M) → End R M₂) a : End R M₂)
        (((conjAlgEquiv S f : AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) : (a : End R M) → End R M₂) a :
          End R M₂)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₁ :
  (∀ (a : End R M),
      (↑g : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) = (↑f : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑f.symm : M₂ →ₗ[R] M)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₂ :
  (∀ (a : End R M),
      a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) = (↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑f.symm : M₂ →ₗ[R] M)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₃ :
  (∀ (a : End R M),
      a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) = (((↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂)) ∘ₗ a) ∘ₗ (↑f.symm : M₂ →ₗ[R] M)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₄ :
  (∀ (a : End R M),
      (a ∘ₗ (↑g.symm : M₂ →ₗ[R] M)) ∘ₗ (↑f : M →ₗ[R] M₂) = ((↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂)) ∘ₗ a) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
⊢ Eq (α := AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) (conjAlgEquiv S g) (conjAlgEquiv S f) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
have simp_rw₅ : (∀ (a : End R M), a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂) = (↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂) ∘ₗ a) ↔
  ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
Tactic: simp_rw [AlgEquiv.ext_iff, conjAlgEquiv_apply, ← eq_toLinearMap_symm_comp, ← comp_assoc,
    eq_comp_toLinearMap_symm, comp_assoc, ← comp_assoc _ _ g.symm.toLinearMap, comp_coe,
    ← End.mul_eq_comp, ← Subalgebra.mem_center_iff (R := S), Algebra.IsCentral.center_eq_bot,
    ← comp_coe, Algebra.mem_bot, Set.mem_range, Algebra.algebraMap_eq_smul_one,
    eq_toLinearMap_symm_comp, eq_comm, LinearMap.ext_iff, funext_iff, comp_apply, coe_coe,
    LinearMap.smul_apply, End.one_apply, Pi.smul_apply, LinearMapClass.map_smul_of_tower g]
-- Lean 4 proof step from Mathlib.Algebra.Central.End (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : CommSemiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
inst_7 : Algebra S R
inst_8 : IsScalarTower S R M
M₂ : Type u_4
inst_9 : AddCommMonoid M₂
inst_10 : Module R M₂
inst_11 : Module S M₂
inst_12 : SMulCommClass R S M₂
inst_13 : IsScalarTower S R M₂
inst_14 : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
simp_rw :
  (∀ (a : End R M),
      Eq.{u_4 + 1} (α := End R M₂)
        (((conjAlgEquiv S g : AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) : (a : End R M) → End R M₂) a : End R M₂)
        (((conjAlgEquiv S f : AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) : (a : End R M) → End R M₂) a :
          End R M₂)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₁ :
  (∀ (a : End R M),
      (↑g : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) = (↑f : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑f.symm : M₂ →ₗ[R] M)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₂ :
  (∀ (a : End R M),
      a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) = (↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑f.symm : M₂ →ₗ[R] M)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₃ :
  (∀ (a : End R M),
      a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) = (((↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂)) ∘ₗ a) ∘ₗ (↑f.symm : M₂ →ₗ[R] M)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₄ :
  (∀ (a : End R M),
      (a ∘ₗ (↑g.symm : M₂ →ₗ[R] M)) ∘ₗ (↑f : M →ₗ[R] M₂) = ((↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂)) ∘ₗ a) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₅ :
  (∀ (a : End R M),
      a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂) = (↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂) ∘ₗ a) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
⊢ Eq (α := AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) (conjAlgEquiv S g) (conjAlgEquiv S f) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
have simp_rw₆ : (∀ (a : End R M),
    a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂) = ((↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂)) ∘ₗ a) ↔
  ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
Tactic: simp_rw [AlgEquiv.ext_iff, conjAlgEquiv_apply, ← eq_toLinearMap_symm_comp, ← comp_assoc,
    eq_comp_toLinearMap_symm, comp_assoc, ← comp_assoc _ _ g.symm.toLinearMap, comp_coe,
    ← End.mul_eq_comp, ← Subalgebra.mem_center_iff (R := S), Algebra.IsCentral.center_eq_bot,
    ← comp_coe, Algebra.mem_bot, Set.mem_range, Algebra.algebraMap_eq_smul_one,
    eq_toLinearMap_symm_comp, eq_comm, LinearMap.ext_iff, funext_iff, comp_apply, coe_coe,
    LinearMap.smul_apply, End.one_apply, Pi.smul_apply, LinearMapClass.map_smul_of_tower g]
-- Lean 4 proof step from Mathlib.Algebra.Central.End (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
S : Type u_4
M₂ : Type u_5
inst_4 : CommRing S
inst_5 : IsCancelMulZero S
inst_6 : Module S M
inst_7 : SMulCommClass R S M
inst_8 : Algebra S R
inst_9 : IsScalarTower S R M
inst_10 : AddCommGroup M₂
inst_11 : Module R M₂
inst_12 : Module S M₂
inst_13 : SMulCommClass R S M₂
inst_14 : IsScalarTower S R M₂
inst_15 : Algebra.IsCentral S R
inst_16 : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
⊢ Eq (α := AlgEquiv.{u_4, u_3, u_5} S (End R M) (End R M₂)) (conjAlgEquiv S f) (conjAlgEquiv S g) ↔
    ∃ (α : Sˣ), f = α • g
have refine : ∀ (h : Eq (α := AlgEquiv.{u_4, u_3, u_5} S (End R M) (End R M₂)) (conjAlgEquiv S f) (conjAlgEquiv S g)),
  ∃ (α : Sˣ), f = α • g
Tactic: refine ⟨fun h ↦ ?_, fun ⟨y, h⟩ ↦ conjAlgEquiv_ext_iff.mpr ⟨(y : S), congr($h)⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Central.End (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
S : Type u_4
M₂ : Type u_5
inst_4 : CommRing S
inst_5 : IsCancelMulZero S
inst_6 : Module S M
inst_7 : SMulCommClass R S M
inst_8 : Algebra S R
inst_9 : IsScalarTower S R M
inst_10 : AddCommGroup M₂
inst_11 : Module R M₂
inst_12 : Module S M₂
inst_13 : SMulCommClass R S M₂
inst_14 : IsScalarTower S R M₂
inst_15 : Algebra.IsCentral S R
inst_16 : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : Eq (α := AlgEquiv.{u_4, u_3, u_5} S (End R M) (End R M₂)) (conjAlgEquiv S f) (conjAlgEquiv S g)
⊢ ∃ (α : Sˣ), f = α • g
have pos : Subsingleton M → ∃ (α : Sˣ), f = α • g
Tactic: by_cases! Subsingleton M
-- Lean 4 proof step from Mathlib.Algebra.Central.End (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
S : Type u_4
M₂ : Type u_5
inst_4 : CommRing S
inst_5 : IsCancelMulZero S
inst_6 : Module S M
inst_7 : SMulCommClass R S M
inst_8 : Algebra S R
inst_9 : IsScalarTower S R M
inst_10 : AddCommGroup M₂
inst_11 : Module R M₂
inst_12 : Module S M₂
inst_13 : SMulCommClass R S M₂
inst_14 : IsScalarTower S R M₂
inst_15 : Algebra.IsCentral S R
inst_16 : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : Eq (α := AlgEquiv.{u_4, u_3, u_5} S (End R M) (End R M₂)) (conjAlgEquiv S f) (conjAlgEquiv S g)
pos : Subsingleton M → ∃ (α : Sˣ), f = α • g
⊢ ∃ (α : Sˣ), f = α • g
have neg : Nontrivial M → ∃ (α : Sˣ), f = α • g
Tactic: by_cases! Subsingleton M
-- Lean 4 proof step from Mathlib.Algebra.Central.End (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
S : Type u_4
M₂ : Type u_5
inst_4 : CommRing S
inst_5 : IsCancelMulZero S
inst_6 : Module S M
inst_7 : SMulCommClass R S M
inst_8 : Algebra S R
inst_9 : IsScalarTower S R M
inst_10 : AddCommGroup M₂
inst_11 : Module R M₂
inst_12 : Module S M₂
inst_13 : SMulCommClass R S M₂
inst_14 : IsScalarTower S R M₂
inst_15 : Algebra.IsCentral S R
inst_16 : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : Eq (α := AlgEquiv.{u_4, u_3, u_5} S (End R M) (End R M₂)) (conjAlgEquiv S f) (conjAlgEquiv S g)
h_1 : Subsingleton M
⊢ f = HSMul.hSMul (α := Sˣ) 1 g
have h₁ : ∀ (x : M), Eq.{u_5 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((HSMul.hSMul (α := Sˣ) 1 g : (a : M) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Central.End (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
S : Type u_4
M₂ : Type u_5
inst_4 : CommRing S
inst_5 : IsCancelMulZero S
inst_6 : Module S M
inst_7 : SMulCommClass R S M
inst_8 : Algebra S R
inst_9 : IsScalarTower S R M
inst_10 : AddCommGroup M₂
inst_11 : Module R M₂
inst_12 : Module S M₂
inst_13 : SMulCommClass R S M₂
inst_14 : IsScalarTower S R M₂
inst_15 : Algebra.IsCentral S R
inst_16 : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : Eq (α := AlgEquiv.{u_4, u_3, u_5} S (End R M) (End R M₂)) (conjAlgEquiv S f) (conjAlgEquiv S g)
h_1 : Nontrivial M
⊢ ∃ (α : Sˣ), f = α • g
have neg : ∀ (α : S) (hα : (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)), ∃ (α : Sˣ), f = α • g
Tactic: obtain ⟨α, hα⟩ := conjAlgEquiv_ext_iff.mp h
-- Lean 4 proof step from Mathlib.Algebra.Central.End (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
S : Type u_4
M₂ : Type u_5
inst_4 : CommRing S
inst_5 : IsCancelMulZero S
inst_6 : Module S M
inst_7 : SMulCommClass R S M
inst_8 : Algebra S R
inst_9 : IsScalarTower S R M
inst_10 : AddCommGroup M₂
inst_11 : Module R M₂
inst_12 : Module S M₂
inst_13 : SMulCommClass R S M₂
inst_14 : IsScalarTower S R M₂
inst_15 : Algebra.IsCentral S R
inst_16 : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : Eq (α := AlgEquiv.{u_4, u_3, u_5} S (End R M) (End R M₂)) (conjAlgEquiv S f) (conjAlgEquiv S g)
h_1 : Nontrivial M
α : S
hα : (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
⊢ ∃ (α : Sˣ), f = α • g
have neg : ∀ (β : S) (hβ : (⇑g : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) β (⇑f : (a : M) → M₂)), ∃ (α : Sˣ), f = α • g
Tactic: obtain ⟨β, hβ⟩ := conjAlgEquiv_ext_iff.mp h.symm