awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
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
⊢ (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
have 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) sorry) : OnePoint X) : OnePoint X))
    ((fun (p : OnePoint X) ↦ p.elim y f) ∞))
  ∞
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
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
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) ∞))
    ∞
⊢ (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
have coe : ∀ (p : X),
  (fun (q : Y) ↦
        (if hq : q = y then ∞ else (↑(Exists.choose (p := fun (y : X) ↦ f y = q) sorry) : OnePoint X) : OnePoint X))
      ((fun (p : OnePoint X) ↦ p.elim y f) (↑p : OnePoint X)) =
    (↑p : OnePoint X)
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
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
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
⊢ (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
have 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) sorry) : OnePoint X) : OnePoint X))
        q) =
    q
Tactic: rcases eq_or_ne q y with rfl | hq
Cleared hypotheses: y, hy, this
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
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
⊢ (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
have 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) sorry) : OnePoint X) : OnePoint X))
        q) =
    q
Tactic: rcases eq_or_ne q y with rfl | hq
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (hypothesis)
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
⊢ (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
have hq' : q ∈ range f
Tactic: have hq' : q ∈ range f := by simpa [hy]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
R : Type u_1
inst : Semiring R
m : Matrix (Fin 2) (Fin 2) R
v : Fin 2 → R
⊢ m *ᵥ v = ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1]
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
R : Type u_1
inst : Semiring R
m : Matrix (Fin 2) (Fin 2) R
v : Fin 2 → R
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
have h : (m *ᵥ v) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : 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, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
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, ⋯⟩)
⊢ (m *ᵥ v) i = ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1] i
have h₁ : (m *ᵥ v) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : 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, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
p : ℙ K (Fin 2 → K)
⊢ OnePoint K
have 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)
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
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (hypothesis)
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
⊢ 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))
have ht : t ≠ 0
Tactic: have ht : t ≠ 0 := by rintro rfl; simp at hv
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
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
⊢ 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))
have 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))
Tactic: by_cases h₀ : w 1 = 0
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
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))
⊢ 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))
have 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))
Tactic: by_cases h₀ : w 1 = 0
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
p : 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
have 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))
          sorry p :
        OnePoint K))
    ((fun (p : OnePoint K) ↦ (p.elim (mk K ![1, 0] sorry) fun (t : K) ↦ mk K ![t, 1] sorry : ℙ K (Fin 2 → K))) ∞))
  ∞
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
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))) ∞))
    ∞
⊢ (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
have 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))
            sorry p :
          OnePoint K))
      ((fun (p : OnePoint K) ↦ (p.elim (mk K ![1, 0] sorry) fun (t : K) ↦ mk K ![t, 1] sorry : ℙ K (Fin 2 → K)))
        (↑x : OnePoint K)) =
    (↑x : OnePoint K)
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
w : Fin 2 → K
hw : w ≠ 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)
have pos : ∀ (h₀ : w 1 = 0),
  Eq (α := ℙ K (Fin 2 → K))
    ((fun (p : OnePoint K) ↦ (p.elim (mk K ![1, 0] sorry) fun (t : K) ↦ mk K ![t, 1] sorry : ℙ 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))
              sorry p :
            OnePoint K))
        (mk K w hw)))
    (mk K w hw)
Tactic: by_cases h₀ : w 1 = 0
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
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)
⊢ 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)
have neg : ∀ (h₀ : ¬w 1 = 0),
  Eq (α := ℙ K (Fin 2 → K))
    ((fun (p : OnePoint K) ↦ (p.elim (mk K ![1, 0] sorry) fun (t : K) ↦ mk K ![t, 1] sorry : ℙ 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))
              sorry p :
            OnePoint K))
        (mk K w hw)))
    (mk K w hw)
Tactic: by_cases h₀ : w 1 = 0
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
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)
have pos : ∃ (a : K), a • w = ![1, 0]
Tactic: simp only [mk_eq_mk_iff', h₀, Projectivization.lift_mk, if_true,
        if_false, OnePoint.elim_infty, OnePoint.elim_some]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
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)
have neg : ∃ (a : K), a • w = ![(w 1)⁻¹ * w 0, 1]
Tactic: simp only [mk_eq_mk_iff', h₀, Projectivization.lift_mk, if_true,
        if_false, OnePoint.elim_infty, OnePoint.elim_some]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (hypothesis)
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 = ![1, 0]
have this : w 0 ≠ 0
Tactic: have : w 0 ≠ 0 := fun h ↦ hw <| funext <| by simp_all
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
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
⊢ ∃ (a : K), a • w = ![1, 0]
have h : (w 0)⁻¹ • w = ![1, 0]
Tactic: use (w 0)⁻¹
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
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 = ![1, 0]
have h : ∀ (i : Fin 2), ((w 0)⁻¹ • w) i = ![1, 0] i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
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
⊢ ((w 0)⁻¹ • w) i = ![1, 0] i
have h : ((w 0)⁻¹ • w) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) = ![1, 0] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
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, ⋯⟩)
⊢ ((w 0)⁻¹ • w) i = ![1, 0] i
have h₁ : ((w 0)⁻¹ • w) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) = ![1, 0] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
p : ℙ 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))
        p) =
    p
have h : ∀ (w : Fin 2 → K) (hw : w ≠ 0),
  Eq (α := ℙ K (Fin 2 → K))
    ((fun (p : OnePoint K) ↦ (p.elim (mk K ![1, 0] sorry) fun (t : K) ↦ mk K ![t, 1] sorry : ℙ 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))
              sorry p :
            OnePoint K))
        (mk K w hw)))
    (mk K w hw)
Tactic: induction p using ind with | h w hw =>
    by_cases h₀ : w 1 = 0 <;> simp only [mk_eq_mk_iff', h₀, Projectivization.lift_mk, if_true,
        if_false, OnePoint.elim_infty, OnePoint.elim_some]
    · have : w 0 ≠ 0 := fun h ↦ hw <| funext <| by simp_all
      use (w 0)⁻¹
      ext i
      fin_cases i <;> simp_all
    · exact ⟨(w 1)⁻¹, funext <| by simp [inv_mul_cancel₀ h₀]⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
x : OnePoint K
⊢ (equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K)) (g • x) =
    HSMul.hSMul (β := ℙ K (Fin 2 → K)) g
      ((equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K)) x : ℙ K (Fin 2 → K))
have rw : (equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K))
    ((Equiv.symm (equivProjectivization K) : (a : ℙ K (Fin 2 → K)) → OnePoint K)
      (HSMul.hSMul (β := ℙ K (Fin 2 → K)) g
        ((equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K)) x : ℙ K (Fin 2 → K)))) =
  HSMul.hSMul (β := ℙ K (Fin 2 → K)) g
    ((equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K)) x : ℙ K (Fin 2 → K))
Tactic: rw [Equiv.smul_def, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
x : OnePoint K
rw :
  (equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K))
      ((Equiv.symm (equivProjectivization K) : (a : ℙ K (Fin 2 → K)) → OnePoint K)
        (HSMul.hSMul (β := ℙ K (Fin 2 → K)) g
          ((equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K)) x : ℙ K (Fin 2 → K)))) =
    HSMul.hSMul (β := ℙ K (Fin 2 → K)) g
      ((equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K)) x : ℙ K (Fin 2 → K))
⊢ (equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K)) (g • x) =
    HSMul.hSMul (β := ℙ K (Fin 2 → K)) g
      ((equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K)) x : ℙ K (Fin 2 → K))
have rw₁ : HSMul.hSMul (β := ℙ K (Fin 2 → K)) g
    ((equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K)) x : ℙ K (Fin 2 → K)) =
  HSMul.hSMul (β := ℙ K (Fin 2 → K)) g
    ((equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K)) x : ℙ K (Fin 2 → K))
Tactic: rw [Equiv.smul_def, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
⊢ HSMul.hSMul (β := OnePoint K) g ∞ =
    if (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0 then ∞
    else (↑((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 / (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) : OnePoint K)
have pos : ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0),
  HSMul.hSMul (β := OnePoint K) g ∞ =
    if (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0 then ∞
    else (↑((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 / (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) : OnePoint K)
Tactic: by_cases h : g 1 0 = 0