awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
t : Set (AffineSubspace k P)
p : P
h : ∀ s ∈ t, p ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (⨅ s ∈ t, s.direction) v
⊢ v ∈ (sInf t).direction
have rw : ∀ s ∈ t, v +ᵥ p ∈ s
Tactic: rw [← vadd_mem_iff_mem_direction v ((mem_sInf_iff p t).mpr h), mem_sInf_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
t : Set (AffineSubspace k P)
p : P
h : ∀ s ∈ t, p ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (⨅ s ∈ t, s.direction) v
s : AffineSubspace k P
hs : s ∈ t
⊢ v +ᵥ p ∈ s
have rw : v ∈ s.direction
Tactic: rw [vadd_mem_iff_mem_direction v (h s hs)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
t : Set (AffineSubspace k P)
p : P
h : ∀ s ∈ t, p ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (⨅ s ∈ t, s.direction) v
s : AffineSubspace k P
hs : s ∈ t
⊢ v ∈ s.direction
have hv₁ : ∀ (i : AffineSubspace k P) (i_1 : i ∈ t), v ∈ i.direction
Tactic: simp only [Submodule.mem_iInf] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Sort u_4
s : ι → AffineSubspace k P
⊢ (↑(iInf s) : Set P) = ⋂ (i : ι), (↑(s i) : Set P)
have rw : (↑(sInf (range s)) : Set P) = ⋂ (i : ι), (↑(s i) : Set P)
Tactic: rw [iInf, coe_sInf, Set.biInter_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Sort u_4
s : ι → AffineSubspace k P
rw : (↑(sInf (range s)) : Set P) = ⋂ (i : ι), (↑(s i) : Set P)
⊢ (↑(iInf s) : Set P) = ⋂ (i : ι), (↑(s i) : Set P)
have rw₁ : Eq.{u_3 + 1} (α := Set P) (⋂ s_1 ∈ range s, (↑s_1 : Set P)) (⋂ (i : ι), (↑(s i) : Set P))
Tactic: rw [iInf, coe_sInf, Set.biInter_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Sort u_4
s : ι → AffineSubspace k P
rw : (↑(sInf (range s)) : Set P) = ⋂ (i : ι), (↑(s i) : Set P)
rw₁ : Eq.{u_3 + 1} (α := Set P) (⋂ s_1 ∈ range s, (↑s_1 : Set P)) (⋂ (i : ι), (↑(s i) : Set P))
⊢ (↑(iInf s) : Set P) = ⋂ (i : ι), (↑(s i) : Set P)
have rw₂ : Eq.{u_3 + 1} (α := Set P) (⋂ (y : ι), (↑(s y) : Set P)) (⋂ (i : ι), (↑(s i) : Set P))
Tactic: rw [iInf, coe_sInf, Set.biInter_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Sort u_4
s : ι → AffineSubspace k P
p : P
⊢ p ∈ iInf s ↔ ∀ (i : ι), p ∈ s i
have rw : p ∈ sInf (range s) ↔ ∀ (i : ι), p ∈ s i
Tactic: rw [iInf, mem_sInf_iff, Set.forall_mem_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Sort u_4
s : ι → AffineSubspace k P
p : P
rw : p ∈ sInf (range s) ↔ ∀ (i : ι), p ∈ s i
⊢ p ∈ iInf s ↔ ∀ (i : ι), p ∈ s i
have rw₁ : (∀ s_1 ∈ range s, p ∈ s_1) ↔ ∀ (i : ι), p ∈ s i
Tactic: rw [iInf, mem_sInf_iff, Set.forall_mem_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Sort u_4
s : ι → AffineSubspace k P
p : P
rw : p ∈ sInf (range s) ↔ ∀ (i : ι), p ∈ s i
rw₁ : (∀ s_1 ∈ range s, p ∈ s_1) ↔ ∀ (i : ι), p ∈ s i
⊢ p ∈ iInf s ↔ ∀ (i : ι), p ∈ s i
have rw₂ : (∀ (i : ι), p ∈ s i) ↔ ∀ (i : ι), p ∈ s i
Tactic: rw [iInf, mem_sInf_iff, Set.forall_mem_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Sort u_4
s : ι → AffineSubspace k P
⊢ (iInf s).direction ≤ ⨅ (i : ι), (s i).direction
have apply : Eq.{u_2 + 1} (α := Submodule k V) (⨅ s_1 ∈ range s, s_1.direction) (⨅ (i : ι), (s i).direction)
Tactic: apply (direction_sInf _).trans_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Sort u_4
s : ι → AffineSubspace k P
⊢ Eq.{u_2 + 1} (α := Submodule k V) (⨅ s_1 ∈ range s, s_1.direction) (⨅ (i : ι), (s i).direction)
have rw : Eq.{u_2 + 1} (α := Submodule k V) (⨅ (i : ι), (s i).direction) (⨅ (i : ι), (s i).direction)
Tactic: rw [iInf_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Sort u_4
s : ι → AffineSubspace k P
p : P
h : ∀ (i : ι), p ∈ s i
⊢ (iInf s).direction = ⨅ (i : ι), (s i).direction
have rw : ∀ s_1 ∈ range s, p ∈ s_1
Tactic: rw [iInf, direction_sInf_of_mem _ p ?_, iInf_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Sort u_4
s : ι → AffineSubspace k P
p : P
h : p ∈ iInf s
⊢ (iInf s).direction = ⨅ (i : ι), (s i).direction
have rw : (sInf (range s)).direction = ⨅ (i : ι), (s i).direction
Tactic: rw [iInf, direction_sInf_of_mem_sInf _ p h, iInf_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Sort u_4
s : ι → AffineSubspace k P
p : P
h : p ∈ iInf s
rw : (sInf (range s)).direction = ⨅ (i : ι), (s i).direction
⊢ (iInf s).direction = ⨅ (i : ι), (s i).direction
have rw₁ : Eq.{u_2 + 1} (α := Submodule k V) (⨅ s_1 ∈ range s, s_1.direction) (⨅ (i : ι), (s i).direction)
Tactic: rw [iInf, direction_sInf_of_mem_sInf _ p h, iInf_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Sort u_4
s : ι → AffineSubspace k P
p : P
h : p ∈ iInf s
rw : (sInf (range s)).direction = ⨅ (i : ι), (s i).direction
rw₁ : Eq.{u_2 + 1} (α := Submodule k V) (⨅ s_1 ∈ range s, s_1.direction) (⨅ (i : ι), (s i).direction)
⊢ (iInf s).direction = ⨅ (i : ι), (s i).direction
have rw₂ : Eq.{u_2 + 1} (α := Submodule k V) (⨅ (i : ι), (s i).direction) (⨅ (i : ι), (s i).direction)
Tactic: rw [iInf, direction_sInf_of_mem_sInf _ p h, iInf_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
⊢ s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction
have obtain : ∀ (p₁ : P) (hp₁ : p₁ ∈ (↑s₁ : Set P)), s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction
Tactic: obtain ⟨p₁, hp₁⟩ := h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h2 : (↑s₂ : Set P).Nonempty
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
⊢ s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction
have obtain : ∀ (p₂ : P) (hp₂ : p₂ ∈ (↑s₂ : Set P)), s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction
Tactic: obtain ⟨p₂, hp₂⟩ := h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
⊢ s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction
have rw : s₁.direction ⊔ s₂.direction ≤ (s₁ ⊔ s₂).direction ∧ ∃ x ∈ (s₁ ⊔ s₂).direction, x ∉ s₁.direction ⊔ s₂.direction
Tactic: rw [SetLike.lt_iff_le_and_exists]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
⊢ s₁.direction ⊔ s₂.direction ≤ (s₁ ⊔ s₂).direction ∧ ∃ x ∈ (s₁ ⊔ s₂).direction, x ∉ s₁.direction ⊔ s₂.direction
have right : p₂ -ᵥ p₁ ∉ s₁.direction ⊔ s₂.direction
Tactic: use sup_direction_le s₁ s₂, p₂ -ᵥ p₁,
    vsub_mem_direction ((le_sup_right : s₂ ≤ s₁ ⊔ s₂) hp₂) ((le_sup_left : s₁ ≤ s₁ ⊔ s₂) hp₁)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
h : p₂ -ᵥ p₁ ∈ s₁.direction ⊔ s₂.direction
⊢ False
have h₁ : ∃ y ∈ s₁.direction, ∃ z ∈ s₂.direction, y + z = p₂ -ᵥ p₁
Tactic: rw [Submodule.mem_sup] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
h : ∃ y ∈ s₁.direction, ∃ z ∈ s₂.direction, y + z = p₂ -ᵥ p₁
⊢ False
have right : ∀ (v₁ : V) (hv₁ : v₁ ∈ s₁.direction) (v₂ : V) (hv₂ : v₂ ∈ s₂.direction) (hv₁v₂ : v₁ + v₂ = p₂ -ᵥ p₁), False
Tactic: rcases h with ⟨v₁, hv₁, v₂, hv₂, hv₁v₂⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₁ + v₂ = p₂ -ᵥ p₁
⊢ False
have hv₁v₃ : v₁ +ᵥ p₁ = -v₂ +ᵥ p₂
Tactic: rw [← sub_eq_zero, sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_comm v₁, add_assoc, ←
    vadd_vsub_assoc, ← neg_neg v₂, add_comm, ← sub_eq_add_neg, ← vsub_vadd_eq_vsub_sub,
    vsub_eq_zero_iff_eq] at hv₁v₂
Cleared hypotheses: hv₁v₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₁ +ᵥ p₁ = -v₂ +ᵥ p₂
⊢ False
have right : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
Tactic: refine Set.Nonempty.ne_empty ?_ he
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₁ +ᵥ p₁ = -v₂ +ᵥ p₂
⊢ ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
have right : v₁ +ᵥ p₁ ∈ (↑s₂ : Set P)
Tactic: use v₁ +ᵥ p₁, vadd_mem_of_mem_direction hv₁ hp₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₁ +ᵥ p₁ = -v₂ +ᵥ p₂
⊢ v₁ +ᵥ p₁ ∈ (↑s₂ : Set P)
have right : -v₂ +ᵥ p₂ ∈ (↑s₂ : Set P)
Tactic: rw [hv₁v₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
⊢ ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
have by_contra : ∀ (h : ¬((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : ¬((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
⊢ False
have h₁ : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
Tactic: rw [Set.not_nonempty_iff_eq_empty] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
⊢ False
have hlt : s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction
Tactic: have hlt := sup_direction_lt_of_nonempty_of_inter_empty h1 h2 h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
hlt : s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction
⊢ False
have hlt₁ : ⊤ < (s₁ ⊔ s₂).direction
Tactic: rw [hd] at hlt
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : IsCompl s₁.direction s₂.direction
⊢ ∃ (p : P), (↑s₁ : Set P) ∩ (↑s₂ : Set P) = {p}
have obtain : ∀ (p : P) (hp : p ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)), ∃ (p : P), (↑s₁ : Set P) ∩ (↑s₂ : Set P) = {p}
Tactic: obtain ⟨p, hp⟩ := inter_nonempty_of_nonempty_of_sup_direction_eq_top h1 h2 hd.sup_eq_top
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)
⊢ ∃ (p : P), (↑s₁ : Set P) ∩ (↑s₂ : Set P) = {p}
have h : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = {p}
Tactic: use p
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)
⊢ (↑s₁ : Set P) ∩ (↑s₂ : Set P) = {p}
have h : ∀ (q : P), q ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P) ↔ Membership.mem (γ := Set P) {p} q
Tactic: ext q
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)
q : P
⊢ q ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P) ↔ q = p
have h : q ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P) → q = p
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)
q : P
h : q ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P) → q = p
⊢ q ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P) ↔ q = p
have h₁ : q = p → q ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)
q : P
hq1 : q ∈ (↑s₁ : Set P)
hq2 : q ∈ (↑s₂ : Set P)
⊢ q = p
have hqp : q -ᵥ p ∈ s₁.direction ⊓ s₂.direction
Tactic: have hqp : q -ᵥ p ∈ s₁.direction ⊓ s₂.direction :=
      ⟨vsub_mem_direction hq1 hp.1, vsub_mem_direction hq2 hp.2⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)
q : P
hq1 : q ∈ (↑s₁ : Set P)
hq2 : q ∈ (↑s₂ : Set P)
hqp : q -ᵥ p ∈ s₁.direction ⊓ s₂.direction
⊢ q = p
have h : ∀ (hqp : Membership.mem (γ := Submodule k V) ⊥ (q -ᵥ p)), q = p
Tactic: rwa [hd.inf_eq_bot, Submodule.mem_bot, vsub_eq_zero_iff_eq] at hqp
Cleared hypotheses: hqp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)
q : P
hq1 : q ∈ (↑s₁ : Set P)
hq2 : q ∈ (↑s₂ : Set P)
hqp : q -ᵥ p ∈ s₁.direction ⊓ s₂.direction
h : ∀ (hqp : Membership.mem (γ := Submodule k V) ⊥ (q -ᵥ p)), q = p
⊢ q = p
have h₁ : ∀ (hqp : q -ᵥ p = 0), q = p
Tactic: rwa [hd.inf_eq_bot, Submodule.mem_bot, vsub_eq_zero_iff_eq] at hqp
Cleared hypotheses: hqp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)
q : P
hq1 : q ∈ (↑s₁ : Set P)
hq2 : q ∈ (↑s₂ : Set P)
hqp : q -ᵥ p ∈ s₁.direction ⊓ s₂.direction
h : ∀ (hqp : Membership.mem (γ := Submodule k V) ⊥ (q -ᵥ p)), q = p
h₁ : ∀ (hqp : q -ᵥ p = 0), q = p
⊢ q = p
have h₂ : ∀ (hqp : q = p), q = p
Tactic: rwa [hd.inf_eq_bot, Submodule.mem_bot, vsub_eq_zero_iff_eq] at hqp
Cleared hypotheses: hqp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s : AffineSubspace k P
⊢ affineSpan k (↑s : Set P) = s
have refine : affineSpan k (↑s : Set P) ≤ s
Tactic: refine le_antisymm ?_ (subset_affineSpan _ _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
p : P
d₁ d₂ : Submodule k V
⊢ LE.le (α := AffineSubspace k P) (mk' p d₁) (mk' p d₂) ↔ d₁ ≤ d₂
have simp_rw : (∀ ⦃x : P⦄, x -ᵥ p ∈ d₁ → x -ᵥ p ∈ d₂) ↔ ∀ ⦃x : V⦄, x ∈ d₁ → x ∈ d₂
Tactic: simp_rw [SetLike.le_def, mem_mk']
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
p : P
d₁ d₂ : Submodule k V
⊢ (∀ ⦃x : P⦄, x -ᵥ p ∈ d₁ → x -ᵥ p ∈ d₂) ↔ ∀ ⦃x : V⦄, x ∈ d₁ → x ∈ d₂
have refine : ∀ (h : ∀ ⦃x : P⦄, x -ᵥ p ∈ d₁ → x -ᵥ p ∈ d₂) (x : V) (hx : x ∈ d₁), x ∈ d₂
Tactic: refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ h hx⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ s = ∅
have rw : ¬Eq (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ ¬s = ∅
Tactic: rw [← not_iff_not, ← Ne, ← Ne, ← nonempty_iff_ne_bot, affineSpan_nonempty,
    nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
rw : ¬Eq (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ ¬s = ∅
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ s = ∅
have rw₁ : Ne (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ ¬s = ∅
Tactic: rw [← not_iff_not, ← Ne, ← Ne, ← nonempty_iff_ne_bot, affineSpan_nonempty,
    nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
rw : ¬Eq (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ ¬s = ∅
rw₁ : Ne (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ ¬s = ∅
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ s = ∅
have rw₂ : Ne (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ s ≠ ∅
Tactic: rw [← not_iff_not, ← Ne, ← Ne, ← nonempty_iff_ne_bot, affineSpan_nonempty,
    nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
rw : ¬Eq (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ ¬s = ∅
rw₁ : Ne (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ ¬s = ∅
rw₂ : Ne (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ s ≠ ∅
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ s = ∅
have rw₃ : (↑(affineSpan k s) : Set P).Nonempty ↔ s ≠ ∅
Tactic: rw [← not_iff_not, ← Ne, ← Ne, ← nonempty_iff_ne_bot, affineSpan_nonempty,
    nonempty_iff_ne_empty]