awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
inst_3 : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ p : P
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : r • (p₂ -ᵥ p₁) + v₂ = p -ᵥ p₁
⊢ p = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁
have hp₂ : p -ᵥ p₁ = r • (p₂ -ᵥ p₁) + v₂
Tactic: symm at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
inst_3 : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ p : P
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : p -ᵥ p₁ = r • (p₂ -ᵥ p₁) + v₂
⊢ p = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁
have hp₂ : p = (r • (p₂ -ᵥ p₁) + v₂) +ᵥ p₁
Tactic: rw [← sub_eq_zero, ← vsub_vadd_eq_vsub_sub, vsub_eq_zero_iff_eq] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ p : P
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : p = (r • (p₂ -ᵥ p₁) + v₂) +ᵥ p₁
⊢ p = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁
have right : (r • (p₂ -ᵥ p₁) + v₂) +ᵥ p₁ = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁
Tactic: rw [hp, vadd_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ p : P
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : p = (r • (p₂ -ᵥ p₁) + v₂) +ᵥ p₁
right : (r • (p₂ -ᵥ p₁) + v₂) +ᵥ p₁ = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁
⊢ p = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁
have right₁ : (r • (p₂ -ᵥ p₁) + v₂) +ᵥ p₁ = (r • (p₂ -ᵥ p₁) + v₂) +ᵥ p₁
Tactic: rw [hp, vadd_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ : P
r : k
p₃ : P
hp₃ : p₃ ∈ s
⊢ ∃ (y : V),
    Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) y ∧ ∃ z ∈ s.direction, y + z = (r • (p₂ -ᵥ p₁) +ᵥ p₃) -ᵥ p₁
have right : r • (p₂ -ᵥ p₁) + (p₃ -ᵥ p₁) = (r • (p₂ -ᵥ p₁) +ᵥ p₃) -ᵥ p₁
Tactic: use r • (p₂ -ᵥ p₁), Submodule.mem_span_singleton.2 ⟨r, rfl⟩, p₃ -ᵥ p₁,
      vsub_mem_direction hp₃ hp₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ : P
r : k
p₃ : P
hp₃ : p₃ ∈ s
⊢ r • (p₂ -ᵥ p₁) + (p₃ -ᵥ p₁) = (r • (p₂ -ᵥ p₁) +ᵥ p₃) -ᵥ p₁
have right : r • (p₂ -ᵥ p₁) + (p₃ -ᵥ p₁) = r • (p₂ -ᵥ p₁) + (p₃ -ᵥ p₁)
Tactic: rw [vadd_vsub_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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₁ s₂ : Set P
p : P
hp₁ : p ∈ s₁
hp₂ : p ∈ s₂
⊢ Eq (α := Submodule k V) (vectorSpan k (s₁ ∪ s₂)) (vectorSpan k s₁ ⊔ vectorSpan k s₂)
have simp_rw : Eq (α := Submodule k V) (direction (affineSpan k (s₁ ∪ s₂))) (direction (affineSpan k s₁) ⊔ direction (affineSpan k s₂))
Tactic: simp_rw [← direction_affineSpan, span_union,
    direction_sup_eq_sup_direction (mem_affineSpan k hp₁) (mem_affineSpan k hp₂)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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₁ s₂ : Set P
p : P
hp₁ : p ∈ s₁
hp₂ : p ∈ s₂
simp_rw :
  Eq (α := Submodule k V) (direction (affineSpan k (s₁ ∪ s₂)))
    (direction (affineSpan k s₁) ⊔ direction (affineSpan k s₂))
⊢ Eq (α := Submodule k V) (vectorSpan k (s₁ ∪ s₂)) (vectorSpan k s₁ ⊔ vectorSpan k s₂)
have simp_rw₁ : Eq (α := Submodule k V) (direction (affineSpan k s₁ ⊔ affineSpan k s₂))
  (direction (affineSpan k s₁) ⊔ direction (affineSpan k s₂))
Tactic: simp_rw [← direction_affineSpan, span_union,
    direction_sup_eq_sup_direction (mem_affineSpan k hp₁) (mem_affineSpan k hp₂)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : AddCommGroup V₃
inst_8 : Module k V₃
inst_9 : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ (↑s : Set P₁)
p₂ : P₁
h₂ : p₂ ∈ (↑s : Set P₁)
p₃ : P₁
h₃ : p₃ ∈ (↑s : Set P₁)
⊢ Membership.mem (γ := Set P₂) ((⇑f : (a : P₁) → P₂) '' (↑s : Set P₁))
    (HVAdd.hVAdd (β := P₂)
      (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
      ((f : (a : P₁) → P₂) p₃ : P₂))
have h : t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ (↑s : Set P₁) ∧
  (f : (a : P₁) → P₂) (t • (p₁ -ᵥ p₂) +ᵥ p₃) =
    HVAdd.hVAdd (β := P₂)
      (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
      ((f : (a : P₁) → P₂) p₃ : P₂)
Tactic: use t • (p₁ -ᵥ p₂) +ᵥ p₃
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : AddCommGroup V₃
inst_8 : Module k V₃
inst_9 : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ (↑s : Set P₁)
p₂ : P₁
h₂ : p₂ ∈ (↑s : Set P₁)
p₃ : P₁
h₃ : p₃ ∈ (↑s : Set P₁)
this : t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s
⊢ t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ (↑s : Set P₁) ∧
    (f : (a : P₁) → P₂) (t • (p₁ -ᵥ p₂) +ᵥ p₃) =
      HVAdd.hVAdd (β := P₂)
        (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
        ((f : (a : P₁) → P₂) p₃ : P₂)
have simp : (f : (a : P₁) → P₂) (t • (p₁ -ᵥ p₂) +ᵥ p₃) =
  HVAdd.hVAdd (β := P₂) (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
    ((f : (a : P₁) → P₂) p₃ : P₂)
Tactic: simp only [SetLike.mem_coe, true_and, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : AddCommGroup V₃
inst_8 : Module k V₃
inst_9 : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ (↑s : Set P₁)
p₂ : P₁
h₂ : p₂ ∈ (↑s : Set P₁)
p₃ : P₁
h₃ : p₃ ∈ (↑s : Set P₁)
this : t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s
⊢ (f : (a : P₁) → P₂) (t • (p₁ -ᵥ p₂) +ᵥ p₃) =
    HVAdd.hVAdd (β := P₂)
      (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
      ((f : (a : P₁) → P₂) p₃ : P₂)
have rw : HVAdd.hVAdd.{u_4, u_5, u_5} (α := V₂) (β := P₂) ((f.linear : (a : V₁) → V₂) (t • (p₁ -ᵥ p₂)) : V₂)
    ((f : (a : P₁) → P₂) p₃ : P₂) =
  HVAdd.hVAdd (β := P₂) (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
    ((f : (a : P₁) → P₂) p₃ : P₂)
Tactic: rw [AffineMap.map_vadd, map_smul, AffineMap.linearMap_vsub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : AddCommGroup V₃
inst_8 : Module k V₃
inst_9 : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ (↑s : Set P₁)
p₂ : P₁
h₂ : p₂ ∈ (↑s : Set P₁)
p₃ : P₁
h₃ : p₃ ∈ (↑s : Set P₁)
this : t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s
rw :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := V₂) (β := P₂) ((f.linear : (a : V₁) → V₂) (t • (p₁ -ᵥ p₂)) : V₂)
      ((f : (a : P₁) → P₂) p₃ : P₂) =
    HVAdd.hVAdd (β := P₂)
      (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
      ((f : (a : P₁) → P₂) p₃ : P₂)
⊢ (f : (a : P₁) → P₂) (t • (p₁ -ᵥ p₂) +ᵥ p₃) =
    HVAdd.hVAdd (β := P₂)
      (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
      ((f : (a : P₁) → P₂) p₃ : P₂)
have rw₁ : HVAdd.hVAdd (β := P₂) (HSMul.hSMul (β := V₂) t ((f.linear : (a : V₁) → V₂) (p₁ -ᵥ p₂) : V₂))
    ((f : (a : P₁) → P₂) p₃ : P₂) =
  HVAdd.hVAdd (β := P₂) (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
    ((f : (a : P₁) → P₂) p₃ : P₂)
Tactic: rw [AffineMap.map_vadd, map_smul, AffineMap.linearMap_vsub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : AddCommGroup V₃
inst_8 : Module k V₃
inst_9 : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ (↑s : Set P₁)
p₂ : P₁
h₂ : p₂ ∈ (↑s : Set P₁)
p₃ : P₁
h₃ : p₃ ∈ (↑s : Set P₁)
this : t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s
rw :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := V₂) (β := P₂) ((f.linear : (a : V₁) → V₂) (t • (p₁ -ᵥ p₂)) : V₂)
      ((f : (a : P₁) → P₂) p₃ : P₂) =
    HVAdd.hVAdd (β := P₂)
      (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
      ((f : (a : P₁) → P₂) p₃ : P₂)
rw₁ :
  HVAdd.hVAdd (β := P₂) (HSMul.hSMul (β := V₂) t ((f.linear : (a : V₁) → V₂) (p₁ -ᵥ p₂) : V₂))
      ((f : (a : P₁) → P₂) p₃ : P₂) =
    HVAdd.hVAdd (β := P₂)
      (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
      ((f : (a : P₁) → P₂) p₃ : P₂)
⊢ (f : (a : P₁) → P₂) (t • (p₁ -ᵥ p₂) +ᵥ p₃) =
    HVAdd.hVAdd (β := P₂)
      (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
      ((f : (a : P₁) → P₂) p₃ : P₂)
have rw₂ : HVAdd.hVAdd (β := P₂) (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
    ((f : (a : P₁) → P₂) p₃ : P₂) =
  HVAdd.hVAdd (β := P₂) (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
    ((f : (a : P₁) → P₂) p₃ : P₂)
Tactic: rw [AffineMap.map_vadd, map_smul, AffineMap.linearMap_vsub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : AddCommGroup V₃
inst_8 : Module k V₃
inst_9 : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ (↑s : Set P₁)
p₂ : P₁
h₂ : p₂ ∈ (↑s : Set P₁)
p₃ : P₁
h₃ : p₃ ∈ (↑s : Set P₁)
this : t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s
⊢ t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ (↑s : Set P₁) ∧
    (f : (a : P₁) → P₂) (t • (p₁ -ᵥ p₂) +ᵥ p₃) =
      HVAdd.hVAdd (β := P₂)
        (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
        ((f : (a : P₁) → P₂) p₃ : P₂)
have simp : (f : (a : P₁) → P₂) (t • (p₁ -ᵥ p₂) +ᵥ p₃) =
  HVAdd.hVAdd (β := P₂) (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
    ((f : (a : P₁) → P₂) p₃ : P₂)
Tactic: { simp only [SetLike.mem_coe, true_and, this]
      rw [AffineMap.map_vadd, map_smul, AffineMap.linearMap_vsub] }
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : AddCommGroup V₃
inst_8 : Module k V₃
inst_9 : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ (↑s : Set P₁)
p₂ : P₁
h₂ : p₂ ∈ (↑s : Set P₁)
p₃ : P₁
h₃ : p₃ ∈ (↑s : Set P₁)
⊢ t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ (↑s : Set P₁) ∧
    (f : (a : P₁) → P₂) (t • (p₁ -ᵥ p₂) +ᵥ p₃) =
      HVAdd.hVAdd (β := P₂)
        (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
        ((f : (a : P₁) → P₂) p₃ : P₂)
have h : t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s
Tactic: suffices t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s by
    { simp only [SetLike.mem_coe, true_and, this]
      rw [AffineMap.map_vadd, map_smul, AffineMap.linearMap_vsub] }
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
⊢ map f s = ⊥ ↔ s = ⊥
have refine_1 : ∀ (h : map f s = ⊥), s = ⊥
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
refine_1 : ∀ (h : map f s = ⊥), s = ⊥
⊢ map f s = ⊥ ↔ s = ⊥
have refine_2 : ∀ (h : s = ⊥), map f s = ⊥
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
h : map f s = ⊥
⊢ s = ⊥
have refine_1 : ∀ (h : (↑(map f s) : Set P₂) = ∅), s = ⊥
Tactic: rwa [← coe_eq_bot_iff, coe_map, image_eq_empty, coe_eq_bot_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
h : map f s = ⊥
refine_1 : ∀ (h : (↑(map f s) : Set P₂) = ∅), s = ⊥
⊢ s = ⊥
have refine_1₁ : ∀ (h : Eq.{u_5 + 1} (α := Set P₂) ((⇑f : (a : P₁) → P₂) '' (↑s : Set P₁)) ∅), s = ⊥
Tactic: rwa [← coe_eq_bot_iff, coe_map, image_eq_empty, coe_eq_bot_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
h : map f s = ⊥
refine_1 : ∀ (h : (↑(map f s) : Set P₂) = ∅), s = ⊥
refine_1₁ : ∀ (h : Eq.{u_5 + 1} (α := Set P₂) ((⇑f : (a : P₁) → P₂) '' (↑s : Set P₁)) ∅), s = ⊥
⊢ s = ⊥
have refine_1₂ : ∀ (h : (↑s : Set P₁) = ∅), s = ⊥
Tactic: rwa [← coe_eq_bot_iff, coe_map, image_eq_empty, coe_eq_bot_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
h : map f s = ⊥
refine_1 : ∀ (h : (↑(map f s) : Set P₂) = ∅), s = ⊥
refine_1₁ : ∀ (h : Eq.{u_5 + 1} (α := Set P₂) ((⇑f : (a : P₁) → P₂) '' (↑s : Set P₁)) ∅), s = ⊥
refine_1₂ : ∀ (h : (↑s : Set P₁) = ∅), s = ⊥
⊢ s = ⊥
have refine_1₃ : ∀ (h : s = ⊥), s = ⊥
Tactic: rwa [← coe_eq_bot_iff, coe_map, image_eq_empty, coe_eq_bot_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
h : s = ⊥
⊢ map f s = ⊥
have refine_2 : map f ⊥ = ⊥
Tactic: rw [h, map_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
h : s = ⊥
refine_2 : map f ⊥ = ⊥
⊢ map f s = ⊥
have refine_2₁ : Eq.{u_5 + 1} (α := AffineSubspace k P₂) ⊥ ⊥
Tactic: rw [h, map_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
⊢ map f (affineSpan k s) = affineSpan k ((⇑f : (a : P₁) → P₂) '' s)
have inl : map f (affineSpan k ∅) = affineSpan k (image.{u_3, u_5} (α := P₁) (⇑f : (a : P₁) → P₂) ∅)
Tactic: rcases s.eq_empty_or_nonempty with (rfl | ⟨p, hp⟩)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
inl : map f (affineSpan k ∅) = affineSpan k (image.{u_3, u_5} (α := P₁) (⇑f : (a : P₁) → P₂) ∅)
⊢ map f (affineSpan k s) = affineSpan k ((⇑f : (a : P₁) → P₂) '' s)
have inr : ∀ (p : P₁) (hp : p ∈ s), map f (affineSpan k s) = affineSpan k ((⇑f : (a : P₁) → P₂) '' s)
Tactic: rcases s.eq_empty_or_nonempty with (rfl | ⟨p, hp⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
p : P₁
hp : p ∈ s
⊢ map f (affineSpan k s) = affineSpan k ((⇑f : (a : P₁) → P₂) '' s)
have inr : (map f (affineSpan k s)).direction = direction.{u_1, u_4, u_5} (P := P₂) (affineSpan k ((⇑f : (a : P₁) → P₂) '' s))
Tactic: apply ext_of_direction_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
p : P₁
hp : p ∈ s
inr :
  (map f (affineSpan k s)).direction = direction.{u_1, u_4, u_5} (P := P₂) (affineSpan k ((⇑f : (a : P₁) → P₂) '' s))
⊢ map f (affineSpan k s) = affineSpan k ((⇑f : (a : P₁) → P₂) '' s)
have inr₁ : ((↑(map f (affineSpan k s)) : Set P₂) ∩ (↑(affineSpan k ((⇑f : (a : P₁) → P₂) '' s)) : Set P₂)).Nonempty
Tactic: apply ext_of_direction_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
hf : Function.Injective.{u_3 + 1, u_5 + 1} (α := P₁) (β := P₂) (⇑f : (a : P₁) → P₂)
s₁ s₂ : AffineSubspace k P₁
⊢ map f (s₁ ⊓ s₂) = map f s₁ ⊓ map f s₂
have h : ∀ (p : P₂), p ∈ map f (s₁ ⊓ s₂) ↔ p ∈ map f s₁ ⊓ map f s₂
Tactic: ext p
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
p : P₁
direction : Submodule k V₁
⊢ map f (mk' p direction) = mk' ((f : (a : P₁) → P₂) p) (Submodule.map f.linear direction)
have h : ∀ (q : P₂),
  q ∈ map f (mk' p direction) ↔
    Membership.mem (γ := AffineSubspace k P₂)
      (mk' ((f : (a : P₁) → P₂) p) (Submodule.map f.linear direction) : AffineSubspace k P₂) q
Tactic: ext q
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
p : P₁
direction : Submodule k V₁
q : P₂
⊢ q ∈ map f (mk' p direction) ↔
    Membership.mem (γ := AffineSubspace k P₂)
      (mk' ((f : (a : P₁) → P₂) p) (Submodule.map f.linear direction) : AffineSubspace k P₂) q
have h : (∃ (y : P₁), y -ᵥ p ∈ direction ∧ (f : (a : P₁) → P₂) y = q) ↔
  ∃ y ∈ direction, (f.linear : (a : V₁) → V₂) y = q -ᵥ (f : (a : P₁) → P₂) p
Tactic: simp only [mem_map, mem_mk', Submodule.mem_map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
p : P₁
direction : Submodule k V₁
q : P₂
⊢ (∃ (y : P₁), y -ᵥ p ∈ direction ∧ (f : (a : P₁) → P₂) y = q) ↔
    ∃ y ∈ direction, (f.linear : (a : V₁) → V₂) y = q -ᵥ (f : (a : P₁) → P₂) p
have h : (∃ (y : P₁), y -ᵥ p ∈ direction ∧ (f : (a : P₁) → P₂) y = q) →
  ∃ y ∈ direction, (f.linear : (a : V₁) → V₂) y = q -ᵥ (f : (a : P₁) → P₂) p
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
p : P₁
direction : Submodule k V₁
q : P₂
h :
  (∃ (y : P₁), y -ᵥ p ∈ direction ∧ (f : (a : P₁) → P₂) y = q) →
    ∃ y ∈ direction, (f.linear : (a : V₁) → V₂) y = q -ᵥ (f : (a : P₁) → P₂) p
⊢ (∃ (y : P₁), y -ᵥ p ∈ direction ∧ (f : (a : P₁) → P₂) y = q) ↔
    ∃ y ∈ direction, (f.linear : (a : V₁) → V₂) y = q -ᵥ (f : (a : P₁) → P₂) p
have h₁ : (∃ y ∈ direction, (f.linear : (a : V₁) → V₂) y = q -ᵥ (f : (a : P₁) → P₂) p) →
  ∃ (y : P₁), y -ᵥ p ∈ direction ∧ (f : (a : P₁) → P₂) y = q
Tactic: constructor