awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
sR : Set R
s_1 : Set S
N : Submodule R M
inst_5 : SMulCommClass R R M
s t : Set R
x : Submodule R M
r : R
m : M
hr : r ∈ s
hm : m ∈ t • x
this : SMulCommClass.{u_2, u_2, u_3} R R ↥x
obtain :
  ∀ (c : Finsupp.{u_2, u_3} R ↥x) (hc1 : (↑c.support : Set R) ⊆ t)
    (hm : (↑(c.sum fun (r : R) (m : ↥x) ↦ r • m) : M) ∈ t • x),
    HSMul.hSMul (β := M) r (↑(c.sum fun (r : R) (m : ↥x) ↦ r • m) : M) ∈ (s * t) • x
⊢ r • m ∈ (s * t) • x

Tactic:
obtain ⟨c, hc1, rfl⟩ := mem_set_smul _ _ _ |>.mp hm

Premises used: Iff.mp, Submodule.mem_set_smul, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
sR : Set R
s_1 : Set S
N : Submodule R M
inst_5 : SMulCommClass R R M
s t : Set R
x : Submodule R M
r : R
hr : r ∈ s
this : SMulCommClass.{u_2, u_2, u_3} R R ↥x
c : Finsupp.{u_2, u_3} R ↥x
hc1 : (↑c.support : Set R) ⊆ t
hm : (↑(c.sum fun (r : R) (m : ↥x) ↦ r • m) : M) ∈ t • x
rw :
  HSMul.hSMul (β := M) r (∑ i ∈ c.support, (↑(HSMul.hSMul (β := ↥x) i ((c : (a : R) → ↥x) i : ↥x)) : M)) ∈ (s * t) • x
⊢ HSMul.hSMul (β := M) r (↑(c.sum fun (r : R) (m : ↥x) ↦ r • m) : M) ∈ (s * t) • x

Tactic:
rw [Finsupp.sum, AddSubmonoid.coe_finsetSum]

Premises used: Finsupp.sum, AddSubmonoid.coe_finsetSum
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
sR : Set R
s_1 : Set S
N : Submodule R M
inst_5 : SMulCommClass R R M
s t : Set R
x : Submodule R M
r : R
hr : r ∈ s
this : SMulCommClass.{u_2, u_2, u_3} R R ↥x
c : Finsupp.{u_2, u_3} R ↥x
hc1 : (↑c.support : Set R) ⊆ t
hm : (↑(c.sum fun (r : R) (m : ↥x) ↦ r • m) : M) ∈ t • x
simp : ∑ x_1 ∈ c.support, HSMul.hSMul (β := M) (r * x_1) (↑((c : (a : R) → ↥x) x_1) : M) ∈ (s * t) • x
⊢ HSMul.hSMul (β := M) r (∑ i ∈ c.support, (↑(HSMul.hSMul (β := ↥x) i ((c : (a : R) → ↥x) i : ↥x)) : M)) ∈ (s * t) • x

Tactic:
simp only [SetLike.val_smul, Finset.smul_sum, smul_smul]

Premises used: smul_smul, SetLike.val_smul, Finset.smul_sum
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
sR : Set R
s_1 : Set S
N : Submodule R M
inst_5 : SMulCommClass R R M
s t : Set R
x : Submodule R M
r : R
hr : r ∈ s
this : SMulCommClass.{u_2, u_2, u_3} R R ↥x
c : Finsupp.{u_2, u_3} R ↥x
hc1 : (↑c.support : Set R) ⊆ t
hm : (↑(c.sum fun (r : R) (m : ↥x) ↦ r • m) : M) ∈ t • x
⊢ ∑ x_1 ∈ c.support, HSMul.hSMul (β := M) (r * x_1) (↑((c : (a : R) → ↥x) x_1) : M) ∈ (s * t) • x

Tactic:
Submodule.sum_mem _ fun r' hr' ↦
        mem_set_smul_of_mem_mem (Set.mul_mem_mul hr (hc1 hr')) (c _).2

Premises used: Submodule.sum_mem, Submodule.mem_set_smul_of_mem_mem, DFunLike.coe, Set.mul_mem_mul, Subtype.property
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
sR : Set R
s_1 : Set S
N : Submodule R M
inst_5 : SMulCommClass R R M
s t : Set R
x : Submodule R M
r : R
hr : r ∈ s
this : SMulCommClass.{u_2, u_2, u_3} R R ↥x
c : Finsupp.{u_2, u_3} R ↥x
hc1 : (↑c.support : Set R) ⊆ t
hm : (↑(c.sum fun (r : R) (m : ↥x) ↦ r • m) : M) ∈ t • x
⊢ ∑ x_1 ∈ c.support, HSMul.hSMul (β := M) (r * x_1) (↑((c : (a : R) → ↥x) x_1) : M) ∈ (s * t) • x

Tactic:
exact Submodule.sum_mem _ fun r' hr' ↦
        mem_set_smul_of_mem_mem (Set.mul_mem_mul hr (hc1 hr')) (c _).2

Premises used: Submodule.sum_mem, Submodule.mem_set_smul_of_mem_mem, DFunLike.coe, Set.mul_mem_mul, Subtype.property
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
sR : Set R
s : Set S
N : Submodule R M
inst_5 : SMulCommClass R R M
x : Submodule R M
w : M
h rwa rwa₁ rwa₂ rwa₃ : w ∈ x
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) 1 w ∈ x

Tactic:
rwa [one_smul]

Premises used: one_smul
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
sR : Set R
s_1 : Set S
N : Submodule R M
inst_5 : SMulCommClass R R M
s : Set R
x y : Submodule R M
r : R
m : M
hr : r ∈ s
hm : m ∈ x + y
⊢ ∃ y_1 ∈ x, ∃ z ∈ y, y_1 + z = m

Tactic:
rw [add_eq_sup, Submodule.mem_sup] at hm

Premises used: Submodule.mem_sup, Submodule.add_eq_sup
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
sR : Set R
s_1 : Set S
N : Submodule R M
inst_5 : SMulCommClass R R M
s : Set R
x y : Submodule R M
r : R
m : M
hr : r ∈ s
hm : ∃ y_1 ∈ x, ∃ z ∈ y, y_1 + z = m
obtain : ∀ (a : M) (ha : a ∈ x) (b : M) (hb : b ∈ y), r • (a + b) ∈ s • x + s • y
⊢ r • m ∈ s • x + s • y

Tactic:
obtain ⟨a, ha, b, hb, rfl⟩ := hm

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
sR : Set R
s_1 : Set S
N : Submodule R M
inst_5 : SMulCommClass R R M
s : Set R
x y : Submodule R M
r : R
hr : r ∈ s
a : M
ha : a ∈ x
b : M
hb : b ∈ y
rw : ∃ y_1 ∈ s • x, ∃ z ∈ s • y, y_1 + z = r • a + r • b
⊢ r • (a + b) ∈ s • x + s • y

Tactic:
rw [smul_add, add_eq_sup, Submodule.mem_sup]

Premises used: Submodule.mem_sup, Submodule.add_eq_sup, smul_add
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
sR : Set R
s_1 : Set S
N : Submodule R M
inst_5 : SMulCommClass R R M
s : Set R
x y : Submodule R M
r : R
hr : r ∈ s
a : M
ha : a ∈ x
b : M
hb : b ∈ y
⊢ ∃ y_1 ∈ s • x, ∃ z ∈ s • y, y_1 + z = r • a + r • b

Tactic:
⟨r • a, mem_set_smul_of_mem_mem (mem1 := hr) (mem2 := ha),
        r • b, mem_set_smul_of_mem_mem (mem1 := hr) (mem2 := hb), rfl⟩

Premises used: Submodule.mem_set_smul_of_mem_mem, And.intro, Exists.intro, HSMul.hSMul, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Finsupp
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
sR : Set R
s_1 : Set S
N : Submodule R M
inst_5 : SMulCommClass R R M
s : Set R
x y : Submodule R M
r : R
hr : r ∈ s
a : M
ha : a ∈ x
b : M
hb : b ∈ y
⊢ ∃ y_1 ∈ s • x, ∃ z ∈ s • y, y_1 + z = r • a + r • b

Tactic:
exact ⟨r • a, mem_set_smul_of_mem_mem (mem1 := hr) (mem2 := ha),
        r • b, mem_set_smul_of_mem_mem (mem1 := hr) (mem2 := hb), rfl⟩
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : End R M
p : Submodule R M
hp : Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | p ≤ Submodule.comap f p} p
q : Submodule R M
hq : Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | p ≤ Submodule.comap f p} q
simp : p ⊓ q ≤ Submodule.comap f p ∧ p ⊓ q ≤ Submodule.comap f q
⊢ Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | p ≤ Submodule.comap f p} (p ⊓ q)

Tactic:
simp only [Set.mem_setOf_eq, Submodule.comap_inf, le_inf_iff]

Premises used: Submodule.comap_inf, Set.mem_setOf_eq, le_inf_iff
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : End R M
p : Submodule R M
hp : Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | p ≤ Submodule.comap f p} p
q : Submodule R M
hq : Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | p ≤ Submodule.comap f p} q
⊢ p ⊓ q ≤ Submodule.comap f p ∧ p ⊓ q ≤ Submodule.comap f q

Tactic:
⟨inf_le_of_left_le hp, inf_le_of_right_le hq⟩

Premises used: inf_le_of_right_le, inf_le_of_left_le, And.intro
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : End R M
p : Submodule R M
hp : Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | p ≤ Submodule.comap f p} p
q : Submodule R M
hq : Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | p ≤ Submodule.comap f p} q
⊢ p ⊓ q ≤ Submodule.comap f p ∧ p ⊓ q ≤ Submodule.comap f q

Tactic:
exact ⟨inf_le_of_left_le hp, inf_le_of_right_le hq⟩
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p : Submodule R M
⊢ p ∈ f.invtSubmodule ↔ p ≤ Submodule.comap f p

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p : Submodule R M
⊢ p ∈ f.invtSubmodule ↔ Submodule.map f p ≤ p

Tactic:
Submodule.map_le_iff_le_comap.symm

Premises used: Set.Mem, setOf, Submodule.map_le_iff_le_comap, Iff.symm
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p : Submodule R M
⊢ p ∈ f.invtSubmodule ↔ Set.MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.MapsTo
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p : Submodule R M
⊢ p ∈ f.invtSubmodule ↔ ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : M ≃ₗ[R] M
p : Submodule R M
⊢ p ∈ invtSubmodule (↑f.symm : M →ₗ[R] M) ↔ p ≤ Submodule.map (↑f : M →ₗ[R] M) p

Tactic:
(mem_invtSubmodule_iff_map_le _).trans (f.toEquiv.symm.subset_symm_image _ _).symm

Premises used: LinearEquiv.toEquiv, Iff.trans, Equiv.subset_symm_image, Equiv.symm, Module.End.mem_invtSubmodule_iff_map_le, Iff.symm
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : End R M
⊢ f.invtSubmodule ⊓ g.invtSubmodule ≤ (f + g).invtSubmodule

Tactic:
fun p ⟨hfp, hgp⟩ _ hx ↦ p.add_mem (hfp hx) (hgp hx)

Premises used: Set.Mem, setOf, _private.0.Module.End.invtSubmodule_inf_invtSubmodule_le_invtSubmodule_add.match_1, Membership.mem, Submodule.comap, HAdd.hAdd, Submodule.add_mem
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
M : Type u_2
inst : AddCommMonoid M
R : Type u_3
S : Type u_4
inst_1 : Semiring R
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : Module S M
inst_5 : DistribSMul S R
inst_6 : SMulCommClass R S M
inst_7 : IsScalarTower S R M
f : End R M
c : S
⊢ f.invtSubmodule ≤ (c • f).invtSubmodule

Tactic:
fun p hfp _ hx ↦ p.smul_of_tower_mem c (hfp hx)

Premises used: Set.Mem, setOf, Set.preimage, Submodule.smul_of_tower_mem
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
M : Type u_2
inst : AddCommMonoid M
R : Type u_3
S : Type u_4
inst_1 : Semiring R
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : Module S M
inst_5 : DistribSMul S R
inst_6 : SMulCommClass R S M
inst_7 : IsScalarTower S R M
f : End R M
c : Sˣ
apply : ((↑c : S) • f).invtSubmodule ≤ f.invtSubmodule
⊢ (c • f).invtSubmodule = f.invtSubmodule

Tactic:
apply le_antisymm ?_ (invtSubmodule_le_invtSubmodule_smul f c.1)

Premises used: Units.val, Module.End.invtSubmodule_le_invtSubmodule_smul, le_antisymm
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
M : Type u_2
inst : AddCommMonoid M
R : Type u_3
S : Type u_4
inst_1 : Semiring R
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : Module S M
inst_5 : DistribSMul S R
inst_6 : SMulCommClass R S M
inst_7 : IsScalarTower S R M
f : End R M
c : Sˣ
grw : ((↑c⁻¹ : S) • (↑c : S) • f).invtSubmodule ≤ f.invtSubmodule
⊢ ((↑c : S) • f).invtSubmodule ≤ f.invtSubmodule

Tactic:
grw [invtSubmodule_le_invtSubmodule_smul (c.1 • f) c⁻¹.1]

Premises used: Units.val, Module.End.invtSubmodule_le_invtSubmodule_smul, Inv.inv, HSMul.hSMul
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
M : Type u_2
inst : AddCommMonoid M
R : Type u_3
S : Type u_4
inst_1 : Semiring R
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : Module S M
inst_5 : DistribSMul S R
inst_6 : SMulCommClass R S M
inst_7 : IsScalarTower S R M
f : End R M
c : Sˣ
⊢ ((↑c⁻¹ : S) • (↑c : S) • f).invtSubmodule ≤ f.invtSubmodule

Tactic:
simp [smul_smul]

Premises used: smul_smul
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ p ⊓ q ∈ f.invtSubmodule

Tactic:
Sublattice.inf_mem hp hq

Premises used: Sublattice.inf_mem, Set.Mem, setOf
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ p ⊔ q ∈ f.invtSubmodule

Tactic:
Sublattice.sup_mem hp hq

Premises used: Sublattice.sup_mem
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
⊢ ⊤ ∈ f.invtSubmodule

Tactic:
simp [invtSubmodule]

Premises used: Module.End.invtSubmodule
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
⊢ ⊥ ∈ f.invtSubmodule

Tactic:
simp [invtSubmodule]

Premises used: Module.End.invtSubmodule
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : End R M
x : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp ≤
    Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) ⊤ ⋯

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : End R M
x : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) ⊥ ⋯ ≤
    Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : Submodule R M
⊢ Membership.mem (γ := Sublattice (Submodule R M)) ⊤ x →
    Membership.mem (γ := Sublattice (Submodule R M)) (invtSubmodule 0) x

Tactic:
simp [invtSubmodule]

Premises used: Module.End.invtSubmodule
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : Submodule R M
⊢ Membership.mem (γ := Sublattice (Submodule R M)) ⊤ x →
    Membership.mem (γ := Sublattice (Submodule R M)) (invtSubmodule LinearMap.id) x

Tactic:
simp [invtSubmodule]

Premises used: Module.End.invtSubmodule
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{u_2 + 1} (α := Sublattice (Submodule R M)) (invtSubmodule 1) ⊤

Tactic:
invtSubmodule.id

Premises used: Module.End.invtSubmodule.id
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ ⊥ ∈ f.invtSubmodule

Tactic:
simp [invtSubmodule]

Premises used: Module.End.invtSubmodule
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ ⊤ ∈ f.invtSubmodule

Tactic:
simp [invtSubmodule]

Premises used: Module.End.invtSubmodule
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
rw :
  Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp ⊓
        Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq =
      ⊥ ↔
    Disjoint p q
rw₁ :
  Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp ⊓
        Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq =
      ⊥ ↔
    p ⊓ q = ⊥
rw₂ : Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) (p ⊓ q) ⋯ = ⊥ ↔ p ⊓ q = ⊥
rw₃ rw₄ : p ⊓ q = ⊥ ↔ p ⊓ q = ⊥
⊢ Disjoint (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp)
      (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq) ↔
    Disjoint p q

Tactic:
rw [disjoint_iff, disjoint_iff, Sublattice.mk_inf_mk,
    Subtype.mk_eq_bot_iff (⊥ : f.invtSubmodule).property]

Premises used: disjoint_iff, Sublattice.mk_inf_mk, Bot.bot, Subtype.mk_eq_bot_iff, Subtype.property
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : ↥f.invtSubmodule
obtain :
  ∀ (p : Submodule R M) (hp : p ∈ f.invtSubmodule),
    Disjoint (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) q ↔
      Disjoint (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) : Submodule R M)
        (↑q : Submodule R M)
⊢ Disjoint p q ↔ Disjoint (↑p : Submodule R M) (↑q : Submodule R M)

Tactic:
obtain ⟨p, hp⟩ := p
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
q : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
obtain :
  ∀ (q : Submodule R M) (hq : q ∈ f.invtSubmodule),
    Disjoint (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp)
        (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq) ↔
      Disjoint (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) : Submodule R M)
        (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq) : Submodule R M)
⊢ Disjoint (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) q ↔
    Disjoint (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) : Submodule R M)
      (↑q : Submodule R M)

Tactic:
obtain ⟨q, hq⟩ := q
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq : q ∈ f.invtSubmodule
⊢ Disjoint (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp)
      (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq) ↔
    Disjoint (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) : Submodule R M)
      (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq) : Submodule R M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
rw :
  Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp ⊔
        Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq =
      ⊤ ↔
    Codisjoint p q
rw₁ :
  Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp ⊔
        Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq =
      ⊤ ↔
    p ⊔ q = ⊤
rw₂ : Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) (p ⊔ q) ⋯ = ⊤ ↔ p ⊔ q = ⊤
rw₃ rw₄ : p ⊔ q = ⊤ ↔ p ⊔ q = ⊤
⊢ Codisjoint (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp)
      (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq) ↔
    Codisjoint p q

Tactic:
rw [codisjoint_iff, codisjoint_iff, Sublattice.mk_sup_mk,
    Subtype.mk_eq_top_iff (⊤ : f.invtSubmodule).property]

Premises used: codisjoint_iff, Subtype.mk_eq_top_iff, Sublattice.mk_sup_mk, Top.top, Subtype.property
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : ↥f.invtSubmodule
obtain :
  ∀ (p : Submodule R M) (hp : p ∈ f.invtSubmodule),
    Codisjoint (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) q ↔
      Codisjoint (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) : Submodule R M)
        (↑q : Submodule R M)
⊢ Codisjoint p q ↔ Codisjoint (↑p : Submodule R M) (↑q : Submodule R M)

Tactic:
obtain ⟨p, hp⟩ := p
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
q : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
obtain :
  ∀ (q : Submodule R M) (hq : q ∈ f.invtSubmodule),
    Codisjoint (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp)
        (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq) ↔
      Codisjoint (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) : Submodule R M)
        (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq) : Submodule R M)
⊢ Codisjoint (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) q ↔
    Codisjoint (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) : Submodule R M)
      (↑q : Submodule R M)

Tactic:
obtain ⟨q, hq⟩ := q
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq : q ∈ f.invtSubmodule
⊢ Codisjoint (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp)
      (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq) ↔
    Codisjoint (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) : Submodule R M)
      (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq) : Submodule R M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ IsCompl (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp)
      (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq) ↔
    IsCompl p q

Tactic:
simp [isCompl_iff]

Premises used: isCompl_iff