awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
succ : (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = f.iterateMapComap i (n + 1 + 1) K
succ₁ :
  (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1 + 1] K
succ₂ :
  ((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n]) K =
    (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1 + 1] K
succ₃ :
  Eq (α := Submodule R N)
    (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n]) K)
    (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1]) K)
succ₄ :
  comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n] K)) =
    ((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1]) K
succ₅ :
  comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n] K)) =
    comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K))
succ₆ :
  comap f (map i (f.iterateMapComap i n K)) = comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K))
succ₇ : comap f (map i (f.iterateMapComap i n K)) = comap f (map i (f.iterateMapComap i (n + 1) K))
succ₈ succ₉ : comap f (map i (f.iterateMapComap i (n + 1) K)) = comap f (map i (f.iterateMapComap i (n + 1) K))
⊢ f.iterateMapComap i (n + 1) K = f.iterateMapComap i (n + 1 + 1) K

Tactic:
rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ',
      Function.comp_apply, Function.comp_apply, ← iterateMapComap, ← iterateMapComap, ih]

Premises used: Function.iterate_succ', LinearMap.iterateMapComap, Function.comp_apply
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
n : ℕ
zero : f.iterateMapComap i 0 K = f.iterateMapComap i (HAdd.hAdd (α := ℕ) 0 1) K
succ :
  ∀ (n : ℕ) (ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K),
    f.iterateMapComap i (n + 1) K = f.iterateMapComap i (n + 1 + 1) K
⊢ f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K

Tactic:
induction n with
  | zero =>
    contrapose! heq
    induction m with
    | zero => exact heq
    | succ m ih =>
      rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ']
      exact fun H ↦ ih (map_injective_of_injective hi (comap_injective_of_surjective hf H))
  | succ n ih =>
    rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ',
      Function.comp_apply, Function.comp_apply, ← iterateMapComap, ← iterateMapComap, ih]

Premises used: Function.iterate_succ', LinearMap.iterateMapComap, Submodule.zero, Function.comp_apply
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
rw : f.ker ≤ f.iterateMapComap i (HAdd.hAdd (α := ℕ) 0 1) K
⊢ f.ker ≤ K

Tactic:
rw [show K = _ from f.iterateMapComap_eq_succ i K m heq hf hi 0]

Premises used: OfNat.ofNat, LinearMap.iterateMapComap_eq_succ
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
⊢ f.ker ≤ f.iterateMapComap i (HAdd.hAdd (α := ℕ) 0 1) K

Tactic:
f.ker_le_comap

Premises used: Set.Mem, LinearMap.ker_le_comap
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
⊢ f.ker ≤ f.iterateMapComap i (HAdd.hAdd (α := ℕ) 0 1) K

Tactic:
exact f.ker_le_comap

Premises used: LinearMap.ker_le_comap
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
p q : Submodule R M
⊢ ∀ (c : R) {x : M}, Membership.mem (γ := Set M) {0} x → Membership.mem (γ := Set M) {0} (c • x)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ (↑⊥ : Set M) = {0}

Tactic:
rfl

Premises used: setOf, Set.singleton, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{u_3 + 1} (α := AddSubmonoid M) (toAddSubmonoid.{u_1, u_3} (R := R) ⊥) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_4
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq.{u_5 + 1} (α := AddSubgroup M) (toAddSubgroup.{u_4, u_5} (R := R) (module_M := inst_2) ⊥) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ Membership.mem (γ := Submodule R M) ⊥ x ↔ x = 0

Tactic:
Set.mem_singleton_iff

Premises used: Set.Mem, setOf, Set.mem_singleton_iff, Set.singleton
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
carrier : AddSubmonoid M
smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier.carrier → c • x ∈ carrier.carrier
⊢ { toAddSubmonoid := carrier, smul_mem' := smul_mem' : Submodule R M } = ⊥ ↔ carrier = ⊥

Tactic:
simp [← toAddSubmonoid_inj]

Premises used: Submodule.toAddSubmonoid_inj
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
p_1 q p : Submodule R M
x : M
⊢ Membership.mem (γ := Submodule R M) ⊥ x → x ∈ p

Tactic:
simp +contextual [zero_mem]

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ p = ⊥ ↔ ∀ x ∈ p, x = 0

Tactic:
⟨fun h ↦ h.symm ▸ fun _ hx ↦ (mem_bot R).mp hx,
    fun h ↦ eq_bot_iff.mpr fun x hx ↦ (mem_bot R).mpr (h x hx)⟩

Premises used: Iff.mpr, Submodule.mem_bot, Eq.rec, Iff.intro, Iff.mp, eq_bot_iff, Eq.symm
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : ↥⊥
⊢ x = y

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ p ≠ ⊥ ↔ ∃ x ∈ p, x ≠ 0

Tactic:
simp only [ne_eq, p.eq_bot_iff, not_forall, exists_prop]

Premises used: exists_prop, ne_eq, Submodule.eq_bot_iff, Classical.not_forall
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
bot_lt : ⊥ < p
⊢ ∃ (a : ↥p), a ≠ 0

Tactic:
let ⟨b, hb₁, hb₂⟩ := p.ne_bot_iff.mp bot_lt.ne'
  ⟨⟨b, hb₁⟩, hb₂ ∘ congr_arg Subtype.val⟩

Premises used: Function.comp, Exists, Ne, _private.0.Submodule.nonzero_mem_of_bot_lt.match_1, Subtype.mk, congr_arg, LT.lt.ne', Submodule.ne_bot_iff, Exists.intro, Iff.mp, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h : p ≠ ⊥
⊢ ∃ b ∈ p, b ≠ 0

Tactic:
let ⟨b, hb₁, hb₂⟩ := p.ne_bot_iff.mp h
  ⟨b, hb₁, hb₂⟩

Premises used: Membership.mem, Exists, Ne, _private.0.Submodule.nonzero_mem_of_bot_lt.match_1, And, And.intro, Submodule.ne_bot_iff, Exists.intro, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
rw : (∀ (x y : ↥p), x = y) ↔ ∀ x ∈ p, x = 0
⊢ Subsingleton.{u_3 + 1} ↥p ↔ p = ⊥

Tactic:
rw [subsingleton_iff, Submodule.eq_bot_iff]

Premises used: subsingleton_iff, Submodule.eq_bot_iff
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h : ∀ (x y : ↥p), x = y
x : M
hx : x ∈ p
⊢ x = 0

Tactic:
simpa using h ⟨x, hx⟩ ⟨0, p.zero_mem⟩

Premises used: Subtype.mk, Submodule.zero_mem, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h : ∀ x ∈ p, x = 0
x_1 x_2 : ↥p
x : M
hx : x ∈ p
y : M
hy : y ∈ p
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx = Subtype.mk (p := fun (x : M) ↦ x ∈ p) y hy

Tactic:
simp [h x hx, h y hy]
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ (∀ (x y : ↥p), x = y) ↔ ∀ x ∈ p, x = 0

Tactic:
refine ⟨fun h x hx ↦ by simpa using h ⟨x, hx⟩ ⟨0, p.zero_mem⟩,
    fun h ⟨x, hx⟩ ⟨y, hy⟩ ↦ by simp [h x hx, h y hy]⟩
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
inst_3 : Subsingleton.{u_3 + 1} ↥p
⊢ p = ⊥

Tactic:
subsingleton_iff_eq_bot.mp inferInstance

Premises used: Submodule.subsingleton_iff_eq_bot, inferInstance, Iff.mp
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
rw : p = ⊥ ↔ ¬Nontrivial.{u_3} ↥p
rw₁ : p = ⊥ ↔ Subsingleton.{u_3 + 1} ↥p
rw₂ rw₃ : p = ⊥ ↔ p = ⊥
⊢ Nontrivial.{u_3} ↥p ↔ p ≠ ⊥

Tactic:
rw [iff_not_comm, not_nontrivial_iff_subsingleton, subsingleton_iff_eq_bot]

Premises used: Submodule.subsingleton_iff_eq_bot, iff_not_comm, not_nontrivial_iff_subsingleton
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ (↑⊤ : Set M) = Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
rw : p = ⊤ ↔ (↑p : Set M) = Set.univ
rw₁ : (↑p : Set M) = (↑⊤ : Set M) ↔ (↑p : Set M) = Set.univ
rw₂ rw₃ : (↑p : Set M) = Set.univ ↔ (↑p : Set M) = Set.univ
⊢ (↑p : Set M) = Set.univ ↔ p = ⊤

Tactic:
rw [iff_comm, ← SetLike.coe_set_eq, top_coe]

Premises used: iff_comm, SetLike.coe_set_eq, Submodule.top_coe
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ Membership.mem (γ := Submodule R M) ⊤ x

Tactic:
trivial

Premises used: trivial, Set.Mem, Set.univ, setOf
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{u_3 + 1} (α := AddSubmonoid M) (toAddSubmonoid.{u_1, u_3} (R := R) ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_4
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq.{u_5 + 1} (α := AddSubgroup M) (toAddSubgroup.{u_4, u_5} (R := R) (module_M := inst_2) ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_4
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
⊢ p.toAddSubgroup = ⊤ ↔ p = ⊤

Tactic:
simp [← toAddSubgroup_inj]

Premises used: Submodule.toAddSubgroup_inj
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
carrier : AddSubmonoid M
smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier.carrier → c • x ∈ carrier.carrier
⊢ { toAddSubmonoid := carrier, smul_mem' := smul_mem' : Submodule R M } = ⊤ ↔ carrier = ⊤

Tactic:
simp [← toAddSubmonoid_inj]

Premises used: Submodule.toAddSubmonoid_inj
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ p = ⊤ ↔ ∀ (x : M), x ∈ p

Tactic:
eq_top_iff.trans ⟨fun h _ ↦ h trivial, fun h x _ ↦ h x⟩

Premises used: trivial, eq_top_iff, Iff.intro, Iff.trans
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
S_1 : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S_1
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S_1 M
inst_5 : SMul S_1 R
inst_6 : IsScalarTower S_1 R M
p q : Submodule R M
S : Set (Submodule R M)
⊢ ∀ {a b : M},
    Membership.mem (γ := Set M) (⋂ s ∈ S, (↑s : Set M)) a →
      Membership.mem (γ := Set M) (⋂ s ∈ S, (↑s : Set M)) b →
        Membership.mem (γ := Set M) (⋂ s ∈ S, (↑s : Set M)) (a + b)

Tactic:
simp +contextual [add_mem]

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
S_1 : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S_1
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S_1 M
inst_5 : SMul S_1 R
inst_6 : IsScalarTower S_1 R M
p q : Submodule R M
S : Set (Submodule R M)
⊢ Membership.mem (γ := Set M) (⋂ s ∈ S, (↑s : Set M)) 0

Tactic:
simp [zero_mem]

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
S_1 : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S_1
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S_1 M
inst_5 : SMul S_1 R
inst_6 : IsScalarTower S_1 R M
p q : Submodule R M
S : Set (Submodule R M)
⊢ ∀ (c : R) {x : M},
    Membership.mem (γ := Set M) (⋂ s ∈ S, (↑s : Set M)) x → Membership.mem (γ := Set M) (⋂ s ∈ S, (↑s : Set M)) (c • x)

Tactic:
simp +contextual [smul_mem]

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set (Submodule R M)
⊢ IsGLB S (sInf S)

Tactic:
.of_image SetLike.coe_subset_coe isGLB_biInf

Premises used: IsGLB.of_image, isGLB_biInf, SetLike.coe_subset_coe
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
p_1 q_1 p q : Submodule R M
⊢ ∀ {a b : M}, a ∈ (↑p : Set M) ∩ (↑q : Set M) → b ∈ (↑p : Set M) ∩ (↑q : Set M) → a + b ∈ (↑p : Set M) ∩ (↑q : Set M)

Tactic:
simp +contextual [add_mem]

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
p_1 q_1 p q : Submodule R M
⊢ 0 ∈ (↑p : Set M) ∩ (↑q : Set M)

Tactic:
simp [zero_mem]

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
p_1 q_1 p q : Submodule R M
⊢ ∀ (c : R) {x : M}, x ∈ (↑p : Set M) ∩ (↑q : Set M) → c • x ∈ (↑p : Set M) ∩ (↑q : Set M)

Tactic:
simp +contextual [smul_mem]

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
⊢ (↑(p ⊓ q) : Set M) = (↑p : Set M) ∩ (↑q : Set M)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
x : M
⊢ x ∈ p ⊓ q ↔ x ∈ p ∧ x ∈ q

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : Set (Submodule R M)
⊢ (↑(sInf P) : Set M) = ⋂ p ∈ P, (↑p : Set M)

Tactic:
rfl

Premises used: iInf, Set.iInter, setOf, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ (↑(s.inf p) : Set M) = ⋂ i ∈ s, (↑(p i) : Set M)

Tactic:
s.induction_on ?_ fun i s _ ih ↦ ?_

Premises used: Finset.induction_on
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
refine_1 : (↑(Finset.inf ∅ p) : Set M) = ⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(p i) : Set M)
refine_2 :
  ∀ (i : ι) (s : Finset ι),
    i ∉ s →
      ∀ (ih : (↑(s.inf p) : Set M) = ⋂ i ∈ s, (↑(p i) : Set M)),
        (↑((insert i s).inf p) : Set M) = ⋂ i_1 ∈ insert i s, (↑(p i_1) : Set M)
⊢ (↑(s.inf p) : Set M) = ⋂ i ∈ s, (↑(p i) : Set M)

Tactic:
refine s.induction_on ?_ fun i s _ ih ↦ ?_
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ (↑(Finset.inf ∅ p) : Set M) = ⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(p i) : Set M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
s_1 : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
h : i ∉ s
ih : (↑(s.inf p) : Set M) = ⋂ i ∈ s, (↑(p i) : Set M)
refine_2 : (↑(p i) : Set M) ∩ ⋂ i ∈ s, (↑(p i) : Set M) = ⋂ i_1 ∈ insert i s, (↑(p i_1) : Set M)
⊢ (↑((insert i s).inf p) : Set M) = ⋂ i_1 ∈ insert i s, (↑(p i_1) : Set M)

Tactic:
rw [Finset.inf_insert, coe_inf, ih]

Premises used: Finset.inf_insert, Submodule.coe_inf
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
s_1 : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
h : i ∉ s
ih : (↑(s.inf p) : Set M) = ⋂ i ∈ s, (↑(p i) : Set M)
⊢ (↑(p i) : Set M) ∩ ⋂ i ∈ s, (↑(p i) : Set M) = ⋂ i_1 ∈ insert i s, (↑(p i_1) : Set M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Sort u_4
p : ι → Submodule R M
⊢ Eq.{u_3 + 1} (α := Set M)
    (⋂ (p_1 : Submodule R M),
      ⋂ (_ : Membership.mem (γ := Set (Submodule R M)) (Set.range fun (i : ι) ↦ p i) p_1), (↑p_1 : Set M))
    (⋂ (i : ι), (↑(p i) : Set M))

Tactic:
simp only [Set.mem_range, Set.iInter_exists, Set.iInter_iInter_eq']

Premises used: Set.mem_range, Set.iInter_exists, Set.iInter_iInter_eq'
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set (Submodule R M)
x : M
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
Set.mem_iInter₂

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.mem_iInter₂
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Sort u_4
p : ι → Submodule R M
x : M
rw : (∀ (i : ι), x ∈ (↑(p i) : Set M)) ↔ ∀ (i : ι), x ∈ p i
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ι), p i) x ↔ ∀ (i : ι), x ∈ p i

Tactic:
rw [← SetLike.mem_coe, coe_iInf, Set.mem_iInter]

Premises used: Set.mem_iInter, Submodule.coe_iInf, SetLike.mem_coe
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Sort u_4
p : ι → Submodule R M
x : M
⊢ (∀ (i : ι), x ∈ (↑(p i) : Set M)) ↔ ∀ (i : ι), x ∈ p i

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
x : M
⊢ x ∈ s.inf p ↔ ∀ i ∈ s, x ∈ p i

Tactic:
simp only [← SetLike.mem_coe, coe_finsetInf, Set.mem_iInter]

Premises used: Submodule.coe_finsetInf, Set.mem_iInter, SetLike.mem_coe
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Sort u_4
inst_3 : Nonempty ι
p : ι → Submodule R M
q : Submodule R M
⊢ (↑(q ⊓ ⨅ (i : ι), p i) : Set M) = (↑(⨅ (i : ι), q ⊓ p i) : Set M)

Tactic:
simpa only [coe_inf, coe_iInf] using Set.inter_iInter _ _

Premises used: Submodule.coe_iInf, Submodule.coe_inf, Set.inter_iInter
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
⊢ S ≤ S ⊔ T

Tactic:
have : S ≤ S ⊔ T := le_sup_left
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
this : S ≤ S ⊔ T
⊢ (Preorder.toLE : LE (Submodule R M)).1 S (S ⊔ T)

Tactic:
rw [LE.le] at this

Premises used: LE.le
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
this : (Preorder.toLE : LE (Submodule R M)).1 S (S ⊔ T)
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Tactic:
this
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
this : (Preorder.toLE : LE (Submodule R M)).1 S (S ⊔ T)
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Tactic:
exact this
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
⊢ T ≤ S ⊔ T

Tactic:
have : T ≤ S ⊔ T := le_sup_right
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
this : T ≤ S ⊔ T
⊢ (Preorder.toLE : LE (Submodule R M)).1 T (S ⊔ T)

Tactic:
rw [LE.le] at this

Premises used: LE.le