awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X_1 Y_1 : Type u
X Y : Semigrp
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj (forget Semigrp (FC := fun (x1 x2 : Semigrp.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget Semigrp (FC := fun (x1 x2 : Semigrp.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier)) f)
i : Functor.obj (forget Semigrp (FC := fun (x1 x2 : Semigrp.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier))
    X ≅
  Functor.obj (forget Semigrp (FC := fun (x1 x2 : Semigrp.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget Semigrp (FC := fun (x1 x2 : Semigrp.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := carrier)) f)
e : (↑X : Type u) ≃* (↑Y : Type u) :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toFun := __src.toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
exact e.toSemigrpIso.isIso_hom

Premises used: MulEquiv.toSemigrpIso, CategoryTheory.Iso.isIso_hom
-- Module: Mathlib.Algebra.Category.Semigrp.Basic
Goal:
X Y : Type u
⊢ Functor.ReflectsIsomorphisms
    (forget₂ Semigrp (FC := fun (x1 x2 : Semigrp.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CC := Semigrp.carrier)
      MagmaCat (FD := fun (x1 x2 : MagmaCat.{u_1}) ↦ (↑x1 : Type u_1) →ₙ* (↑x2 : Type u_1)) (CD := MagmaCat.carrier))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Central.Basic
Goal:
K : Type u
inst : CommSemiring K
D : Type v
inst_1 : Semiring D
inst_2 : Algebra K D
h : IsCentral K D
⊢ Eq (α := Subalgebra K D) (Subalgebra.center K D) ⊥

Tactic:
eq_bot_iff.2 IsCentral.out

Premises used: Iff.mpr, eq_bot_iff, Algebra.IsCentral.out
-- Module: Mathlib.Algebra.Central.Basic
Goal:
K : Type u
inst : CommSemiring K
D : Type v
inst_1 : Semiring D
inst_2 : Algebra K D
h : IsCentral K D
x : D
rw :
  Membership.mem (γ := Set D) (Set.range.{v, u + 1} (ι := K) (⇑(algebraMap K D) : (a : K) → D)) x ↔
    ∃ (a : K), x = (algebraMap K D : (a : K) → D) a
⊢ Membership.mem (γ := Subalgebra K D) (Subalgebra.center K D) x ↔ ∃ (a : K), x = (algebraMap K D : (a : K) → D) a

Tactic:
rw [center_eq_bot, Algebra.mem_bot]

Premises used: Algebra.mem_bot, Algebra.IsCentral.center_eq_bot
-- Module: Mathlib.Algebra.Central.Basic
Goal:
K : Type u
inst : CommSemiring K
D : Type v
inst_1 : Semiring D
inst_2 : Algebra K D
h : IsCentral K D
x : D
⊢ Membership.mem (γ := Set D) (Set.range.{v, u + 1} (ι := K) (⇑(algebraMap K D) : (a : K) → D)) x ↔
    ∃ (a : K), x = (algebraMap K D : (a : K) → D) a

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Algebra.Central.Basic
Goal:
K : Type u
inst : CommSemiring K
D D' : Type v
inst_1 : Semiring D
inst_2 : Algebra K D
h : IsCentral K D
inst_3 : Semiring D'
inst_4 : Algebra K D'
x : K
⊢ Membership.mem (γ := Subalgebra K K) (Subalgebra.center K K) x → Membership.mem (γ := Subalgebra K K) ⊥ x

Tactic:
simp [Algebra.mem_bot]

Premises used: Algebra.mem_bot
-- Module: Mathlib.Algebra.Central.Basic
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
x : D
simp : ∀ (x_1 : k) (h : (algebraMap k D : (a : k) → D) x_1 = x), ∃ (y : K), (algebraMap K D : (a : K) → D) y = x
⊢ Membership.mem (γ := Subalgebra k D) (Subalgebra.center k D) x → Membership.mem (γ := Subalgebra K D) ⊥ x

Tactic:
simp only [center_eq_bot, mem_bot, Set.mem_range, forall_exists_index]

Premises used: Set.mem_range, Algebra.mem_bot, forall_exists_index, Algebra.IsCentral.center_eq_bot
-- Module: Mathlib.Algebra.Central.Basic
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
x : k
⊢ Eq.{u_3 + 1} (α := D) ((algebraMap K D : (a : K) → D) ((algebraMap k K : (a : k) → K) x : K) : D)
    ((algebraMap k D : (a : k) → D) x : D)

Tactic:
simp [algebraMap_eq_smul_one, smul_assoc]

Premises used: smul_assoc, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Central.Basic
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
x : k
⊢ ∃ (y : K), Eq.{u_3 + 1} (α := D) ((algebraMap K D : (a : K) → D) y : D) ((algebraMap k D : (a : k) → D) x : D)

Tactic:
exact ⟨algebraMap k K x, by simp [algebraMap_eq_smul_one, smul_assoc]⟩
-- Module: Mathlib.Algebra.Central.Basic
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
⊢ IsCentral K D

Tactic:
haveI : IsCentral K D :=
  { out := fun x ↦ show x ∈ Subalgebra.center k D → _ by
      simp only [center_eq_bot, mem_bot, Set.mem_range, forall_exists_index]
      rintro x rfl
      exact ⟨algebraMap k K x, by simp [algebraMap_eq_smul_one, smul_assoc]⟩ }
-- Module: Mathlib.Algebra.Central.Basic
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
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := k) (β := K) (⇑(algebraMap k K) : (a : k) → K)

Tactic:
⟨FaithfulSMul.algebraMap_injective k K, fun x => ?_⟩

Premises used: FaithfulSMul.algebraMap_injective, And.intro, Function.Bijective
-- Module: Mathlib.Algebra.Central.Basic
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
refine : ∀ (x : K), ∃ (a : k), (algebraMap k K : (a : k) → K) a = x
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := k) (β := K) (⇑(algebraMap k K) : (a : k) → K)

Tactic:
refine ⟨FaithfulSMul.algebraMap_injective k K, fun x => ?_⟩
-- Module: Mathlib.Algebra.Central.Basic
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
⊢ Membership.mem (α := D) (↑(Subalgebra.center K D) : Set D) ((algebraMap K D : (a : K) → D) x : D)

Tactic:
have H : algebraMap K D x ∈ (Subalgebra.center K D : Set D) := Subalgebra.algebraMap_mem _ _
-- Module: Mathlib.Algebra.Central.Basic
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 : Membership.mem (α := D) (↑(Subalgebra.center K D) : Set D) ((algebraMap K D : (a : K) → D) x : D)
⊢ (↑(Subalgebra.center K D) : Set D) = (↑(Subalgebra.center k D) : Set D)

Tactic:
rfl
-- Module: Mathlib.Algebra.Central.Basic
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 : Membership.mem (α := D) (↑(Subalgebra.center K D) : Set D) ((algebraMap K D : (a : K) → D) x : D)
⊢ Membership.mem (α := D) (↑(Subalgebra.center k D) : Set D) ((algebraMap K D : (a : K) → D) x : D)

Tactic:
rw [show (Subalgebra.center K D : Set D) = Subalgebra.center k D by rfl] at H
-- Module: Mathlib.Algebra.Central.Basic
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 : Membership.mem (α := D) (↑(Subalgebra.center k D) : Set D) ((algebraMap K D : (a : K) → D) x : D)
⊢ ∃ (y : k), Eq.{u_3 + 1} (α := D) ((algebraMap k D : (a : k) → D) y : D) ((algebraMap K D : (a : K) → D) x : D)

Tactic:
simp only [center_eq_bot, coe_bot, Set.mem_range] at H

Premises used: Set.mem_range, Algebra.coe_bot, Algebra.IsCentral.center_eq_bot
-- Module: Mathlib.Algebra.Central.Basic
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)
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
⊢ ∃ (a : k), (algebraMap k K : (a : k) → K) a = x

Tactic:
obtain ⟨x', H⟩ := H
-- Module: Mathlib.Algebra.Central.Basic
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
x' : k
H : Eq.{u_3 + 1} (α := D) ((algebraMap k D : (a : k) → D) x' : D) ((algebraMap K D : (a : K) → D) x : D)
⊢ Eq.{u_3 + 1} (α := D) (((algebraMap K D : K →+* D) : (a : K) → D) ((algebraMap k K : (a : k) → K) x' : K) : D)
    (((algebraMap K D : K →+* D) : (a : K) → D) x : D)

Tactic:
simp [← H, algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Central.Basic
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
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:
exact ⟨x', (algebraMap K D).injective <| by simp [← H, algebraMap_eq_smul_one]⟩
-- Module: Mathlib.Algebra.Central.Basic
Goal:
K : Type u
inst : CommSemiring K
D D' : Type v
inst_1 : Semiring D
inst_2 : Algebra K D
h : IsCentral K D
inst_3 : Semiring D'
inst_4 : Algebra K D'
e : D ≃ₐ[K] D'
x : D'
hx : Membership.mem (γ := Subalgebra K D') (Subalgebra.center K D') x
k : K
hk : Eq.{v + 1} (α := D) ((AlgHom.toRingHom (ofId K D) : (a : K) → D) k : D) ((e.symm : (a : D') → D) x : D)
⊢ (AlgHom.toRingHom (ofId K D') : (a : K) → D') k = x

Tactic:
simpa [ofId] using congr(e $hk)

Premises used: Algebra.ofId
-- Module: Mathlib.Algebra.Central.Basic
Goal:
K : Type u
inst : CommSemiring K
D D' : Type v
inst_1 : Semiring D
inst_2 : Algebra K D
h : IsCentral K D
inst_3 : Semiring D'
inst_4 : Algebra K D'
z : Dᵐᵒᵖ
hz : Membership.mem (γ := Subalgebra K Dᵐᵒᵖ) (Subalgebra.center K Dᵐᵒᵖ) z
k : K
hk : (AlgHom.toRingHom (ofId K D) : (a : K) → D) k = unop z
⊢ (AlgHom.toRingHom (ofId K Dᵐᵒᵖ) : (a : K) → Dᵐᵒᵖ) k = z

Tactic:
simpa using congr(op $hk)
-- Module: Mathlib.Algebra.Central.End
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
f : End R M
⊢ Membership.mem (γ := Subsemiring (End R M)) (Subsemiring.center (End R M)) f ↔
    ∃ (α : R) (hα : Membership.mem (γ := Subsemiring R) (Subsemiring.center R) α), f = smulLeft α hα

Tactic:
mem_center_iff

Premises used: Set.Mem, setOf, Set.center, Module.End.mem_center_iff
-- Module: Mathlib.Algebra.Central.End
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
f : End R M
⊢ Membership.mem (γ := Subalgebra S (End R M)) (Subalgebra.center S (End R M)) f ↔
    ∃ (α : R) (hα : Membership.mem (γ := Subalgebra S R) (Subalgebra.center S R) α), f = smulLeft α hα

Tactic:
mem_center_iff

Premises used: Set.Mem, setOf, Set.center, Module.End.mem_center_iff
-- Module: Mathlib.Algebra.Central.End
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
inst_9 : IsCentral S R
T : End R M
hT : Membership.mem (γ := Subalgebra S (End R M)) (Subalgebra.center S (End R M)) T
w : R
h : Membership.mem (γ := Subalgebra S R) (Subalgebra.center S R) w
h_1 : T = End.smulLeft w h
y : S
h_2 : (AlgHom.toRingHom (ofId S R) : (a : S) → R) y = w
⊢ (AlgHom.toRingHom (ofId S (End R M)) : (a : S) → End R M) y = T

Tactic:
aesop
-- Module: Mathlib.Algebra.Central.End
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₂
rw : Eq (α := AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) (conjAlgEquiv S g) (conjAlgEquiv S f)
| Eq (α := AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) (conjAlgEquiv S f) (conjAlgEquiv S g)

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Algebra.Central.End
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₂
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₂)
⊢ 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₂)

Tactic:
conv_lhs => rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Algebra.Central.End
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

Tactic:
⟨fun h ↦ ?_, fun ⟨y, h⟩ ↦ conjAlgEquiv_ext_iff.mpr ⟨(y : S), congr($h)⟩⟩

Premises used: Iff.mpr, Units.val, congrArg, LinearEquiv.conjAlgEquiv, id, _private.0.LinearEquiv.conjAlgEquiv_ext_iff'.match_1, Iff.intro, Exists.intro, Eq, DFunLike.coe, LinearEquiv.conjAlgEquiv_ext_iff
-- Module: Mathlib.Algebra.Central.End
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₂
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
⊢ 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)⟩⟩
-- Module: Mathlib.Algebra.Central.End
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
neg : Nontrivial M → ∃ (α : Sˣ), f = α • g
⊢ ∃ (α : Sˣ), f = α • g

Tactic:
by_cases! Subsingleton M

Premises used: Subsingleton
-- Module: Mathlib.Algebra.Central.End
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
h₁ : ∀ (x : M), Eq.{u_5 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((HSMul.hSMul (α := Sˣ) 1 g : (a : M) → M₂) x : M₂)
⊢ f = HSMul.hSMul (α := Sˣ) 1 g

Tactic:
ext
-- Module: Mathlib.Algebra.Central.End
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
x : M
⊢ Eq.{u_5 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((HSMul.hSMul (α := Sˣ) 1 g : (a : M) → M₂) x : M₂)

Tactic:
simp [Subsingleton.eq_zero]

Premises used: Subsingleton.eq_zero
-- Module: Mathlib.Algebra.Central.End
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
⊢ ∃ (α : Sˣ), f = α • g

Tactic:
exact ⟨1, by ext; simp [Subsingleton.eq_zero]⟩
-- Module: Mathlib.Algebra.Central.End
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
neg :
  ∀ (α : S) (hα : (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)), ∃ (α : Sˣ), f = α • g
⊢ ∃ (α : Sˣ), f = α • g

Tactic:
obtain ⟨α, hα⟩ := conjAlgEquiv_ext_iff.mp h

Premises used: Iff.mp, LinearEquiv.conjAlgEquiv_ext_iff
-- Module: Mathlib.Algebra.Central.End
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₂)
neg :
  ∀ (β : S) (hβ : (⇑g : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) β (⇑f : (a : M) → M₂)), ∃ (α : Sˣ), f = α • g
⊢ ∃ (α : Sˣ), f = α • g

Tactic:
obtain ⟨β, hβ⟩ := conjAlgEquiv_ext_iff.mp h.symm

Premises used: Iff.mp, Eq.symm, LinearEquiv.conjAlgEquiv_ext_iff
-- Module: Mathlib.Algebra.Central.End
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
hβ : (⇑g : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) β (⇑f : (a : M) → M₂)
neg : ∀ (x : M) (hx : x ≠ 0), ∃ (α : Sˣ), f = α • g
⊢ ∃ (α : Sˣ), f = α • g

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : M)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Central.End
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
hβ : (⇑g : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) β (⇑f : (a : M) → M₂)
x : M
hx : x ≠ 0
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := S) (β := M₂) 1 ((f : (a : M) → M₂) x : M₂) =
    HSMul.hSMul (β := M₂) (α * β) ((f : (a : M) → M₂) x : M₂)

Tactic:
simpa [hβ, smul_smul] using congr($hα x)

Premises used: smul_smul