awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s_1 s : Set V
hs : Convex k s
hs' : IsClosed[inst_7] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ᶠ (p : V) in asymptoticNhds k V (a • v + b • u), p ∈ s
have inr : ∀ᶠ (x : k) in atTop, id x • (a • v + b • u) +ᵥ p ∈ s
Tactic: refine tendsto_id.atTop_smul_const_tendsto_asymptoticNhds _ |>.asymptoticNhds_vadd_const p
    |>.frequently (Eventually.frequently ?_)
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s_1 s : Set V
hs : Convex k s
hs' : IsClosed[inst_7] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∀ᶠ (x : k) in atTop, id x • (a • v + b • u) +ᵥ p ∈ s
have h : ∀ (c : k) (hc : 0 ≤ c), id c • (a • v + b • u) +ᵥ p ∈ s
Tactic: filter_upwards [eventually_ge_atTop 0] with c hc
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s_1 s : Set V
hs : Convex k s
hs' : IsClosed[inst_7] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
⊢ id c • (a • v + b • u) +ᵥ p ∈ s
have h : ((c * a) • v + (c * b) • u) +ᵥ p ∈ s
Tactic: simp_rw [id, smul_add, smul_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (hypothesis)
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s_1 s : Set V
hs : Convex k s
hs' : IsClosed[inst_7] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
⊢ ((c * a) • v + (c * b) • u) +ᵥ p ∈ s
have h₁ : c • v +ᵥ p ∈ s
Tactic: have h₁ : c • v +ᵥ p ∈ s := hs.smul_vadd_mem_of_isClosed_of_mem_asymptoticCone hs' hc hv hp
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (hypothesis)
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s_1 s : Set V
hs : Convex k s
hs' : IsClosed[inst_7] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
h₁ : c • v +ᵥ p ∈ s
⊢ ((c * a) • v + (c * b) • u) +ᵥ p ∈ s
have h₂ : c • u +ᵥ p ∈ s
Tactic: have h₂ : c • u +ᵥ p ∈ s := hs.smul_vadd_mem_of_isClosed_of_mem_asymptoticCone hs' hc hu hp
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s_1 s : Set V
hs : Convex k s
hs' : IsClosed[inst_7] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
h₁ : c • v +ᵥ p ∈ s
h₂ : c • u +ᵥ p ∈ s
⊢ ((c * a) • v + (c * b) • u) +ᵥ p ∈ s
have h : ((c * a) • v + (c * b) • u) +ᵥ p ∈ [c • v +ᵥ p -[k] c • u +ᵥ p]
Tactic: apply hs.segment_subset h₁ h₂
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s_1 s : Set V
hs : Convex k s
hs' : IsClosed[inst_7] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
h₁ : c • v +ᵥ p ∈ s
h₂ : c • u +ᵥ p ∈ s
⊢ ((c * a) • v + (c * b) • u) +ᵥ p ∈ [c • v +ᵥ p -[k] c • u +ᵥ p]
have h : (c * a) • v + (c * b) • u ∈ [c • v -[k] c • u]
Tactic: rw [← affineSegment_eq_segment, mem_vadd_const_affineSegment, affineSegment_eq_segment]
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s_1 s : Set V
hs : Convex k s
hs' : IsClosed[inst_7] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
h₁ : c • v +ᵥ p ∈ s
h₂ : c • u +ᵥ p ∈ s
⊢ (c * a) • v + (c * b) • u ∈ [c • v -[k] c • u]
have h : a • c • v + b • c • u = (c * a) • v + (c * b) • u
Tactic: exists a, b, ha, hb, hab
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (hypothesis)
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : v ∈ asymptoticCone k s
⊢ c • v +ᵥ p ∈ s
have hv₁ : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
Tactic: rw [mem_asymptoticCone_iff, asymptoticNhds_eq_smul_vadd v (c • v +ᵥ p), vadd_pure,
    frequently_map, ← map₂_smul, ← map_prod_eq_map₂, frequently_map] at hv
Cleared hypotheses: hv
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
⊢ c • v +ᵥ p ∈ s
have refine : ∀ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), x.1 • x.2 +ᵥ c • v +ᵥ p ∈ s → c • v +ᵥ p ∈ s
Tactic: refine frequently_const.mp (hv.mp ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (hypothesis)
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
⊢ ∀ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), x.1 • x.2 +ᵥ c • v +ᵥ p ∈ s → c • v +ᵥ p ∈ s
have this : Tendsto (fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
Tactic: have : Tendsto (fun u => -(c • u : V) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p) :=
    Continuous.tendsto' (by fun_prop) _ _ (by simp)
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
⊢ 0 < (t, u).1 →
    Membership.mem (γ := Set (k × V)) ((fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) ∘ Prod.snd ⁻¹' s) (t, u) →
      (t, u).1 • (t, u).2 +ᵥ c • v +ᵥ p ∈ s → c • v +ᵥ p ∈ s
have h : ∀ (ht : 0 < t),
  Membership.mem (γ := Set (k × V)) ((fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) ∘ Prod.snd ⁻¹' s) (t, u) →
    (t, u).1 • (t, u).2 +ᵥ c • v +ᵥ p ∈ s → c • v +ᵥ p ∈ s
Tactic: (ht : 0 < t)
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
⊢ Membership.mem (γ := Set (k × V)) ((fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) ∘ Prod.snd ⁻¹' s) (t, u) →
    (t, u).1 • (t, u).2 +ᵥ c • v +ᵥ p ∈ s → c • v +ᵥ p ∈ s
have h : ∀ (hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s), (t, u).1 • (t, u).2 +ᵥ c • v +ᵥ p ∈ s → c • v +ᵥ p ∈ s
Tactic: (hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s)
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s
⊢ (t, u).1 • (t, u).2 +ᵥ c • v +ᵥ p ∈ s → c • v +ᵥ p ∈ s
have h : ∀ (h : t • u +ᵥ c • v +ᵥ p ∈ s), c • v +ᵥ p ∈ s
Tactic: (h : t • u +ᵥ c • v +ᵥ p ∈ s)
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
⊢ ∀ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), x.1 • x.2 +ᵥ c • v +ᵥ p ∈ s → c • v +ᵥ p ∈ s
have h : ∀ (t : k) (u : V) (ht : 0 < t) (hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s) (h : t • u +ᵥ c • v +ᵥ p ∈ s), c • v +ᵥ p ∈ s
Tactic: filter_upwards [tendsto_fst.eventually <| eventually_gt_atTop 0, this.comp tendsto_snd hp]
    with ⟨t, u⟩ (ht : 0 < t) (hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s) (h : t • u +ᵥ c • v +ᵥ p ∈ s)
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s
h : t • u +ᵥ c • v +ᵥ p ∈ s
⊢ c • v +ᵥ p ∈ s
have h₁ : c • v +ᵥ p ∈ [-(c • u) +ᵥ c • v +ᵥ p -[k] t • u +ᵥ c • v +ᵥ p]
Tactic: apply hs.segment_subset hu h
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s
h : t • u +ᵥ c • v +ᵥ p ∈ s
⊢ c • v +ᵥ p ∈ [-(c • u) +ᵥ c • v +ᵥ p -[k] t • u +ᵥ c • v +ᵥ p]
have h₁ : SameRay k ((c • v +ᵥ p) -ᵥ (-(c • u) +ᵥ c • v +ᵥ p)) ((t • u +ᵥ c • v +ᵥ p) -ᵥ (c • v +ᵥ p))
Tactic: simp_rw [mem_segment_iff_sameRay, ← vsub_eq_sub]
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s
h : t • u +ᵥ c • v +ᵥ p ∈ s
⊢ SameRay k ((c • v +ᵥ p) -ᵥ (-(c • u) +ᵥ c • v +ᵥ p)) ((t • u +ᵥ c • v +ᵥ p) -ᵥ (c • v +ᵥ p))
have h₁ : SameRay k (c • u) (t • u)
Tactic: rw [vsub_vadd_eq_vsub_sub, vsub_self, zero_sub, neg_neg, vadd_vsub]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : ContinuousMul G
H K : OpenNormalSubgroup G
h : H.toFiniteIndexNormalSubgroup = K.toFiniteIndexNormalSubgroup
⊢ H = K
have a : Eq.{u_1 + 1} (α := Subgroup G) ((fun (H : OpenNormalSubgroup G) ↦ (↑H.toOpenSubgroup : Subgroup G)) H)
  ((fun (H : OpenNormalSubgroup G) ↦ (↑H.toOpenSubgroup : Subgroup G)) K)
Tactic: apply toSubgroup_injective
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion (goal)
Goal:
G : GrpCat
H : FiniteIndexNormalSubgroup (↑G : Type u)
⊢ FiniteGrp.ofHom (QuotientGroup.map H.toSubgroup H.toSubgroup (MonoidHom.id (↑G : Type u)) ⋯) =
    𝟙 (FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup))
have h : ∀ (x : (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u)) (x : (↑G : Type u)),
  Eq (α := (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u}) ↦ (↑x1.toGrp : Type u) →* (↑x2.toGrp : Type u)) (CC :=
            fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (X := FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)) (Y :=
            FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup))
            (FiniteGrp.ofHom (QuotientGroup.map H.toSubgroup H.toSubgroup (MonoidHom.id (↑G : Type u)) sorry)) :
          (a : (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u)) →
            (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u))
        (Quot.mk (⇑(QuotientGroup.leftRel H.toSubgroup) : (↑G : Type u) → (↑G : Type u) → Prop) x) :
      (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u}) ↦ (↑x1.toGrp : Type u) →* (↑x2.toGrp : Type u)) (CC :=
            fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (𝟙 (FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup))) :
          (a : (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u)) →
            (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u))
        (Quot.mk (⇑(QuotientGroup.leftRel H.toSubgroup) : (↑G : Type u) → (↑G : Type u) → Prop) x) :
      (↑(FiniteGrp.of ((↑G : Type u) ⧸ H.toSubgroup)).toGrp : Type u))
Tactic: ext ⟨x⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion (goal)
Goal:
G : GrpCat
X Y Z : FiniteIndexNormalSubgroup (↑G : Type u)
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := FiniteGrp.of ((↑G : Type u) ⧸ X.toSubgroup) ⟶ FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup))
    (FiniteGrp.ofHom (QuotientGroup.map X.toSubgroup Z.toSubgroup (MonoidHom.id (↑G : Type u)) ⋯))
    (CategoryStruct.comp (Y := FiniteGrp.of ((↑G : Type u) ⧸ Y.toSubgroup))
      (FiniteGrp.ofHom (QuotientGroup.map X.toSubgroup Y.toSubgroup (MonoidHom.id (↑G : Type u)) ⋯))
      (FiniteGrp.ofHom (QuotientGroup.map Y.toSubgroup Z.toSubgroup (MonoidHom.id (↑G : Type u)) ⋯)))
have h : ∀ (x : (↑(FiniteGrp.of ((↑G : Type u) ⧸ X.toSubgroup)).toGrp : Type u)) (x : (↑G : Type u)),
  Eq (α := (↑(FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup)).toGrp : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u}) ↦ (↑x1.toGrp : Type u) →* (↑x2.toGrp : Type u)) (CC :=
            fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (X := FiniteGrp.of ((↑G : Type u) ⧸ X.toSubgroup)) (Y :=
            FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup))
            (FiniteGrp.ofHom (QuotientGroup.map X.toSubgroup Z.toSubgroup (MonoidHom.id (↑G : Type u)) sorry)) :
          (a : (↑(FiniteGrp.of ((↑G : Type u) ⧸ X.toSubgroup)).toGrp : Type u)) →
            (↑(FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup)).toGrp : Type u))
        (Quot.mk (⇑(QuotientGroup.leftRel X.toSubgroup) : (↑G : Type u) → (↑G : Type u) → Prop) x) :
      (↑(FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup)).toGrp : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u}) ↦ (↑x1.toGrp : Type u) →* (↑x2.toGrp : Type u)) (CC :=
            fun (X : FiniteGrp.{u}) ↦ (↑X.toGrp : Type u)) (X := FiniteGrp.of ((↑G : Type u) ⧸ X.toSubgroup)) (Y :=
            FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup))
            (CategoryStruct.comp (Y := FiniteGrp.of ((↑G : Type u) ⧸ Y.toSubgroup))
              (FiniteGrp.ofHom (QuotientGroup.map X.toSubgroup Y.toSubgroup (MonoidHom.id (↑G : Type u)) sorry))
              (FiniteGrp.ofHom (QuotientGroup.map Y.toSubgroup Z.toSubgroup (MonoidHom.id (↑G : Type u)) sorry))) :
          (a : (↑(FiniteGrp.of ((↑G : Type u) ⧸ X.toSubgroup)).toGrp : Type u)) →
            (↑(FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup)).toGrp : Type u))
        (Quot.mk (⇑(QuotientGroup.leftRel X.toSubgroup) : (↑G : Type u) → (↑G : Type u) → Prop) x) :
      (↑(FiniteGrp.of ((↑G : Type u) ⧸ Z.toSubgroup)).toGrp : Type u))
Tactic: ext ⟨x⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion (goal)
Goal:
G : GrpCat
⊢ Mono (eta G) ↔ Group.ResiduallyFinite.{u} (↑G : Type u)
have rw : (∀ (a : (↑G : Type u)),
    Eq (α :=
        (↑(GrpCat.of
              (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                Type u)) :
          Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                GrpCat.carrier) (eta G) :
              (a : (↑G : Type u)) → (↑(GrpCat.of (↑(completion G).toProfinite.toTop : Type u)) : Type u))
            a :
          (↑(GrpCat.of
                (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)) :
            Type u))
        (1 :
          (↑(GrpCat.of
                (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)) :
            Type u)) →
      a = 1) ↔
  ∀ (g : (↑G : Type u)), (∀ (H : FiniteIndexNormalSubgroup (↑G : Type u)), g ∈ H) → g = 1
Tactic: rw [GrpCat.mono_iff_injective, injective_iff_map_eq_one,
    Group.residuallyFinite_iff_forall_finiteIndexNormalSubgroup]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion (goal)
Goal:
G : GrpCat
⊢ (∀ (a : (↑G : Type u)),
      Eq (α :=
          (↑(GrpCat.of
                (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)) :
            Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                  GrpCat.carrier) (eta G) :
                (a : (↑G : Type u)) → (↑(GrpCat.of (↑(completion G).toProfinite.toTop : Type u)) : Type u))
              a :
            (↑(GrpCat.of
                  (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)) :
              Type u))
          (1 :
            (↑(GrpCat.of
                  (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)) :
              Type u)) →
        a = 1) ↔
    ∀ (g : (↑G : Type u)), (∀ (H : FiniteIndexNormalSubgroup (↑G : Type u)), g ∈ H) → g = 1
have refine : ∀ (g : (↑G : Type u)),
  Eq (α :=
      (↑(GrpCat.of
            (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u))) :
              Type u)) :
        Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := GrpCat.carrier)
              (eta G) :
            (a : (↑G : Type u)) → (↑(GrpCat.of (↑(completion G).toProfinite.toTop : Type u)) : Type u))
          g :
        (↑(GrpCat.of
              (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                Type u)) :
          Type u))
      (1 :
        (↑(GrpCat.of
              (↑((completion G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                Type u)) :
          Type u)) ↔
    ∀ (H : FiniteIndexNormalSubgroup (↑G : Type u)), g ∈ H
Tactic: refine forall_congr' fun g ↦ imp_congr_left ?_