awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁
⊢ comap (AffineMap.id k P₁) s = s

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, AffineSubspace.comap, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₃
s : AffineSubspace k P₃
f : P₁ →ᵃ[k] P₂
g : P₂ →ᵃ[k] P₃
⊢ comap f (comap g s) = comap (g.comp f) s

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, AffineMap.comp, AffineSubspace.comap, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁
t : AffineSubspace k P₂
⊢ map f s ≤ t ↔ s ≤ comap f t

Tactic:
image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image, Set.image_subset_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
⊢ GaloisConnection (map f) (comap f)

Tactic:
fun _ _ =>
  map_le_iff_le_comap

Premises used: AffineSubspace.map_le_iff_le_comap, GaloisConnection
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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 (comap f s) ≤ s

Tactic:
(gc_map_comap f).l_u_le _

Premises used: AffineSubspace.gc_map_comap, GaloisConnection.l_u_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁
⊢ s ≤ comap f (map f s)

Tactic:
(gc_map_comap f).le_u_l _

Premises used: GaloisConnection.le_u_l, AffineSubspace.gc_map_comap
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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 t : AffineSubspace k P₁
f : P₁ →ᵃ[k] P₂
⊢ map f (s ⊔ t) = map f s ⊔ map f t

Tactic:
(gc_map_comap f).l_sup

Premises used: AffineSubspace.gc_map_comap, GaloisConnection.l_sup
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
ι : Sort u_8
f : P₁ →ᵃ[k] P₂
s : ι → AffineSubspace k P₁
⊢ map f (iSup s) = ⨆ (i : ι), map f (s i)

Tactic:
(gc_map_comap f).l_iSup

Premises used: GaloisConnection.l_iSup, AffineSubspace.gc_map_comap
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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 t : AffineSubspace k P₂
f : P₁ →ᵃ[k] P₂
⊢ comap f (s ⊓ t) = comap f s ⊓ comap f t

Tactic:
(gc_map_comap f).u_inf

Premises used: GaloisConnection.u_inf, AffineSubspace.gc_map_comap
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
ι : Sort u_8
f : P₁ →ᵃ[k] P₂
s : ι → AffineSubspace k P₂
⊢ comap f (iInf s) = ⨅ (i : ι), comap f (s i)

Tactic:
(gc_map_comap f).u_iInf

Premises used: GaloisConnection.u_iInf, AffineSubspace.gc_map_comap
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
e : P₁ ≃ᵃ[k] P₂
s : AffineSubspace k P₁
⊢ comap (↑e.symm : P₂ →ᵃ[k] P₁) s = map (↑e : P₁ →ᵃ[k] P₂) s

Tactic:
coe_injective <| e.preimage_symm _

Premises used: AffineSubspace.coe_injective, AffineEquiv.preimage_symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
e : P₁ ≃ᵃ[k] P₂
s : AffineSubspace k P₂
⊢ map (↑e.symm : P₂ →ᵃ[k] P₁) s = comap (↑e : P₁ →ᵃ[k] P₂) s

Tactic:
coe_injective <| e.image_symm _

Premises used: AffineEquiv.image_symm, AffineSubspace.coe_injective
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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))
rw₃ rw₄ :
  Eq.{u_3 + 1} (α := AffineSubspace k P₁) (affineSpan k ((⇑f : (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)

Tactic:
rw [← map_symm, map_span, AffineEquiv.coe_coe, f.image_symm]

Premises used: AffineSubspace.map_symm, AffineSubspace.map_span, AffineEquiv.image_symm, AffineEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁
simp : ∀ x ∈ s, Eq.{u_5 + 1} (α := P₂) ((f : (a : P₁) → P₂) x : P₂) ((f : (a : P₁) → P₂) p : P₂) → p ∈ s
⊢ p ∈ comap f (map f s) → p ∈ s

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁
⊢ ∀ x ∈ s, Eq.{u_5 + 1} (α := P₂) ((f : (a : P₁) → P₂) x : P₂) ((f : (a : P₁) → P₂) p : P₂) → p ∈ s

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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 : AffineSubspace k P₁
⊢ comap f (map f s) = s

Tactic:
(gciMapComap hf).u_l_eq _

Premises used: AffineSubspace.gciMapComap, GaloisCoinsertion.u_l_eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
rcases : ∀ (v : V), map (↑(constVAdd k P v) : P →ᵃ[k] P) s₁ ∥ s₁
⊢ s₂ ∥ s₁

Tactic:
rcases h with ⟨v, rfl⟩

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁

Tactic:
⟨-v, ?_⟩

Premises used: AffineSubspace.Parallel, Exists.intro, Neg.neg
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
refine : s₁ = map (↑(constVAdd k P (-v)) : P →ᵃ[k] P) (map (↑(constVAdd k P v) : P →ᵃ[k] P) s₁)
⊢ map (↑(constVAdd k P v) : P →ᵃ[k] P) s₁ ∥ s₁

Tactic:
refine ⟨-v, ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁
rw₆ rw₇ : s₁ = s₁
⊢ s₁ = map (↑(constVAdd k P (-v)) : P →ᵃ[k] P) (map (↑(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]

Premises used: AffineEquiv.constVAdd_add, AffineEquiv.coe_trans_to_affineMap, AffineEquiv.constVAdd_zero, neg_add_cancel, AffineSubspace.map_map, AffineEquiv.coe_refl_to_affineMap, AffineSubspace.map_id
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
⊢ s₁ ∥ s₂ ↔ s₂ ∥ s₁

Tactic:
⟨Parallel.symm, Parallel.symm⟩

Premises used: Iff.intro, AffineSubspace.Parallel.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
⊢ s = map (↑(constVAdd k P 0) : P →ᵃ[k] P) s

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₃
rcases : ∀ (v₁₂ : V) (h₂₃ : map (↑(constVAdd k P v₁₂) : P →ᵃ[k] P) s₁ ∥ s₃), s₁ ∥ s₃
⊢ s₁ ∥ s₃

Tactic:
rcases h₁₂ with ⟨v₁₂, rfl⟩

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₃
rcases : ∀ (v₂₃ : V), s₁ ∥ map (↑(constVAdd k P v₂₃) : P →ᵃ[k] P) (map (↑(constVAdd k P v₁₂) : P →ᵃ[k] P) s₁)
⊢ s₁ ∥ s₃

Tactic:
rcases h₂₃ with ⟨v₂₃, rfl⟩

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁)

Tactic:
⟨v₂₃ + v₁₂, ?_⟩

Premises used: AffineSubspace.Parallel, HAdd.hAdd, Exists.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
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₁
⊢ s₁ ∥ map (↑(constVAdd k P v₂₃) : P →ᵃ[k] P) (map (↑(constVAdd k P v₁₂) : P →ᵃ[k] P) s₁)

Tactic:
refine ⟨v₂₃ + v₁₂, ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁
rw₂ rw₃ : map (↑(constVAdd k P (v₂₃ + 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₁

Tactic:
rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add]

Premises used: AffineEquiv.constVAdd_add, AffineEquiv.coe_trans_to_affineMap, AffineSubspace.map_map
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
⊢ Equivalence.{u_3 + 1} (α := AffineSubspace k P) Parallel

Tactic:
⟨.refl, .symm, .trans⟩

Premises used: AffineSubspace.Parallel.symm, Equivalence.mk, AffineSubspace.Parallel.trans, AffineSubspace.Parallel.refl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
rcases : ∀ (v : V), s₁.direction = (map (↑(constVAdd k P v) : P →ᵃ[k] P) s₁).direction
⊢ s₁.direction = s₂.direction

Tactic:
rcases h with ⟨v, rfl⟩

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁.direction = (map (↑(constVAdd k P v) : P →ᵃ[k] P) s₁).direction

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
⊢ s ∥ ⊥ ↔ s = ⊥

Tactic:
⟨fun h => ?_, fun h => h ▸ Parallel.refl _⟩

Premises used: Eq.rec, Iff.intro, AffineSubspace.Parallel.refl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
refine : ∀ (h : s ∥ ⊥), s = ⊥
⊢ s ∥ ⊥ ↔ s = ⊥

Tactic:
refine ⟨fun h => ?_, fun h => h ▸ Parallel.refl _⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
h : s ∥ ⊥
rcases : ∀ (v : V) (h : ⊥ = map (↑(constVAdd k P v) : P →ᵃ[k] P) s), s = ⊥
⊢ s = ⊥

Tactic:
rcases h with ⟨v, h⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
h : ⊥ = map (↑(constVAdd k P v) : P →ᵃ[k] P) s
rwa : ∀ (h : map (↑(constVAdd k P v) : P →ᵃ[k] P) s = ⊥), s = ⊥
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : s = ⊥), s = ⊥
⊢ s = ⊥

Tactic:
rwa [eq_comm, map_eq_bot_iff] at h

Premises used: eq_comm, AffineSubspace.map_eq_bot_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
rw : s ∥ ⊥ ↔ s = ⊥
rw₁ rw₂ : s = ⊥ ↔ s = ⊥
⊢ ⊥ ∥ s ↔ s = ⊥

Tactic:
rw [parallel_comm, parallel_bot_iff_eq_bot]

Premises used: AffineSubspace.parallel_bot_iff_eq_bot, AffineSubspace.parallel_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
⊢ s₁ ∥ s₂ ↔ s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)

Tactic:
⟨fun h => ⟨h.direction_eq, ?_, ?_⟩, fun h => ?_⟩

Premises used: AffineSubspace.Parallel.direction_eq, And.intro, Iff.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
refine_1 : ∀ (h : s₁ ∥ s₂), s₁ = ⊥ → s₂ = ⊥
refine_2 : ∀ (h : s₁ ∥ s₂), s₂ = ⊥ → s₁ = ⊥
refine_3 : ∀ (h : s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)), s₁ ∥ s₂
⊢ s₁ ∥ s₂ ↔ s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)

Tactic:
refine ⟨fun h => ⟨h.direction_eq, ?_, ?_⟩, fun h => ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
h : ⊥ ∥ s₂
⊢ s₂ = ⊥

Tactic:
bot_parallel_iff_eq_bot.1 h

Premises used: Iff.mp, AffineSubspace.bot_parallel_iff_eq_bot
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
h : ⊥ ∥ s₂
⊢ s₂ = ⊥

Tactic:
exact bot_parallel_iff_eq_bot.1 h

Premises used: Iff.mp, AffineSubspace.bot_parallel_iff_eq_bot
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
h : s₁ ∥ ⊥
⊢ s₁ = ⊥

Tactic:
parallel_bot_iff_eq_bot.1 h

Premises used: AffineSubspace.parallel_bot_iff_eq_bot, Iff.mp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
h : s₁ ∥ ⊥
⊢ s₁ = ⊥

Tactic:
exact parallel_bot_iff_eq_bot.1 h

Premises used: AffineSubspace.parallel_bot_iff_eq_bot, Iff.mp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)
⊢ s₁.direction = s₂.direction

Tactic:
rcases h with ⟨hd, hb⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)
hd : s₁.direction = s₂.direction
⊢ s₁ = ⊥ ↔ s₂ = ⊥

Tactic:
rcases h with ⟨hd, hb⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
pos : ∀ (hs₁ : s₁ = ⊥), s₁ ∥ s₂
neg : ∀ (hs₁ : ¬s₁ = ⊥), s₁ ∥ s₂
⊢ s₁ ∥ s₂

Tactic:
by_cases hs₁ : s₁ = ⊥
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : s₁ = ⊥
pos : s₂ = ⊥
⊢ s₁ ∥ s₂

Tactic:
rw [hs₁, bot_parallel_iff_eq_bot]

Premises used: AffineSubspace.bot_parallel_iff_eq_bot
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : s₁ = ⊥
⊢ s₂ = ⊥

Tactic:
hb.1 hs₁

Premises used: Iff.mp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : s₁ = ⊥
⊢ s₂ = ⊥

Tactic:
exact hb.1 hs₁

Premises used: Iff.mp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
⊢ s₂ ≠ ⊥

Tactic:
have hs₂ : s₂ ≠ ⊥ := hb.not.1 hs₁
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
neg : ∀ (p₁ : P) (hp₁ : p₁ ∈ (↑s₁ : Set P)), s₁ ∥ s₂
⊢ s₁ ∥ s₂

Tactic:
rcases (nonempty_iff_ne_bot s₁).2 hs₁ with ⟨p₁, hp₁⟩

Premises used: Iff.mpr, AffineSubspace.nonempty_iff_ne_bot
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
neg : ∀ (p₂ : P) (hp₂ : p₂ ∈ (↑s₂ : Set P)), s₁ ∥ s₂
⊢ s₁ ∥ s₂

Tactic:
rcases (nonempty_iff_ne_bot s₂).2 hs₂ with ⟨p₂, hp₂⟩

Premises used: Iff.mpr, AffineSubspace.nonempty_iff_ne_bot
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
⊢ s₁ ∥ s₂

Tactic:
⟨p₂ -ᵥ p₁, (eq_iff_direction_eq_of_mem hp₂ ?_).2 ?_⟩

Premises used: Iff.mpr, VSub.vsub, AffineSubspace.eq_iff_direction_eq_of_mem, AffineSubspace.Parallel, Exists.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
neg : p₂ ∈ map (↑(constVAdd k P (p₂ -ᵥ p₁)) : P →ᵃ[k] P) s₁
neg₁ : s₂.direction = (map (↑(constVAdd k P (p₂ -ᵥ p₁)) : P →ᵃ[k] P) s₁).direction
⊢ s₁ ∥ s₂

Tactic:
refine ⟨p₂ -ᵥ p₁, (eq_iff_direction_eq_of_mem hp₂ ?_).2 ?_⟩