awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ht : t₁ ≠ t₂
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
⊢ x + t₁ • y - (x + t₂ • y) ∈ p k

Tactic:
sub_mem ht₁ ht₂

Premises used: sub_mem
-- 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
ht : t₁ ≠ t₂
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
h : (t₁ - t₂) • y = x + t₁ • y - (x + t₂ • y)
⊢ (t₁ - t₂) • y ∈ p k

Tactic:
convert! sub_mem ht₁ ht₂ using 1

Premises used: sub_mem
-- 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
ht : t₁ ≠ t₂
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
⊢ (t₁ - t₂) • y = x + t₁ • y - (x + t₂ • y)

Tactic:
module
-- 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
ht : t₁ ≠ t₂
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
⊢ (t₁ - t₂) • y ∈ p k

Tactic:
have : (t₁ - t₂) • y ∈ p k := by convert! sub_mem ht₁ ht₂ using 1; module
-- 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
ht : t₁ ≠ t₂
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
this : (t₁ - t₂) • y ∈ p k
⊢ y ∈ p k

Tactic:
((p k).smul_mem_iff ?_).mp this

Premises used: Submodule.smul_mem_iff, Iff.mp
-- 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
ht : t₁ ≠ t₂
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
this : (t₁ - t₂) • y ∈ p k
refine : t₁ - t₂ ≠ 0
⊢ y ∈ p k

Tactic:
refine ((p k).smul_mem_iff ?_).mp this

Premises used: Submodule.smul_mem_iff, Iff.mp
-- 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
ht : t₁ ≠ t₂
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
this : (t₁ - t₂) • y ∈ p k
rwa rwa₁ rwa₂ rwa₃ : t₁ ≠ t₂
⊢ t₁ - t₂ ≠ 0

Tactic:
rwa [sub_ne_zero]

Premises used: sub_ne_zero
-- 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
ht : t₁ ≠ t₂
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
⊢ y ∈ p k

Tactic:
replace ht : y ∈ p k := by
      have : (t₁ - t₂) • y ∈ p k := by convert! sub_mem ht₁ ht₂ using 1; module
      refine ((p k).smul_mem_iff ?_).mp this
      rwa [sub_ne_zero]
-- 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
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
ht : y ∈ p k
⊢ x + t₁ • y - t₁ • y ∈ p k

Tactic:
sub_mem ht₁ ((p k).smul_mem t₁ ht)

Premises used: sub_mem, Submodule.smul_mem
-- 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
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
ht : y ∈ p k
h : x = x + t₁ • y - t₁ • y
⊢ x ∈ p k

Tactic:
convert! sub_mem ht₁ ((p k).smul_mem t₁ ht)

Premises used: sub_mem, Submodule.smul_mem
-- 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
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
ht : y ∈ p k
⊢ x = x + t₁ • y - t₁ • y

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
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
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
ht : y ∈ p k
⊢ x ∈ p k

Tactic:
replace ht : x ∈ p k := by convert! sub_mem ht₁ ((p k).smul_mem t₁ ht); 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
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
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
ht : x ∈ p k
⊢ Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x

Tactic:
simpa using ⟨k, hk, 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
inst_3 : Finite ι
inst_4 : Infinite K
p : ι → Submodule K M
h : ∀ (i : ι), p i ≠ ⊤
_i : Fintype ι := Fintype.ofFinite ι
this : SSubset.{u_3} (α := Set M) (⋃ (i : ι), (↑(p i) : Set M)) univ
⊢ ∃ (x : M), ∀ (i : ι), x ∉ p i

Tactic:
simpa [ssubset_univ_iff, iUnion_eq_univ_iff] using this

Premises used: Set.iUnion_eq_univ_iff, 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
inst_3 : Finite ι
inst_4 : Infinite K
p : ι → Submodule K M
h : ∀ (i : ι), p i ≠ ⊤
_i : Fintype ι := Fintype.ofFinite ι
suffices : SSubset.{u_3} (α := Set M) (⋃ (i : ι), (↑(p i) : Set M)) univ
⊢ ∃ (x : M), ∀ (i : ι), x ∉ p i

Tactic:
suffices ⋃ i, (p i : Set M) ⊂ univ by simpa [ssubset_univ_iff, iUnion_eq_univ_iff] using this
-- 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
inst_3 : Finite ι
inst_4 : Infinite K
p : ι → Submodule K M
h : ∀ (i : ι), p i ≠ ⊤
_i : Fintype ι := Fintype.ofFinite ι
⊢ (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℕ∞) < ENat.card K

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
inst_3 : Finite ι
inst_4 : Infinite K
p : ι → Submodule K M
h : ∀ (i : ι), p i ≠ ⊤
_i : Fintype ι := Fintype.ofFinite ι
⊢ SSubset.{u_3} (α := Set M) (⋃ (i : ι), (↑(p i) : Set M)) univ

Tactic:
simpa using iUnion_ssubset_of_forall_ne_top_of_card_lt Finset.univ p h (by simp)

Premises used: Submodule.iUnion_ssubset_of_forall_ne_top_of_card_lt, Finset.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
inst_3 : Finite ι
inst_4 : Infinite K
f : ι → Dual K M
h : ∀ (i : ι), ∃ (x : M), Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
p : (i : ι) → Submodule K M := fun (i : ι) ↦ LinearMap.ker (f i)
i : ι
⊢ ∃ (x : M), Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)

Tactic:
specialize h i
-- 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
inst_3 : Finite ι
inst_4 : Infinite K
f : ι → Dual K M
p : (i : ι) → Submodule K M := fun (i : ι) ↦ LinearMap.ker (f i)
i : ι
h : ∃ (x : M), Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
⊢ p i ≠ ⊤

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
inst_3 : Finite ι
inst_4 : Infinite K
f : ι → Dual K M
h : ∀ (i : ι), ∃ (x : M), Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
p : (i : ι) → Submodule K M := fun (i : ι) ↦ LinearMap.ker (f i)
⊢ ∀ (i : ι), p i ≠ ⊤

Tactic:
replace h i : p i ≠ ⊤ := by specialize h i; 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
inst_3 : Finite ι
inst_4 : Infinite K
f : ι → Dual K M
p : (i : ι) → Submodule K M := fun (i : ι) ↦ LinearMap.ker (f i)
h : ∀ (i : ι), p i ≠ ⊤
obtain :
  ∀ (x : M) (hx : ∀ (i : ι), x ∉ p i), ∃ (x : M), ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
⊢ ∃ (x : M), ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)

Tactic:
obtain ⟨x, hx⟩ := Submodule.exists_forall_notMem_of_forall_ne_top p h

Premises used: Submodule.exists_forall_notMem_of_forall_ne_top
-- 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
inst_3 : Finite ι
inst_4 : Infinite K
f : ι → Dual K M
p : (i : ι) → Submodule K M := fun (i : ι) ↦ LinearMap.ker (f i)
h : ∀ (i : ι), p i ≠ ⊤
x : M
hx : ∀ (i : ι), x ∉ p i
⊢ ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)

Tactic:
simpa [p] using hx
-- 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
inst_3 : Finite ι
inst_4 : Infinite K
f : ι → Dual K M
p : (i : ι) → Submodule K M := fun (i : ι) ↦ LinearMap.ker (f i)
h : ∀ (i : ι), p i ≠ ⊤
x : M
hx : ∀ (i : ι), x ∉ p i
⊢ ∃ (x : M), ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)

Tactic:
exact ⟨x, by simpa [p] using hx⟩
-- 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
inst_3 : Finite ι
inst_4 : Infinite K
p : Submodule K M
f : ι → Dual K M
h : ∀ (i : ι), ∃ x ∈ p, Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
f' : (i : ι) → Dual.{u_2, u_3} K ↥p := fun (i : ι) ↦ LinearMap.domRestrict (f i) p
i : ι
obtain :
  ∀ (x : M) (hxp : x ∈ p) (hx₀ : Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)),
    ∃ (x : ↥p), Ne.{u_2 + 1} (α := K) ((f' i : (a : ↥p) → K) x : K) (0 : K)
⊢ ∃ (x : ↥p), Ne.{u_2 + 1} (α := K) ((f' i : (a : ↥p) → K) x : K) (0 : K)

Tactic:
obtain ⟨x, hxp, hx₀⟩ := h i
-- 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
inst_3 : Finite ι
inst_4 : Infinite K
p : Submodule K M
f : ι → Dual K M
h : ∀ (i : ι), ∃ x ∈ p, Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
f' : (i : ι) → Dual.{u_2, u_3} K ↥p := fun (i : ι) ↦ LinearMap.domRestrict (f i) p
i : ι
x : M
hxp : x ∈ p
hx₀ : Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
⊢ ∃ (x : ↥p), Ne.{u_2 + 1} (α := K) ((f' i : (a : ↥p) → K) x : K) (0 : K)

Tactic:
⟨⟨x, hxp⟩, hx₀⟩

Premises used: Subtype.mk, Exists.intro
-- 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
inst_3 : Finite ι
inst_4 : Infinite K
p : Submodule K M
f : ι → Dual K M
h : ∀ (i : ι), ∃ x ∈ p, Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
f' : (i : ι) → Dual.{u_2, u_3} K ↥p := fun (i : ι) ↦ LinearMap.domRestrict (f i) p
i : ι
x : M
hxp : x ∈ p
hx₀ : Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
⊢ ∃ (x : ↥p), Ne.{u_2 + 1} (α := K) ((f' i : (a : ↥p) → K) x : K) (0 : K)

Tactic:
exact ⟨⟨x, hxp⟩, hx₀⟩
-- 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
inst_3 : Finite ι
inst_4 : Infinite K
p : Submodule K M
f : ι → Dual K M
h : ∀ (i : ι), ∃ x ∈ p, Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
f' : (i : ι) → Dual.{u_2, u_3} K ↥p := fun (i : ι) ↦ LinearMap.domRestrict (f i) p
⊢ ∀ (i : ι), ∃ (x : ↥p), Ne.{u_2 + 1} (α := K) ((f' i : (a : ↥p) → K) x : K) (0 : K)

Tactic:
replace h (i : ι) : ∃ x : p, f' i x ≠ 0 := by obtain ⟨x, hxp, hx₀⟩ := h i; exact ⟨⟨x, hxp⟩, hx₀⟩
-- 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
inst_3 : Finite ι
inst_4 : Infinite K
p : Submodule K M
f : ι → Dual K M
f' : (i : ι) → Dual.{u_2, u_3} K ↥p := fun (i : ι) ↦ LinearMap.domRestrict (f i) p
h : ∀ (i : ι), ∃ (x : ↥p), Ne.{u_2 + 1} (α := K) ((f' i : (a : ↥p) → K) x : K) (0 : K)
obtain :
  ∀ (x : M) (hxp : x ∈ p)
    (hx₀ :
      ∀ (i : ι),
        Ne.{u_2 + 1} (α := K) ((f' i : (a : ↥p) → K) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hxp) : K) (0 : K)),
    ∃ x ∈ p, ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
⊢ ∃ x ∈ p, ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)

Tactic:
obtain ⟨⟨x, hxp⟩, hx₀⟩ := exists_forall_ne_zero_of_forall_exists f' h

Premises used: Module.Dual.exists_forall_ne_zero_of_forall_exists
-- 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
inst_3 : Finite ι
inst_4 : Infinite K
p : Submodule K M
f : ι → Dual K M
f' : (i : ι) → Dual.{u_2, u_3} K ↥p := fun (i : ι) ↦ LinearMap.domRestrict (f i) p
h : ∀ (i : ι), ∃ (x : ↥p), Ne.{u_2 + 1} (α := K) ((f' i : (a : ↥p) → K) x : K) (0 : K)
x : M
hxp : x ∈ p
hx₀ : ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f' i : (a : ↥p) → K) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hxp) : K) (0 : K)
⊢ ∃ x ∈ p, ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)

Tactic:
⟨x, hxp, hx₀⟩

Premises used: And.intro, Exists.intro
-- 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
inst_3 : Finite ι
inst_4 : Infinite K
p : Submodule K M
f : ι → Dual K M
f' : (i : ι) → Dual.{u_2, u_3} K ↥p := fun (i : ι) ↦ LinearMap.domRestrict (f i) p
h : ∀ (i : ι), ∃ (x : ↥p), Ne.{u_2 + 1} (α := K) ((f' i : (a : ↥p) → K) x : K) (0 : K)
x : M
hxp : x ∈ p
hx₀ : ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f' i : (a : ↥p) → K) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hxp) : K) (0 : K)
⊢ ∃ x ∈ p, ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)

Tactic:
exact ⟨x, hxp, hx₀⟩
-- 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
inst_3 : Finite ι
inst_4 : Infinite K
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ ∃ (f : Dual K M), ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f : (a : M) → K) (v i) : K) (0 : K)

Tactic:
Dual.exists_forall_ne_zero_of_forall_exists (fun i ↦ Dual.eval K M (v i)) fun i ↦ ?_

Premises used: Module.Dual.exists_forall_ne_zero_of_forall_exists, DFunLike.coe, Module.Dual.eval
-- 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
inst_3 : Finite ι
inst_4 : Infinite K
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
refine :
  ∀ (i : ι),
    ∃ (x : Dual K M),
      Ne.{u_2 + 1} (α := K)
        (((fun (i : ι) ↦ ((Dual.eval K M : (a : M) → Dual K (Dual K M)) (v i) : Dual K (Dual K M))) i :
              (a : Dual K M) → K)
            x :
          K)
        (0 : K)
⊢ ∃ (f : Dual K M), ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f : (a : M) → K) (v i) : K) (0 : K)

Tactic:
refine Dual.exists_forall_ne_zero_of_forall_exists (fun i ↦ Dual.eval K M (v i)) fun i ↦ ?_

Premises used: Module.Dual.exists_forall_ne_zero_of_forall_exists, DFunLike.coe, Module.Dual.eval
-- 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
inst_3 : Finite ι
inst_4 : Infinite K
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
i : ι
by_contra! :
  ∀
    (contra :
      ∀ (x : Dual K M),
        Eq.{u_2 + 1} (α := K)
          ((((Dual.eval K M : (a : M) → Dual K (Dual K M)) (v i) : Dual K (Dual K M)) : (a : Dual K M) → K) x : K)
          (0 : K)),
    False
⊢ ∃ (x : Dual K M),
    Ne.{u_2 + 1} (α := K)
      (((fun (i : ι) ↦ ((Dual.eval K M : (a : M) → Dual K (Dual K M)) (v i) : Dual K (Dual K M))) i :
            (a : Dual K M) → K)
          x :
        K)
      (0 : K)

Tactic:
by_contra! contra
-- 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
inst_3 : Finite ι
inst_4 : Infinite K
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
i : ι
contra :
  ∀ (x : Dual K M),
    Eq.{u_2 + 1} (α := K)
      ((((Dual.eval K M : (a : M) → Dual K (Dual K M)) (v i) : Dual K (Dual K M)) : (a : Dual K M) → K) x : K) (0 : K)
⊢ v i = 0

Tactic:
simp_rw [Dual.eval_apply, forall_dual_apply_eq_zero_iff] at contra

Premises used: Module.forall_dual_apply_eq_zero_iff, Module.Dual.eval_apply
-- 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
inst_3 : Finite ι
inst_4 : Infinite K
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
i : ι
contra : v i = 0
⊢ False

Tactic:
hv i contra
-- 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
inst_3 : Finite ι
inst_4 : Infinite K
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
i : ι
contra : v i = 0
⊢ False

Tactic:
exact hv i contra
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := Ideal R) (torsionOf R M 0) ⊤

Tactic:
simp [torsionOf]

Premises used: Ideal.torsionOf
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
a : R
⊢ Membership.mem (γ := Ideal R) (torsionOf R M x) a ↔ a • x = 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
h : m = 0
⊢ Eq (α := Ideal R) (torsionOf R M m) ⊤

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
refine : ∀ (h : Eq (α := Ideal R) (torsionOf R M m) ⊤), m = 0
⊢ Eq (α := Ideal R) (torsionOf R M m) ⊤ ↔ m = 0

Tactic:
refine ⟨fun h => ?_, fun h => by simp [h]⟩
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
h : Eq (α := Ideal R) (torsionOf R M m) ⊤
rw : Membership.mem (γ := Ideal R) ⊤ 1
⊢ m = 0

Tactic:
rw [← one_smul R m, ← mem_torsionOf_iff m (1 : R), h]

Premises used: one_smul, Ideal.mem_torsionOf_iff, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
h : Eq (α := Ideal R) (torsionOf R M m) ⊤
⊢ Membership.mem (γ := Ideal R) ⊤ 1

Tactic:
Submodule.mem_top

Premises used: Set.Mem, Submodule.mem_top
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
h : Eq (α := Ideal R) (torsionOf R M m) ⊤
⊢ Membership.mem (γ := Ideal R) ⊤ 1

Tactic:
exact Submodule.mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
m : M
⊢ Eq (α := Ideal R) (torsionOf R M m) ⊥ ↔ m ≠ 0

Tactic:
⟨fun h contra => ?_, fun h => (Submodule.eq_bot_iff _).mpr fun r hr => ?_⟩

Premises used: Iff.mpr, Ideal.torsionOf, Iff.intro, Submodule.eq_bot_iff