mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: case iff
q : AndKind
⊢ Ordering

Tactic:
cases q

Goal state after:
case iff.and
⊢ Ordering

case iff.iff
⊢ Ordering

case iff.eq
⊢ Ordering
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: case eq
q : AndKind
⊢ Ordering

Tactic:
cases q

Goal state after:
case eq.and
⊢ Ordering

case eq.iff
⊢ Ordering

case eq.eq
⊢ Ordering
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: case var
q : IProp
a✝ : Nat
⊢ Ordering

Tactic:
cases q

Goal state after:
case var.var
a✝¹ a✝ : Nat
⊢ Ordering

case var.true
a✝ : Nat
⊢ Ordering

case var.false
a✝ : Nat
⊢ Ordering

case var.and'
a✝³ : Nat
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case var.or
a✝² : Nat
a✝¹ a✝ : IProp
⊢ Ordering

case var.imp
a✝² : Nat
a✝¹ a✝ : IProp
⊢ Ordering
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: case true
q : IProp
⊢ Ordering

Tactic:
cases q

Goal state after:
case true.var
a✝ : Nat
⊢ Ordering

case true.true
⊢ Ordering

case true.false
⊢ Ordering

case true.and'
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case true.or
a✝¹ a✝ : IProp
⊢ Ordering

case true.imp
a✝¹ a✝ : IProp
⊢ Ordering
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: case false
q : IProp
⊢ Ordering

Tactic:
cases q

Goal state after:
case false.var
a✝ : Nat
⊢ Ordering

case false.true
⊢ Ordering

case false.false
⊢ Ordering

case false.and'
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case false.or
a✝¹ a✝ : IProp
⊢ Ordering

case false.imp
a✝¹ a✝ : IProp
⊢ Ordering
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: case and'
q : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

Tactic:
cases q

Goal state after:
case and'.var
a✝³ : AndKind
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

case and'.true
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case and'.false
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case and'.and'
a✝⁵ : AndKind
a✝⁴ a✝³ : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case and'.or
a✝⁴ : AndKind
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

case and'.imp
a✝⁴ : AndKind
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: case or
q a✝¹ a✝ : IProp
⊢ Ordering

Tactic:
cases q

Goal state after:
case or.var
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

case or.true
a✝¹ a✝ : IProp
⊢ Ordering

case or.false
a✝¹ a✝ : IProp
⊢ Ordering

case or.and'
a✝⁴ a✝³ : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case or.or
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

case or.imp
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: case imp
q a✝¹ a✝ : IProp
⊢ Ordering

Tactic:
cases q

Goal state after:
case imp.var
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

case imp.true
a✝¹ a✝ : IProp
⊢ Ordering

case imp.false
a✝¹ a✝ : IProp
⊢ Ordering

case imp.and'
a✝⁴ a✝³ : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case imp.or
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

case imp.imp
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering
Module: Mathlib.Tactic.NormNum.PowMod

Goal state before:
pp: a✝ b✝ m✝ : Q(ℕ)
depth : ℕ
a m b₀ c₀ b : Q(ℕ)
p : Q(Prop)
hp : «$p» =Q ((«$a».pow «$b₀»).mod «$m» = «$c₀»)
b' : ℕ := Expr.natLit! b
m' : ℕ := Expr.natLit! m
d : ℕ := depth >>> 1
hi : Q(ℕ)
⊢ «$p» =Q ((«$a».pow «$b₀»).mod «$m» = «$c₀»)

Tactic:
by exact hp

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case h₁
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))
hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup
⊢ xs₀ ~ xs₁

Tactic:
← hxs,

Goal state after:
case h₁
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup
⊢ xs₀ ~ xs₁
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⋯
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := ⋯
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
⊢ ↑(etaFn G origin) ∈ (↑J).pi fJ

Tactic:
intro a a_in_J

Goal state after:
case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
a : FiniteIndexNormalSubgroup ↑G
a_in_J : a ∈ ↑J
⊢ ↑(etaFn G origin) a ∈ fJ a
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
⊢ ∀ (x_1 : G), ∀ s ∈ 𝓝 x_1, (fun g ↦ g • x) '' s ∈ 𝓝 (x_1 • x)

Tactic:
intro g

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
g : G
⊢ ∀ s ∈ 𝓝 g, (fun g ↦ g • x) '' s ∈ 𝓝 (g • x)
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝¹⁰ : CommSemiring 𝕜
inst✝⁹ : TopologicalSpace 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 F
inst : TopologicalSpace E
inst✝⁴ : AddCommMonoid E'
inst✝³ : Module 𝕜 E'
inst✝² : AddCommMonoid F'
inst✝¹ : Module 𝕜 F'
inst✝ : TopologicalSpace E'
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
B' : E' →ₗ[𝕜] F' →ₗ[𝕜] 𝕜
e : E ≃L[𝕜] E'
f : F ≃ₗ[𝕜] F'
hBB' : ((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B = B'
hB : B.IsWeak
⊢ TopologicalSpace.induced (⇑e.symm) (TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace) =
    TopologicalSpace.induced (fun x1 x2 ↦ (B' x1) x2) Pi.topologicalSpace

Tactic:
simp_rw [induced_compose, ← hBB', induced_to_pi]

Goal state after:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝¹⁰ : CommSemiring 𝕜
inst✝⁹ : TopologicalSpace 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 F
inst : TopologicalSpace E
inst✝⁴ : AddCommMonoid E'
inst✝³ : Module 𝕜 E'
inst✝² : AddCommMonoid F'
inst✝¹ : Module 𝕜 F'
inst✝ : TopologicalSpace E'
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
B' : E' →ₗ[𝕜] F' →ₗ[𝕜] 𝕜
e : E ≃L[𝕜] E'
f : F ≃ₗ[𝕜] F'
hBB' : ((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B = B'
hB : B.IsWeak
⊢ ⨅ i, TopologicalSpace.induced (fun x ↦ ((fun x1 x2 ↦ (B x1) x2) ∘ ⇑e.symm) x i) inferInstance =
    ⨅ i,
      TopologicalSpace.induced (fun x ↦ ((((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B) x) i) inferInstance
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
c : 𝕜₁
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
c_ne : c ≠ 0
cV_mem : c • V ∈ 𝓕₂ ⊓ 𝓟 V
basis_𝓕₂ : 𝓕₂.HasBasis (fun s ↦ s ∈ 𝓕₂ ∧ Balanced 𝕜₁ s) id
W : Set E
hW : id W ∩ V ⊆ c • V
W_mem_𝓕₂ : W ∈ 𝓕₂
W_bal : Balanced 𝕜₁ W
⊢ W ⊆ V

Tactic:
intro w

Goal state after:
𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
c : 𝕜₁
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
c_ne : c ≠ 0
cV_mem : c • V ∈ 𝓕₂ ⊓ 𝓟 V
basis_𝓕₂ : 𝓕₂.HasBasis (fun s ↦ s ∈ 𝓕₂ ∧ Balanced 𝕜₁ s) id
W : Set E
hW : id W ∩ V ⊆ c • V
W_mem_𝓕₂ : W ∈ 𝓕₂
W_bal : Balanced 𝕜₁ W
w : E
⊢ w ∈ W → w ∈ V
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝ : ContinuousAdd 𝕜
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] ((fun x1 x2 ↦ (B x1) x2) ∘ fun p ↦ p.1 + p.2)

Tactic:
simp only [Function.comp_def, map_add, add_apply]

Goal state after:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝ : ContinuousAdd 𝕜
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] fun x x2 ↦ (B x.1) x2 + (B x.2) x2
Module: Mathlib.Topology.CWComplex.Classical.Graph

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
⊢ (∃ x, (OneSkeletonGraph C).IsLoopAt e x) ↔ ∃ x, cellFrontier 1 e = closedCell 0 x

Tactic:
by
  refine exists_congr fun x ↦ ?_
  change cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 x ↔ _
  rw [union_self]

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
J : (m : ℕ) → Finset (cell C m)
hJ : cellFrontier n ↑i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ J m, openCell m j
⊢ MapsTo (↑(map n ↑i)) (sphere 0 1)
    (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ (fun m ↦ (J m).preimage Subtype.val ⋯) m, ↑(map m ↑j) '' closedBall 0 1)

Tactic:
rw [mapsTo_iff_image_subset]

Goal state after:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
J : (m : ℕ) → Finset (cell C m)
hJ : cellFrontier n ↑i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ J m, openCell m j
⊢ ↑(map n ↑i) '' sphere 0 1 ⊆
    D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ (fun m ↦ (J m).preimage Subtype.val ⋯) m, ↑(map m ↑j) '' closedBall 0 1
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A : Set X.A
F : Ultrafilter X.A
⊢ cl A ∈ F → X.str F ∈ cl A

Tactic:
hF

Goal state after:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : cl A ∈ F
⊢ X.str F ∈ cl A
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
x✝ : x ∈ π C J
y : I → Bool
hy : y ∈ C
h : Proj J y = x
⊢ x ∈ C

pp: case refine_2
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
h : x ∈ C
⊢ Proj J x = x

Tactic:
· rwa [← h, proj_eq_self]; exact (hh · y hy)

Goal state after:
case refine_2
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
h : x ∈ C
⊢ Proj J x = x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case cons
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := s.sort fun x1 x2 ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hc' :
  (c.sum fun i a ↦ a • Products.eval (π C fun x ↦ x ∈ s) i) =
    (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) as).prod
⊢ (if ↑x a = true then e (π C fun x ↦ x ∈ s) a else 1 - e (π C fun x ↦ x ∈ s) a) *
      (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) as).prod ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
← hc'

Goal state after:
case cons
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := s.sort fun x1 x2 ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hc' :
  (c.sum fun i a ↦ a • Products.eval (π C fun x ↦ x ∈ s) i) =
    (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) as).prod
⊢ ((if ↑x a = true then e (π C fun x ↦ x ∈ s) a else 1 - e (π C fun x ↦ x ∈ s) a) *
      c.sum fun i a ↦ a • Products.eval (π C fun x ↦ x ∈ s) i) ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_2
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
i : I
h : term I ho = i
⊢ ord I i = o

Tactic:
subst h
    exact ord_term_aux ho

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
hslt : ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o
he :
  eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
hlt : ∀ i ∈ ↑l, ord I i < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)
⊢ eval (π C fun x ↦ ord I x < o) l ∈
    Submodule.span ℤ
      (⇑(πs' C ⋯) '' eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})

Tactic:
← eval_πs' C (le_of_lt hslt) hlt,

Goal state after:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
hslt : ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o
he :
  eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
hlt : ∀ i ∈ ↑l, ord I i < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)
⊢ (πs' C ⋯) (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l) ∈
    Submodule.span ℤ
      (⇑(πs' C ⋯) '' eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case e_I
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I✝¹ : (n : ℕ) → Set (cell C n)
closed'✝¹ : IsClosed[t] E
hE : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
F : Set X
I✝ : (n : ℕ) → Set (cell C n)
closed'✝ : IsClosed[t] F
hF : D ∪ ⋃ n, ⋃ j, openCell n ↑j = F
h :
  (fun E ↦ E.carrier) { carrier := E, I := I✝¹, closed' := closed'✝¹, union' := hE } =
    (fun E ↦ E.carrier) { carrier := F, I := I✝, closed' := closed'✝, union' := hF }
⊢ E = D ∪ ⋃ n, ⋃ j, openCell n ↑j

Tactic:
hF

Goal state after:
case e_I
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I✝¹ : (n : ℕ) → Set (cell C n)
closed'✝¹ : IsClosed[t] E
hE : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
F : Set X
I✝ : (n : ℕ) → Set (cell C n)
closed'✝ : IsClosed[t] F
hF : D ∪ ⋃ n, ⋃ j, openCell n ↑j = F
h :
  (fun E ↦ E.carrier) { carrier := E, I := I✝¹, closed' := closed'✝¹, union' := hE } =
    (fun E ↦ E.carrier) { carrier := F, I := I✝, closed' := closed'✝, union' := hF }
⊢ E = F
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
⊢ (f.concat g).comp IccInclusionRight = g

Tactic:
ext ⟨x, hx⟩
  obtain rfl | hxb := eq_or_ne x b
  · simpa [concat, IccInclusionRight, IccExtendCM, projIccCM, inclusion, hb]
  · have h : ¬ x ≤ b := lt_of_le_of_ne hx.1 (Ne.symm hxb) |>.not_ge
    simp [concat, hb, IccInclusionRight, h, IccExtendCM, projIccCM, projIcc, inclusion, hx.2, hx.1]

Goal state after:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
⊢ auxGroup i = auxGroup j

Tactic:
by_cases h : i = j; · rw [h]
  refine Group.ext (EckmannHilton.mul (isUnital_auxGroup i) (isUnital_auxGroup j) ?_)
  rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ ⟨d⟩
  change Quotient.mk' _ = _
  apply congr_arg Quotient.mk'
  simp only [fromLoop_trans_toLoop, transAt_distrib h, coe_toEquiv, loopHomeo_apply,
    coe_symm_toEquiv, loopHomeo_symm_apply]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
⊢ LipschitzWith 2 fun p ↦ infDist p.1 ↑p.2

Tactic:
by
  rw [← one_add_one_eq_two]
  exact LipschitzWith.uncurry
    (fun s : NonemptyCompacts α => lipschitz_infDist_pt (s : Set α)) lipschitz_infDist_set

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
x✝ : ℝ≥0∞
⊢ (∀ x ∈ s, ∀ y ∈ s, x ≠ y → x✝ ≤ edist x y) ↔ x✝ ≤ ⨅ d, uncurry edist ↑d

Tactic:
le_iInf_iff,

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
x✝ : ℝ≥0∞
⊢ (∀ x ∈ s, ∀ y ∈ s, x ≠ y → x✝ ≤ edist x y) ↔ ∀ (i : ↑s.offDiag), x✝ ≤ uncurry edist ↑i
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
𝕜 : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : Module 𝕜 Y
inst✝ : NormSMulClass 𝕜 Y
c : 𝕜
hc : ‖c‖₊ ≠ 0
⊢ MemHolder r (c • f) ↔ MemHolder r f

Tactic:
refine ⟨fun ⟨h, hh⟩ => ⟨h * ‖c‖₊⁻¹, ?_⟩, .smul⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
𝕜 : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : Module 𝕜 Y
inst✝ : NormSMulClass 𝕜 Y
c : 𝕜
hc : ‖c‖₊ ≠ 0
x✝ : MemHolder r (c • f)
h : ℝ≥0
hh : HolderWith h r (c • f)
⊢ HolderWith (h * ‖c‖₊⁻¹) r f
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_1
X : Type u
inst✝⁶ : MetricSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : Nonempty X
Y : Type v
inst✝³ : MetricSpace Y
inst✝² : CompactSpace Y
inst✝¹ : Nonempty Y
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
Φ' : X → ↑s := fun y ↦ ⟨Φ y, ⋯⟩
Ψ' : Y → ↑s := fun y ↦ ⟨Ψ y, ⋯⟩
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this✝² : IsCompact s
this✝¹ : CompactSpace ↑s
ΦΦ' : Φ = Subtype.val ∘ Φ'
ΨΨ' : Ψ = Subtype.val ∘ Ψ'
this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : ↑s → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding ↑s
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
AX : ⟦A⟧ = toGHSpace X
BY : ⟦B⟧ = toGHSpace Y
t : ℝ
x✝¹ x✝ : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
a✝¹ : ⟦x✝¹⟧ = toGHSpace X
a✝ : ⟦x✝⟧ = toGHSpace Y
ht : hausdorffDist ↑x✝¹ ↑x✝ = t
⊢ 0 ≤ hausdorffDist ↑x✝¹ ↑x✝

Tactic:
exact hausdorffDist_nonneg

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
a : WithUpper α
⊢ IsOpen[inst✝¹] (⇑toUpper ⁻¹' (Iic a)ᶜ)

Tactic:
exact isClosed_Iic.isOpen_compl

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} = (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}

Tactic:
ext s

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
⊢ s ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} ↔ s ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: case mpr.inr
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
a : α
⊢ IsOpen[inst✝¹] (Iic a)ᶜ

Tactic:
exact isClosed_Iic.isOpen_compl

Goal state after:
Module: Mathlib.Topology.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α (range fun c ↦ range ⇑c)
f : α → Prop
a b : α
hab : a ≤ b
⊢ {a, b} ∈ range fun c ↦ range ⇑c

Tactic:
use Chain.pair a b hab; exact OmegaCompletePartialOrder.Chain.range_pair a b hab

Goal state after:
Module: Mathlib.Topology.Order.NhdsSet

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a < b
⊢ 𝓝ˢ (Ico a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)

Tactic:
rw [← Ioo_insert_left h, nhdsSet_insert, nhdsSet_Ioo]

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: x : GHSpace
y : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hy : ⟦y⟧ = x
u v : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
⊢ 0 ≤ (fun p ↦ hausdorffDist ↑p.1 ↑p.2) (u, v)

Tactic:
exact hausdorffDist_nonneg

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case h₂
x : GHSpace
y : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hy : ⟦y⟧ = x
u v : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
⊢ 0 ≤ (fun p ↦ hausdorffDist ↑p.1 ↑p.2) (u, v)

Tactic:
exact hausdorffDist_nonneg

Goal state after: