mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: 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
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
⊢ List.IsChain (fun x x_1 ↦ x > x_1) (term I ho :: ↑q)

Tactic:
List.isChain_iff_pairwise

Goal state after:
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
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
⊢ List.Pairwise (fun x x_1 ↦ x > x_1) (term I ho :: ↑q)
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
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this✝ : Inhabited I
a : I
ha : a ∈ ↑q
hM : ¬↑(↑l).Tail = []
this : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑(↑l).Tail)
⊢ (↑(↑l).Tail).head! < term I ho

Tactic:
List.isChain_iff_pairwise

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
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this✝ : Inhabited I
a : I
ha : a ∈ ↑q
hM : ¬↑(↑l).Tail = []
this : List.Pairwise (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑(↑l).Tail)
⊢ (↑(↑l).Tail).head! < term I ho
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
⊢ IsCountablyCompact A ↔
    ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i

Tactic:
by
  simp [isCountablyCompact_iff_countable_open_cover, Finset.exists]

Goal state after:
Module: Mathlib.Topology.Hom.Open

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
toFun✝¹ : α → β
continuous_toFun✝¹ : Continuous toFun✝¹
map_open'✝¹ : IsOpenMap { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹ }.toFun
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
map_open'✝ : IsOpenMap { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹, map_open' := map_open'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, continuous_toFun := continuous_toFun✝, map_open' := map_open'✝ }
⊢ { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹, map_open' := map_open'✝¹ } =
    { toFun := toFun✝, continuous_toFun := continuous_toFun✝, map_open' := map_open'✝ }

Tactic:
congr

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
x✝² x✝¹ : ↑(Ω^ N X x)
f : (N → ↑I) → X
continuous_toFun✝¹ : Continuous[_, inst✝] f
property✝¹ : { toFun := f, continuous_toFun := continuous_toFun✝¹ } ∈ Ω^ N X x
g : (N → ↑I) → X
continuous_toFun✝ : Continuous[_, inst✝] g
property✝ : { toFun := g, continuous_toFun := continuous_toFun✝ } ∈ Ω^ N X x
x✝ :
  (fun f ↦ ⇑↑f) ⟨{ toFun := f, continuous_toFun := continuous_toFun✝¹ }, property✝¹⟩ =
    (fun f ↦ ⇑↑f) ⟨{ toFun := g, continuous_toFun := continuous_toFun✝ }, property✝⟩
⊢ ⟨{ toFun := f, continuous_toFun := continuous_toFun✝¹ }, property✝¹⟩ =
    ⟨{ toFun := g, continuous_toFun := continuous_toFun✝ }, property✝⟩

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)
j : ↑Sᶜ
⊢ reorderRestrictProd S s p ↑j = ↑p.1 j

Tactic:
by
  have hj : ↑j ∉ S := j.prop
  simp [reorderRestrictProd, hj]

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 : N
p : ↑(Ω^ N X x)
y✝ : N → ↑I
⊢ (fromLoop i (toLoop i p)) y✝ = p y✝

Tactic:
exact congr_arg p (by dsimp; exact Equiv.apply_symm_apply _ _)

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
⊢ (if x ∈ Set.Icc 0 (1 / 3) then 3 * x else 3 * x - 2) ∈ cantorSet

Tactic:
obtain ⟨y, hy, rfl | rfl⟩ : ∃ y ∈ cantorSet, y / 3 = x ∨ (2 + y) / 3 = x := by
    rw [cantorSet_eq_union_halves] at hx
    grind

Goal state after:
case inl
y : ℝ
hy : y ∈ cantorSet
hx : y / 3 ∈ cantorSet
⊢ (if y / 3 ∈ Set.Icc 0 (1 / 3) then 3 * (y / 3) else 3 * (y / 3) - 2) ∈ cantorSet

case inr
y : ℝ
hy : y ∈ cantorSet
hx : (2 + y) / 3 ∈ cantorSet
⊢ (if (2 + y) / 3 ∈ Set.Icc 0 (1 / 3) then 3 * ((2 + y) / 3) else 3 * ((2 + y) / 3) - 2) ∈ cantorSet
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I
⊢ ∀ x_1 ∈ {0, 1},
    {
          toFun := fun x_2 ↦
            { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                  map_one_left := ⋯ }.toFun
              (t, x_2),
          continuous_toFun := ⋯ }
        x_1 =
      (toLoop i p).toContinuousMap x_1

Tactic:
y

Goal state after:
case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t y : ↑I
⊢ y ∈ {0, 1} →
    {
          toFun := fun x_1 ↦
            { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                  map_one_left := ⋯ }.toFun
              (t, x_1),
          continuous_toFun := ⋯ }
        y =
      (toLoop i p).toContinuousMap y
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x : X
⊢ ∀ (y z : X), d x z ⊔ d' x z ≤ d x y ⊔ d' x y + d y z ⊔ d' y z

Tactic:
y

Goal state after:
X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x y : X
⊢ ∀ (z : X), d x z ⊔ d' x z ≤ d x y ⊔ d' x y + d y z ⊔ d' y z
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝⁵ : AddZeroClass R
inst✝⁴ : SemilatticeSup R
inst✝³ : AddLeftMono R
inst✝² : AddRightMono R
d d' : PseudoMetric X R
inst✝¹ : d.IsUltra
inst✝ : d'.IsUltra
x : X
⊢ ∀ (y z : X), (d ⊔ d') x z ≤ (d ⊔ d') x y ⊔ (d ⊔ d') y z

Tactic:
y

Goal state after:
X : Type u_1
R : Type u_2
inst✝⁵ : AddZeroClass R
inst✝⁴ : SemilatticeSup R
inst✝³ : AddLeftMono R
inst✝² : AddRightMono R
d d' : PseudoMetric X R
inst✝¹ : d.IsUltra
inst✝ : d'.IsUltra
x y : X
⊢ ∀ (z : X), (d ⊔ d') x z ≤ (d ⊔ d') x y ⊔ (d ⊔ d') y z
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: 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 : X
⊢ ∀ (y z : X), (s.sup f) x z ≤ max ((s.sup f) x y) ((s.sup f) y z)

Tactic:
y

Goal state after:
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 : X
⊢ ∀ (z : X), (s.sup f) x z ≤ max ((s.sup f) x y) ((s.sup f) y z)
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
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ (↑(logSizeBallSeq J hJ a c l).radius - 1 + 1) * c = ↑(logSizeBallSeq J hJ a c l).radius * c

Tactic:
congr

Goal state after:
case e_a
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ ↑(logSizeBallSeq J hJ a c l).radius - 1 + 1 = ↑(logSizeBallSeq J hJ a c l).radius
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 : N
f : ↑(Ω^ N X x)
x✝ : N → ↑I
⊢ (f fun j ↦ if j = i then σ (x✝ i) else x✝ j) =
    f (↑(Cube.insertAt i) (σ (↑(Cube.splitAt i) x✝).1, (↑(Cube.splitAt i) x✝).2))

Tactic:
congr

Goal state after:
case e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f : ↑(Ω^ N X x)
x✝ : N → ↑I
⊢ (fun j ↦ if j = i then σ (x✝ i) else x✝ j) = ↑(Cube.insertAt i) (σ (↑(Cube.splitAt i) x✝).1, (↑(Cube.splitAt i) x✝).2)
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ coveringNumber ε A ≤ packingNumber ε A

Tactic:
by_cases! h_top : packingNumber ε A ≠ ⊤
  · rw [← encard_maximalSeparatedSet h_top]
    exact isCover_maximalSeparatedSet h_top |>.coveringNumber_le_encard maximalSeparatedSet_subset
  · simp [h_top]

Goal state after:
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:
by
    rw [dist_comm]
    exact infDist_le_infDist_add_hausdorffDist (edist_ne_top t s)

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

Goal state before:
pp: Y : Type u_2
inst✝¹ : PseudoEMetricSpace Y
r : ℝ≥0
X : Type u_3
inst✝ : PseudoMetricSpace X
hX : BoundedSpace X
f : X → Y
s : ℝ≥0
hs : s ≤ r
C : ℝ≥0
hf : HolderWith C r f
C' : ℝ≥0
hC' : ∀ (a b : X), edist a b ≤ ↑C'
⊢ MemHolder s f

Tactic:
exact ⟨C * C' ^ (r - s : ℝ),
    holderOnWith_univ.1 <| (holderOnWith_univ.2 hf).of_le (fun x _ y _ ↦ hC' x y) hs⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
s t : ℝ≥0
A : Set X
hf₁ : ∃ C, HolderOnWith C r f A
hf₂ : ∃ C, HolderOnWith C t f A
hrs : r ≤ s
hst : s ≤ t
⊢ ∃ C, HolderOnWith C s f A

Tactic:
by
  obtain ⟨C₁, hf₁⟩ := hf₁
  obtain ⟨C₂, hf₂⟩ := hf₂
  exact ⟨max C₁ C₂, hf₁.of_le_of_le hf₂ hrs hst⟩

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

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : eHolderNorm r f = 0
x₁ x₂ : X
hx : x₁ = x₂
⊢ f x₁ = f x₂

pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : eHolderNorm r f = 0
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ f x₁ = f x₂

Tactic:
· rw [hx]

Goal state after:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : eHolderNorm r f = 0
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ f x₁ = f x₂
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case mpr.inr
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (x₁ x₂ : X), f x₁ = f x₂
hX : Nonempty X
⊢ eHolderNorm r f = eHolderNorm r (Function.const X (f hX.some))

Tactic:
congr

Goal state after:
case mpr.inr.e_f
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (x₁ x₂ : X), f x₁ = f x₂
hX : Nonempty X
⊢ f = Function.const X (f hX.some)
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
⊢ ∀ (y : Snowflaking X α hα₀ hα₁), 0 ≤ dist x y

Tactic:
y

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x y : Snowflaking X α hα₀ hα₁
⊢ 0 ≤ dist x y
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
⊢ ∀ (y : Snowflaking X α hα₀ hα₁), edist x y = ENNReal.ofReal (dist x y)

Tactic:
y

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x y : Snowflaking X α hα₀ hα₁
⊢ edist x y = ENNReal.ofReal (dist x y)
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: case h
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯
s : Set (Snowflaking X α hα₀ hα₁)
C : ℝ
hC : ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
x : X
hx : x ∈ ⇑toSnowflaking ⁻¹' s
⊢ ∀ ⦃y : X⦄, y ∈ ⇑toSnowflaking ⁻¹' s → dist x y ≤ C ^ α⁻¹

Tactic:
y

Goal state after:
case h
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯
s : Set (Snowflaking X α hα₀ hα₁)
C : ℝ
hC : ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
x : X
hx : x ∈ ⇑toSnowflaking ⁻¹' s
y : X
⊢ y ∈ ⇑toSnowflaking ⁻¹' s → dist x y ≤ C ^ α⁻¹
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: ⊢ generateFrom {∅, {True}} = generateFrom {s | ∃ a, (Iic a)ᶜ = s}

Tactic:
congr

Goal state after:
⊢ {∅, {True}} = {s | ∃ a, (Iic a)ᶜ = s}
Module: Mathlib.Topology.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
continuous_toFun✝¹ : Continuous { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
continuous_toFun✝ : Continuous { toFun := toFun✝, monotone' := monotone'✝ }.toFun
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, monotone' := monotone'✝¹, continuous_toFun := continuous_toFun✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, monotone' := monotone'✝, continuous_toFun := continuous_toFun✝ }
⊢ { toFun := toFun✝¹, monotone' := monotone'✝¹, continuous_toFun := continuous_toFun✝¹ } =
    { toFun := toFun✝, monotone' := monotone'✝, continuous_toFun := continuous_toFun✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.Order.Hom.Esakia

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
exists_map_eq_of_map_le'✝¹ :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun a ≤ b →
      ∃ c, a ≤ c ∧ { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun c = b
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
exists_map_eq_of_map_le'✝ :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    { toFun := toFun✝, monotone' := monotone'✝ }.toFun a ≤ b →
      ∃ c, a ≤ c ∧ { toFun := toFun✝, monotone' := monotone'✝ }.toFun c = b
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝¹, monotone' := monotone'✝¹, exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := toFun✝, monotone' := monotone'✝, exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ }
⊢ { toFun := toFun✝¹, monotone' := monotone'✝¹, exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝¹ } =
    { toFun := toFun✝, monotone' := monotone'✝, exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.Order.Hom.Esakia

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
continuous_toFun✝¹ : Continuous { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun
exists_map_eq_of_map_le'✝¹ :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    { toFun := toFun✝¹, monotone' := monotone'✝¹, continuous_toFun := continuous_toFun✝¹ }.toFun a ≤ b →
      ∃ c, a ≤ c ∧ { toFun := toFun✝¹, monotone' := monotone'✝¹, continuous_toFun := continuous_toFun✝¹ }.toFun c = b
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
continuous_toFun✝ : Continuous { toFun := toFun✝, monotone' := monotone'✝ }.toFun
exists_map_eq_of_map_le'✝ :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    { toFun := toFun✝, monotone' := monotone'✝, continuous_toFun := continuous_toFun✝ }.toFun a ≤ b →
      ∃ c, a ≤ c ∧ { toFun := toFun✝, monotone' := monotone'✝, continuous_toFun := continuous_toFun✝ }.toFun c = b
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝¹, monotone' := monotone'✝¹, continuous_toFun := continuous_toFun✝¹,
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := toFun✝, monotone' := monotone'✝, continuous_toFun := continuous_toFun✝,
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ }
⊢ { toFun := toFun✝¹, monotone' := monotone'✝¹, continuous_toFun := continuous_toFun✝¹,
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝¹ } =
    { toFun := toFun✝, monotone' := monotone'✝, continuous_toFun := continuous_toFun✝,
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.Partial

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
h : PContinuous f
x : X
⊢ ∀ {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)

Tactic:
y

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
h : PContinuous f
x : X
y : Y
⊢ y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
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
⊢ ∃ Φ Ψ, Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

Tactic:
let F := kuratowskiEmbedding (OptimalGHCoupling X Y)
  let Φ := F ∘ optimalGHInjl X Y
  let Ψ := F ∘ optimalGHInjr X Y
  refine ⟨Φ, Ψ, ?_, ?_, ?_⟩
  · exact (kuratowskiEmbedding.isometry _).comp (isometry_optimalGHInjl X Y)
  · exact (kuratowskiEmbedding.isometry _).comp (isometry_optimalGHInjr X Y)
  · rw [← image_univ, ← image_univ, image_comp F, image_univ, image_comp F (optimalGHInjr X Y),
      image_univ, ← hausdorffDist_optimal]
    exact (hausdorffDist_image (kuratowskiEmbedding.isometry _)).symm

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LE α
carrier✝¹ : Set α
isClopen'✝¹ : IsClopen carrier✝¹
upper'✝¹ : IsUpperSet { carrier := carrier✝¹, isClopen' := isClopen'✝¹ }.carrier
carrier✝ : Set α
isClopen'✝ : IsClopen carrier✝
upper'✝ : IsUpperSet { carrier := carrier✝, isClopen' := isClopen'✝ }.carrier
h :
  (fun s ↦ s.carrier) { carrier := carrier✝¹, isClopen' := isClopen'✝¹, upper' := upper'✝¹ } =
    (fun s ↦ s.carrier) { carrier := carrier✝, isClopen' := isClopen'✝, upper' := upper'✝ }
⊢ { carrier := carrier✝¹, isClopen' := isClopen'✝¹, upper' := upper'✝¹ } =
    { carrier := carrier✝, isClopen' := isClopen'✝, upper' := upper'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.Sheaves.PUnit

Goal state before:
pp: case e'_5.inr.inr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
this : IndiscreteTopology ↑X
s : Sieve ⊤
hs : s ∈ (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
f : ⊤ ⟶ ⊤
hf : s.arrows f
hm : x ∈ ⊤
⊢ s.arrows (𝟙 ⊤)

Tactic:
· convert! hf

Goal state after:
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case e'_2
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
hd : (U : Opens ↑(of PUnit.{u + 1})) → Decidable (PUnit.unit ∈ U)
⊢ skyscraperPresheaf p₀ A = skyscraperPresheaf p₀ A

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case convert_2
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
hd : (U : Opens ↑(of PUnit.{u + 1})) → Decidable (PUnit.unit ∈ U)
⊢ skyscraperPresheaf p₀ A =
    (Presheaf.pushforward C (ofHom (ContinuousMap.const (↑(of PUnit.{u + 1})) p₀))).obj
      (skyscraperPresheaf PUnit.unit A)

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: case neg.refine_2
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s : Set X
hs : IsClosed[inst✝] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
⊢ ⇑f ⁻¹' {0} = ⇑f ⁻¹' ⋂ i, range ⇑f ∩ Iio (1 / (↑i + 1))

Tactic:
congr

Goal state after:
case neg.refine_2.e_s
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s : Set X
hs : IsClosed[inst✝] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
⊢ {0} = ⋂ i, range ⇑f ∩ Iio (1 / (↑i + 1))
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_3
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x : ↑(s p)
⊢ ∀ (y : ↑(s p)), |dist x y - dist (Φ x) (Φ y)| ≤ ε

Tactic:
y

Goal state after:
case refine_3
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε