awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Semiring C
inst_6 : TopologicalSpace C
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
g : A ≃A[R] B
f' : A ≃ₐ[R] B
continuous_toFun : Continuous[inst_2, inst_4] f'.toFun
continuous_invFun : Continuous[inst_4, inst_2] f'.invFun
h₁ :
  { toAlgEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun : A ≃A[R] B }.toFun =
    g.toFun
h₂ :
  { toAlgEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        A ≃A[R] B }.invFun =
    g.invFun
⊢ { toAlgEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun : A ≃A[R] B } = g
have obtain : ∀ (g' : A ≃ₐ[R] B) (continuous_toFun_1 : Continuous[inst_2, inst_4] g'.toFun)
  (continuous_invFun_1 : Continuous[inst_4, inst_2] g'.invFun)
  (h₁ :
    { toAlgEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
          A ≃A[R] B }.toFun =
      { toAlgEquiv := g', continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
          A ≃A[R] B }.toFun)
  (h₂ :
    { toAlgEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
          A ≃A[R] B }.invFun =
      { toAlgEquiv := g', continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
          A ≃A[R] B }.invFun),
  { toAlgEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun : A ≃A[R] B } =
    { toAlgEquiv := g', continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 }
Tactic: obtain ⟨g', _⟩ := g
Cleared hypotheses: g, h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
S : Set B
⊢ Eq.{u_2 + 1} (α := Set A) ((⇑e.symm : (a : B) → A) '' S) ((⇑e : (a : A) → B) ⁻¹' S)
have rw : Eq.{u_2 + 1} (α := Set A) ((⇑e.symm.symm : (a : A) → B) ⁻¹' S) ((⇑e : (a : A) → B) ⁻¹' S)
Tactic: rw [e.symm.image_eq_preimage_symm, e.symm_symm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
S : Set B
rw : Eq.{u_2 + 1} (α := Set A) ((⇑e.symm.symm : (a : A) → B) ⁻¹' S) ((⇑e : (a : A) → B) ⁻¹' S)
⊢ Eq.{u_2 + 1} (α := Set A) ((⇑e.symm : (a : B) → A) '' S) ((⇑e : (a : A) → B) ⁻¹' S)
have rw₁ : Eq.{u_2 + 1} (α := Set A) ((⇑e : (a : A) → B) ⁻¹' S) ((⇑e : (a : A) → B) ⁻¹' S)
Tactic: rw [e.symm.image_eq_preimage_symm, e.symm_symm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra.Equiv (goal)
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A_1
inst_2 : TopologicalSpace A_1
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Semiring C
inst_6 : TopologicalSpace C
inst_7 : Algebra R A_1
inst_8 : Algebra R B
inst_9 : Algebra R C
ι : Type u_5
A : ι → Type u_6
inst_10 : (i : ι) → Semiring (A i)
inst_11 : (i : ι) → Algebra.{u_1, u_6} R (A i)
inst_12 : (i : ι) → TopologicalSpace (A i)
i j : ι
h : i = j
⊢ Continuous[inst_12 i, inst_12 j] (Equiv.toFun (AlgEquiv.toEquiv.{u_1, u_6, u_6} (R := R) (AlgEquiv.cast (A := A) h)))
have refl : Continuous[inst_12 i, inst_12 i] (Equiv.toFun (AlgEquiv.toEquiv.{u_1, u_6, u_6} (R := R) (AlgEquiv.cast (A := A) sorry)))
Tactic: cases h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra.Equiv (goal)
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A_1
inst_2 : TopologicalSpace A_1
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Semiring C
inst_6 : TopologicalSpace C
inst_7 : Algebra R A_1
inst_8 : Algebra R B
inst_9 : Algebra R C
ι : Type u_5
A : ι → Type u_6
inst_10 : (i : ι) → Semiring (A i)
inst_11 : (i : ι) → Algebra.{u_1, u_6} R (A i)
inst_12 : (i : ι) → TopologicalSpace (A i)
i j : ι
h : i = j
⊢ Continuous[inst_12 j, inst_12 i] (Equiv.invFun (AlgEquiv.toEquiv.{u_1, u_6, u_6} (R := R) (AlgEquiv.cast (A := A) h)))
have refl : Continuous[inst_12 i, inst_12 i] (Equiv.invFun (AlgEquiv.toEquiv.{u_1, u_6, u_6} (R := R) (AlgEquiv.cast (A := A) sorry)))
Tactic: cases h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra (goal)
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : ContinuousSMul R A
⊢ Continuous[inst_3, inst_4] (⇑(algebraMap R A) : (a : R) → A)
have rw : Continuous[inst_3, inst_4] fun (r : R) ↦ HSMul.hSMul (β := A) r 1
Tactic: rw [algebraMap_eq_smul_one']
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra (goal)
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : ContinuousMul A
⊢ Continuous[inst_3, inst_4] (⇑(algebraMap R A) : (a : R) → A) ↔
    Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦ p.1 • p.2
have refine : ∀ (h : Continuous[inst_3, inst_4] (⇑(algebraMap R A) : (a : R) → A)),
  Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦ p.1 • p.2
Tactic: refine ⟨fun h => ?_, fun h => have : ContinuousSMul R A := ⟨h⟩; continuous_algebraMap _ _⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra (goal)
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : ContinuousMul A
h : Continuous[inst_3, inst_4] (⇑(algebraMap R A) : (a : R) → A)
⊢ Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦ p.1 • p.2
have simp : Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) p.1 : A) p.2
Tactic: simp only [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra (goal)
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : ContinuousSMul R A
⊢ Eq (α := R →L[R] A) (toSpanSingleton R 1) (algebraMapCLM R A)
have h : Eq.{u + 1} (α := A) ((toSpanSingleton R 1 : (a : R) → A) 1 : A) ((algebraMapCLM R A : (a : R) → A) 1 : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f g : A →A[R] B
h :
  Eq (α := (a : A) → B) ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) f)
    ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) g)
⊢ f = g
have mk : ∀ (toAlgHom : A →ₐ[R] B) (cont : Continuous[inst_2, inst_4] (↑(↑toAlgHom.toRingHom : A →* B) : OneHom A B).toFun)
  (h :
    Eq (α := (a : A) → B)
      ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) { toAlgHom := toAlgHom, cont := cont })
      ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) g)),
  { toAlgHom := toAlgHom, cont := cont : A →A[R] B } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
g : A →A[R] B
toAlgHom : A →ₐ[R] B
cont : Continuous[inst_2, inst_4] (↑(↑toAlgHom.toRingHom : A →* B) : OneHom A B).toFun
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) { toAlgHom := toAlgHom, cont := cont })
    ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) g)
⊢ { toAlgHom := toAlgHom, cont := cont : A →A[R] B } = g
have mk : ∀ (toAlgHom_1 : A →ₐ[R] B) (cont_1 : Continuous[inst_2, inst_4] (↑(↑toAlgHom_1.toRingHom : A →* B) : OneHom A B).toFun)
  (h :
    Eq (α := (a : A) → B)
      ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) { toAlgHom := toAlgHom, cont := cont })
      ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) { toAlgHom := toAlgHom_1, cont := cont_1 })),
  { toAlgHom := toAlgHom, cont := cont : A →A[R] B } = { toAlgHom := toAlgHom_1, cont := cont_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
toAlgHom : A →ₐ[R] B
cont : Continuous[inst_2, inst_4] (↑(↑toAlgHom.toRingHom : A →* B) : OneHom A B).toFun
toAlgHom_1 : A →ₐ[R] B
cont_1 : Continuous[inst_2, inst_4] (↑(↑toAlgHom_1.toRingHom : A →* B) : OneHom A B).toFun
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) { toAlgHom := toAlgHom, cont := cont })
    ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) { toAlgHom := toAlgHom_1, cont := cont_1 })
⊢ { toAlgHom := toAlgHom, cont := cont : A →A[R] B } = { toAlgHom := toAlgHom_1, cont := cont_1 }
have mk : toAlgHom = toAlgHom_1
Tactic: simp only [mk.injEq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f g : A →A[R] B
⊢ (↑f : A →ₐ[R] B) = (↑g : A →ₐ[R] B) ↔ f = g
have mk : ∀ (toAlgHom : A →ₐ[R] B) (cont : Continuous[inst_2, inst_4] (↑(↑toAlgHom.toRingHom : A →* B) : OneHom A B).toFun),
  (↑{ toAlgHom := toAlgHom, cont := cont : A →A[R] B } : A →ₐ[R] B) = (↑g : A →ₐ[R] B) ↔
    { toAlgHom := toAlgHom, cont := cont : A →A[R] B } = g
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
g : A →A[R] B
toAlgHom : A →ₐ[R] B
cont : Continuous[inst_2, inst_4] (↑(↑toAlgHom.toRingHom : A →* B) : OneHom A B).toFun
⊢ (↑{ toAlgHom := toAlgHom, cont := cont : A →A[R] B } : A →ₐ[R] B) = (↑g : A →ₐ[R] B) ↔
    { toAlgHom := toAlgHom, cont := cont : A →A[R] B } = g
have mk : ∀ (toAlgHom_1 : A →ₐ[R] B) (cont_1 : Continuous[inst_2, inst_4] (↑(↑toAlgHom_1.toRingHom : A →* B) : OneHom A B).toFun),
  (↑{ toAlgHom := toAlgHom, cont := cont : A →A[R] B } : A →ₐ[R] B) =
      (↑{ toAlgHom := toAlgHom_1, cont := cont_1 : A →A[R] B } : A →ₐ[R] B) ↔
    { toAlgHom := toAlgHom, cont := cont : A →A[R] B } = { toAlgHom := toAlgHom_1, cont := cont_1 }
Tactic: cases g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : IsSemitopologicalSemiring A
s : Subalgebra R A
r : R
⊢ Membership.mem (α := A) (closure[inst_2] (↑s : Set A)) ((algebraMap R A : (a : R) → A) r : A)
have a : Membership.mem (α := A) (↑s : Set A) ((algebraMap R A : (a : R) → A) r : A)
Tactic: apply subset_closure
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : IsSemitopologicalSemiring A
inst_8 : IsSemitopologicalSemiring B
f : A →A[R] B
hf' : DenseRange.{u_3, u_2} (X := B) (α := A) (⇑f : (a : A) → B)
s : Subalgebra R A
hs : s.topologicalClosure = ⊤
⊢ (map (↑f : A →ₐ[R] B) s).topologicalClosure = ⊤
have rw : ∀ (hs : (↑s.topologicalClosure : Set A) = (↑⊤ : Set A)),
  (↑(map (↑f : A →ₐ[R] B) s).topologicalClosure : Set B) = (↑⊤ : Set B)
Tactic: rw [SetLike.ext'_iff] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : IsSemitopologicalSemiring A
inst_8 : IsSemitopologicalSemiring B
f : A →A[R] B
hf' : DenseRange.{u_3, u_2} (X := B) (α := A) (⇑f : (a : A) → B)
s : Subalgebra R A
hs : (↑s.topologicalClosure : Set A) = (↑⊤ : Set A)
⊢ (↑(map (↑f : A →ₐ[R] B) s).topologicalClosure : Set B) = (↑⊤ : Set B)
have simp : ∀ (hs : Dense (↑s : Set A)), Dense.{u_3} (X := B) ((⇑(↑f : A →ₐ[R] B) : (a : A) → B) '' (↑s : Set A))
Tactic: simp only [Subalgebra.topologicalClosure_coe, coe_top, ← dense_iff_closure_eq,
    Subalgebra.coe_map] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
f : A →A[R] A
⊢ (↑f : A →ₐ[R] A) = AlgHom.id R A ↔ f = ContinuousAlgHom.id R A
have rw : (↑f : A →ₐ[R] A) = (↑(ContinuousAlgHom.id R A) : A →ₐ[R] A) ↔ f = ContinuousAlgHom.id R A
Tactic: rw [← coe_id, coe_inj]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
f : A →A[R] A
rw : (↑f : A →ₐ[R] A) = (↑(ContinuousAlgHom.id R A) : A →ₐ[R] A) ↔ f = ContinuousAlgHom.id R A
⊢ (↑f : A →ₐ[R] A) = AlgHom.id R A ↔ f = ContinuousAlgHom.id R A
have rw₁ : f = ContinuousAlgHom.id R A ↔ f = ContinuousAlgHom.id R A
Tactic: rw [← coe_id, coe_inj]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
s : Subalgebra R A
B : Type u_2
inst_5 : TopologicalSpace B
inst_6 : Ring B
inst_7 : IsSemitopologicalRing B
inst_8 : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : Eq (α := (a : B) → A) (⇑f : (a : B) → A) (⇑f' : (a : B) → A)
⊢ comap f s.topologicalClosure = (comap f s).topologicalClosure
have h : (↑(comap f s.topologicalClosure) : Set B) = (↑(comap f s).topologicalClosure : Set B)
Tactic: apply SetLike.ext'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
s : Subalgebra R A
B : Type u_2
inst_5 : TopologicalSpace B
inst_6 : Ring B
inst_7 : IsSemitopologicalRing B
inst_8 : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : Eq (α := (a : B) → A) (⇑f : (a : B) → A) (⇑f' : (a : B) → A)
⊢ (↑(comap f s.topologicalClosure) : Set B) = closure[inst_5] (↑(comap f s) : Set B)
have h : Eq.{u_2 + 1} (α := Set B) ((⇑f : (a : B) → A) ⁻¹' (↑s.topologicalClosure : Set A))
  (closure[inst_5] ((⇑f : (a : B) → A) ⁻¹' (↑s : Set A)))
Tactic: simp only [Subalgebra.coe_comap]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Algebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
s : Subalgebra R A
B : Type u_2
inst_5 : TopologicalSpace B
inst_6 : Ring B
inst_7 : IsSemitopologicalRing B
inst_8 : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : Eq (α := (a : B) → A) (⇑f : (a : B) → A) (⇑f' : (a : B) → A)
⊢ Eq.{u_2 + 1} (α := Set B) ((⇑f : (a : B) → A) ⁻¹' (↑s.topologicalClosure : Set A))
    (closure[inst_5] ((⇑f : (a : B) → A) ⁻¹' (↑s : Set A)))
have h : Eq.{u_2 + 1} (α := Set B) ((⇑f' : (a : B) → A) ⁻¹' (↑s.topologicalClosure : Set A))
  (closure[inst_5] ((⇑f' : (a : B) → A) ⁻¹' (↑s : Set A)))
Tactic: rw [w]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
v : V
p : P
⊢ HVAdd.hVAdd (β := Filter P) (asymptoticNhds k V v) (pure p) = asymptoticNhds k P v
have simp_rw : Eq.{u_3 + 1} (α := Filter P)
  (⨆ (i : V), map (fun (x : V) ↦ (x +ᵥ i) +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
  (⨆ (p : P), map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
Tactic: simp_rw [asymptoticNhds, vadd_pure, map_iSup, map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
v : V
p : P
⊢ Eq.{u_3 + 1} (α := Filter P)
    (⨆ (i : V), map (fun (x : V) ↦ (x +ᵥ i) +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
    (⨆ (p : P), map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
have refine : ∀ (x : V),
  Eq.{u_3 + 1} (α := Filter P)
    (map (fun (x_1 : V) ↦ HVAdd.hVAdd (β := P) x_1 ((Equiv.vaddConst p : (a : V) → P) x : P))
      (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
    (map (fun (x_1 : V) ↦ (x_1 +ᵥ x) +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
Tactic: refine (Equiv.vaddConst p).iSup_congr fun _ => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
u v : V
⊢ u +ᵥ asymptoticNhds k P v = asymptoticNhds k P v
have have : ∀ (p : P), u +ᵥ asymptoticNhds k P v = asymptoticNhds k P v
Tactic: have ⟨p⟩ : Nonempty P := inferInstance
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
u v : V
p : P
⊢ u +ᵥ asymptoticNhds k P v = asymptoticNhds k P v
have nth_rw : u +ᵥ HVAdd.hVAdd (β := Filter P) (asymptoticNhds k V v) (pure p) = asymptoticNhds k P v
Tactic: nth_rw 1 [← asymptoticNhds_vadd_pure v p]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
u v : V
p : P
⊢ u +ᵥ HVAdd.hVAdd (β := Filter P) (asymptoticNhds k V v) (pure p) = asymptoticNhds k P v
have simp_rw : Eq.{u_3 + 1} (α := Filter P) (map ((fun (b : P) ↦ u +ᵥ b) ∘ fun (x : V) ↦ x +ᵥ p) (asymptoticNhds k V v))
  (map (fun (x : V) ↦ x +ᵥ u +ᵥ p) (asymptoticNhds k V v))
Tactic: simp_rw [← asymptoticNhds_vadd_pure v (u +ᵥ p), vadd_pure, ← Filter.map_vadd, map_map]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
u v : V
p : P
⊢ Eq.{u_3 + 1} (α := Filter P) (map ((fun (b : P) ↦ u +ᵥ b) ∘ fun (x : V) ↦ x +ᵥ p) (asymptoticNhds k V v))
    (map (fun (x : V) ↦ x +ᵥ u +ᵥ p) (asymptoticNhds k V v))
have e_m : ∀ (v : V), ((fun (b : P) ↦ u +ᵥ b) ∘ fun (x : V) ↦ x +ᵥ p) v = v +ᵥ u +ᵥ p
Tactic: congr with v
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
α : Type u_4
l : Filter α
f : α → V
v : V
p : P
hf : Tendsto f l (asymptoticNhds k V v)
⊢ Tendsto (fun (x : α) ↦ f x +ᵥ p) l (asymptoticNhds k P v)
have rw : Tendsto.{u_4, u_3} (β := P) (fun (x : α) ↦ f x +ᵥ p) l (map (fun (x : V) ↦ x +ᵥ p) (asymptoticNhds k V v))
Tactic: rw [← asymptoticNhds_vadd_pure, vadd_pure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
α : Type u_4
l : Filter α
f : α → P
v u : V
hf : Tendsto f l (asymptoticNhds k P v)
⊢ Tendsto (fun (x : α) ↦ u +ᵥ f x) l (asymptoticNhds k P v)
have rw : Tendsto (β := P) (fun (x : α) ↦ u +ᵥ f x) l (map (fun (b : P) ↦ u +ᵥ b) (asymptoticNhds k P v))
Tactic: rw [← vadd_asymptoticNhds u, ← Filter.map_vadd]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
v : V
⊢ asymptoticNhds k V v = HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)
have unfold : ⨆ (p : V), HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)
Tactic: unfold asymptoticNhds
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
v : V
⊢ ⨆ (p : V), HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)
have a : ⨆ (p : V), HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p) ≤
  HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
v : V
a :
  ⨆ (p : V), HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p) ≤
    HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)
⊢ ⨆ (p : V), HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)
have a₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v) ≤
  ⨆ (p : V), HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
v : V
⊢ ⨆ (p : V), HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p) ≤
    HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)
have a : ∀ (u : V),
  HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure u) ≤
    HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)
Tactic: refine iSup_le fun u => ?_