awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.Surjective.{u_3 + 1, u_5 + 1} (α := P₁) (β := P₂) (⇑f : (a : P₁) → P₂)
⊢ AffineSubspace.map f ⊤ = ⊤
have rw : (↑(AffineSubspace.map f ⊤) : Set P₂) = (↑⊤ : Set P₂)
Tactic: rw [AffineSubspace.ext_iff]
-- 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₁
hf : Function.Surjective.{u_3 + 1, u_5 + 1} (α := P₁) (β := P₂) (⇑f : (a : P₁) → P₂)
h : Eq (α := AffineSubspace k P₁) (affineSpan k s) ⊤
⊢ Eq.{u_5 + 1} (α := AffineSubspace k P₂) (affineSpan k ((⇑f : (a : P₁) → P₂) '' s)) ⊤
have rw : AffineSubspace.map f (affineSpan k s) = ⊤
Tactic: rw [← AffineSubspace.map_span, h, map_top_of_surjective f hf]
-- 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₁
hf : Function.Surjective.{u_3 + 1, u_5 + 1} (α := P₁) (β := P₂) (⇑f : (a : P₁) → P₂)
h : Eq (α := AffineSubspace k P₁) (affineSpan k s) ⊤
rw : AffineSubspace.map f (affineSpan k s) = ⊤
⊢ Eq.{u_5 + 1} (α := AffineSubspace k P₂) (affineSpan k ((⇑f : (a : P₁) → P₂) '' s)) ⊤
have rw₁ : AffineSubspace.map f ⊤ = ⊤
Tactic: rw [← AffineSubspace.map_span, h, map_top_of_surjective f hf]
-- 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₁
hf : Function.Surjective.{u_3 + 1, u_5 + 1} (α := P₁) (β := P₂) (⇑f : (a : P₁) → P₂)
h : Eq (α := AffineSubspace k P₁) (affineSpan k s) ⊤
rw : AffineSubspace.map f (affineSpan k s) = ⊤
rw₁ : AffineSubspace.map f ⊤ = ⊤
⊢ Eq.{u_5 + 1} (α := AffineSubspace k P₂) (affineSpan k ((⇑f : (a : P₁) → P₂) '' s)) ⊤
have rw₂ : Eq.{u_5 + 1} (α := AffineSubspace k P₂) ⊤ ⊤
Tactic: rw [← AffineSubspace.map_span, h, map_top_of_surjective f hf]
-- 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₁
V₂ : Type u_8
P₂ : Type u_9
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
s : Set P₁
f g : P₁ →ᵃ[k] P₂
h_agree : EqOn.{u_3, u_9} (β := P₂) (⇑f : (a : P₁) → P₂) (⇑g : (a : P₁) → P₂) s
⊢ EqOn.{u_2, u_8} (β := V₂) (⇑f.linear : (a : V₁) → V₂) (⇑g.linear : (a : V₁) → V₂)
    (↑(Submodule.span k (s -ᵥ s)) : Set V₁)
have H : EqOn.{u_2, u_8} (β := V₂) (⇑f.linear : (a : V₁) → V₂) (⇑g.linear : (a : V₁) → V₂) (s -ᵥ s)
Tactic: apply LinearMap.eqOn_span
-- 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₁
V₂ : Type u_8
P₂ : Type u_9
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
s : Set P₁
f g : P₁ →ᵃ[k] P₂
h_agree : EqOn.{u_3, u_9} (β := P₂) (⇑f : (a : P₁) → P₂) (⇑g : (a : P₁) → P₂) s
⊢ EqOn.{u_3, u_9} (β := P₂) (⇑f : (a : P₁) → P₂) (⇑g : (a : P₁) → P₂) (↑(affineSpan k s) : Set P₁)
have inl : ∀ (h_agree : EqOn.{u_3, u_9} (α := P₁) (β := P₂) (⇑f : (a : P₁) → P₂) (⇑g : (a : P₁) → P₂) ∅),
  EqOn.{u_3, u_9} (β := P₂) (⇑f : (a : P₁) → P₂) (⇑g : (a : P₁) → P₂) (↑(affineSpan k ∅) : Set P₁)
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨q, hq⟩
Cleared hypotheses: s, h_agree
-- 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₁
V₂ : Type u_8
P₂ : Type u_9
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
s : Set P₁
f g : P₁ →ᵃ[k] P₂
h_agree : EqOn.{u_3, u_9} (β := P₂) (⇑f : (a : P₁) → P₂) (⇑g : (a : P₁) → P₂) s
inl :
  ∀ (h_agree : EqOn.{u_3, u_9} (α := P₁) (β := P₂) (⇑f : (a : P₁) → P₂) (⇑g : (a : P₁) → P₂) ∅),
    EqOn.{u_3, u_9} (β := P₂) (⇑f : (a : P₁) → P₂) (⇑g : (a : P₁) → P₂) (↑(affineSpan k ∅) : Set P₁)
⊢ EqOn.{u_3, u_9} (β := P₂) (⇑f : (a : P₁) → P₂) (⇑g : (a : P₁) → P₂) (↑(affineSpan k s) : Set P₁)
have inr : ∀ (q : P₁) (hq : q ∈ s),
  EqOn.{u_3, u_9} (β := P₂) (⇑f : (a : P₁) → P₂) (⇑g : (a : P₁) → P₂) (↑(affineSpan k s) : Set P₁)
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨q, hq⟩
-- 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₂ : AffineSubspace k P₁
inst_4 : Nonempty.{u_3 + 1} ↥S₁
inst_5 : Nonempty.{u_3 + 1} ↥S₂
h : S₁ = S₂
⊢ Eq (α := AffineEquiv.{u_1, u_3, u_3, u_2, u_2} k ↥S₂ ↥S₁) (symm (ofEq S₁ S₂ h)) (ofEq S₂ S₁ ⋯)
have h₁ : ∀ (x : ↥S₂),
  Eq.{u_3 + 1} (α := P₁) (↑((symm (ofEq S₁ S₂ h) : (a : ↥S₂) → ↥S₁) x) : P₁)
    (↑((ofEq S₂ S₁ sorry : (a : ↥S₂) → ↥S₁) x) : P₁)
Tactic: ext
-- 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₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
⊢ Eq (α := AffineSubspace k P₁) (affineSpan k s) ⊤ ↔
    Eq.{u_5 + 1} (α := AffineSubspace k P₂) (affineSpan k ((⇑e : (a : P₁) → P₂) '' s)) ⊤
have refine : Eq.{u_5 + 1} (α := AffineSubspace k P₂) (affineSpan k ((⇑e : (a : P₁) → P₂) '' s)) ⊤ →
  Eq (α := AffineSubspace k P₁) (affineSpan k s) ⊤
Tactic: refine ⟨(e : P₁ →ᵃ[k] P₂).span_eq_top_of_surjective e.surjective, ?_⟩
-- 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₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : Eq.{u_5 + 1} (α := AffineSubspace k P₂) (affineSpan k ((⇑e : (a : P₁) → P₂) '' s)) ⊤
⊢ s = image.{u_5, u_3} (α := P₂) (⇑e.symm : (a : P₂) → P₁) ((⇑e : (a : P₁) → P₂) '' s)
have rw : s = Function.comp.{u_3 + 1, u_5 + 1, u_3 + 1} (β := P₂) (⇑e.symm : (a : P₂) → P₁) (⇑e : (a : P₁) → P₂) '' s
Tactic: rw [← image_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
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₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : Eq.{u_5 + 1} (α := AffineSubspace k P₂) (affineSpan k ((⇑e : (a : P₁) → P₂) '' s)) ⊤
⊢ Eq (α := AffineSubspace k P₁) (affineSpan k s) ⊤
have this : s = image.{u_5, u_3} (α := P₂) (⇑e.symm : (a : P₂) → P₁) ((⇑e : (a : P₁) → P₂) '' s)
Tactic: have : s = e.symm '' e '' s := by rw [← image_comp]; simp
-- 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₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : Eq.{u_5 + 1} (α := AffineSubspace k P₂) (affineSpan k ((⇑e : (a : P₁) → P₂) '' s)) ⊤
this : s = image.{u_5, u_3} (α := P₂) (⇑e.symm : (a : P₂) → P₁) ((⇑e : (a : P₁) → P₂) '' s)
⊢ Eq (α := AffineSubspace k P₁) (affineSpan k s) ⊤
have rw : Eq.{u_3 + 1} (α := AffineSubspace k P₁)
  (affineSpan k (image.{u_5, u_3} (α := P₂) (⇑e.symm : (a : P₂) → P₁) ((⇑e : (a : P₁) → P₂) '' s))) ⊤
Tactic: rw [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₂ p₃ : P₁
hp₁ : Membership.mem (α := P₂) s ((f : (a : P₁) → P₂) p₁ : P₂)
hp₂ : Membership.mem (α := P₂) s ((f : (a : P₁) → P₂) p₂ : P₂)
hp₃ : Membership.mem (α := P₂) s ((f : (a : P₁) → P₂) p₃ : P₂)
⊢ Membership.mem (α := P₂) s ((f : (a : P₁) → P₂) (t • (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₂) ∈
  s
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
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₂
⊢ comap f ⊤ = ⊤
have rw : (↑(comap f ⊤) : Set P₁) = (↑⊤ : Set P₁)
Tactic: rw [AffineSubspace.ext_iff]
-- 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₂
⊢ comap (↑f : P₁ →ᵃ[k] P₂) (affineSpan k s) = affineSpan k ((⇑f : (a : P₁) → P₂) ⁻¹' s)
have rw : map (↑f.symm : P₂ →ᵃ[k] P₁) (affineSpan k s) = affineSpan k ((⇑f : (a : P₁) → P₂) ⁻¹' s)
Tactic: rw [← map_symm, map_span, AffineEquiv.coe_coe, f.image_symm]
-- 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₂
rw : map (↑f.symm : P₂ →ᵃ[k] P₁) (affineSpan k s) = affineSpan k ((⇑f : (a : P₁) → P₂) ⁻¹' s)
⊢ comap (↑f : P₁ →ᵃ[k] P₂) (affineSpan k s) = affineSpan k ((⇑f : (a : P₁) → P₂) ⁻¹' s)
have rw₁ : Eq.{u_3 + 1} (α := AffineSubspace k P₁) (affineSpan k ((⇑(↑f.symm : P₂ →ᵃ[k] P₁) : (a : P₂) → P₁) '' s))
  (affineSpan k ((⇑f : (a : P₁) → P₂) ⁻¹' s))
Tactic: rw [← map_symm, map_span, AffineEquiv.coe_coe, f.image_symm]
-- 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₂
rw : map (↑f.symm : P₂ →ᵃ[k] P₁) (affineSpan k s) = affineSpan k ((⇑f : (a : P₁) → P₂) ⁻¹' s)
rw₁ :
  Eq.{u_3 + 1} (α := AffineSubspace k P₁) (affineSpan k ((⇑(↑f.symm : P₂ →ᵃ[k] P₁) : (a : P₂) → P₁) '' s))
    (affineSpan k ((⇑f : (a : P₁) → P₂) ⁻¹' s))
⊢ comap (↑f : P₁ →ᵃ[k] P₂) (affineSpan k s) = affineSpan k ((⇑f : (a : P₁) → P₂) ⁻¹' s)
have rw₂ : Eq.{u_3 + 1} (α := AffineSubspace k P₁) (affineSpan k ((⇑f.symm : (a : P₂) → P₁) '' s))
  (affineSpan k ((⇑f : (a : P₁) → P₂) ⁻¹' s))
Tactic: rw [← map_symm, map_span, AffineEquiv.coe_coe, f.image_symm]
-- 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₂
rw : map (↑f.symm : P₂ →ᵃ[k] P₁) (affineSpan k s) = affineSpan k ((⇑f : (a : P₁) → P₂) ⁻¹' s)
rw₁ :
  Eq.{u_3 + 1} (α := AffineSubspace k P₁) (affineSpan k ((⇑(↑f.symm : P₂ →ᵃ[k] P₁) : (a : P₂) → P₁) '' s))
    (affineSpan k ((⇑f : (a : P₁) → P₂) ⁻¹' s))
rw₂ :
  Eq.{u_3 + 1} (α := AffineSubspace k P₁) (affineSpan k ((⇑f.symm : (a : P₂) → P₁) '' s))
    (affineSpan k ((⇑f : (a : P₁) → P₂) ⁻¹' s))
⊢ comap (↑f : P₁ →ᵃ[k] P₂) (affineSpan k s) = affineSpan k ((⇑f : (a : P₁) → P₂) ⁻¹' s)
have rw₃ : Eq.{u_3 + 1} (α := AffineSubspace k P₁) (affineSpan k ((⇑f : (a : P₁) → P₂) ⁻¹' s))
  (affineSpan k ((⇑f : (a : P₁) → P₂) ⁻¹' s))
Tactic: rw [← map_symm, map_span, AffineEquiv.coe_coe, f.image_symm]
-- 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₂
hf : Function.Injective.{u_3 + 1, u_5 + 1} (α := P₁) (β := P₂) (⇑f : (a : P₁) → P₂)
s : AffineSubspace k P₁
p : P₁
⊢ p ∈ comap f (map f s) → p ∈ s
have simp : ∀ x ∈ s, Eq.{u_5 + 1} (α := P₂) ((f : (a : P₁) → P₂) x : P₂) ((f : (a : P₁) → P₂) p : P₂) → p ∈ s
Tactic: simp
-- 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₂ : AffineSubspace k P
h : s₁ ∥ s₂
⊢ s₂ ∥ s₁
have rcases : ∀ (v : V), map (↑(constVAdd k P v) : P →ᵃ[k] P) s₁ ∥ s₁
Tactic: rcases h with ⟨v, rfl⟩
Cleared hypotheses: s₂, 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
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ : AffineSubspace k P
v : V
⊢ map (↑(constVAdd k P v) : P →ᵃ[k] P) s₁ ∥ s₁
have refine : s₁ = map (↑(constVAdd k P (-v)) : P →ᵃ[k] P) (map (↑(constVAdd k P v) : P →ᵃ[k] P) s₁)
Tactic: refine ⟨-v, ?_⟩
-- 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
v : V
⊢ s₁ = map (↑(constVAdd k P (-v)) : P →ᵃ[k] P) (map (↑(constVAdd k P v) : P →ᵃ[k] P) s₁)
have rw : s₁ = map (AffineMap.comp (↑(constVAdd k P (-v)) : P →ᵃ[k] P) (↑(constVAdd k P v) : P →ᵃ[k] P)) s₁
Tactic: rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add, neg_add_cancel, constVAdd_zero,
    coe_refl_to_affineMap, map_id]
-- 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
v : V
rw : s₁ = map (AffineMap.comp (↑(constVAdd k P (-v)) : P →ᵃ[k] P) (↑(constVAdd k P v) : P →ᵃ[k] P)) s₁
⊢ s₁ = map (↑(constVAdd k P (-v)) : P →ᵃ[k] P) (map (↑(constVAdd k P v) : P →ᵃ[k] P) s₁)
have rw₁ : s₁ = map (↑(AffineEquiv.trans (constVAdd k P v) (constVAdd k P (-v))) : P →ᵃ[k] P) s₁
Tactic: rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add, neg_add_cancel, constVAdd_zero,
    coe_refl_to_affineMap, map_id]
-- 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
v : V
rw : s₁ = map (AffineMap.comp (↑(constVAdd k P (-v)) : P →ᵃ[k] P) (↑(constVAdd k P v) : P →ᵃ[k] P)) s₁
rw₁ : s₁ = map (↑(AffineEquiv.trans (constVAdd k P v) (constVAdd k P (-v))) : P →ᵃ[k] P) s₁
⊢ s₁ = map (↑(constVAdd k P (-v)) : P →ᵃ[k] P) (map (↑(constVAdd k P v) : P →ᵃ[k] P) s₁)
have rw₂ : s₁ = map (↑(constVAdd k P (-v + v)) : P →ᵃ[k] P) s₁
Tactic: rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add, neg_add_cancel, constVAdd_zero,
    coe_refl_to_affineMap, map_id]
-- 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
v : V
rw : s₁ = map (AffineMap.comp (↑(constVAdd k P (-v)) : P →ᵃ[k] P) (↑(constVAdd k P v) : P →ᵃ[k] P)) s₁
rw₁ : s₁ = map (↑(AffineEquiv.trans (constVAdd k P v) (constVAdd k P (-v))) : P →ᵃ[k] P) s₁
rw₂ : s₁ = map (↑(constVAdd k P (-v + v)) : P →ᵃ[k] P) s₁
⊢ s₁ = map (↑(constVAdd k P (-v)) : P →ᵃ[k] P) (map (↑(constVAdd k P v) : P →ᵃ[k] P) s₁)
have rw₃ : s₁ = map (↑(constVAdd k P 0) : P →ᵃ[k] P) s₁
Tactic: rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add, neg_add_cancel, constVAdd_zero,
    coe_refl_to_affineMap, map_id]
-- 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
v : V
rw : s₁ = map (AffineMap.comp (↑(constVAdd k P (-v)) : P →ᵃ[k] P) (↑(constVAdd k P v) : P →ᵃ[k] P)) s₁
rw₁ : s₁ = map (↑(AffineEquiv.trans (constVAdd k P v) (constVAdd k P (-v))) : P →ᵃ[k] P) s₁
rw₂ : s₁ = map (↑(constVAdd k P (-v + v)) : P →ᵃ[k] P) s₁
rw₃ : s₁ = map (↑(constVAdd k P 0) : P →ᵃ[k] P) s₁
⊢ s₁ = map (↑(constVAdd k P (-v)) : P →ᵃ[k] P) (map (↑(constVAdd k P v) : P →ᵃ[k] P) s₁)
have rw₄ : s₁ = map (↑(AffineEquiv.refl k P) : P →ᵃ[k] P) s₁
Tactic: rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add, neg_add_cancel, constVAdd_zero,
    coe_refl_to_affineMap, map_id]
-- 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
v : V
rw : s₁ = map (AffineMap.comp (↑(constVAdd k P (-v)) : P →ᵃ[k] P) (↑(constVAdd k P v) : P →ᵃ[k] P)) s₁
rw₁ : s₁ = map (↑(AffineEquiv.trans (constVAdd k P v) (constVAdd k P (-v))) : P →ᵃ[k] P) s₁
rw₂ : s₁ = map (↑(constVAdd k P (-v + v)) : P →ᵃ[k] P) s₁
rw₃ : s₁ = map (↑(constVAdd k P 0) : P →ᵃ[k] P) s₁
rw₄ : s₁ = map (↑(AffineEquiv.refl k P) : P →ᵃ[k] P) s₁
⊢ s₁ = map (↑(constVAdd k P (-v)) : P →ᵃ[k] P) (map (↑(constVAdd k P v) : P →ᵃ[k] P) s₁)
have rw₅ : s₁ = map (AffineMap.id k P) s₁
Tactic: rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add, neg_add_cancel, constVAdd_zero,
    coe_refl_to_affineMap, map_id]
-- 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
v : V
rw : s₁ = map (AffineMap.comp (↑(constVAdd k P (-v)) : P →ᵃ[k] P) (↑(constVAdd k P v) : P →ᵃ[k] P)) s₁
rw₁ : s₁ = map (↑(AffineEquiv.trans (constVAdd k P v) (constVAdd k P (-v))) : P →ᵃ[k] P) s₁
rw₂ : s₁ = map (↑(constVAdd k P (-v + v)) : P →ᵃ[k] P) s₁
rw₃ : s₁ = map (↑(constVAdd k P 0) : P →ᵃ[k] P) s₁
rw₄ : s₁ = map (↑(AffineEquiv.refl k P) : P →ᵃ[k] P) s₁
rw₅ : s₁ = map (AffineMap.id k P) s₁
⊢ s₁ = map (↑(constVAdd k P (-v)) : P →ᵃ[k] P) (map (↑(constVAdd k P v) : P →ᵃ[k] P) s₁)
have rw₆ : s₁ = s₁
Tactic: rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add, neg_add_cancel, constVAdd_zero,
    coe_refl_to_affineMap, map_id]
-- 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₂ s₃ : AffineSubspace k P
h₁₂ : s₁ ∥ s₂
h₂₃ : s₂ ∥ s₃
⊢ s₁ ∥ s₃
have rcases : ∀ (v₁₂ : V) (h₂₃ : map (↑(constVAdd k P v₁₂) : P →ᵃ[k] P) s₁ ∥ s₃), s₁ ∥ s₃
Tactic: rcases h₁₂ with ⟨v₁₂, rfl⟩
Cleared hypotheses: s₂, h₁₂, 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
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₃ : AffineSubspace k P
v₁₂ : V
h₂₃ : map (↑(constVAdd k P v₁₂) : P →ᵃ[k] P) s₁ ∥ s₃
⊢ s₁ ∥ s₃
have rcases : ∀ (v₂₃ : V), s₁ ∥ map (↑(constVAdd k P v₂₃) : P →ᵃ[k] P) (map (↑(constVAdd k P v₁₂) : P →ᵃ[k] P) s₁)
Tactic: rcases h₂₃ with ⟨v₂₃, rfl⟩
Cleared hypotheses: s₃, 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
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ : AffineSubspace k P
v₁₂ v₂₃ : V
⊢ s₁ ∥ map (↑(constVAdd k P v₂₃) : P →ᵃ[k] P) (map (↑(constVAdd k P v₁₂) : P →ᵃ[k] P) s₁)
have refine : map (↑(constVAdd k P v₂₃) : P →ᵃ[k] P) (map (↑(constVAdd k P v₁₂) : P →ᵃ[k] P) s₁) =
  map (↑(constVAdd k P (v₂₃ + v₁₂)) : P →ᵃ[k] P) s₁
Tactic: refine ⟨v₂₃ + v₁₂, ?_⟩
-- 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
v₁₂ v₂₃ : V
⊢ map (↑(constVAdd k P v₂₃) : P →ᵃ[k] P) (map (↑(constVAdd k P v₁₂) : P →ᵃ[k] P) s₁) =
    map (↑(constVAdd k P (v₂₃ + v₁₂)) : P →ᵃ[k] P) s₁
have rw : map (AffineMap.comp (↑(constVAdd k P v₂₃) : P →ᵃ[k] P) (↑(constVAdd k P v₁₂) : P →ᵃ[k] P)) s₁ =
  map (↑(constVAdd k P (v₂₃ + v₁₂)) : P →ᵃ[k] P) s₁
Tactic: rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add]
-- 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
v₁₂ v₂₃ : V
rw :
  map (AffineMap.comp (↑(constVAdd k P v₂₃) : P →ᵃ[k] P) (↑(constVAdd k P v₁₂) : P →ᵃ[k] P)) s₁ =
    map (↑(constVAdd k P (v₂₃ + v₁₂)) : P →ᵃ[k] P) s₁
⊢ map (↑(constVAdd k P v₂₃) : P →ᵃ[k] P) (map (↑(constVAdd k P v₁₂) : P →ᵃ[k] P) s₁) =
    map (↑(constVAdd k P (v₂₃ + v₁₂)) : P →ᵃ[k] P) s₁
have rw₁ : map (↑(AffineEquiv.trans (constVAdd k P v₁₂) (constVAdd k P v₂₃)) : P →ᵃ[k] P) s₁ =
  map (↑(constVAdd k P (v₂₃ + v₁₂)) : P →ᵃ[k] P) s₁
Tactic: rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add]
-- 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
v₁₂ v₂₃ : V
rw :
  map (AffineMap.comp (↑(constVAdd k P v₂₃) : P →ᵃ[k] P) (↑(constVAdd k P v₁₂) : P →ᵃ[k] P)) s₁ =
    map (↑(constVAdd k P (v₂₃ + v₁₂)) : P →ᵃ[k] P) s₁
rw₁ :
  map (↑(AffineEquiv.trans (constVAdd k P v₁₂) (constVAdd k P v₂₃)) : P →ᵃ[k] P) s₁ =
    map (↑(constVAdd k P (v₂₃ + v₁₂)) : P →ᵃ[k] P) s₁
⊢ map (↑(constVAdd k P v₂₃) : P →ᵃ[k] P) (map (↑(constVAdd k P v₁₂) : P →ᵃ[k] P) s₁) =
    map (↑(constVAdd k P (v₂₃ + v₁₂)) : P →ᵃ[k] P) s₁
have rw₂ : map (↑(constVAdd k P (v₂₃ + v₁₂)) : P →ᵃ[k] P) s₁ = map (↑(constVAdd k P (v₂₃ + v₁₂)) : P →ᵃ[k] P) s₁
Tactic: rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add]
-- 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₂ : AffineSubspace k P
h : s₁ ∥ s₂
⊢ s₁.direction = s₂.direction
have rcases : ∀ (v : V), s₁.direction = (map (↑(constVAdd k P v) : P →ᵃ[k] P) s₁).direction
Tactic: rcases h with ⟨v, rfl⟩
Cleared hypotheses: s₂, h