awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
ι : Sort u_4
s : ι → Submodule R M
h :
  ∀ (x : M),
    Membership.mem (γ := Submodule S M) (restrictScalars S (iInf s)) x ↔
      Membership.mem (γ := Submodule S M) (⨅ (i : ι), restrictScalars S (s i)) x
⊢ Eq (α := Submodule S M) (restrictScalars S (iInf s)) (⨅ (i : ι), restrictScalars S (s i))

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
ι : Sort u_4
s : ι → Submodule R M
x : M
⊢ Membership.mem (γ := Submodule S M) (restrictScalars S (iInf s)) x ↔
    Membership.mem (γ := Submodule S M) (⨅ (i : ι), restrictScalars S (s i)) x

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
ι : Sort u_4
s : ι → Submodule R M
⊢ Eq (α := Submodule S M) (restrictScalars S (iSup s)) (⨆ (i : ι), restrictScalars S (s i))

Tactic:
map_iSup (restrictScalarsLatticeHom S R M) s

Premises used: Set.Mem, Submodule.restrictScalars, setOf, Submodule.restrictScalarsLatticeHom, map_iSup
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
s t : Submodule R M
h :
  ∀ (x : M),
    Membership.mem (γ := Submodule S M) (restrictScalars S (s ⊓ t)) x ↔
      Membership.mem (γ := Submodule S M) (restrictScalars S s ⊓ restrictScalars S t) x
⊢ Eq (α := Submodule S M) (restrictScalars S (s ⊓ t)) (restrictScalars S s ⊓ restrictScalars S t)

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
s t : Submodule R M
x : M
⊢ Membership.mem (γ := Submodule S M) (restrictScalars S (s ⊓ t)) x ↔
    Membership.mem (γ := Submodule S M) (restrictScalars S s ⊓ restrictScalars S t) x

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
s t : Submodule R M
⊢ Eq (α := Submodule S M) (restrictScalars S (s ⊔ t)) (restrictScalars S s ⊔ restrictScalars S t)

Tactic:
simpa [Set.image_insert_eq] using restrictScalars_sSup S (s := {s, t})

Premises used: Insert.insert, Submodule.restrictScalars_sSup, Set.image_insert_eq, Singleton.singleton
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
R : Type u_4
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
⊢ Eq (α := Submodule ℤ M)
    ((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) N.toAddSubgroup : Submodule ℤ M)
    (restrictScalars ℤ N : Submodule ℤ M)

Tactic:
rfl

Premises used: Submodule.restrictScalars, rfl
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
s t : Submodule R M
⊢ Codisjoint (α := Submodule S M) (restrictScalars S s) (restrictScalars S t) ↔ Codisjoint s t

Tactic:
simp [codisjoint_iff, ← restrictScalars_sup]

Premises used: codisjoint_iff, Submodule.restrictScalars_sup
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
s t : Submodule R M
⊢ Disjoint (α := Submodule S M) (restrictScalars S s) (restrictScalars S t) ↔ Disjoint s t

Tactic:
simp [disjoint_def]

Premises used: Submodule.disjoint_def
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
s t : Submodule R M
⊢ IsCompl (α := Submodule S M) (restrictScalars S s) (restrictScalars S t) ↔ IsCompl s t

Tactic:
simp [isCompl_iff]

Premises used: isCompl_iff
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
h₂ : (↑(Finset.card.{u_1} (α := ι) ∅) : ℕ∞) < ENat.card K
⊢ SSubset.{u_3} (α := Set M) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(p i) : Set M)) univ

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hj' : ∀ (h₂ : (↑s.card : ℕ∞) < ENat.card K), SSubset.{u_3} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
h₂ : (↑(Insert.insert j s).card : ℕ∞) < ENat.card K
insert :
  ∀ (hj' : ∀ (h₂ : (↑s.card : ℕ∞) < ENat.card K), Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ),
    Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ Insert.insert j s, (↑(p i) : Set M)) univ
⊢ SSubset.{u_3} (α := Set M) (⋃ i ∈ Insert.insert j s, (↑(p i) : Set M)) univ

Tactic:
simp only [ssubset_univ_iff] at hj' ⊢

Premises used: Set.ssubset_univ_iff
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
h₂ : (↑(Insert.insert j s).card : ℕ∞) < ENat.card K
hj' : ∀ (h₂ : (↑s.card : ℕ∞) < ENat.card K), Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
insert :
  ∀ (hj : j ∉ ∅) (h₂ : (↑(Finset.card (α := ι) (Insert.insert j ∅)) : ℕ∞) < ENat.card K)
    (hj' :
      ∀ (h₂ : (↑(Finset.card.{u_1} (α := ι) ∅) : ℕ∞) < ENat.card K),
        Ne.{u_3 + 1} (α := Set M) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(p i) : Set M)) univ),
    Ne.{u_3 + 1} (α := Set M)
      (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) (Insert.insert j ∅) i), (↑(p i) : Set M)) univ
insert₁ : ∀ (hs : s.Nonempty), Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ Insert.insert j s, (↑(p i) : Set M)) univ
⊢ Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ Insert.insert j s, (↑(p i) : Set M)) univ

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
hj : j ∉ ∅
h₂ : (↑(Finset.card (α := ι) (insert j ∅)) : ℕ∞) < ENat.card K
hj' :
  ∀ (h₂ : (↑(Finset.card.{u_1} (α := ι) ∅) : ℕ∞) < ENat.card K),
    Ne.{u_3 + 1} (α := Set M) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(p i) : Set M)) univ
⊢ Ne.{u_3 + 1} (α := Set M) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) (insert j ∅) i), (↑(p i) : Set M)) univ

Tactic:
simpa using h₁ j
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
h₂ : (↑(insert j s).card : ℕ∞) < ENat.card K
hj' : ∀ (h₂ : (↑s.card : ℕ∞) < ENat.card K), Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
hs : s.Nonempty
⊢ HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K

Tactic:
simpa [Finset.card_insert_of_notMem hj] using h₂

Premises used: Finset.card_insert_of_notMem
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
h₂ : (↑(insert j s).card : ℕ∞) < ENat.card K
hj' : ∀ (h₂ : (↑s.card : ℕ∞) < ENat.card K), Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
hs : s.Nonempty
⊢ HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K

Tactic:
replace h₂ : s.card + 1 < ENat.card K := by simpa [Finset.card_insert_of_notMem hj] using h₂
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hj' : ∀ (h₂ : (↑s.card : ℕ∞) < ENat.card K), Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
⊢ Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ

Tactic:
specialize hj' (lt_trans ENat.natCast_lt_succ h₂)

Premises used: lt_trans, ENat.natCast_lt_succ
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
insert :
  ∀ (hj' : Eq.{u_3 + 1} (α := Set M) (⋃ i ∈ Insert.insert j s, (↑(p i) : Set M)) univ),
    Eq.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
⊢ Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ Insert.insert j s, (↑(p i) : Set M)) univ

Tactic:
contrapose hj'
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : Eq.{u_3 + 1} (α := Set M) (⋃ i ∈ insert j s, (↑(p i) : Set M)) univ
⊢ (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ

Tactic:
simpa only [Finset.mem_insert, iUnion_iUnion_eq_or_left] using hj'

Premises used: Finset.mem_insert, Set.iUnion_iUnion_eq_or_left
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : Eq.{u_3 + 1} (α := Set M) (⋃ i ∈ insert j s, (↑(p i) : Set M)) univ
⊢ (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ

Tactic:
replace hj' : (p j : Set M) ∪ (⋃ i ∈ s, p i) = univ := by
      simpa only [Finset.mem_insert, iUnion_iUnion_eq_or_left] using hj'
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
this : (↑(p j) : Set M) ⊆ ⋃ i ∈ s, (↑(p i) : Set M)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hj' : Eq.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ)
    (this : (↑(p j) : Set M) ⊆ ⋃ i ∈ s, (↑(p i) : Set M)), Eq.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
⊢ Eq.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ

Tactic:
rwa [union_eq_right.mpr this] at hj'

Premises used: Iff.mpr, Set.union_eq_right
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
insert : (↑(p j) : Set M) ⊆ ⋃ i ∈ s, (↑(p i) : Set M)
⊢ Eq.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ

Tactic:
suffices (p j : Set M) ⊆ ⋃ i ∈ s, p i by rwa [union_eq_right.mpr this] at hj'
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
insert : ∀ (hx : x ∈ p j), Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x
⊢ x ∈ (↑(p j) : Set M) → Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x

Tactic:
(hx : x ∈ p j)
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
insert : ∀ (hx : 0 ∈ p j), Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) 0
insert₁ : ∀ (hx₀ : x ≠ 0), Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x
⊢ Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x

Tactic:
rcases eq_or_ne x 0 with rfl | hx₀

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
hx : 0 ∈ p j
⊢ Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) 0

Tactic:
simpa using hs
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
⊢ p j ≠ ⊤

Tactic:
specialize h₁ j
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
h₁ : p j ≠ ⊤
contrapose! : ∀ (h₁ : ∀ (y : M), y ∈ p j), p j = ⊤
⊢ ∃ (y : M), y ∉ p j

Tactic:
contrapose! h₁
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
h₁ : ∀ (y : M), y ∈ p j
h : ∀ (x : M), x ∈ p j ↔ Membership.mem (γ := Submodule K M) ⊤ x
⊢ p j = ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
h₁ : ∀ (y : M), y ∈ p j
x_1 : M
⊢ x_1 ∈ p j ↔ Membership.mem (γ := Submodule K M) ⊤ x_1

Tactic:
simp [h₁]
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
insert : ∀ (y : M) (hy : y ∉ p j), Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x
⊢ Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x

Tactic:
obtain ⟨y, hy⟩ : ∃ y, y ∉ p j := by specialize h₁ j; contrapose! h₁; ext; simp [h₁]
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
⊢ y ≠ 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
⊢ y ≠ 0

Tactic:
have hy₀ : y ≠ 0 := by aesop
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 : M | ∃ (t : K) (_ : t ≠ 0), x + t • y = x_1}
suffices : Disjoint sxy (↑(p j) : Set M)
⊢ sxy ⊆ ⋃ i ∈ s, (↑(p i) : Set M)

Tactic:
suffices Disjoint sxy (p j) from this.subset_right_of_subset_union <| hj' ▸ sxy.subset_univ
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 : M | ∃ (t : K) (_ : t ≠ 0), x + t • y = x_1}
rw : sxy ∩ (↑(p j) : Set M) ⊆ ∅
⊢ Disjoint sxy (↑(p j) : Set M)

Tactic:
rw [Set.disjoint_iff]

Premises used: Set.disjoint_iff
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 : M | ∃ (t : K) (_ : t ≠ 0), x + t • y = x_1}
t : K
ht₀ : t ≠ 0
ht : x + t • y ∈ p j
⊢ y ∈ p j

Tactic:
rw [(p j).add_mem_iff_right hx, (p j).smul_mem_iff ht₀] at ht

Premises used: Submodule.smul_mem_iff, Submodule.add_mem_iff_right
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 : M | ∃ (t : K) (_ : t ≠ 0), x + t • y = x_1}
t : K
ht₀ : t ≠ 0
ht : y ∈ p j
⊢ Membership.mem (γ := Set M) ∅ (x + t • y)

Tactic:
contradiction
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 : M | ∃ (t : K) (_ : t ≠ 0), x + t • y = x_1}
⊢ sxy ⊆ ⋃ i ∈ s, (↑(p i) : Set M)

Tactic:
have hsxy : sxy ⊆ ⋃ i ∈ s, p i := by
      suffices Disjoint sxy (p j) from this.subset_right_of_subset_union <| hj' ▸ sxy.subset_univ
      rw [Set.disjoint_iff]
      rintro - ⟨⟨t, ht₀, rfl⟩, ht : x + t • y ∈ p j⟩
      rw [(p j).add_mem_iff_right hx, (p j).smul_mem_iff ht₀] at ht
      contradiction
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 : M | ∃ (t : K) (_ : t ≠ 0), x + t • y = x_1}
hsxy : sxy ⊆ ⋃ i ∈ s, (↑(p i) : Set M)
this : ∃ k ∈ s, ∃ z₁ ∈ sxy, ∃ z₂ ∈ sxy, z₁ ≠ z₂ ∧ z₁ ∈ p k ∧ z₂ ∈ p k
obtain :
  ∀ (k : ι) (hk : k ∈ s) (t₁ t₂ : K) (htne : x + t₁ • y ≠ x + t₂ • y) (ht₁ : x + t₁ • y ∈ p k) (ht₂ : x + t₂ • y ∈ p k),
    ∃ k ∈ s, ∃ (t₁ : K) (t₂ : K), t₁ ≠ t₂ ∧ x + t₁ • y ∈ p k ∧ x + t₂ • y ∈ p k
⊢ ∃ k ∈ s, ∃ (t₁ : K) (t₂ : K), t₁ ≠ t₂ ∧ x + t₁ • y ∈ p k ∧ x + t₂ • y ∈ p k

Tactic:
obtain ⟨k, hk, -, ⟨t₁, -, rfl⟩, -, ⟨t₂, -, rfl⟩, htne, ht₁, ht₂⟩ := this

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 : M | ∃ (t : K) (_ : t ≠ 0), x + t • y = x_1}
hsxy : sxy ⊆ ⋃ i ∈ s, (↑(p i) : Set M)
k : ι
hk : k ∈ s
t₁ t₂ : K
htne : x + t₁ • y ≠ x + t₂ • y
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
⊢ t₁ ≠ t₂

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 : M | ∃ (t : K) (_ : t ≠ 0), x + t • y = x_1}
hsxy : sxy ⊆ ⋃ i ∈ s, (↑(p i) : Set M)
k : ι
hk : k ∈ s
t₁ t₂ : K
htne : x + t₁ • y ≠ x + t₂ • y
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
⊢ ∃ k ∈ s, ∃ (t₁ : K) (t₂ : K), t₁ ≠ t₂ ∧ x + t₁ • y ∈ p k ∧ x + t₂ • y ∈ p k

Tactic:
exact ⟨k, hk, t₁, t₂, by aesop, ht₁, ht₂⟩
-- Module: Mathlib.Algebra.Module.Submodule.Union
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 : M | ∃ (t : K) (_ : t ≠ 0), x + t • y = x_1}
hsxy : sxy ⊆ ⋃ i ∈ s, (↑(p i) : Set M)
suffices : ∃ k ∈ s, ∃ z₁ ∈ sxy, ∃ z₂ ∈ sxy, z₁ ≠ z₂ ∧ z₁ ∈ p k ∧ z₂ ∈ p k
⊢ ∃ k ∈ s, ∃ (t₁ : K) (t₂ : K), t₁ ≠ t₂ ∧ x + t₁ • y ∈ p k ∧ x + t₂ • y ∈ p k

Tactic:
suffices ∃ᵉ (k ∈ s) (z₁ ∈ sxy) (z₂ ∈ sxy), z₁ ≠ z₂ ∧ z₁ ∈ p k ∧ z₂ ∈ p k by
        obtain ⟨k, hk, -, ⟨t₁, -, rfl⟩, -, ⟨t₂, -, rfl⟩, htne, ht₁, ht₂⟩ := this
        exact ⟨k, hk, t₁, t₂, by aesop, ht₁, ht₂⟩