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)
choose :
  ∀ (f : (z : (↑sxy : Type u_3)) → ι)
    (hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)),
    ∃ k ∈ s, ∃ z₁ ∈ sxy, ∃ z₂ ∈ sxy, z₁ ≠ z₂ ∧ z₁ ∈ p k ∧ z₂ ∈ p k
⊢ ∃ k ∈ s, ∃ z₁ ∈ sxy, ∃ z₂ ∈ sxy, z₁ ≠ z₂ ∧ z₁ ∈ p k ∧ z₂ ∈ p k

Tactic:
choose f hf using fun z : sxy ↦ mem_iUnion.mp (hsxy z.property)

Premises used: Set.mem_iUnion, Iff.mp, Subtype.property
-- 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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
z : (↑sxy : Type u_3)
h : Membership.mem (γ := Set (↑sxy : Type u_3)) univ z
⊢ Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)

Tactic:
specialize hf z
-- 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)
f : (z : (↑sxy : Type u_3)) → ι
z : (↑sxy : Type u_3)
h : Membership.mem (γ := Set (↑sxy : Type u_3)) univ z
hf : Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
⊢ f z ∈ (↑s : Set ι)

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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
⊢ MapsTo f univ (↑s : Set ι)

Tactic:
have hf' : MapsTo f univ s := fun z _ ↦ by specialize hf z; 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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
hf' : MapsTo f univ (↑s : Set ι)
this : ∃ (z₁ : (↑sxy : Type u_3)) (z₂ : (↑sxy : Type u_3)), z₁ ≠ z₂ ∧ f z₁ = f z₂
obtain :
  ∀ (z₁ z₂ : (↑sxy : Type u_3)) (hne : z₁ ≠ z₂) (heq : f z₁ = f z₂),
    ∃ k ∈ s, ∃ z₁ ∈ sxy, ∃ z₂ ∈ sxy, z₁ ≠ z₂ ∧ z₁ ∈ p k ∧ z₂ ∈ p k
⊢ ∃ k ∈ s, ∃ z₁ ∈ sxy, ∃ z₂ ∈ sxy, z₁ ≠ z₂ ∧ z₁ ∈ p k ∧ z₂ ∈ p k

Tactic:
obtain ⟨z₁, z₂, hne, heq⟩ := 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
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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
hf' : MapsTo f univ (↑s : Set ι)
z₁ z₂ : (↑sxy : Type u_3)
hne : z₁ ≠ z₂
heq : f z₁ = f z₂
⊢ Membership.mem (γ := Set M) (⋃ (_ : f z₁ ∈ s), (↑(p (f z₁)) : Set M)) (↑z₁ : M)

Tactic:
specialize hf z₁
-- 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)
f : (z : (↑sxy : Type u_3)) → ι
hf' : MapsTo f univ (↑s : Set ι)
z₁ z₂ : (↑sxy : Type u_3)
hne : z₁ ≠ z₂
heq : f z₁ = f z₂
hf : Membership.mem (γ := Set M) (⋃ (_ : f z₁ ∈ s), (↑(p (f z₁)) : Set M)) (↑z₁ : M)
⊢ (↑z₁ : M) ∈ p (f z₁)

Tactic:
simp_all
-- 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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
hf' : MapsTo f univ (↑s : Set ι)
z₁ z₂ : (↑sxy : Type u_3)
hne : z₁ ≠ z₂
heq : f z₁ = f z₂
⊢ Membership.mem (γ := Set M) (⋃ (_ : f z₂ ∈ s), (↑(p (f z₂)) : Set M)) (↑z₂ : M)

Tactic:
specialize hf z₂
-- 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)
f : (z : (↑sxy : Type u_3)) → ι
hf' : MapsTo f univ (↑s : Set ι)
z₁ z₂ : (↑sxy : Type u_3)
hne : z₁ ≠ z₂
heq : f z₁ = f z₂
hf : Membership.mem (γ := Set M) (⋃ (_ : f z₂ ∈ s), (↑(p (f z₂)) : Set M)) (↑z₂ : M)
⊢ (↑z₂ : M) ∈ p (f z₁)

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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
hf' : MapsTo f univ (↑s : Set ι)
z₁ z₂ : (↑sxy : Type u_3)
hne : z₁ ≠ z₂
heq : f z₁ = f z₂
⊢ ∃ k ∈ s, ∃ z₁ ∈ sxy, ∃ z₂ ∈ sxy, z₁ ≠ z₂ ∧ z₁ ∈ p k ∧ z₂ ∈ p k

Tactic:
exact ⟨f z₁, hf' (mem_univ _), z₁, z₁.property, z₂, z₂.property,
          Subtype.coe_ne_coe.mpr hne, by specialize hf z₁; simp_all, by specialize hf z₂; 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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
hf' : MapsTo f univ (↑s : Set ι)
suffices : ∃ (z₁ : (↑sxy : Type u_3)) (z₂ : (↑sxy : Type u_3)), z₁ ≠ z₂ ∧ f z₁ = f z₂
⊢ ∃ k ∈ s, ∃ z₁ ∈ sxy, ∃ z₂ ∈ sxy, z₁ ≠ z₂ ∧ z₁ ∈ p k ∧ z₂ ∈ p k

Tactic:
suffices ∃ z₁ z₂, z₁ ≠ z₂ ∧ f z₁ = f z₂ by
        obtain ⟨z₁, z₂, hne, heq⟩ := this
        exact ⟨f z₁, hf' (mem_univ _), z₁, z₁.property, z₂, z₂.property,
          Subtype.coe_ne_coe.mpr hne, by specialize hf z₁; simp_all, by specialize hf z₂; 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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
hf' : MapsTo f univ (↑s : Set ι)
⊢ (↑s.card : ℕ∞) < sxy.encard

Tactic:
lt_of_add_lt_add_right <| lt_of_lt_of_le h₂ ?_

Premises used: lt_of_add_lt_add_right, lt_of_lt_of_le
-- 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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
hf' : MapsTo f univ (↑s : Set ι)
refine : ENat.card K ≤ sxy.encard + 1
⊢ (↑s.card : ℕ∞) < sxy.encard

Tactic:
refine lt_of_add_lt_add_right <| lt_of_lt_of_le h₂ ?_

Premises used: lt_of_add_lt_add_right, lt_of_lt_of_le
-- 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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
hf' : MapsTo f univ (↑s : Set ι)
t₁ t₂ : K
ht : Eq.{u_3 + 1} (α := M) ((fun (t : K) ↦ x + t • y) t₁) ((fun (t : K) ↦ x + t • y) t₂)
⊢ Eq.{u_3 + 1} (α := M) ((fun (x : K) ↦ x • y) t₁) ((fun (x : K) ↦ x • y) t₂)

Tactic:
simpa using 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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
hf' : MapsTo f univ (↑s : Set ι)
⊢ Injective.{u_2 + 1, u_3 + 1} (β := M) fun (t : K) ↦ x + t • y

Tactic:
have : Injective (fun t : K ↦ x + t • y) :=
          fun t₁ t₂ ht ↦ smul_left_injective K hy₀ <| by simpa using 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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
hf' : MapsTo f univ (↑s : Set ι)
this : Injective.{u_2 + 1, u_3 + 1} (β := M) fun (t : K) ↦ x + t • y
h : ∀ (x_1 : M), x_1 ∈ sxy ↔ Membership.mem (γ := Set M) ((fun (t : K) ↦ x + t • y) '' {t : K | t ≠ 0}) x_1
⊢ sxy = (fun (t : K) ↦ x + t • y) '' {t : K | t ≠ 0}

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
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_2 : M | ∃ (t : K) (_ : t ≠ 0), x + t • y = x_2}
hsxy : sxy ⊆ ⋃ i ∈ s, (↑(p i) : Set M)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
hf' : MapsTo f univ (↑s : Set ι)
this : Injective.{u_2 + 1, u_3 + 1} (β := M) fun (t : K) ↦ x + t • y
x_1 : M
⊢ x_1 ∈ sxy ↔ Membership.mem (γ := Set M) ((fun (t : K) ↦ x + t • y) '' {t : K | t ≠ 0}) x_1

Tactic:
simp [sxy]
-- 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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
hf' : MapsTo f univ (↑s : Set ι)
this : Injective.{u_2 + 1, u_3 + 1} (β := M) fun (t : K) ↦ x + t • y
⊢ sxy = (fun (t : K) ↦ x + t • y) '' {t : K | t ≠ 0}

Tactic:
have aux : sxy = ((fun t : K ↦ x + t • y) '' {t | t ≠ 0}) := by ext; simp [sxy]
-- 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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
hf' : MapsTo f univ (↑s : Set ι)
this : Injective.{u_2 + 1, u_3 + 1} (β := M) fun (t : K) ↦ x + t • y
aux : sxy = (fun (t : K) ↦ x + t • y) '' {t : K | t ≠ 0}
rw : ENat.card K ≤ encard.{u_3} (α := M) ((fun (t : K) ↦ x + t • y) '' {t : K | t ≠ 0}) + 1
rw₁ : ENat.card K ≤ encard.{u_2} (α := K) {t : K | t ≠ 0} + 1
rw₂ rw₃ : ENat.card K ≤ ENat.card K
⊢ ENat.card K ≤ sxy.encard + 1

Tactic:
rw [aux, this.encard_image, encard_ne_add_one]

Premises used: Function.Injective.encard_image, Set.encard_ne_add_one
-- 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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
hf' : MapsTo f univ (↑s : Set ι)
⊢ (↑s.card : ℕ∞) < sxy.encard

Tactic:
have key : s.card < sxy.encard := by
        refine lt_of_add_lt_add_right <| lt_of_lt_of_le h₂ ?_
        have : Injective (fun t : K ↦ x + t • y) :=
          fun t₁ t₂ ht ↦ smul_left_injective K hy₀ <| by simpa using ht
        have aux : sxy = ((fun t : K ↦ x + t • y) '' {t | t ≠ 0}) := by ext; simp [sxy]
        rw [aux, this.encard_image, encard_ne_add_one]
-- 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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
hf' : MapsTo f univ (↑s : Set ι)
key : (↑s.card : ℕ∞) < sxy.encard
⊢ (↑s : Set ι).encard < encard.{u_3} (α := (↑sxy : Type u_3)) univ

Tactic:
simpa
-- 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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
hf' : MapsTo f univ (↑s : Set ι)
key : (↑s.card : ℕ∞) < sxy.encard
obtain :
  ∀ (z₁ z₂ : (↑sxy : Type u_3)) (h : z₁ ≠ z₂ ∧ f z₁ = f z₂),
    ∃ (z₁ : (↑sxy : Type u_3)) (z₂ : (↑sxy : Type u_3)), z₁ ≠ z₂ ∧ f z₁ = f z₂
⊢ ∃ (z₁ : (↑sxy : Type u_3)) (z₂ : (↑sxy : Type u_3)), z₁ ≠ z₂ ∧ f z₁ = f z₂

Tactic:
obtain ⟨z₁, -, z₂, -, h⟩ := exists_ne_map_eq_of_encard_lt_of_maps_to (by simpa) hf'

Premises used: Set.exists_ne_map_eq_of_encard_lt_of_maps_to
-- 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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
hf' : MapsTo f univ (↑s : Set ι)
key : (↑s.card : ℕ∞) < sxy.encard
z₁ z₂ : (↑sxy : Type u_3)
h : z₁ ≠ z₂ ∧ f z₁ = f z₂
⊢ ∃ (z₁ : (↑sxy : Type u_3)) (z₂ : (↑sxy : Type u_3)), z₁ ≠ z₂ ∧ f z₁ = f z₂

Tactic:
⟨z₁, z₂, h⟩

Premises used: 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
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)
f : (z : (↑sxy : Type u_3)) → ι
hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
hf' : MapsTo f univ (↑s : Set ι)
key : (↑s.card : ℕ∞) < sxy.encard
z₁ z₂ : (↑sxy : Type u_3)
h : z₁ ≠ z₂ ∧ f z₁ = f z₂
⊢ ∃ (z₁ : (↑sxy : Type u_3)) (z₂ : (↑sxy : Type u_3)), z₁ ≠ z₂ ∧ f z₁ = f z₂

Tactic:
exact ⟨z₁, z₂, 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
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)
insert :
  ∀ (k : ι) (hk : k ∈ s) (t₁ t₂ : K) (ht : t₁ ≠ t₂) (ht₁ : x + t₁ • y ∈ p k) (ht₂ : x + t₂ • y ∈ p k),
    Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x
⊢ Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x

Tactic:
obtain ⟨k, hk, t₁, t₂, ht, ht₁, ht₂⟩ : ∃ᵉ (k ∈ s) (t₁ : K) (t₂ : K),
        t₁ ≠ t₂ ∧ x + t₁ • y ∈ p k ∧ x + t₂ • y ∈ p k := by
      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₂⟩
      choose f hf using fun z : sxy ↦ mem_iUnion.mp (hsxy z.property)
      have hf' : MapsTo f univ s := fun z _ ↦ by specialize hf z; aesop
      suffices ∃ z₁ z₂, z₁ ≠ z₂ ∧ f z₁ = f z₂ by
        obtain ⟨z₁, z₂, hne, heq⟩ := this
        exact ⟨f z₁, hf' (mem_univ _), z₁, z₁.property, z₂, z₂.property,
          Subtype.coe_ne_coe.mpr hne, by specialize hf z₁; simp_all, by specialize hf z₂; aesop⟩
      have key : s.card < sxy.encard := by
        refine lt_of_add_lt_add_right <| lt_of_lt_of_le h₂ ?_
        have : Injective (fun t : K ↦ x + t • y) :=
          fun t₁ t₂ ht ↦ smul_left_injective K hy₀ <| by simpa using ht
        have aux : sxy = ((fun t : K ↦ x + t • y) '' {t | t ≠ 0}) := by ext; simp [sxy]
        rw [aux, this.encard_image, encard_ne_add_one]
      obtain ⟨z₁, -, z₂, -, h⟩ := exists_ne_map_eq_of_encard_lt_of_maps_to (by simpa) hf'
      exact ⟨z₁, z₂, h⟩