mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: b₁ b₂ b₃ : ℝ → ℝ
bs₁ bs₂ bs₃ : Basis
f₁ : ℝ → ℝ
g₁ : MultiseriesExpansion bs₁ → MultiseriesExpansion bs₂
f₂ : ℝ → ℝ
g₂ : MultiseriesExpansion bs₂ → MultiseriesExpansion bs₃
ms : Multiseries b₁ bs₁
⊢ map (f₂ ∘ f₁) (g₂ ∘ g₁) ms = map f₂ g₂ (map f₁ g₁ ms)

Tactic:
simp [map, ← Stream'.Seq.map_comp]

Goal state after:
b₁ b₂ b₃ : ℝ → ℝ
bs₁ bs₂ bs₃ : Basis
f₁ : ℝ → ℝ
g₁ : MultiseriesExpansion bs₁ → MultiseriesExpansion bs₂
f₂ : ℝ → ℝ
g₂ : MultiseriesExpansion bs₂ → MultiseriesExpansion bs₃
ms : Multiseries b₁ bs₁
⊢ Seq.map (fun x ↦ (f₂ (f₁ x.1), g₂ (g₁ x.2))) ms = Seq.map ((fun x ↦ (f₂ x.1, g₂ x.2)) ∘ fun x ↦ (f₁ x.1, g₁ x.2)) ms
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.Sorted
⊢ ms.seq.Sorted

Tactic:
cases h with

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.seq.Sorted
⊢ ms.Sorted

Tactic:
cases h with

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case seq.right.cons.left
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
tl_tl : Multiseries basis_hd basis_tl
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq, x.2.Sorted
h_Pairwise✝ :
  Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq
h_all : ∀ x ∈ Multiseries.cons tl_exp tl_coef tl_tl, (exp, coef) > x
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (Multiseries.cons tl_exp tl_coef tl_tl)
⊢ tl_exp < exp

Tactic:
exact h_all (tl_exp, tl_coef) (by simp [Multiseries.cons])

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : (Multiseries.cons exp coef tl).Sorted
⊢ coef.Sorted ∧ tl.leadingExp < ↑exp ∧ tl.Sorted

Tactic:
cases h with

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
basis : Basis
⊢ { coef := coef, unit := [] }.toFun basis = fun x ↦ coef

Tactic:
ext x
  simp [toFun]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
m' : ℕ
e' : m.natPred = m' + 1
⊢ m = (m' + 1).succPNat

Tactic:
rw [← e', ← PNat.coe_inj, Nat.succPNat_coe, ← Nat.add_one, PNat.natPred_add_one]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
⊢ m = (m' + 1).succPNat

Tactic:
rw [← e', ← PNat.coe_inj, Nat.succPNat_coe, ← Nat.add_one, PNat.natPred_add_one]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
⊢ m = (m' + 1).succPNat

Tactic:
rw [← e', ← PNat.coe_inj, Nat.succPNat_coe, ← Nat.add_one, PNat.natPred_add_one]

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
hs : ms.seq = s
h : s.Trimmed
⊢ ms.Trimmed

Tactic:
cases h with

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl ms : Multiseries basis_hd basis_tl
h_ms : Multiseries.cons exp coef tl = ms
h : ms.Trimmed
⊢ coef.Trimmed ∧ ¬coef.IsZero

Tactic:
cases h with

Goal state after:
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b : ℕ
r : ℤ
ha : a % 4 = 3
hb : b % 4 = 3
hr : jacobiSymNat b a = r
⊢ jacobiSymNat a b = -r

Tactic:
by
  rwa [jacobiSymNat, jacobiSym.quadratic_reciprocity_three_mod_four ha hb, neg_inj]

Goal state after:
Module: Mathlib.Tactic.NormNum.PowMod

Goal state before:
pp: a b m c : ℕ
h1 : (a.pow b).mod m = c
⊢ (a ^ b * a ^ b).mod m = ((a ^ b).mod m * (a ^ b).mod m).mod m

Tactic:
exact Nat.mul_mod ..

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

Goal state before:
pp: case pos.e_a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ ys[j]? = some (List.applyId (xs.zip ys) y)

Tactic:
← List.applyId_zip_eq

Goal state after:
case pos.e_a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ List.applyId (zip ?m.157 ys) ?pos.e_a.x✝ = List.applyId (xs.zip ys) y

case pos.e_a.h₀
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ Nodup ?m.157

case pos.e_a.h₁
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ length ?m.157 = ys.length

case pos.e_a.x
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ α

case pos.e_a.h₂
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ ?m.157[j]? = some ?pos.e_a.x✝

α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ List α
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
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, ⟨g, hg⟩))).Nonempty
I : (interior ((g • V) • {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (V • {x})
⊢ U • {x} ∈ 𝓝 x

Tactic:
have J : (g'⁻¹ • V) • {x} ∈ 𝓝 x := by
    apply mem_interior_iff_mem_nhds.1
    rwa [smul_assoc, interior_smul, mem_inv_smul_set_iff]

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
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, ⟨g, hg⟩))).Nonempty
I : (interior ((g • V) • {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (V • {x})
J : (g'⁻¹ • V) • {x} ∈ 𝓝 x
⊢ U • {x} ∈ 𝓝 x
Module: Mathlib.Topology.Baire.BaireMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hc : Continuous[inst✝¹, inst✝] f
ho : IsOpenMap f
s u : Set β
hu : MeasurableSet u
hsu : s =ᶠ[residual β] u
⊢ MeasurableSet (f ⁻¹' u)

Tactic:
borelize α β

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hc : Continuous[inst✝¹, inst✝] f
ho : IsOpenMap f
s u : Set β
hu : MeasurableSet u
hsu : s =ᶠ[residual β] u
this✝³ : MeasurableSpace α := borel α
this✝² : BorelSpace α
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ MeasurableSet (f ⁻¹' u)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
i : ι
f : C(X i, Y)
⊢ Continuous[inst✝¹ i, _] (⇑WithGeneratedByTopology.equiv.symm ∘ ⇑f)

Tactic:
rw [continuous_iff X]

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
i : ι
f : C(X i, Y)
⊢ ∀ ⦃i_1 : ι⦄ (f_1 : C(X i_1, X i)), Continuous[inst✝¹ i_1, _] ((⇑WithGeneratedByTopology.equiv.symm ∘ ⇑f) ∘ ⇑f_1)
Module: Mathlib.Topology.Convenient.Category

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
X✝ Y✝ : TopCat
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (TopCat.toContinuousGeneratedByCat X).map a₁✝ = (TopCat.toContinuousGeneratedByCat X).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
by ext x; exact ConcreteCategory.congr_hom h x

Goal state after:
Module: Mathlib.Topology.Convenient.Category

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
X✝ Y✝ : TopCat
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : TopCat.toGeneratedByTopCat.map a₁✝ = TopCat.toGeneratedByTopCat.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
by ext x; exact ConcreteCategory.congr_hom h x

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case inr
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
this : ∀ S ∈ T2, S ∈ T0 ∨ ∃ Q ∈ T0, S = AA ∩ Q
S : Set (Ultrafilter X.A)
hS : S ∈ T2
h : ∃ Q ∈ T0, S = AA ∩ Q
⊢ S.Nonempty

Tactic:
rcases h with ⟨Q, hQ, rfl⟩
        exact claim4 Q hQ

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝³ : (i : I) → Decidable (J i)
inst✝² : (i : I) → Decidable (K i)
inst✝¹ : (i : I) → Decidable (L i)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
⊢ ∀ ⦃X Y : (Finset I)ᵒᵖ⦄ (f : X ⟶ Y),
    ((Functor.const (Finset I)ᵒᵖ).obj (of ↑C)).map f ≫
        ConcreteCategory.ofHom { toFun := ProjRestrict C fun x ↦ x ∈ unop Y, continuous_toFun := ⋯ } =
      ConcreteCategory.ofHom { toFun := ProjRestrict C fun x ↦ x ∈ unop X, continuous_toFun := ⋯ } ≫
        (spanFunctor hC).map f

Tactic:
intro X Y h
      simp only [Functor.const_obj_map,
        ← projRestricts_comp_projRestrict C (leOfHom h.unop)]
      rfl

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

Goal state before:
pp: case neg.h₁.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 := ⋯
a : I
c : Products I →₀ ℤ
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
m : Products I
hm : c m ≠ 0
b : I
bs : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: b :: bs)
hc : ↑c.support ⊆ {m | ↑m ≤ b :: bs}
hmas : ↑m ≤ b :: bs
⊢ b :: bs < a :: b :: bs

Tactic:
List.isChain_cons_cons

Goal state after:
case neg.h₁.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
c : Products I →₀ ℤ
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
m : Products I
hm : c m ≠ 0
b : I
bs : List I
ha : a > b ∧ List.IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
hc : ↑c.support ⊆ {m | ↑m ≤ b :: bs}
hmas : ↑m ≤ b :: bs
⊢ b :: bs < a :: b :: bs
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m ↦ Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})
⊢ L l

Tactic:
suffices Products.eval C '' {m | m < l} ⊆ span ℤ (Set.range (GoodProducts.eval C)) by
      rw [← span_le] at this
      exact this hl

Goal state after:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m ↦ Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})
⊢ Products.eval C '' {m | m < l} ⊆ ↑(Submodule.span ℤ (Set.range (eval C)))
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
E : Subcomplex C
⊢ ⋃ n, ⋃ j, openCell n ↑j = ↑E

Tactic:
have := RelCWComplex.Subcomplex.union E (C := C)

Goal state after:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
E : Subcomplex C
this : ∅ ∪ ⋃ n, ⋃ j, openCell n ↑j = ↑E
⊢ ⋃ n, ⋃ j, openCell n ↑j = ↑E
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
i : I
hi : i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩) ∧ ↑x i ≠ true
⊢ False

Tactic:
rw [hi' i hi.1] at hi

Goal state after:
case neg
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
i : I
hi : i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩) ∧ SwapTrue o (↑x) i ≠ true
⊢ False
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : Equicontinuous fun x ↦ ⇑↑x
⊢ IsCompact A

Tactic:
Equicontinuous,

Goal state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : ∀ (x₀ : α), EquicontinuousAt (fun x ↦ ⇑↑x) x₀
⊢ IsCompact A
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
i : ℕ
⊢ 1 ≤ (logSizeBallSeq J hJ a c i).radius

Tactic:
by
  match i with
  | 0 => exact one_le_logSizeRadius ha
  | i + 1 => exact one_le_logSizeRadius ha

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
⊢ (logSizeBallSeq J hJ a c i).point ∈ J

Tactic:
induction i with
  | zero => exact point_mem_finset_logSizeBallSeq hJ 0 hJ
  | succ i ih =>
    by_cases h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
    · refine Finset.mem_of_subset ?_ (point_mem_finset_logSizeBallSeq hJ (i + 1) h)
      apply finset_logSizeBallSeq_subset_logSizeBallSeq_init
    simp [point_logSizeBallSeq_add_one, ih, h]

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

Goal state before:
pp: case inl
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
M : Type u_3
x : X
p : ↑(Ω^ M (↑(Ω^ N X x)) const)
y : M ⊕ N → ↑I
hy : y ∈ Cube.boundary (M ⊕ N)
hM : y ∘ Sum.inl ∈ Cube.boundary M
⊢ (p (y ∘ Sum.inl)) (y ∘ Sum.inr) = x

Tactic:
have : p (y ∘ Sum.inl) = const := p.property (y ∘ Sum.inl) hM

Goal state after:
case inl
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
M : Type u_3
x : X
p : ↑(Ω^ M (↑(Ω^ N X x)) const)
y : M ⊕ N → ↑I
hy : y ∈ Cube.boundary (M ⊕ N)
hM : y ∘ Sum.inl ∈ Cube.boundary M
this : p (y ∘ Sum.inl) = const
⊢ (p (y ∘ Sum.inl)) (y ∘ Sum.inr) = x
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ_card : ↑(#J) ≤ a ^ n
s t : T
h : (s, t) ∈ pairSet J a c
⊢ ∃ i < #J, (s, t) ∈ pairSetSeq J a c i

Tactic:
by simpa [pairSet] using h

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

Goal state before:
pp: case inr
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
⊢ (∃ b ∈ s, (f i) x z ≤ (f b) x y) ∨ ∃ b ∈ s, (f i) x z ≤ (f b) y z

Tactic:
refine h.imp ?_ ?_

Goal state after:
case inr.refine_1
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
⊢ (f i) x z ≤ (f i) x y → ∃ b ∈ s, (f i) x z ≤ (f b) x y

case inr.refine_2
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
⊢ (f i) x z ≤ (f i) y z → ∃ b ∈ s, (f i) x z ≤ (f b) y z
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case right
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
⊢ f (z, t) - f (x, y) ≤ ↑(2 * maxVar X Y) * dist (x, y) (z, t)

Tactic:
dist_comm

Goal state after:
case right
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
⊢ f (z, t) - f (x, y) ≤ ↑(2 * maxVar X Y) * dist (z, t) (x, y)
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case h₁
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A C : Set X
hC_cover : IsCover ε A C
D : Set X
hD_subset : D ⊆ A
hD_separated : IsSeparated (2 * ↑ε) D
f : ↑D → ↑C := ⋯
hf' : ∀ (x : ↑D), edist ↑x ↑(f x) ≤ ↑ε
x y : ↑D
hxy : f x = f y
⊢ edist ↑x ↑(f x) ≤ ↑ε

pp: case h₂
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A C : Set X
hC_cover : IsCover ε A C
D : Set X
hD_subset : D ⊆ A
hD_separated : IsSeparated (2 * ↑ε) D
f : ↑D → ↑C := ⋯
hf' : ∀ (x : ↑D), edist ↑x ↑(f x) ≤ ↑ε
x y : ↑D
hxy : f x = f y
⊢ edist ↑(f x) ↑y ≤ ↑ε

Tactic:
· exact hf' x

Goal state after:
case h₂
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A C : Set X
hC_cover : IsCover ε A C
D : Set X
hD_subset : D ⊆ A
hD_separated : IsSeparated (2 * ↑ε) D
f : ↑D → ↑C := ⋯
hf' : ∀ (x : ↑D), edist ↑x ↑(f x) ≤ ↑ε
x y : ↑D
hxy : f x = f y
⊢ edist ↑(f x) ↑y ≤ ↑ε
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
x : α
s t : NonemptyCompacts α
⊢ infDist x ↑s ≤ infDist x ↑t + dist s t

Tactic:
dist_comm

Goal state after:
α : Type u_1
inst✝ : MetricSpace α
x : α
s t : NonemptyCompacts α
⊢ infDist x ↑s ≤ infDist x ↑t + dist t s
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case neg
α : Type u_1
inst✝² : PseudoMetricSpace α
s : Set α
inst✝¹ : Decidable s.Nontrivial
inst✝ : Fintype ↑s
hs : ¬s.Nontrivial
⊢ s.infsep = 0

Tactic:
rw [not_nontrivial_iff] at hs
    exact hs.infsep_zero

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : ¬s.Nontrivial
⊢ s.infsep = 0

Tactic:
rw [not_nontrivial_iff] at hs
    exact hs.infsep_zero

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Ici (toLowerSet b) ⊆ Ici (toLowerSet a) ↔ a ≤ b

Tactic:
Ici_subset_Ici,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ toLowerSet a ≤ toLowerSet b ↔ a ≤ b
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
s : Set α
inst✝¹ : Preorder α
t : TopologicalSpace α
inst✝ : IsScottHausdorff α univ
⊢ IsClosed[t] s ↔ DirSupClosed s

Tactic:
rw [isClosed_iff_dirSupClosedOn isLowerSet_univ, dirSupClosedOn_univ]

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

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this✝¹ : hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist ↑p ↑q < r
x : X
this✝ : f (inl x) ∈ ↑p
z : ↥(lp (fun n ↦ ℝ) ∞)
zq : z ∈ ↑q
hz : dist (f (inl x)) z < r
this : z ∈ range Ψ
y : Y
hy : Ψ y = z
⊢ dist (Φ x) (Ψ y) = dist (f (inl x)) z

Tactic:
rw [hy]

Goal state after: