awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_2 : NeZero.{u_1} (R := K) 2
c : OnePoint K
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) ∉ Set.range (ι := K) (⇑(Matrix.scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
hdisc :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    0
infty : HSMul.hSMul (β := OnePoint K) g ∞ = ∞ ↔ ∞ = g.parabolicFixedPoint
⊢ g • c = c ↔ c = g.parabolicFixedPoint
have coe : ∀ (c : K), g • (↑c : OnePoint K) = (↑c : OnePoint K) ↔ (↑c : OnePoint K) = g.parabolicFixedPoint
Tactic: cases c with
  | infty => by_cases h : g 1 0 = 0 <;> simp [parabolicFixedPoint, smul_infty_eq_ite, h]
  | coe c =>
    suffices g 1 0 * c ^ 2 + (g 1 1 - g 0 0) * c - g 0 1 = 0 ↔ c = g.parabolicFixedPoint by
      simpa [← fixpointPolynomial_aeval_eq_zero_iff, fixpointPolynomial]
    by_cases hc : g 1 0 = 0
    · have hd : g 1 1 = g 0 0 := by grind
      suffices g 0 1 ≠ 0 by simpa [parabolicFixedPoint, hc, hd]
      -- can't have `g 0 1 ≠ 0` since that would force `g` to be scalar
      refine fun hb ↦ fixpointPolynomial_eq_zero_iff.not.mpr hg ?_
      simp [fixpointPolynomial, hb, hc, hd]
    · have : discrim (g 1 0) (g 1 1 - g 0 0) (-g 0 1) = 0 := by rw [discrim]; grind
      simpa [parabolicFixedPoint, if_neg hc, sq, sub_eq_add_neg]
        using quadratic_eq_zero_iff_of_discrim_eq_zero hc this c
Cleared hypotheses: c
-- 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
hg : g.IsParabolic
inst_2 : CharZero K
n : ℕ
hn : n ≠ 0
⊢ (g ^ n).parabolicFixedPoint = g.parabolicFixedPoint
have rw : g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint
Tactic: rw [eq_comm, ← IsParabolic.smul_eq_self_iff (hg.pow hn)]
-- 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
hg : g.IsParabolic
inst_2 : CharZero K
n : ℕ
IH : g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint
⊢ g ^ (n + 1) • g.parabolicFixedPoint = g.parabolicFixedPoint
have succ : (g ^ n * g) • g.parabolicFixedPoint = g.parabolicFixedPoint
Tactic: rw [pow_succ, mul_smul, hg.smul_eq_self_iff.mpr rfl, IH]
-- 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
hg : g.IsParabolic
inst_2 : CharZero K
n : ℕ
IH : g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint
succ : (g ^ n * g) • g.parabolicFixedPoint = g.parabolicFixedPoint
⊢ g ^ (n + 1) • g.parabolicFixedPoint = g.parabolicFixedPoint
have succ₁ : g ^ n • g • g.parabolicFixedPoint = g.parabolicFixedPoint
Tactic: rw [pow_succ, mul_smul, hg.smul_eq_self_iff.mpr rfl, IH]
-- 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
hg : g.IsParabolic
inst_2 : CharZero K
n : ℕ
IH : g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint
succ : (g ^ n * g) • g.parabolicFixedPoint = g.parabolicFixedPoint
succ₁ : g ^ n • g • g.parabolicFixedPoint = g.parabolicFixedPoint
succ₂ : g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint
⊢ g ^ (n + 1) • g.parabolicFixedPoint = g.parabolicFixedPoint
have succ₃ : g.parabolicFixedPoint = g.parabolicFixedPoint
Tactic: rw [pow_succ, mul_smul, hg.smul_eq_self_iff.mpr rfl, IH]
-- 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
hg : g.IsParabolic
inst_2 : CharZero K
n : ℕ
⊢ g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint
have zero : HPow.hPow (β := ℕ) g 0 • g.parabolicFixedPoint = g.parabolicFixedPoint
Tactic: induction n with
  | zero => simp
  | succ n IH => rw [pow_succ, mul_smul, hg.smul_eq_self_iff.mpr rfl, IH]
Cleared hypotheses: n
-- 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
hg : g.IsParabolic
inst_2 : CharZero K
n : ℕ
zero : HPow.hPow (β := ℕ) g 0 • g.parabolicFixedPoint = g.parabolicFixedPoint
⊢ g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint
have succ : ∀ (n : ℕ) (IH : g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint),
  g ^ (n + 1) • g.parabolicFixedPoint = g.parabolicFixedPoint
Tactic: induction n with
  | zero => simp
  | succ n IH => rw [pow_succ, mul_smul, hg.smul_eq_self_iff.mpr rfl, IH]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
⊢ HSMul.hSMul (β := OnePoint K) g ∞ ≠ ∞
have infty : ¬(↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
Tactic: rw [Ne, smul_infty_eq_self_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
⊢ ¬(↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
have infty : ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0), 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) K).discr
Tactic: refine fun h ↦ not_le_of_gt hg ?_
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) K).discr =
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 - (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2
have simp : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
    4 *
      ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
        (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 - (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2
Tactic: simp only [discr_fin_two, trace_fin_two, det_fin_two]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
⊢ 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) K).discr
have this : (↑g : Matrix (Fin 2) (Fin 2) K).discr =
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 - (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2
Tactic: have : g.val.discr = (g 0 0 - g 1 1) ^ 2 := by
      simp only [discr_fin_two, trace_fin_two, det_fin_two]
      grind
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
this :
  (↑g : Matrix (Fin 2) (Fin 2) K).discr =
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 - (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2
⊢ 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) K).discr
have infty : 0 ≤ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 - (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
⊢ g • (↑c : OnePoint K) ≠ (↑c : OnePoint K)
have coe : ∀ (h : g • (↑c : OnePoint K) = (↑c : OnePoint K)), 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) K).discr
Tactic: refine fun h ↦ not_le_of_gt hg ?_
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
h : g • (↑c : OnePoint K) = (↑c : OnePoint K)
⊢ (↑g : Matrix (Fin 2) (Fin 2) K).discr =
    HPow.hPow (β := ℕ)
      (2 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c +
        ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0))
      2
have h₁ : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * (c * c) +
      ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0) * c +
    -(↑g : Matrix (Fin 2) (Fin 2) K) 0 1 =
  0
Tactic: replace h : g 1 0 * (c * c) + (g 1 1 + -g 0 0) * c + -g 0 1 = 0 := by
        simpa [← fixpointPolynomial_aeval_eq_zero_iff, fixpointPolynomial, sq, sub_eq_add_neg]
          using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
h :
  (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * (c * c) +
        ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0) * c +
      -(↑g : Matrix (Fin 2) (Fin 2) K) 0 1 =
    0
⊢ (↑g : Matrix (Fin 2) (Fin 2) K).discr =
    HPow.hPow (β := ℕ)
      (2 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c +
        ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0))
      2
have simp : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
    4 *
      ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
        (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0) 2 -
    4 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * -(↑g : Matrix (Fin 2) (Fin 2) K) 0 1
Tactic: simp only [← discrim_eq_sq_of_quadratic_eq_zero h, discr_fin_two, discrim, trace_fin_two,
        det_fin_two]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
h : g • (↑c : OnePoint K) = (↑c : OnePoint K)
⊢ 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) K).discr
have this : (↑g : Matrix (Fin 2) (Fin 2) K).discr =
  HPow.hPow (β := ℕ)
    (2 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c +
      ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0))
    2
Tactic: have : g.val.discr = (2 * g 1 0 * c + (g 1 1 + -g 0 0)) ^ 2 := by
      replace h : g 1 0 * (c * c) + (g 1 1 + -g 0 0) * c + -g 0 1 = 0 := by
        simpa [← fixpointPolynomial_aeval_eq_zero_iff, fixpointPolynomial, sq, sub_eq_add_neg]
          using h
      simp only [← discrim_eq_sq_of_quadratic_eq_zero h, discr_fin_two, discrim, trace_fin_two,
        det_fin_two]
      grind
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
h : g • (↑c : OnePoint K) = (↑c : OnePoint K)
this :
  (↑g : Matrix (Fin 2) (Fin 2) K).discr =
    HPow.hPow (β := ℕ)
      (2 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c +
        ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0))
      2
⊢ 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) K).discr
have coe : 0 ≤
  HPow.hPow (β := ℕ)
    (2 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c +
      ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0))
    2
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : OnePoint K
⊢ g • c ≠ c
have infty : HSMul.hSMul (β := OnePoint K) g ∞ ≠ ∞
Tactic: cases c with
  | infty =>
    rw [Ne, smul_infty_eq_self_iff]
    refine fun h ↦ not_le_of_gt hg ?_
    have : g.val.discr = (g 0 0 - g 1 1) ^ 2 := by
      simp only [discr_fin_two, trace_fin_two, det_fin_two]
      grind
    rw [this]
    apply sq_nonneg
  | coe c =>
    refine fun h ↦ not_le_of_gt hg ?_
    have : g.val.discr = (2 * g 1 0 * c + (g 1 1 + -g 0 0)) ^ 2 := by
      replace h : g 1 0 * (c * c) + (g 1 1 + -g 0 0) * c + -g 0 1 = 0 := by
        simpa [← fixpointPolynomial_aeval_eq_zero_iff, fixpointPolynomial, sq, sub_eq_add_neg]
          using h
      simp only [← discrim_eq_sq_of_quadratic_eq_zero h, discr_fin_two, discrim, trace_fin_two,
        det_fin_two]
      grind
    rw [this]
    apply sq_nonneg
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : OnePoint K
infty : HSMul.hSMul (β := OnePoint K) g ∞ ≠ ∞
⊢ g • c ≠ c
have coe : ∀ (c : K), g • (↑c : OnePoint K) ≠ (↑c : OnePoint K)
Tactic: cases c with
  | infty =>
    rw [Ne, smul_infty_eq_self_iff]
    refine fun h ↦ not_le_of_gt hg ?_
    have : g.val.discr = (g 0 0 - g 1 1) ^ 2 := by
      simp only [discr_fin_two, trace_fin_two, det_fin_two]
      grind
    rw [this]
    apply sq_nonneg
  | coe c =>
    refine fun h ↦ not_le_of_gt hg ?_
    have : g.val.discr = (2 * g 1 0 * c + (g 1 1 + -g 0 0)) ^ 2 := by
      replace h : g 1 0 * (c * c) + (g 1 1 + -g 0 0) * c + -g 0 1 = 0 := by
        simpa [← fixpointPolynomial_aeval_eq_zero_iff, fixpointPolynomial, sq, sub_eq_add_neg]
          using h
      simp only [← discrim_eq_sq_of_quadratic_eq_zero h, discr_fin_two, discrim, trace_fin_two,
        det_fin_two]
      grind
    rw [this]
    apply sq_nonneg
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Sphere (hypothesis)
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
⊢ Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have this : Nonempty ι
Tactic: have : Nonempty ι := Fintype.card_pos_iff.mp <| by lia
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Sphere (hypothesis)
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
⊢ Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have hv : ‖v‖ = 1
Tactic: have hv : ‖v‖ = 1 := by simp [v]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Sphere (hypothesis)
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
hv : ‖v‖ = 1
⊢ Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have hv₀ : v ≠ 0
Tactic: have hv₀ : v ≠ 0 := fun contra ↦ by simp [contra] at hv
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Sphere (hypothesis)
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
hv : ‖v‖ = 1
hv₀ : v ≠ 0
⊢ Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have this₁ : Fact (finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1)
Tactic: have : Fact (finrank ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1) := ⟨by simp [h]⟩
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Sphere (hypothesis)
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this_1 : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
hv : ‖v‖ = 1
hv₀ : v ≠ 0
this : Fact (finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1)
⊢ Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have hV : finrank ℝ V = finrank.{0, u_1} ℝ ↥(ℝ ∙ v)ᗮ
Tactic: have hV : finrank ℝ V = finrank ℝ (ℝ ∙ v)ᗮ := (finrank_orthogonal_span_singleton hv₀).symm
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Sphere (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
⊢ Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have have : (this : Nonempty ι) → Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
Tactic: classical
  have : Nonempty ι := Fintype.card_pos_iff.mp <| by lia
  let v : EuclideanSpace ℝ ι := .single (Classical.arbitrary ι) 1
  have hv : ‖v‖ = 1 := by simp [v]
  have hv₀ : v ≠ 0 := fun contra ↦ by simp [contra] at hv
  have : Fact (finrank ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1) := ⟨by simp [h]⟩
  have hV : finrank ℝ V = finrank ℝ (ℝ ∙ v)ᗮ := (finrank_orthogonal_span_singleton hv₀).symm
  letI e : V ≃ₜ (ℝ ∙ v)ᗮ := (FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq hV).some
  exact e.onePointCongr.trans <| onePointHyperplaneHomeoUnitSphere hv
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Sphere (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
have have₁ have₂ have₃ : (this : Nonempty ι) → Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
⊢ Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have have₄ : (this : Nonempty ι) →
  let v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1;
  (hv : ‖v‖ = 1) → Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
Tactic: classical
  have : Nonempty ι := Fintype.card_pos_iff.mp <| by lia
  let v : EuclideanSpace ℝ ι := .single (Classical.arbitrary ι) 1
  have hv : ‖v‖ = 1 := by simp [v]
  have hv₀ : v ≠ 0 := fun contra ↦ by simp [contra] at hv
  have : Fact (finrank ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1) := ⟨by simp [h]⟩
  have hV : finrank ℝ V = finrank ℝ (ℝ ∙ v)ᗮ := (finrank_orthogonal_span_singleton hv₀).symm
  letI e : V ≃ₜ (ℝ ∙ v)ᗮ := (FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq hV).some
  exact e.onePointCongr.trans <| onePointHyperplaneHomeoUnitSphere hv
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Sphere (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
have have₁ have₂ have₃ : (this : Nonempty ι) → Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have₄ :
  (this : Nonempty ι) →
    let v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1;
    (hv : ‖v‖ = 1) → Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
⊢ Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have have₅ : (this : Nonempty ι) →
  let v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1;
  (hv : ‖v‖ = 1) → (hv₀ : v ≠ 0) → Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
Tactic: classical
  have : Nonempty ι := Fintype.card_pos_iff.mp <| by lia
  let v : EuclideanSpace ℝ ι := .single (Classical.arbitrary ι) 1
  have hv : ‖v‖ = 1 := by simp [v]
  have hv₀ : v ≠ 0 := fun contra ↦ by simp [contra] at hv
  have : Fact (finrank ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1) := ⟨by simp [h]⟩
  have hV : finrank ℝ V = finrank ℝ (ℝ ∙ v)ᗮ := (finrank_orthogonal_span_singleton hv₀).symm
  letI e : V ≃ₜ (ℝ ∙ v)ᗮ := (FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq hV).some
  exact e.onePointCongr.trans <| onePointHyperplaneHomeoUnitSphere hv
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Sphere (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
have have₁ have₂ have₃ : (this : Nonempty ι) → Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have₄ :
  (this : Nonempty ι) →
    let v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1;
    (hv : ‖v‖ = 1) → Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have₅ :
  (this : Nonempty ι) →
    let v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1;
    (hv : ‖v‖ = 1) → (hv₀ : v ≠ 0) → Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
⊢ Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have have₆ : (this : Nonempty ι) →
  let v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1;
  (hv : ‖v‖ = 1) →
    (hv₀ : v ≠ 0) →
      (this : Fact (finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1)) →
        Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
Tactic: classical
  have : Nonempty ι := Fintype.card_pos_iff.mp <| by lia
  let v : EuclideanSpace ℝ ι := .single (Classical.arbitrary ι) 1
  have hv : ‖v‖ = 1 := by simp [v]
  have hv₀ : v ≠ 0 := fun contra ↦ by simp [contra] at hv
  have : Fact (finrank ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1) := ⟨by simp [h]⟩
  have hV : finrank ℝ V = finrank ℝ (ℝ ∙ v)ᗮ := (finrank_orthogonal_span_singleton hv₀).symm
  letI e : V ≃ₜ (ℝ ∙ v)ᗮ := (FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq hV).some
  exact e.onePointCongr.trans <| onePointHyperplaneHomeoUnitSphere hv