awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
A B : Submodule R M
hAB : A ≤ B
f : Submodule R ↥B ≃o (↑(Set.Iic B) : Type u_4) := B.mapIic
hf : f = B.mapIic
rw :
  IsCoatom (α := { x : Submodule R M // x ∈ Set.Iic B })
      (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ Set.Iic B) A hAB) ↔
    IsCoatom (α := (↑(Set.Iic B) : Type u_4))
      ((B.mapIic : (a : Submodule R ↥B) → (↑(Set.Iic B) : Type u_4)) (Submodule.comap B.subtype A) :
        (↑(Set.Iic B) : Type u_4))
⊢ A ⋖ B ↔ IsSimpleModule.{u_2, u_4} R (↥B ⧸ Submodule.comap B.subtype A)

Tactic:
rw [covBy_iff_coatom_Iic hAB, isSimpleModule_iff_isCoatom, ← OrderIso.isCoatom_iff f, hf]

Premises used: OrderIso.isCoatom_iff, covBy_iff_coatom_Iic, isSimpleModule_iff_isCoatom
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
A B : Submodule R M
hAB : A ≤ B
f : Submodule R ↥B ≃o (↑(Set.Iic B) : Type u_4) := B.mapIic
hf : f = B.mapIic
⊢ IsCoatom (α := { x : Submodule R M // x ∈ Set.Iic B })
      (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ Set.Iic B) A hAB) ↔
    IsCoatom (α := (↑(Set.Iic B) : Type u_4))
      ((B.mapIic : (a : Submodule R ↥B) → (↑(Set.Iic B) : Type u_4)) (Submodule.comap B.subtype A) :
        (↑(Set.Iic B) : Type u_4))

Tactic:
simp [-OrderIso.isCoatom_iff, Submodule.map_comap_subtype, inf_eq_right.2 hAB]

Premises used: Iff.mpr, OrderIso.isCoatom_iff, Submodule.map_comap_subtype, inf_eq_right
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
m : Submodule R M
inst_3 : IsSimpleModule.{u_2, u_4} R ↥m
⊢ IsAtom m

Tactic:
isSimpleModule_iff_isAtom.1 ‹_›

Premises used: isSimpleModule_iff_isAtom, Iff.mp
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ Eq (α := Submodule R M) (R ∙ m) ⊤

Tactic:
(eq_bot_or_eq_top _).resolve_left fun h ↦ hm (h.le <| Submodule.mem_span_singleton_self m)

Premises used: Eq.le, Or.resolve_left, Submodule.mem_span_singleton_self, IsSimpleOrder.eq_bot_or_eq_top
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S_1 : Type u_3
inst : Ring R
inst_1 : Ring S_1
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : IsSimpleModule R M
S : Submodule R M
inl : ∃ (a : M), Eq (α := Submodule R M) ⊥ (R ∙ a)
inr : ∃ (a : M), Eq (α := Submodule R M) ⊤ (R ∙ a)
⊢ ∃ (a : M), S = R ∙ a

Tactic:
obtain rfl | rfl := eq_bot_or_eq_top S

Premises used: IsSimpleOrder.eq_bot_or_eq_top, rfl
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : IsSimpleModule R M
⊢ ∃ (a : M), Eq (α := Submodule R M) ⊥ (R ∙ a)

Tactic:
⟨0, Submodule.span_zero.symm⟩

Premises used: Exists.intro, OfNat.ofNat, Eq.symm, Submodule.span_zero
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : IsSimpleModule R M
⊢ ∃ (a : M), Eq (α := Submodule R M) ⊥ (R ∙ a)

Tactic:
exact ⟨0, Submodule.span_zero.symm⟩
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : IsSimpleModule R M
⊢ Nontrivial M

Tactic:
have := IsSimpleModule.nontrivial R M
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : IsSimpleModule R M
this : Nontrivial M
inr : ∀ (m : M) (hm : m ≠ 0), ∃ (a : M), Eq (α := Submodule R M) ⊤ (R ∙ a)
⊢ ∃ (a : M), Eq (α := Submodule R M) ⊤ (R ∙ a)

Tactic:
have ⟨m, hm⟩ := exists_ne (0 : M)
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m_1 : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : IsSimpleModule R M
this : Nontrivial M
m : M
hm : m ≠ 0
⊢ ∃ (a : M), Eq (α := Submodule R M) ⊤ (R ∙ a)

Tactic:
⟨m, (span_singleton_eq_top R hm).symm⟩

Premises used: IsSimpleModule.span_singleton_eq_top, Exists.intro, Eq.symm
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m_1 : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : IsSimpleModule R M
this : Nontrivial M
m : M
hm : m ≠ 0
⊢ ∃ (a : M), Eq (α := Submodule R M) ⊤ (R ∙ a)

Tactic:
exact ⟨m, (span_singleton_eq_top R hm).symm⟩
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSimpleModule R M
m : M
hm : m ≠ 0
rw : Eq (α := Submodule R M) (range (toSpanSingleton R M m)) ⊤
rw₁ : Eq (α := Submodule R M) (R ∙ m) ⊤
rw₂ rw₃ : Eq.{u_4 + 1} (α := Submodule R M) ⊤ ⊤
⊢ Function.Surjective.{u_2 + 1, u_4 + 1} (α := R) (β := M) (⇑(toSpanSingleton R M m) : (a : R) → M)

Tactic:
rw [← range_eq_top, ← span_singleton_eq_range, span_singleton_eq_top R hm]

Premises used: LinearMap.range_eq_top, IsSimpleModule.span_singleton_eq_top, LinearMap.span_singleton_eq_range
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSimpleModule R M
m : M
hm : m ≠ 0
rw : IsSimpleModule R (HasQuotient.Quotient R (B := Submodule R R) (ker (toSpanSingleton R M m)))
⊢ Ideal.IsMaximal (ker (toSpanSingleton R M m))

Tactic:
rw [Ideal.isMaximal_def, ← isSimpleModule_iff_isCoatom]

Premises used: isSimpleModule_iff_isCoatom, Ideal.isMaximal_def
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ IsSimpleModule R (HasQuotient.Quotient R (B := Submodule R R) (ker (toSpanSingleton R M m)))

Tactic:
congr (quotKerEquivOfSurjective _ <| toSpanSingleton_surjective R hm)

Premises used: IsSimpleModule.toSpanSingleton_surjective, LinearMap.quotKerEquivOfSurjective, IsSimpleModule.congr
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ IsSimpleModule R (HasQuotient.Quotient R (B := Submodule R R) (ker (toSpanSingleton R M m)))

Tactic:
exact congr (quotKerEquivOfSurjective _ <| toSpanSingleton_surjective R hm)

Premises used: IsSimpleModule.toSpanSingleton_surjective, LinearMap.quotKerEquivOfSurjective, IsSimpleModule.congr
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : IsSimpleModule R M
⊢ IsNoetherian R M

Tactic:
isNoetherian_iff'.mpr inferInstance

Premises used: isNoetherian_iff', Iff.mpr, inferInstance
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ IsSimpleModule R M ↔ ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)

Tactic:
⟨fun h ↦ ?_, fun ⟨I, ⟨coatom⟩, ⟨equiv⟩⟩ ↦ ?_⟩

Premises used: _private.0.isSimpleModule_iff_quot_maximal.match_1, IsSimpleModule, Iff.intro
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
refine_1 : ∀ (h : IsSimpleModule R M), ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
refine_2 :
  (∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)) →
    ∀ (I : Ideal R) (coatom : IsCoatom I) (equiv : M ≃ₗ[R] R ⧸ I), IsSimpleModule R M
⊢ IsSimpleModule R M ↔ ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨I, ⟨coatom⟩, ⟨equiv⟩⟩ ↦ ?_⟩
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsSimpleModule R M
⊢ Nontrivial M

Tactic:
have := IsSimpleModule.nontrivial R M
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsSimpleModule R M
this : Nontrivial M
refine_1 : ∀ (m : M) (hm : m ≠ 0), ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
⊢ ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)

Tactic:
have ⟨m, hm⟩ := exists_ne (0 : M)
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsSimpleModule R M
this : Nontrivial M
m : M
hm : m ≠ 0
⊢ ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)

Tactic:
⟨_, ker_toSpanSingleton_isMaximal R hm,
      ⟨(LinearMap.quotKerEquivOfSurjective _ <| toSpanSingleton_surjective R hm).symm⟩⟩

Premises used: LinearEquiv.symm, IsSimpleModule.toSpanSingleton_surjective, Nonempty.intro, And.intro, LinearMap.quotKerEquivOfSurjective, Exists.intro, IsSimpleModule.ker_toSpanSingleton_isMaximal
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsSimpleModule R M
this : Nontrivial M
m : M
hm : m ≠ 0
⊢ ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)

Tactic:
exact ⟨_, ker_toSpanSingleton_isMaximal R hm,
      ⟨(LinearMap.quotKerEquivOfSurjective _ <| toSpanSingleton_surjective R hm).symm⟩⟩
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
I : Ideal R
coatom : IsCoatom I
equiv : M ≃ₗ[R] R ⧸ I
⊢ IsSimpleModule R M

Tactic:
congr equiv

Premises used: IsSimpleModule.congr
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
I : Ideal R
coatom : IsCoatom I
equiv : M ≃ₗ[R] R ⧸ I
refine_2 : IsSimpleModule R (R ⧸ I)
⊢ IsSimpleModule R M

Tactic:
convert! congr equiv
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : ∃ (I : Ideal R), I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
I : Ideal R
coatom : IsCoatom I
equiv : M ≃ₗ[R] R ⧸ I
refine_2 refine_2₁ refine_2₂ refine_2₃ : IsCoatom I
⊢ IsSimpleModule R (R ⧸ I)

Tactic:
rwa [isSimpleModule_iff_isCoatom]

Premises used: isSimpleModule_iff_isCoatom
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
M : Type u_4
inst : AddCommGroup M
R : Type u_6
inst_1 : CommRing R
inst_2 : Module R M
simple : IsSimpleModule R M
have : ∀ (I : Ideal R) (max : I.IsMaximal) (e : M ≃ₗ[R] R ⧸ I), Ideal.IsMaximal (Module.annihilator R M)
⊢ Ideal.IsMaximal (Module.annihilator R M)

Tactic:
have ⟨I, max, ⟨e⟩⟩ := isSimpleModule_iff_quot_maximal.mp simple
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
M : Type u_4
inst : AddCommGroup M
R : Type u_6
inst_1 : CommRing R
inst_2 : Module R M
simple : IsSimpleModule R M
I : Ideal R
max : I.IsMaximal
e : M ≃ₗ[R] R ⧸ I
rwa : Ideal.IsMaximal (Module.annihilator R (R ⧸ I))
rwa₁ rwa₂ rwa₃ rwa₄ : I.IsMaximal
⊢ Ideal.IsMaximal (Module.annihilator R M)

Tactic:
rwa [e.annihilator_eq, I.annihilator_quotient]

Premises used: Ideal.annihilator_quotient, LinearEquiv.annihilator_eq
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 :
  Nontrivial M ∧
    ∀ (x : M),
      x ≠ 0 →
        Function.Surjective.{u_2 + 1, u_4 + 1} (α := R) (β := M) (⇑(LinearMap.toSpanSingleton R M x) : (a : R) → M)
left : Nontrivial M
h :
  ∀ (x : M),
    x ≠ 0 → Function.Surjective.{u_2 + 1, u_4 + 1} (α := R) (β := M) (⇑(LinearMap.toSpanSingleton R M x) : (a : R) → M)
m : Submodule R M
ne_bot : ¬m = ⊥
x : M
hxm : x ∈ m
hx0 : x ≠ 0
z : M
h_2 : Membership.mem (γ := Submodule R M) ⊤ z
obtain :
  ∀ (y : R),
    Membership.mem.{u_4, u_4} (α := M) (γ := Submodule R M) ⊤ ((LinearMap.toSpanSingleton R M x : (a : R) → M) y : M) →
      Membership.mem (α := M) m ((LinearMap.toSpanSingleton R M x : (a : R) → M) y : M)
⊢ z ∈ m

Tactic:
obtain ⟨y, rfl⟩ := h x hx0 z

Premises used: rfl
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 :
  Nontrivial M ∧
    ∀ (x : M),
      x ≠ 0 →
        Function.Surjective.{u_2 + 1, u_4 + 1} (α := R) (β := M) (⇑(LinearMap.toSpanSingleton R M x) : (a : R) → M)
left : Nontrivial M
h :
  ∀ (x : M),
    x ≠ 0 → Function.Surjective.{u_2 + 1, u_4 + 1} (α := R) (β := M) (⇑(LinearMap.toSpanSingleton R M x) : (a : R) → M)
m : Submodule R M
ne_bot : ¬m = ⊥
x : M
hxm : x ∈ m
hx0 : x ≠ 0
y : R
h_2 : Membership.mem.{u_4, u_4} (α := M) (γ := Submodule R M) ⊤ ((LinearMap.toSpanSingleton R M x : (a : R) → M) y : M)
⊢ Membership.mem (α := M) m ((LinearMap.toSpanSingleton R M x : (a : R) → M) y : M)

Tactic:
m.smul_mem _ hxm

Premises used: Set.Mem, Submodule.smul_mem
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 :
  Nontrivial M ∧
    ∀ (x : M),
      x ≠ 0 →
        Function.Surjective.{u_2 + 1, u_4 + 1} (α := R) (β := M) (⇑(LinearMap.toSpanSingleton R M x) : (a : R) → M)
left : Nontrivial M
h :
  ∀ (x : M),
    x ≠ 0 → Function.Surjective.{u_2 + 1, u_4 + 1} (α := R) (β := M) (⇑(LinearMap.toSpanSingleton R M x) : (a : R) → M)
m : Submodule R M
ne_bot : ¬m = ⊥
x : M
hxm : x ∈ m
hx0 : x ≠ 0
y : R
h_2 : Membership.mem.{u_4, u_4} (α := M) (γ := Submodule R M) ⊤ ((LinearMap.toSpanSingleton R M x : (a : R) → M) y : M)
⊢ Membership.mem (α := M) m ((LinearMap.toSpanSingleton R M x : (a : R) → M) y : M)

Tactic:
exact m.smul_mem _ hxm

Premises used: Submodule.smul_mem
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
h : Nontrivial R
⊢ (∀ (x : R), x ≠ 0 → Function.Surjective (α := R) (β := R) (⇑(LinearMap.toSpanSingleton R R x) : (a : R) → R)) ↔
    ∀ (x : R), x ≠ 0 → IsUnit x

Tactic:
⟨fun h x hx ↦ ?_, fun h x hx ↦ (h x hx).unit.mulRight_bijective.surjective⟩

Premises used: Units.mulRight_bijective, Function.Bijective.surjective, Iff.intro, IsUnit.unit
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
h : Nontrivial R
refine :
  ∀ (h : ∀ (x : R), x ≠ 0 → Function.Surjective (α := R) (β := R) (⇑(LinearMap.toSpanSingleton R R x) : (a : R) → R))
    (x : R) (hx : x ≠ 0), IsUnit x
⊢ (∀ (x : R), x ≠ 0 → Function.Surjective (α := R) (β := R) (⇑(LinearMap.toSpanSingleton R R x) : (a : R) → R)) ↔
    ∀ (x : R), x ≠ 0 → IsUnit x

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ (h x hx).unit.mulRight_bijective.surjective⟩
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
h_1 : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective (α := R) (β := R) (⇑(LinearMap.toSpanSingleton R R x) : (a : R) → R)
x : R
hx : x ≠ 0
obtain : ∀ (y : R) (hyx : y * x = 1), IsUnit x
⊢ IsUnit x

Tactic:
obtain ⟨y, hyx : y * x = 1⟩ := h x hx 1

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
h_1 : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective (α := R) (β := R) (⇑(LinearMap.toSpanSingleton R R x) : (a : R) → R)
x : R
hx : x ≠ 0
y : R
hyx : y * x = 1
⊢ y ≠ 0

Tactic:
have hy : y ≠ 0 := left_ne_zero_of_mul (hyx.symm ▸ one_ne_zero)
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
h_1 : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective (α := R) (β := R) (⇑(LinearMap.toSpanSingleton R R x) : (a : R) → R)
x : R
hx : x ≠ 0
y : R
hyx : y * x = 1
hy : y ≠ 0
obtain : ∀ (z : R) (hzy : z * y = 1), IsUnit x
⊢ IsUnit x

Tactic:
obtain ⟨z, hzy : z * y = 1⟩ := h y hy 1

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
h_1 : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective (α := R) (β := R) (⇑(LinearMap.toSpanSingleton R R x) : (a : R) → R)
x : R
hx : x ≠ 0
y : R
hyx : y * x = 1
hy : y ≠ 0
z : R
hzy : z * y = 1
⊢ IsUnit x

Tactic:
⟨⟨x, y, left_inv_eq_right_inv hzy hyx ▸ hzy, hyx⟩, rfl⟩

Premises used: IsUnit, Eq.rec, left_inv_eq_right_inv, Units.mk, Exists.intro, rfl
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
h_1 : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective (α := R) (β := R) (⇑(LinearMap.toSpanSingleton R R x) : (a : R) → R)
x : R
hx : x ≠ 0
y : R
hyx : y * x = 1
hy : y ≠ 0
z : R
hzy : z * y = 1
⊢ IsUnit x

Tactic:
exact ⟨⟨x, y, left_inv_eq_right_inv hzy hyx ▸ hzy, hyx⟩, rfl⟩
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : Eq.{u_4 + 1} (α := Submodule R M) (sSup {m : Submodule R M | IsSimpleModule.{u_2, u_4} R ↥m}) ⊤
simp_rw :
  Eq.{u_4 + 1} (α := Submodule R M) (sSup {a : Submodule R M | IsAtom a})
    (sSup {m : Submodule R M | IsSimpleModule.{u_2, u_4} R ↥m})
⊢ Eq.{u_4 + 1} (α := Submodule R M) (sSup {a : Submodule R M | IsAtom a}) ⊤

Tactic:
simp_rw [← h, isSimpleModule_iff_isAtom]

Premises used: isSimpleModule_iff_isAtom
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
m : Submodule R M
R₀ : Type u_6
P : Type u_7
inst_3 : Semiring R₀
inst_4 : AddCommMonoid P
inst_5 : Module R P
inst_6 : Module R₀ P
inst_7 : SMulCommClass R R₀ P
inst_8 : Module.Finite R₀ (M →ₗ[R] P)
h : IsComplemented m
⊢ Module.Finite R₀ (LinearMap.{u_2, u_2, u_4, u_7} (RingHom.id R) (↥m) P)

Tactic:
.of_surjective (.lcomp R₀ P ..) (LinearMap.surjective_comp_subtype_of_isComplemented h)

Premises used: Module.Finite.of_surjective, LinearMap.lcomp, LinearMap.surjective_comp_subtype_of_isComplemented
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
R₀ : Type u_6
P : Type u_7
inst_6 : Semiring R₀
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module R₀ P
inst_10 : SMulCommClass R R₀ P
inst_11 : Module.Finite R₀ (M →ₗ[R] P)
inst_12 : IsSemisimpleModule R M
⊢ Module.Finite R₀ (LinearMap.{u_2, u_2, u_4, u_7} (RingHom.id R) (↥m) P)

Tactic:
.of_isComplemented_domain _ _ (exists_isCompl m)

Premises used: ComplementedLattice.exists_isCompl, Module.Finite.of_isComplemented_domain
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
m : Submodule R M
R₀ : Type u_6
P : Type u_7
inst_3 : Semiring R₀
inst_4 : AddCommMonoid P
inst_5 : Module R P
inst_6 : Module R₀ M
inst_7 : SMulCommClass R R₀ M
inst_8 : SMul R₀ R
inst_9 : IsScalarTower R₀ R M
inst_10 : Module.Finite R₀ (P →ₗ[R] M)
h : IsComplemented m
⊢ Module.Finite R₀ (LinearMap.{u_2, u_2, u_7, u_4} (RingHom.id R) P ↥m)

Tactic:
.of_surjective (.compRight ..) (LinearMap.surjective_comp_projectionOnto h.choose_spec)

Premises used: Exists.choose_spec, Module.Finite.of_surjective, LinearMap.compRight, LinearMap.surjective_comp_projectionOnto
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Ring R
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
m : Submodule R M
N : Type u_5
inst_4 : AddCommGroup N
inst_5 : Module R N
R₀ : Type u_6
P : Type u_7
inst_6 : Semiring R₀
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module R₀ M
inst_10 : SMulCommClass R R₀ M
inst_11 : SMul R₀ R
inst_12 : IsScalarTower R₀ R M
inst_13 : Module.Finite R₀ (P →ₗ[R] M)
inst_14 : IsSemisimpleModule R M
⊢ Module.Finite R₀ (LinearMap.{u_2, u_2, u_7, u_4} (RingHom.id R) P ↥m)

Tactic:
.of_isComplemented_codomain _ _ (exists_isCompl m)

Premises used: ComplementedLattice.exists_isCompl, Module.Finite.of_isComplemented_codomain
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSemisimpleModule.{u_2, u_4} R ↥N
rw : Eq.{u_4 + 1} (α := Submodule R ↥N) ⊥ ⊤ ∨ ∃ m ≤ N, IsSimpleModule.{u_2, u_4} R ↥m
⊢ N = ⊥ ∨ ∃ m ≤ N, IsSimpleModule.{u_2, u_4} R ↥m

Tactic:
rw [← N.subsingleton_iff_eq_bot, ← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top]

Premises used: Submodule.subsingleton_iff_eq_bot, Submodule.subsingleton_iff, subsingleton_iff_bot_eq_top
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSemisimpleModule.{u_2, u_4} R ↥N
⊢ Eq.{u_4 + 1} (α := Submodule R ↥N) ⊥ ⊤ ∨ ∃ m ≤ N, IsSimpleModule.{u_2, u_4} R ↥m

Tactic:
(eq_bot_or_exists_atom_le _).imp .symm fun ⟨m, h, _⟩ ↦ ⟨_, N.map_subtype_le m, ?_⟩

Premises used: IsAtomic.eq_bot_or_exists_atom_le, Or.imp, Eq.symm
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSemisimpleModule.{u_2, u_4} R ↥N
refine :
  (∃ (a : Submodule R ↥N), IsAtom a ∧ a ≤ ⊤) →
    ∀ (m : Submodule R ↥N) (h : IsAtom m), m ≤ ⊤ → IsSimpleModule.{u_2, u_4} R ↥(Submodule.map N.subtype m)
⊢ Eq.{u_4 + 1} (α := Submodule R ↥N) ⊥ ⊤ ∨ ∃ m ≤ N, IsSimpleModule.{u_2, u_4} R ↥m

Tactic:
refine (eq_bot_or_exists_atom_le _).imp .symm fun ⟨m, h, _⟩ ↦ ⟨_, N.map_subtype_le m, ?_⟩

Premises used: IsAtomic.eq_bot_or_exists_atom_le, Or.imp
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSemisimpleModule.{u_2, u_4} R ↥N
h_1 : ∃ (a : Submodule R ↥N), IsAtom a ∧ a ≤ ⊤
m : Submodule R ↥N
h : IsAtom m
right : m ≤ ⊤
⊢ IsSimpleModule.{u_2, u_4} R ↥m

Tactic:
rw [← isSimpleModule_iff_isAtom] at h

Premises used: isSimpleModule_iff_isAtom
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSemisimpleModule.{u_2, u_4} R ↥N
h_1 : ∃ (a : Submodule R ↥N), IsAtom a ∧ a ≤ ⊤
m : Submodule R ↥N
h : IsAtom m
right : m ≤ ⊤
h₁ : IsSimpleModule.{u_2, u_4} R ↥m
⊢ m ≤ ⊤

Tactic:
rw [← isSimpleModule_iff_isAtom] at h

Premises used: isSimpleModule_iff_isAtom
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSemisimpleModule.{u_2, u_4} R ↥N
h_1 : ∃ (a : Submodule R ↥N), IsAtom a ∧ a ≤ ⊤
m : Submodule R ↥N
h : IsSimpleModule.{u_2, u_4} R ↥m
right : m ≤ ⊤
⊢ IsSimpleModule.{u_2, u_4} R ↥(Submodule.map N.subtype m)

Tactic:
.congr (m.equivMapOfInjective _ N.subtype_injective).symm

Premises used: LinearEquiv.symm, Submodule.equivMapOfInjective, Submodule.subtype_injective, IsSimpleModule.congr
-- Module: Mathlib.RingTheory.SimpleModule.Basic
Goal:
R : Type u_2
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsSemisimpleModule.{u_2, u_4} R ↥N
h_1 : ∃ (a : Submodule R ↥N), IsAtom a ∧ a ≤ ⊤
m : Submodule R ↥N
h : IsSimpleModule.{u_2, u_4} R ↥m
right : m ≤ ⊤
⊢ IsSimpleModule.{u_2, u_4} R ↥(Submodule.map N.subtype m)

Tactic:
exact .congr (m.equivMapOfInjective _ N.subtype_injective).symm