awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
this : Tendsto f (coclosedCompact X) (𝓝 y)
p : OnePoint X
infty :
  Eq.{u_1 + 1} (α := OnePoint X)
    ((fun (q : Y) ↦
        (if hq : q = y then ∞ else (↑(Exists.choose (p := fun (y : X) ↦ f y = q) ⋯) : OnePoint X) : OnePoint X))
      ((fun (p : OnePoint X) ↦ p.elim y f) ∞))
    ∞
coe :
  ∀ (p : X),
    (fun (q : Y) ↦
          (if hq : q = y then ∞ else (↑(Exists.choose (p := fun (y : X) ↦ f y = q) ⋯) : OnePoint X) : OnePoint X))
        ((fun (p : OnePoint X) ↦ p.elim y f) (↑p : OnePoint X)) =
      (↑p : OnePoint X)
⊢ (fun (q : Y) ↦
        (if hq : q = y then ∞ else (↑(Exists.choose (p := fun (y : X) ↦ f y = q) ⋯) : OnePoint X) : OnePoint X))
      ((fun (p : OnePoint X) ↦ p.elim y f) p) =
    p

Tactic:
induction p using OnePoint.rec with
        | infty => simp
        | coe p =>
          have hp : f p ≠ y := by simpa [hy] using mem_range_self (f := f) p
          simpa [hp] using hf.injective (mem_range_self p).choose_spec

Premises used: OnePoint.infty, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
this : Tendsto f (coclosedCompact X) (𝓝 y)
q : Y
inl :
  ∀ (hy : range f = {q}ᶜ) (this : Tendsto f (coclosedCompact X) (𝓝 q)),
    (fun (p : OnePoint X) ↦ p.elim q f)
        ((fun (q_1 : Y) ↦
            (if hq : q_1 = q then ∞ else (↑(Exists.choose (p := fun (y : X) ↦ f y = q_1) ⋯) : OnePoint X) : OnePoint X))
          q) =
      q
inr :
  ∀ (hq : q ≠ y),
    (fun (p : OnePoint X) ↦ p.elim y f)
        ((fun (q : Y) ↦
            (if hq : q = y then ∞ else (↑(Exists.choose (p := fun (y : X) ↦ f y = q) ⋯) : OnePoint X) : OnePoint X))
          q) =
      q
⊢ (fun (p : OnePoint X) ↦ p.elim y f)
      ((fun (q : Y) ↦
          (if hq : q = y then ∞ else (↑(Exists.choose (p := fun (y : X) ↦ f y = q) ⋯) : OnePoint X) : OnePoint X))
        q) =
    q

Tactic:
rcases eq_or_ne q y with rfl | hq

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
f : X → Y
hf : IsEmbedding f
_i : T2Space X
q : Y
hy : range f = {q}ᶜ
this : Tendsto f (coclosedCompact X) (𝓝 q)
⊢ (fun (p : OnePoint X) ↦ p.elim q f)
      ((fun (q_1 : Y) ↦
          (if hq : q_1 = q then ∞ else (↑(Exists.choose (p := fun (y : X) ↦ f y = q_1) ⋯) : OnePoint X) : OnePoint X))
        q) =
    q

Tactic:
simp
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
this : Tendsto f (coclosedCompact X) (𝓝 y)
q : Y
hq : q ≠ y
⊢ q ∈ range f

Tactic:
simpa [hy]
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
this : Tendsto f (coclosedCompact X) (𝓝 y)
q : Y
hq : q ≠ y
⊢ q ∈ range f

Tactic:
have hq' : q ∈ range f := by simpa [hy]
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
this : Tendsto f (coclosedCompact X) (𝓝 y)
q : Y
hq : q ≠ y
hq' : q ∈ range f
⊢ (fun (p : OnePoint X) ↦ p.elim y f)
      ((fun (q : Y) ↦
          (if hq : q = y then ∞ else (↑(Exists.choose (p := fun (y : X) ↦ f y = q) ⋯) : OnePoint X) : OnePoint X))
        q) =
    q

Tactic:
simpa [hq] using hq'.choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
x : X
⊢ (equivOfIsEmbeddingOfRangeEq y f hf hy : (a : OnePoint X) → Y) (↑x : OnePoint X) = f x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
⊢ (equivOfIsEmbeddingOfRangeEq y f hf hy : (a : OnePoint X) → Y) ∞ = y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
⊢ ∃ (α : Type) (β : Type) (x : TopologicalSpace α) (x_1 : TopologicalSpace β),
    CompactSpace α ∧
      T1Space β ∧
        ∃ (f : α ≃ β),
          Continuous (X := α) (Y := β) (⇑f : (a : α) → β) ∧ ¬Continuous (X := β) (Y := α) (⇑f.symm : (a : β) → α)

Tactic:
⟨OnePoint ℕ, CofiniteTopology (OnePoint ℕ), inferInstance, inferInstance, inferInstance,
    inferInstance, CofiniteTopology.of, CofiniteTopology.continuous_of,
    OnePoint.not_continuous_cofiniteTopology_of_symm⟩

Premises used: CofiniteTopology.continuous_of, inferInstance, Nat, And.intro, Exists.intro, OnePoint.not_continuous_cofiniteTopology_of_symm, CofiniteTopology.of, CofiniteTopology, OnePoint
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
R : Type u_1
inst : Semiring R
m : Matrix (Fin 2) (Fin 2) R
v : Fin 2 → R
h : ∀ (i : Fin 2), (m *ᵥ v) i = ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1] i
⊢ m *ᵥ v = ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1]

Tactic:
ext i
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
R : Type u_1
inst : Semiring R
m : Matrix (Fin 2) (Fin 2) R
v : Fin 2 → R
i : Fin 2
h :
  (m *ᵥ v) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
h₁ :
  (m *ᵥ v) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (m *ᵥ v) i = ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1] i

Tactic:
fin_cases i
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
R : Type u_1
inst : Semiring R
m : Matrix (Fin 2) (Fin 2) R
v : Fin 2 → R
⊢ (m *ᵥ v) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [mulVec_eq_sum]

Premises used: Matrix.mulVec_eq_sum
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
R : Type u_1
inst : Semiring R
m : Matrix (Fin 2) (Fin 2) R
v : Fin 2 → R
⊢ (m *ᵥ v) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [mulVec_eq_sum]

Premises used: Matrix.mulVec_eq_sum
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
R : Type u_3
inst : CommRing R
g : GL (Fin 2) R
v : Fin 2 → R
⊢ g • v =
    ![(↑g : Matrix (Fin 2) (Fin 2) R) 0 0 * v 0 + (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 * v 1,
      (↑g : Matrix (Fin 2) (Fin 2) R) 1 0 * v 0 + (↑g : Matrix (Fin 2) (Fin 2) R) 1 1 * v 1]

Tactic:
simp [Units.smul_def]

Premises used: Units.smul_def
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
R : Type u_1
n : Type u_2
inst : Semiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
S : Type u_3
inst_3 : DistribSMul S R
inst_4 : SMulCommClass R S R
⊢ SMulCommClass.{u_1, u_3, u_1} (Matrix (Fin 2) (Fin 2) R) S (R × R)

Tactic:
(LinearEquiv.finTwoArrow R R).symm.smulCommClass _ _

Premises used: Eq.mpr, LinearEquiv.symm, LinearEquiv.finTwoArrow, Fin.cons, Fin.induction.go, LinearEquiv.toAddEquiv, Fin.induction, Equiv.smulCommClass, Fin.cases, AddEquiv.toEquiv, Matrix.vecCons
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
R : Type u_1
inst : Semiring R
g : Matrix (Fin 2) (Fin 2) R
v : R × R
⊢ g • v = (g 0 0 * v.1 + g 0 1 * v.2, g 1 0 * v.1 + g 1 1 * v.2)

Tactic:
simp [Equiv.smul_def, smul_eq_mulVec, Matrix.mulVec_eq_sum]

Premises used: Equiv.smul_def, Matrix.mulVec_eq_sum, Matrix.smul_eq_mulVec
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
R : Type u_3
inst : CommRing R
g : GL (Fin 2) R
v : R × R
⊢ g • v =
    ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0 * v.1 + (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 * v.2,
      (↑g : Matrix (Fin 2) (Fin 2) R) 1 0 * v.1 + (↑g : Matrix (Fin 2) (Fin 2) R) 1 1 * v.2)

Tactic:
simp [Units.smul_def, Matrix.fin_two_smul_prod]

Premises used: Matrix.fin_two_smul_prod, Units.smul_def
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
p : OnePoint K
⊢ Ne.{u_1 + 1} (α := Fin 2 → K) ![1, 0] 0

Tactic:
simp
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
p : OnePoint K
t : K
⊢ ![t, 1] ≠ 0

Tactic:
simp
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
p : ℙ K (Fin 2 → K)
refine :
  ∀ (a b : { v : Fin 2 → K // v ≠ 0 }) (t : K),
    (↑a : Fin 2 → K) = t • (↑b : Fin 2 → K) →
      Eq.{u_1 + 1} (α := OnePoint K)
        ((fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
            if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
          a)
        ((fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
            if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
          b)
⊢ OnePoint K

Tactic:
refine Projectivization.lift
      (fun u : {v : Fin 2 → K // v ≠ 0} ↦ if u.1 1 = 0 then ∞ else ((u.1 1)⁻¹ * u.1 0)) ?_ p

Premises used: OnePoint.infty, Projectivization.lift, OfNat.ofNat, Subtype.val, Eq, ite
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
hv : HSMul.hSMul (α := K) 0 (↑(Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0) w hw) : Fin 2 → K) ≠ 0
⊢ False

Tactic:
simp at hv
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
t : K
hv : t • (↑(Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0) w hw) : Fin 2 → K) ≠ 0
⊢ t ≠ 0

Tactic:
have ht : t ≠ 0 := by rintro rfl; simp at hv
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
t : K
hv : t • (↑(Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0) w hw) : Fin 2 → K) ≠ 0
ht : t ≠ 0
pos :
  ∀ (h₀ : w 1 = 0),
    Eq.{u_1 + 1} (α := OnePoint K)
      ((fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
          if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
        (Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0)
          (t • (↑(Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0) w hw) : Fin 2 → K)) hv))
      ((fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
          if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
        (Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0) w hw))
neg :
  ∀ (h₀ : ¬w 1 = 0),
    Eq.{u_1 + 1} (α := OnePoint K)
      ((fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
          if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
        (Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0)
          (t • (↑(Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0) w hw) : Fin 2 → K)) hv))
      ((fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
          if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
        (Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0) w hw))
⊢ Eq.{u_1 + 1} (α := OnePoint K)
    ((fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
        if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
      (Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0)
        (t • (↑(Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0) w hw) : Fin 2 → K)) hv))
    ((fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
        if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
      (Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0) w hw))

Tactic:
by_cases h₀ : w 1 = 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
t : K
hv : t • (↑(Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0) w hw) : Fin 2 → K) ≠ 0
ht : t ≠ 0
h₀ : w 1 = 0
⊢ Eq.{u_1 + 1} (α := OnePoint K)
    ((fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
        if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
      (Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0)
        (t • (↑(Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0) w hw) : Fin 2 → K)) hv))
    ((fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
        if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
      (Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0) w hw))

Tactic:
simp [h₀, ht, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
t : K
hv : t • (↑(Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0) w hw) : Fin 2 → K) ≠ 0
ht : t ≠ 0
h₀ : ¬w 1 = 0
⊢ Eq.{u_1 + 1} (α := OnePoint K)
    ((fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
        if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
      (Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0)
        (t • (↑(Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0) w hw) : Fin 2 → K)) hv))
    ((fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
        if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
      (Subtype.mk (p := fun (v : Fin 2 → K) ↦ v ≠ 0) w hw))

Tactic:
simp [h₀, ht, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
p : OnePoint K
infty :
  Eq.{u_1 + 1} (α := OnePoint K)
    ((fun (p : ℙ K (Fin 2 → K)) ↦
        (Projectivization.lift
            (fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
              if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
            ⋯ p :
          OnePoint K))
      ((fun (p : OnePoint K) ↦ (p.elim (mk K ![1, 0] ⋯) fun (t : K) ↦ mk K ![t, 1] ⋯ : ℙ K (Fin 2 → K))) ∞))
    ∞
coe :
  ∀ (x : K),
    (fun (p : ℙ K (Fin 2 → K)) ↦
          (Projectivization.lift
              (fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
                if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
              ⋯ p :
            OnePoint K))
        ((fun (p : OnePoint K) ↦ (p.elim (mk K ![1, 0] ⋯) fun (t : K) ↦ mk K ![t, 1] ⋯ : ℙ K (Fin 2 → K)))
          (↑x : OnePoint K)) =
      (↑x : OnePoint K)
⊢ (fun (p : ℙ K (Fin 2 → K)) ↦
        (Projectivization.lift
            (fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
              if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
            ⋯ p :
          OnePoint K))
      ((fun (p : OnePoint K) ↦ (p.elim (mk K ![1, 0] ⋯) fun (t : K) ↦ mk K ![t, 1] ⋯ : ℙ K (Fin 2 → K))) p) =
    p

Tactic:
cases p
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
⊢ Eq.{u_1 + 1} (α := OnePoint K)
    ((fun (p : ℙ K (Fin 2 → K)) ↦
        (Projectivization.lift
            (fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
              if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
            ⋯ p :
          OnePoint K))
      ((fun (p : OnePoint K) ↦ (p.elim (mk K ![1, 0] ⋯) fun (t : K) ↦ mk K ![t, 1] ⋯ : ℙ K (Fin 2 → K))) ∞))
    ∞

Tactic:
simp
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
x : K
⊢ (fun (p : ℙ K (Fin 2 → K)) ↦
        (Projectivization.lift
            (fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
              if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
            ⋯ p :
          OnePoint K))
      ((fun (p : OnePoint K) ↦ (p.elim (mk K ![1, 0] ⋯) fun (t : K) ↦ mk K ![t, 1] ⋯ : ℙ K (Fin 2 → K)))
        (↑x : OnePoint K)) =
    (↑x : OnePoint K)

Tactic:
simp
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
pos :
  ∀ (h₀ : w 1 = 0),
    Eq (α := ℙ K (Fin 2 → K))
      ((fun (p : OnePoint K) ↦ (p.elim (mk K ![1, 0] ⋯) fun (t : K) ↦ mk K ![t, 1] ⋯ : ℙ K (Fin 2 → K)))
        ((fun (p : ℙ K (Fin 2 → K)) ↦
            (Projectivization.lift
                (fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
                  if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
                ⋯ p :
              OnePoint K))
          (mk K w hw)))
      (mk K w hw)
neg :
  ∀ (h₀ : ¬w 1 = 0),
    Eq (α := ℙ K (Fin 2 → K))
      ((fun (p : OnePoint K) ↦ (p.elim (mk K ![1, 0] ⋯) fun (t : K) ↦ mk K ![t, 1] ⋯ : ℙ K (Fin 2 → K)))
        ((fun (p : ℙ K (Fin 2 → K)) ↦
            (Projectivization.lift
                (fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
                  if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
                ⋯ p :
              OnePoint K))
          (mk K w hw)))
      (mk K w hw)
⊢ Eq (α := ℙ K (Fin 2 → K))
    ((fun (p : OnePoint K) ↦ (p.elim (mk K ![1, 0] ⋯) fun (t : K) ↦ mk K ![t, 1] ⋯ : ℙ K (Fin 2 → K)))
      ((fun (p : ℙ K (Fin 2 → K)) ↦
          (Projectivization.lift
              (fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
                if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
              ⋯ p :
            OnePoint K))
        (mk K w hw)))
    (mk K w hw)

Tactic:
by_cases h₀ : w 1 = 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 0
pos : ∃ (a : K), a • w = ![1, 0]
⊢ Eq (α := ℙ K (Fin 2 → K))
    ((fun (p : OnePoint K) ↦ (p.elim (mk K ![1, 0] ⋯) fun (t : K) ↦ mk K ![t, 1] ⋯ : ℙ K (Fin 2 → K)))
      ((fun (p : ℙ K (Fin 2 → K)) ↦
          (Projectivization.lift
              (fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
                if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
              ⋯ p :
            OnePoint K))
        (mk K w hw)))
    (mk K w hw)

Tactic:
simp only [mk_eq_mk_iff', h₀, Projectivization.lift_mk, if_true,
        if_false, OnePoint.elim_infty, OnePoint.elim_some]

Premises used: if_true, if_false, OnePoint.elim_some, OnePoint.elim_infty, Projectivization.lift_mk, Projectivization.mk_eq_mk_iff'
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : ¬w 1 = 0
neg : ∃ (a : K), a • w = ![(w 1)⁻¹ * w 0, 1]
⊢ Eq (α := ℙ K (Fin 2 → K))
    ((fun (p : OnePoint K) ↦ (p.elim (mk K ![1, 0] ⋯) fun (t : K) ↦ mk K ![t, 1] ⋯ : ℙ K (Fin 2 → K)))
      ((fun (p : ℙ K (Fin 2 → K)) ↦
          (Projectivization.lift
              (fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
                if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
              ⋯ p :
            OnePoint K))
        (mk K w hw)))
    (mk K w hw)

Tactic:
simp only [mk_eq_mk_iff', h₀, Projectivization.lift_mk, if_true,
        if_false, OnePoint.elim_infty, OnePoint.elim_some]

Premises used: if_true, if_false, OnePoint.elim_some, OnePoint.elim_infty, Projectivization.lift_mk, Projectivization.mk_eq_mk_iff'
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 0
h : w 0 = 0
⊢ ∀ (x : Fin 2), w x = 0 x

Tactic:
simp_all
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 0
⊢ w 0 ≠ 0

Tactic:
have : w 0 ≠ 0 := fun h ↦ hw <| funext <| by simp_all
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 0
this : w 0 ≠ 0
h : (w 0)⁻¹ • w = ![1, 0]
⊢ ∃ (a : K), a • w = ![1, 0]

Tactic:
use (w 0)⁻¹

Premises used: OfNat.ofNat
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 0
this : w 0 ≠ 0
h : ∀ (i : Fin 2), ((w 0)⁻¹ • w) i = ![1, 0] i
⊢ (w 0)⁻¹ • w = ![1, 0]

Tactic:
ext i
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 0
this : w 0 ≠ 0
i : Fin 2
h : ((w 0)⁻¹ • w) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) = ![1, 0] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
h₁ : ((w 0)⁻¹ • w) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = ![1, 0] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ ((w 0)⁻¹ • w) i = ![1, 0] i

Tactic:
fin_cases i
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 0
this : w 0 ≠ 0
⊢ ((w 0)⁻¹ • w) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) = ![1, 0] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp_all
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 0
this : w 0 ≠ 0
⊢ ((w 0)⁻¹ • w) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = ![1, 0] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp_all
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : ¬w 1 = 0
⊢ ∀ (x : Fin 2), ((w 1)⁻¹ • w) x = ![(w 1)⁻¹ * w 0, 1] x

Tactic:
simp [inv_mul_cancel₀ h₀]

Premises used: inv_mul_cancel₀
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : ¬w 1 = 0
⊢ ∃ (a : K), a • w = ![(w 1)⁻¹ * w 0, 1]

Tactic:
exact ⟨(w 1)⁻¹, funext <| by simp [inv_mul_cancel₀ h₀]⟩