awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
closed_under_smul :
  ∀ ⦃r : R⦄ ⦃n : M⦄,
    r ∈ sR →
      n ∈ N →
        r • n ∈
          map (M := Finsupp.{u_2, u_3} R ↥N)
            (N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N))
            (Finsupp.supported (↥N) R sR)
⊢ sR • N =
    map (M := Finsupp.{u_2, u_3} R ↥N)
      (N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N))
      (Finsupp.supported (↥N) R sR)
have le : map (M := Finsupp.{u_2, u_3} R ↥N)
    (N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N))
    (Finsupp.supported (↥N) R sR) ≤
  sR • N
Tactic: classical
  apply set_smul_eq_of_le
  · intro r n hr hn
    exact ⟨Finsupp.single r ⟨n, hn⟩, Finsupp.single_mem_supported _ _ hr, by simp⟩
  · intro x hx
    obtain ⟨c, hc, rfl⟩ := hx
    simp only [LinearMap.coe_comp, coe_subtype, Finsupp.coe_lsum, Finsupp.sum, Function.comp_apply]
    rw [AddSubmonoid.coe_finsetSum]
    refine Submodule.sum_mem (p := sR • N) (t := c.support) ?_ _ ⟨sR • N, ?_⟩
    · rintro r hr
      rw [mem_set_smul_def, Submodule.mem_sInf]
      rintro p hp
      exact hp (hc hr) (c r).2
    · ext x : 1
      simp only [Set.mem_iInter, SetLike.mem_coe]
      fconstructor
      · refine fun h ↦ h fun r n hr hn ↦ ?_
        rw [mem_set_smul_def, mem_sInf]
        exact fun p hp ↦ hp hr hn
      · simp_all
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
x : M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
⊢ x ∈ sR • N ↔
    ∃ (c : Finsupp.{u_2, u_3} R ↥N), (↑c.support : Set R) ⊆ sR ∧ x = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)
have mp : x ∈ sR • N →
  ∃ (c : Finsupp.{u_2, u_3} R ↥N), (↑c.support : Set R) ⊆ sR ∧ x = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
x : M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
mp :
  x ∈ sR • N →
    ∃ (c : Finsupp.{u_2, u_3} R ↥N), (↑c.support : Set R) ⊆ sR ∧ x = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)
⊢ x ∈ sR • N ↔
    ∃ (c : Finsupp.{u_2, u_3} R ↥N), (↑c.support : Set R) ⊆ sR ∧ x = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)
have mpr : (∃ (c : Finsupp.{u_2, u_3} R ↥N), (↑c.support : Set R) ⊆ sR ∧ x = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)) →
  x ∈ sR • N
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (hypothesis)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
x : M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
h : x ∈ sR • N
⊢ ∃ (c : Finsupp.{u_2, u_3} R ↥N), (↑c.support : Set R) ⊆ sR ∧ x = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)
have h₁ : x ∈
  map (M := Finsupp.{u_2, u_3} R ↥N)
    (N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N))
    (Finsupp.supported (↥N) R sR)
Tactic: rw [set_smul_eq_map] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
x : M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
h :
  x ∈
    map (M := Finsupp.{u_2, u_3} R ↥N)
      (N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N))
      (Finsupp.supported (↥N) R sR)
⊢ ∃ (c : Finsupp.{u_2, u_3} R ↥N), (↑c.support : Set R) ⊆ sR ∧ x = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)
have mp : ∀ (c : Finsupp.{u_2, u_3} R ↥N) (hc : c ∈ (↑(Finsupp.supported (↥N) R sR) : Set (R →₀ ↥N))),
  ∃ (c_1 : Finsupp.{u_2, u_3} R ↥N),
    (↑c_1.support : Set R) ⊆ sR ∧
      Eq (α := M)
        ((N.subtype ∘ₗ (Finsupp.lsum R : (a : R → ↥N →ₗ[R] ↥N) → (R →₀ ↥N) →ₗ[R] ↥N) (DistribSMul.toLinearMap R ↥N) :
              (a : R →₀ ↥N) → M)
            c :
          M)
        ((↑(c_1.sum fun (r : R) (m : ↥N) ↦ r • m) : M) : M)
Tactic: obtain ⟨c, hc, rfl⟩ := h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
x : M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
⊢ (∃ (c : Finsupp.{u_2, u_3} R ↥N), (↑c.support : Set R) ⊆ sR ∧ x = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)) →
    x ∈ sR • N
have mpr : (∃ (c : Finsupp.{u_2, u_3} R ↥N), (↑c.support : Set R) ⊆ sR ∧ x = (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M)) →
  ∀ (p : Submodule R M),
    Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p} p →
      x ∈ p
Tactic: rw [mem_set_smul_def, Submodule.mem_sInf]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
sR : Set R
N : Submodule R M
inst_3 : SMulCommClass.{u_2, u_2, u_3} R R ↥N
c : Finsupp.{u_2, u_3} R ↥N
hc1 : (↑c.support : Set R) ⊆ sR
p : Submodule R M
hp : Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p} p
⊢ (↑(c.sum fun (r : R) (m : ↥N) ↦ r • m) : M) ∈ p
have mpr : ∑ i ∈ c.support, (↑(HSMul.hSMul (β := ↥N) i ((c : (a : R) → ↥N) i : ↥N)) : M) ∈ p
Tactic: rw [Finsupp.sum, AddSubmonoid.coe_finsetSum]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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
n : M
w : R
left : w ∈ s
w_1 : R
left_1 : w_1 ∈ t
h : n ∈ x
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((fun (x1 x2 : R) ↦ x1 * x2) w w_1) n ∈ s • t • x
have rw : w • w_1 • n ∈ s • t • x
Tactic: rw [mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (hypothesis)
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
⊢ r • m ∈ (s * t) • x
have this : SMulCommClass.{u_2, u_2, u_3} R R ↥x
Tactic: have : SMulCommClass R R x := ⟨fun r s m => Subtype.ext <| smul_comm _ _ _⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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
⊢ r • m ∈ (s * t) • x
have 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
Tactic: obtain ⟨c, hc1, rfl⟩ := mem_set_smul _ _ _ |>.mp hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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
⊢ HSMul.hSMul (β := M) r (↑(c.sum fun (r : R) (m : ↥x) ↦ r • m) : M) ∈ (s * t) • x
have rw : HSMul.hSMul (β := M) r (∑ i ∈ c.support, (↑(HSMul.hSMul (β := ↥x) i ((c : (a : R) → ↥x) i : ↥x)) : M)) ∈ (s * t) • x
Tactic: rw [Finsupp.sum, AddSubmonoid.coe_finsetSum]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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
⊢ HSMul.hSMul (β := M) r (∑ i ∈ c.support, (↑(HSMul.hSMul (β := ↥x) i ((c : (a : R) → ↥x) i : ↥x)) : M)) ∈ (s * t) • x
have simp : ∑ x_1 ∈ c.support, HSMul.hSMul (β := M) (r * x_1) (↑((c : (a : R) → ↥x) x_1) : M) ∈ (s * t) • x
Tactic: simp only [SetLike.val_smul, Finset.smul_sum, smul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (hypothesis)
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
⊢ r • m ∈ s • x + s • y
have hm₁ : ∃ y_1 ∈ x, ∃ z ∈ y, y_1 + z = m
Tactic: rw [add_eq_sup, Submodule.mem_sup] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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
⊢ r • m ∈ s • x + s • y
have obtain : ∀ (a : M) (ha : a ∈ x) (b : M) (hb : b ∈ y), r • (a + b) ∈ s • x + s • y
Tactic: obtain ⟨a, ha, b, hb, rfl⟩ := hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Finsupp (goal)
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
⊢ r • (a + b) ∈ s • x + s • y
have rw : ∃ y_1 ∈ s • x, ∃ z ∈ s • y, y_1 + z = r • a + r • b
Tactic: rw [smul_add, add_eq_sup, Submodule.mem_sup]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ Membership.mem (γ := Set (Submodule R M)) {p : Submodule R M | p ≤ Submodule.comap f p} (p ⊓ q)
have simp : p ⊓ q ≤ Submodule.comap f p ∧ p ⊓ q ≤ Submodule.comap f q
Tactic: simp only [Set.mem_setOf_eq, Submodule.comap_inf, le_inf_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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 • f).invtSubmodule = f.invtSubmodule
have apply : ((↑c : S) • f).invtSubmodule ≤ f.invtSubmodule
Tactic: apply le_antisymm ?_ (invtSubmodule_le_invtSubmodule_smul f c.1)
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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) • f).invtSubmodule ≤ f.invtSubmodule
have grw : ((↑c⁻¹ : S) • (↑c : S) • f).invtSubmodule ≤ f.invtSubmodule
Tactic: grw [invtSubmodule_le_invtSubmodule_smul (c.1 • f) c⁻¹.1]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ 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
have 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
Tactic: rw [disjoint_iff, disjoint_iff, Sublattice.mk_inf_mk,
    Subtype.mk_eq_bot_iff (⊥ : f.invtSubmodule).property]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ 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
have 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 = ⊥
Tactic: rw [disjoint_iff, disjoint_iff, Sublattice.mk_inf_mk,
    Subtype.mk_eq_bot_iff (⊥ : f.invtSubmodule).property]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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 = ⊥
⊢ 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
have rw₂ : Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) (p ⊓ q) sorry = ⊥ ↔ p ⊓ q = ⊥
Tactic: rw [disjoint_iff, disjoint_iff, Sublattice.mk_inf_mk,
    Subtype.mk_eq_bot_iff (⊥ : f.invtSubmodule).property]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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 = ⊥
⊢ 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
have rw₃ : p ⊓ q = ⊥ ↔ p ⊓ q = ⊥
Tactic: rw [disjoint_iff, disjoint_iff, Sublattice.mk_inf_mk,
    Subtype.mk_eq_bot_iff (⊥ : f.invtSubmodule).property]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ Disjoint p q ↔ Disjoint (↑p : Submodule R M) (↑q : Submodule R M)
have 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)
Tactic: obtain ⟨p, hp⟩ := p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨q, hq⟩ := q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ 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
have 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
Tactic: rw [codisjoint_iff, codisjoint_iff, Sublattice.mk_sup_mk,
    Subtype.mk_eq_top_iff (⊤ : f.invtSubmodule).property]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ 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
have 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 = ⊤
Tactic: rw [codisjoint_iff, codisjoint_iff, Sublattice.mk_sup_mk,
    Subtype.mk_eq_top_iff (⊤ : f.invtSubmodule).property]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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 = ⊤
⊢ 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
have rw₂ : Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) (p ⊔ q) sorry = ⊤ ↔ p ⊔ q = ⊤
Tactic: rw [codisjoint_iff, codisjoint_iff, Sublattice.mk_sup_mk,
    Subtype.mk_eq_top_iff (⊤ : f.invtSubmodule).property]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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 = ⊤
⊢ 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
have rw₃ : p ⊔ q = ⊤ ↔ p ⊔ q = ⊤
Tactic: rw [codisjoint_iff, codisjoint_iff, Sublattice.mk_sup_mk,
    Subtype.mk_eq_top_iff (⊤ : f.invtSubmodule).property]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ Codisjoint p q ↔ Codisjoint (↑p : Submodule R M) (↑q : Submodule R M)
have 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)
Tactic: obtain ⟨p, hp⟩ := p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨q, hq⟩ := q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ IsCompl p q ↔ IsCompl (↑p : Submodule R M) (↑q : Submodule R M)
have obtain : ∀ (p : Submodule R M) (hp : p ∈ f.invtSubmodule),
  IsCompl (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) q ↔
    IsCompl (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) : Submodule R M)
      (↑q : Submodule R M)
Tactic: obtain ⟨p, hp⟩ := p
Cleared hypotheses: p