awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
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
⊢ f z ∈ (↑s : Set ι)
have hf₁ : Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)
Tactic: specialize hf z
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
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)
⊢ ∃ k ∈ s, ∃ z₁ ∈ sxy, ∃ z₂ ∈ sxy, z₁ ≠ z₂ ∧ z₁ ∈ p k ∧ z₂ ∈ p k
have hf' : MapsTo f univ (↑s : Set ι)
Tactic: have hf' : MapsTo f univ s := fun z _ ↦ by specialize hf z; aesop
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
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₂
⊢ ∃ k ∈ s, ∃ z₁ ∈ sxy, ∃ z₂ ∈ sxy, z₁ ≠ z₂ ∧ z₁ ∈ p k ∧ z₂ ∈ p k
have 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
Tactic: obtain ⟨z₁, z₂, hne, heq⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
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₂
⊢ (↑z₁ : M) ∈ p (f z₁)
have hf₁ : Membership.mem (γ := Set M) (⋃ (_ : f z₁ ∈ s), (↑(p (f z₁)) : Set M)) (↑z₁ : M)
Tactic: specialize hf z₁
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
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₂
⊢ (↑z₂ : M) ∈ p (f z₁)
have hf₁ : Membership.mem (γ := Set M) (⋃ (_ : f z₂ ∈ s), (↑(p (f z₂)) : Set M)) (↑z₂ : M)
Tactic: specialize hf z₂
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
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 ι)
⊢ ∃ k ∈ s, ∃ z₁ ∈ sxy, ∃ z₂ ∈ sxy, z₁ ≠ z₂ ∧ z₁ ∈ p k ∧ z₂ ∈ p k
have suffices : ∃ (z₁ : (↑sxy : Type u_3)) (z₂ : (↑sxy : Type u_3)), z₁ ≠ z₂ ∧ f z₁ = f z₂
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⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
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
have refine : ENat.card K ≤ sxy.encard + 1
Tactic: refine lt_of_add_lt_add_right <| lt_of_lt_of_le h₂ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
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 ι)
⊢ ENat.card K ≤ sxy.encard + 1
have this : 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
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
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}
have h : ∀ (x_1 : M), x_1 ∈ sxy ↔ Membership.mem (γ := Set M) ((fun (t : K) ↦ x + t • y) '' {t : K | t ≠ 0}) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
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
⊢ ENat.card K ≤ sxy.encard + 1
have aux : 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]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
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}
⊢ ENat.card K ≤ sxy.encard + 1
have rw : ENat.card K ≤ encard.{u_3} (α := M) ((fun (t : K) ↦ x + t • y) '' {t : K | t ≠ 0}) + 1
Tactic: rw [aux, this.encard_image, encard_ne_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
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
⊢ ENat.card K ≤ sxy.encard + 1
have rw₁ : ENat.card K ≤ encard.{u_2} (α := K) {t : K | t ≠ 0} + 1
Tactic: rw [aux, this.encard_image, encard_ne_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
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
⊢ ENat.card K ≤ sxy.encard + 1
have rw₂ : ENat.card K ≤ ENat.card K
Tactic: rw [aux, this.encard_image, encard_ne_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
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₁ : (↑sxy : Type u_3)) (z₂ : (↑sxy : Type u_3)), z₁ ≠ z₂ ∧ f z₁ = f z₂
have key : (↑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]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
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₁ : (↑sxy : Type u_3)) (z₂ : (↑sxy : Type u_3)), z₁ ≠ z₂ ∧ f z₁ = f z₂
have 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₂
Tactic: obtain ⟨z₁, -, z₂, -, h⟩ := exists_ne_map_eq_of_encard_lt_of_maps_to (by simpa) hf'
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
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)
⊢ Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x
have 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
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⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
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
have h : (t₁ - t₂) • y = x + t₁ • y - (x + t₂ • y)
Tactic: convert! sub_mem ht₁ ht₂ using 1
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
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
have this : (t₁ - t₂) • y ∈ p k
Tactic: have : (t₁ - t₂) • y ∈ p k := by convert! sub_mem ht₁ ht₂ using 1; module
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
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
have refine : t₁ - t₂ ≠ 0
Tactic: refine ((p k).smul_mem_iff ?_).mp this
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
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
⊢ Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x
have ht₃ : 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]
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
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
have h : x = x + t₁ • y - t₁ • y
Tactic: convert! sub_mem ht₁ ((p k).smul_mem t₁ ht)
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
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
⊢ Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x
have ht₃ : x ∈ p k
Tactic: replace ht : x ∈ p k := by convert! sub_mem ht₁ ((p k).smul_mem t₁ ht); simp
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
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 ι
⊢ ∃ (x : M), ∀ (i : ι), x ∉ p i
have suffices : SSubset.{u_3} (α := Set M) (⋃ (i : ι), (↑(p i) : Set M)) univ
Tactic: suffices ⋃ i, (p i : Set M) ⊂ univ by simpa [ssubset_univ_iff, iUnion_eq_univ_iff] using this
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
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 ≠ ⊤
have h₁ : ∃ (x : M), Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
Tactic: specialize h i
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
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)
⊢ ∃ (x : M), ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
have h₁ : ∀ (i : ι), p i ≠ ⊤
Tactic: replace h i : p i ≠ ⊤ := by specialize h i; aesop
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
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), ∀ (i : ι), Ne.{u_2 + 1} (α := K) ((f i : (a : M) → K) x : K) (0 : K)
have 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)
Tactic: obtain ⟨x, hx⟩ := Submodule.exists_forall_notMem_of_forall_ne_top p h