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
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
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
⊢ (∃ (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
-- 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₂
p : P₁
direction : Submodule k V₁
r : P₁
hr : r -ᵥ p ∈ direction
⊢ (f.linear : (a : V₁) → V₂) (r -ᵥ p) =
    VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) r : P₂) ((f : (a : P₁) → P₂) p : P₂)

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
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₁
r : P₁
hr : r -ᵥ p ∈ direction
⊢ ∃ y ∈ direction,
    (f.linear : (a : V₁) → V₂) y =
      VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) r : P₂) ((f : (a : P₁) → P₂) p : P₂)

Tactic:
exact ⟨r -ᵥ p, hr, by 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
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₂
r : V₁
hr : r ∈ direction
he : (f.linear : (a : V₁) → V₂) r = q -ᵥ (f : (a : P₁) → P₂) p
⊢ (r +ᵥ p) -ᵥ p ∈ direction

Tactic:
simp [hr]
-- 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₂
p : P₁
direction : Submodule k V₁
q : P₂
r : V₁
hr : r ∈ direction
he : (f.linear : (a : V₁) → V₂) r = q -ᵥ (f : (a : P₁) → P₂) p
⊢ (f : (a : P₁) → P₂) (r +ᵥ p) = q

Tactic:
simp [he]
-- 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₂
p : P₁
direction : Submodule k V₁
q : P₂
r : V₁
hr : r ∈ direction
he : (f.linear : (a : V₁) → V₂) r = q -ᵥ (f : (a : P₁) → P₂) p
⊢ ∃ (y : P₁), y -ᵥ p ∈ direction ∧ (f : (a : P₁) → P₂) y = q

Tactic:
exact ⟨r +ᵥ p, by simp [hr], by simp [he]⟩
-- 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₁
inst_4 : Nonempty.{u_3 + 1} ↥S₁
h : S₁ ≤ S₂
x : ↥S₁
⊢ (↑((inclusion h : (a : ↥S₁) → ↥S₂) x) : P₁) = (↑x : P₁)

Tactic:
rfl

Premises used: Set.Mem, 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₁
inst_4 : Nonempty.{u_3 + 1} ↥S₁
⊢ Eq (α := AffineMap.{u_1, u_2, u_3, u_2, u_3} k ↥S₁ ↥S₁) (inclusion ⋯) (AffineMap.id k ↥S₁)

Tactic:
rfl

Premises used: AffineSubspace.inclusion, Submodule.inclusion, AffineMap.id, LinearMap.codRestrict, 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₂
hf : Function.Surjective.{u_3 + 1, u_5 + 1} (α := P₁) (β := P₂) (⇑f : (a : P₁) → P₂)
rw : (↑(AffineSubspace.map f ⊤) : Set P₂) = (↑⊤ : Set P₂)
⊢ AffineSubspace.map f ⊤ = ⊤

Tactic:
rw [AffineSubspace.ext_iff]

Premises used: AffineSubspace.ext_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₂
hf : Function.Surjective.{u_3 + 1, u_5 + 1} (α := P₁) (β := P₂) (⇑f : (a : P₁) → P₂)
⊢ (↑(AffineSubspace.map f ⊤) : Set P₂) = (↑⊤ : Set P₂)

Tactic:
image_univ_of_surjective hf

Premises used: Set.Mem, Set.univ, setOf, Set.image_univ_of_surjective, Set.image
-- 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.Surjective.{u_3 + 1, u_5 + 1} (α := P₁) (β := P₂) (⇑f : (a : P₁) → P₂)
⊢ (↑(AffineSubspace.map f ⊤) : Set P₂) = (↑⊤ : Set P₂)

Tactic:
exact image_univ_of_surjective hf

Premises used: Set.image_univ_of_surjective
-- 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₁
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 ⊤ = ⊤
rw₂ rw₃ : Eq.{u_5 + 1} (α := AffineSubspace k P₂) ⊤ ⊤
⊢ Eq.{u_5 + 1} (α := AffineSubspace k P₂) (affineSpan k ((⇑f : (a : P₁) → P₂) '' s)) ⊤

Tactic:
rw [← AffineSubspace.map_span, h, map_top_of_surjective f hf]

Premises used: AffineSubspace.map_span, AffineMap.map_top_of_surjective
-- 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₁
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
H : EqOn.{u_2, u_8} (β := V₂) (⇑f.linear : (a : V₁) → V₂) (⇑g.linear : (a : V₁) → V₂) (s -ᵥ s)
⊢ EqOn.{u_2, u_8} (β := V₂) (⇑f.linear : (a : V₁) → V₂) (⇑g.linear : (a : V₁) → V₂)
    (↑(Submodule.span k (s -ᵥ s)) : Set V₁)

Tactic:
apply LinearMap.eqOn_span

Premises used: LinearMap.eqOn_span
-- 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₁
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
x : P₁
hx : x ∈ s
y : P₁
hy : y ∈ s
⊢ Eq.{u_8 + 1} (α := V₂) ((f.linear : (a : V₁) → V₂) ((fun (x1 x2 : P₁) ↦ x1 -ᵥ x2) x y) : V₂)
    ((g.linear : (a : V₁) → V₂) ((fun (x1 x2 : P₁) ↦ x1 -ᵥ x2) x y) : V₂)

Tactic:
simp [h_agree hx, h_agree hy]
-- 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₁
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₁)
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₁)
⊢ 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⟩

Premises used: Set.eq_empty_or_nonempty, 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₁
V₂ : Type u_8
P₂ : Type u_9
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f g : P₁ →ᵃ[k] P₂
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:
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₁
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
q : P₁
hq : q ∈ s
x : P₁
hx : x ∈ s
y : V₁
hy : Membership.mem (γ := Submodule k V₁) (vectorSpan k s) y
⊢ Eq.{u_9 + 1} (α := P₂) ((f : (a : P₁) → P₂) (y +ᵥ x) : P₂) ((g : (a : P₁) → P₂) (y +ᵥ x) : P₂)

Tactic:
simp [h_agree hx, linear_eqOn_vectorSpan h_agree hy]

Premises used: AffineMap.linear_eqOn_vectorSpan
-- 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₁
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_span : Eq (α := AffineSubspace k P₁) (affineSpan k s) ⊤
h_agree : EqOn.{u_3, u_9} (β := P₂) (⇑f : (a : P₁) → P₂) (⇑g : (a : P₁) → P₂) s
⊢ f = g

Tactic:
simpa [h_span] using eqOn_affineSpan h_agree

Premises used: AffineMap.eqOn_affineSpan
-- 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₁
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₁
h_span : Eq (α := AffineSubspace k P₁) (affineSpan k s) ⊤
T₁ T₂ : P₁ ≃ᵃ[k] P₂
h_agree : EqOn.{u_3, u_9} (β := P₂) (⇑T₁ : (a : P₁) → P₂) (⇑T₂ : (a : P₁) → P₂) s
⊢ T₁ = T₂

Tactic:
AffineEquiv.toAffineMap_inj.mp <| AffineMap.ext_on h_span h_agree

Premises used: AffineEquiv.toAffineMap_inj, Iff.mp, AffineMap.ext_on
-- 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₁
inst_4 : Nonempty.{u_3 + 1} ↥S₁
inst_5 : Nonempty.{u_3 + 1} ↥S₂
h : S₁ = S₂
x : ↥S₁
⊢ (↑((ofEq S₁ S₂ h : (a : ↥S₁) → ↥S₂) x) : P₁) = (↑x : P₁)

Tactic:
rfl

Premises used: Set.Mem, 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₁
inst_4 : Nonempty.{u_3 + 1} ↥S₁
inst_5 : Nonempty.{u_3 + 1} ↥S₂
h : S₁ = S₂
h₁ :
  ∀ (x : ↥S₂),
    Eq.{u_3 + 1} (α := P₁) (↑((symm (ofEq S₁ S₂ h) : (a : ↥S₂) → ↥S₁) x) : P₁)
      (↑((ofEq S₂ S₁ ⋯ : (a : ↥S₂) → ↥S₁) x) : P₁)
⊢ Eq (α := AffineEquiv.{u_1, u_3, u_3, u_2, u_2} k ↥S₂ ↥S₁) (symm (ofEq S₁ S₂ h)) (ofEq S₂ S₁ ⋯)

Tactic:
ext
-- 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₁
inst_4 : Nonempty.{u_3 + 1} ↥S₁
inst_5 : Nonempty.{u_3 + 1} ↥S₂
h : S₁ = S₂
x : ↥S₂
⊢ Eq.{u_3 + 1} (α := P₁) (↑((symm (ofEq S₁ S₂ h) : (a : ↥S₂) → ↥S₁) x) : P₁)
    (↑((ofEq S₂ S₁ ⋯ : (a : ↥S₂) → ↥S₁) x) : P₁)

Tactic:
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₁
inst_4 : Nonempty.{u_3 + 1} ↥S₁
⊢ Eq (α := AffineEquiv.{u_1, u_3, u_3, u_2, u_2} k ↥S₁ ↥S₁) (ofEq S₁ S₁ ⋯) (refl k ↥S₁)

Tactic:
rfl

Premises used: AffineEquiv.refl, Equiv.setCongr, LinearEquiv.ofEq, Equiv.subtypeEquivProp, LinearEquiv.refl, Equiv.refl, rfl, AffineEquiv.ofEq
-- 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 : 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)) ⊤

Tactic:
⟨(e : P₁ →ᵃ[k] P₂).span_eq_top_of_surjective e.surjective, ?_⟩

Premises used: AffineMap.span_eq_top_of_surjective, AffineEquiv.toAffineMap, Iff.intro, AffineEquiv.surjective
-- 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 : Set P₁
e : P₁ ≃ᵃ[k] P₂
refine :
  Eq.{u_5 + 1} (α := AffineSubspace k P₂) (affineSpan k ((⇑e : (a : P₁) → P₂) '' s)) ⊤ →
    Eq (α := AffineSubspace k P₁) (affineSpan k s) ⊤
⊢ Eq (α := AffineSubspace k P₁) (affineSpan k s) ⊤ ↔
    Eq.{u_5 + 1} (α := AffineSubspace k P₂) (affineSpan k ((⇑e : (a : P₁) → P₂) '' s)) ⊤

Tactic:
refine ⟨(e : P₁ →ᵃ[k] P₂).span_eq_top_of_surjective e.surjective, ?_⟩
-- 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 : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : Eq.{u_5 + 1} (α := AffineSubspace k P₂) (affineSpan k ((⇑e : (a : P₁) → P₂) '' s)) ⊤
rw : s = Function.comp.{u_3 + 1, u_5 + 1, u_3 + 1} (β := P₂) (⇑e.symm : (a : P₂) → P₁) (⇑e : (a : P₁) → P₂) '' s
⊢ s = image.{u_5, u_3} (α := P₂) (⇑e.symm : (a : P₂) → P₁) ((⇑e : (a : P₁) → P₂) '' s)

Tactic:
rw [← image_comp]

Premises used: Set.image_comp
-- 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 : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : Eq.{u_5 + 1} (α := AffineSubspace k P₂) (affineSpan k ((⇑e : (a : P₁) → P₂) '' s)) ⊤
⊢ s = Function.comp.{u_3 + 1, u_5 + 1, u_3 + 1} (β := P₂) (⇑e.symm : (a : P₂) → P₁) (⇑e : (a : P₁) → 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
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)

Tactic:
have : s = e.symm '' e '' s := by rw [← image_comp]; 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
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)
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))) ⊤
⊢ Eq (α := AffineSubspace k P₁) (affineSpan k s) ⊤

Tactic:
rw [this]
-- 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 : 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.{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:
(e.symm : P₂ →ᵃ[k] P₁).span_eq_top_of_surjective e.symm.surjective h

Premises used: AffineMap.span_eq_top_of_surjective, AffineEquiv.symm, AffineEquiv.toAffineMap, AffineEquiv.surjective
-- 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 : 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.{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:
exact (e.symm : P₂ →ᵃ[k] P₁).span_eq_top_of_surjective e.symm.surjective h

Premises used: AffineMap.span_eq_top_of_surjective, AffineEquiv.symm, AffineEquiv.toAffineMap, AffineEquiv.surjective
-- 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₂
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₂)
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
⊢ Membership.mem (α := P₂) s ((f : (a : P₁) → P₂) (t • (p₁ -ᵥ p₂) +ᵥ p₃) : P₂)

Tactic:
rw [AffineMap.map_vadd, map_smul, AffineMap.linearMap_vsub]

Premises used: AffineMap.linearMap_vsub, AffineMap.map_vadd, map_smul
-- 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₂
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₂)
⊢ 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:
apply s.smul_vsub_vadd_mem _ hp₁ hp₂ hp₃

Premises used: AffineSubspace.smul_vsub_vadd_mem
-- 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₂
⊢ (↑(comap f s) : Set P₁) = (⇑f : (a : P₁) → P₂) ⁻¹' (↑s : Set P₂)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, 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₂
x : P₁
s : AffineSubspace k P₂
⊢ x ∈ comap f s ↔ Membership.mem (α := P₂) s ((f : (a : P₁) → P₂) x : P₂)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- 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 t : AffineSubspace k P₂
⊢ s ≤ t → comap f s ≤ comap f t

Tactic:
preimage_mono

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage_mono, Set.preimage
-- 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₂
rw : (↑(comap f ⊤) : Set P₁) = (↑⊤ : Set P₁)
⊢ comap f ⊤ = ⊤

Tactic:
rw [AffineSubspace.ext_iff]

Premises used: AffineSubspace.ext_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₂
⊢ (↑(comap f ⊤) : Set P₁) = (↑⊤ : Set P₁)

Tactic:
preimage_univ (f := f)

Premises used: Set.Mem, Set.univ, setOf, Set.preimage, Set.preimage_univ
-- 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₂
⊢ (↑(comap f ⊤) : Set P₁) = (↑⊤ : Set P₁)

Tactic:
exact preimage_univ (f := f)

Premises used: Set.preimage_univ
-- 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₂
⊢ comap f ⊥ = ⊥

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, AffineSubspace.comap, rfl