mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case none.none
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
xy : edist none none = 0
⊢ none = none

pp: case none.some
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝ : α
xy : edist none (some val✝) = 0
⊢ none = some val✝

pp: case some.none
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝ : α
xy : edist (some val✝) none = 0
⊢ some val✝ = none

pp: case some.some
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝¹ val✝ : α
xy : edist (some val✝¹) (some val✝) = 0
⊢ some val✝¹ = some val✝

Tactic:
· rfl

Goal state after:
case none.some
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝ : α
xy : edist none (some val✝) = 0
⊢ none = some val✝

case some.none
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝ : α
xy : edist (some val✝) none = 0
⊢ some val✝ = none

case some.some
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝¹ val✝ : α
xy : edist (some val✝¹) (some val✝) = 0
⊢ some val✝¹ = some val✝
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case top.coe
x✝ : ℝ≥0
⊢ edist ∞ ↑x✝ = ∞

pp: case coe.top
x✝ : ℝ≥0
⊢ edist ↑x✝ ∞ = ∞

pp: case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ ¬edist ↑x✝¹ ↑x✝ = ∞

Tactic:
· rfl

Goal state after:
case coe.top
x✝ : ℝ≥0
⊢ edist ↑x✝ ∞ = ∞

case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ ¬edist ↑x✝¹ ↑x✝ = ∞
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case coe.top
x✝ : ℝ≥0
⊢ edist ↑x✝ ∞ = ∞

pp: case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ ¬edist ↑x✝¹ ↑x✝ = ∞

Tactic:
· rfl

Goal state after:
case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ ¬edist ↑x✝¹ ↑x✝ = ∞
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case neg
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ γ (qRight (t, 0)) = γ 1

pp: case pos
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ γ (qRight (t, 0)) = γ ⟨2 * ↑t, ⋯⟩

Tactic:
all_goals apply congr_arg γ; ext1; rw [qRight_zero_right]

Goal state after:
case neg
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) = ↑1

case pos
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) = ↑⟨2 * ↑t, ⋯⟩
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: ⊢ ⋂ n, preCantorSet n = ((fun x ↦ x / 3) '' ⋂ n, preCantorSet n) ∪ (fun x ↦ (2 + x) / 3) '' ⋂ n, preCantorSet n

Tactic:
rw [Set.image_iInter, Set.image_iInter]

Goal state after:
⊢ ⋂ n, preCantorSet n = (⋂ i, (fun x ↦ x / 3) '' preCantorSet i) ∪ ⋂ i, (fun x ↦ (2 + x) / 3) '' preCantorSet i

case hf
⊢ Function.Bijective fun x ↦ (2 + x) / 3

case hf
⊢ Function.Bijective fun x ↦ x / 3
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: ⊢ cantorSet = {x | ∃ a, (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x}

Tactic:
by
  ext x
  refine ⟨fun h ↦ ?_, fun ⟨a, ha⟩ ↦ ?_⟩
  · use cantorToTernary x
    exact ⟨fun _ ↦ cantorToTernary_ne_one, ofDigits_cantorToTernary h⟩
  · rw [← ha.right]
    exact ofDigits_zero_two_sequence_mem_cantorSet ha.left

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ Tendsto (eraseIdx i) (𝓝 ⟨l, hl⟩) (𝓝 (eraseIdx i ⟨l, hl⟩))

Tactic:
Vector.eraseIdx,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ Tendsto (eraseIdx i) (𝓝 ⟨l, hl⟩) (𝓝 ⟨l.eraseIdx ↑i, ⋯⟩)
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
inst✝ : Nonempty N
i : N
p q : ↑(Ω^ N X x)
⊢ (fun x1 x2 ↦ x1 * x2) ⟦p⟧ ⟦q⟧ =
    ⟦fromLoop (Classical.arbitrary N)
        (Path.trans (toLoop (Classical.arbitrary N) q) (toLoop (Classical.arbitrary N) p))⟧

Tactic:
apply Quotient.sound

Goal state after:
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nonempty N
i : N
p q : ↑(Ω^ N X x)
⊢ (loopHomeo (Classical.arbitrary N)).symm
      (((loopHomeo (Classical.arbitrary N)).toEquiv q).trans ((loopHomeo (Classical.arbitrary N)).toEquiv p)) ≈
    fromLoop (Classical.arbitrary N) (Path.trans (toLoop (Classical.arbitrary N) q) (toLoop (Classical.arbitrary N) p))
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
inst✝ : Nonempty N
i : N
p : ↑(Ω^ N X x)
⊢ (⟦p⟧)⁻¹ = ⟦fromLoop (Classical.arbitrary N) (Path.symm (toLoop (Classical.arbitrary N) p))⟧

Tactic:
apply Quotient.sound

Goal state after:
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nonempty N
i : N
p : ↑(Ω^ N X x)
⊢ (loopHomeo (Classical.arbitrary N)).symm ((loopHomeo (Classical.arbitrary N)).toEquiv p).symm ≈
    fromLoop (Classical.arbitrary N) (Path.symm (toLoop (Classical.arbitrary N) p))
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✝
N : Type ?u.15
inst✝ : Unique N
a b : HomotopyGroup N X x
p q : ↑(Ω^ N X x)
⊢ (homotopyGroupEquivFundamentalGroupOfUnique N).toFun ⟦transAt default q p⟧ =
    (homotopyGroupEquivFundamentalGroupOfUnique N).toFun ⟦p⟧ * (homotopyGroupEquivFundamentalGroupOfUnique N).toFun ⟦q⟧

Tactic:
apply Quotient.sound

Goal state after:
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a b : HomotopyGroup N X x
p q : ↑(Ω^ N X x)
⊢ (genLoopEquivOfUnique N) (transAt default q p) ≈ ((genLoopEquivOfUnique N) q).trans ((genLoopEquivOfUnique N) p)
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
a b : π_ 1 X x
p q : ↑(Ω^ (Fin 1) X x)
⊢ pi1EquivFundamentalGroup.toFun ⟦transAt 0 q p⟧ =
    pi1EquivFundamentalGroup.toFun ⟦p⟧ * pi1EquivFundamentalGroup.toFun ⟦q⟧

Tactic:
apply Quotient.sound

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
a b : π_ 1 X x
p q : ↑(Ω^ (Fin 1) X x)
⊢ (genLoopEquivOfUnique (Fin 1)) (transAt 0 q p) ≈
    ((genLoopEquivOfUnique (Fin 1)) q).trans ((genLoopEquivOfUnique (Fin 1)) p)
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : X
y : Y
⊢ ↑(maxVar X Y) * 1 ≤ ↑(maxVar X Y) * dist (inl x) (inr y)

Tactic:
by gcongr; apply Sum.one_le_dist_inl_inr

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : Y
y : X
⊢ ↑(maxVar X Y) * 1 ≤ ↑(maxVar X Y) * dist (inl x) (inr y)

Tactic:
by gcongr; apply Sum.one_le_dist_inl_inr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : EDist α
d : ℝ≥0∞
f : β → α
s : Set β
⊢ d ≤ (f '' s).einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≠ f y → d ≤ edist (f x) (f y)

Tactic:
simp_rw [le_einfsep_iff, forall_mem_image]

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) ↔ ∀ (i : ↑s.offDiag), x✝ ≤ uncurry edist ↑i

Tactic:
imp_forall_iff,

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

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

Tactic:
imp_forall_iff,

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Finite
x✝ : ℝ≥0∞
⊢ (∀ x ∈ s, ∀ y ∈ s, x ≠ y → x✝ ≤ edist x y) ↔ x✝ ≤ ⋯.toFinset.inf (uncurry edist)

Tactic:
imp_forall_iff,

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Finite
x✝ : ℝ≥0∞
⊢ (∀ (x x_1 : α), x ∈ s → x_1 ∈ s → x ≠ x_1 → x✝ ≤ edist x x_1) ↔ x✝ ≤ ⋯.toFinset.inf (uncurry edist)
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
x✝ : ℝ
⊢ (∀ x ∈ s, ∀ y ∈ s, x ≠ y → x✝ ≤ dist x y) ↔ ∀ i ∈ s.offDiag, x✝ ≤ uncurry dist i

Tactic:
imp_forall_iff,

Goal state after:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
x✝ : ℝ
⊢ (∀ (x x_1 : α), x ∈ s → x_1 ∈ s → x ≠ x_1 → x✝ ≤ dist x x_1) ↔ ∀ i ∈ s.offDiag, x✝ ≤ uncurry dist i
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case pos
α : Type u_1
inst✝² : PseudoMetricSpace α
s : Set α
inst✝¹ : Decidable s.Nontrivial
inst✝ : Fintype ↑s
hs : s.Nontrivial
x✝ : ℝ
⊢ (∀ x ∈ s, ∀ y ∈ s, x ≠ y → x✝ ≤ dist x y) ↔ x✝ ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)

Tactic:
imp_forall_iff,

Goal state after:
case pos
α : Type u_1
inst✝² : PseudoMetricSpace α
s : Set α
inst✝¹ : Decidable s.Nontrivial
inst✝ : Fintype ↑s
hs : s.Nontrivial
x✝ : ℝ
⊢ (∀ (x x_1 : α), x ∈ s → x_1 ∈ s → x ≠ x_1 → x✝ ≤ dist x x_1) ↔ x✝ ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
x✝ : ℝ
⊢ (∀ x ∈ s, ∀ y ∈ s, x ≠ y → x✝ ≤ dist x y) ↔ x✝ ≤ ⋯.toFinset.inf' ⋯ (uncurry dist)

Tactic:
imp_forall_iff,

Goal state after:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
x✝ : ℝ
⊢ (∀ (x x_1 : α), x ∈ s → x_1 ∈ s → x ≠ x_1 → x✝ ≤ dist x x_1) ↔ x✝ ≤ ⋯.toFinset.inf' ⋯ (uncurry dist)
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
⊢ 0 ∈ lowerBounds ((fun p ↦ hausdorffDist ↑p.1 ↑p.2) '' {a | ⟦a⟧ = toGHSpace X} ×ˢ {b | ⟦b⟧ = toGHSpace Y})

Tactic:
simp only [lowerBounds, mem_image, mem_prod, mem_ofPred_eq, Prod.exists, and_imp,
      forall_exists_index]

Goal state after:
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
⊢ ∀ ⦃a : ℝ⦄ (x x_1 : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦x⟧ = toGHSpace X → ⟦x_1⟧ = toGHSpace Y → hausdorffDist ↑x ↑x_1 = a → 0 ≤ a
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsLowerSet α
inst✝ : Topology.IsLowerSet β
f : α → β
⊢ Monotone f ↔ Continuous[inst✝³, inst✝²] f

Tactic:
by
  rw [← monotone_dual_iff]
  exact IsUpperSet.monotone_iff_continuous (α := αᵒᵈ) (β := βᵒᵈ)
    (f := (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ))

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
⊢ lawson α ≤ scott α univ

Tactic:
exact inf_le_right

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

Goal state before:
pp: case inl
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i : ↑c
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f i)).op)) (StructuredArrow.right ↑i).snd =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f i)).op)) (StructuredArrow.right ↑i).snd

pp: case inr.inl
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
h₁ : Nonempty (↑i ⟶ ↑j)
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f j)).op)) (StructuredArrow.right ↑i).snd =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f j)).op)) (StructuredArrow.right ↑j).snd

pp: case inr.inr
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
h₁ : Nonempty (↑j ⟶ ↑i)
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f j)).op)) (StructuredArrow.right ↑i).snd =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f j)).op)) (StructuredArrow.right ↑j).snd

Tactic:
· rfl

Goal state after:
case inr.inl
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
h₁ : Nonempty (↑i ⟶ ↑j)
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f j)).op)) (StructuredArrow.right ↑i).snd =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f j)).op)) (StructuredArrow.right ↑j).snd

case inr.inr
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
h₁ : Nonempty (↑j ⟶ ↑i)
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f j)).op)) (StructuredArrow.right ↑i).snd =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f j)).op)) (StructuredArrow.right ↑j).snd
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.op.pair.pair.id_pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
a✝¹ a✝ : ι
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map (Quiver.Hom.op (id_pair a✝¹ a✝)) ≫
      Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (Pairwise.pair a✝¹ a✝)) =
    Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op (Pairwise.pair a✝¹ a✝)) ≫
      ((diagram U).op ⋙ F).map (Quiver.Hom.op (id_pair a✝¹ a✝))

Tactic:
· dsimp
          rw [F.map_id]
          simp

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
⊢ ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
    𝟙 ((coneEquiv F U).symm.functor.obj (SheafConditionEqualizerProducts.fork F U)).pt ≫
        (Functor.mapCone F (cocone U).op).π.app j =
      ((coneEquiv F U).symm.functor.obj (SheafConditionEqualizerProducts.fork F U)).π.app j

Tactic:
by
            intro x
            induction x with | op x => ?_
            rcases x with ⟨⟩
            · simp
              rfl
            · dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res,
                SheafConditionEqualizerProducts.leftRes]
              simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app,
                Category.assoc]
              rw [← F.map_comp]
              rfl

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
⊢ ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
    𝟙 (Functor.mapCone F (cocone U).op).pt ≫
        ((coneEquiv F U).symm.functor.obj (SheafConditionEqualizerProducts.fork F U)).π.app j =
      (Functor.mapCone F (cocone U).op).π.app j

Tactic:
by
            intro x
            induction x with | op x => ?_
            rcases x with ⟨⟩
            · simp
              rfl
            · dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res,
                SheafConditionEqualizerProducts.leftRes]
              simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app,
                Category.assoc]
              rw [← F.map_comp]
              rfl

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : CompleteLinearOrder β
inst✝¹⁰ : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst✝⁹ : TopologicalSpace E
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
have hlsc : LowerSemicontinuousOn (fun x => ⨆ y ∈ Y, f x y) X := fun x hx ↦ by
    apply lowerSemicontinuousWithinAt_iSup
    intro i
    exact lowerSemicontinuousWithinAt_iSup fun i_1 ↦ hfy i i_1 x hx
  have husc : UpperSemicontinuousOn (fun y => ⨅ x ∈ X, f x y) Y := fun y hy ↦ by
    apply upperSemicontinuousWithinAt_iInf
    intro i
    exact upperSemicontinuousWithinAt_iInf fun i_1 ↦ hfx i i_1 y hy
  obtain ⟨a, ha, ha'⟩ := LowerSemicontinuousOn.exists_isMinOn
   ne_X kX hlsc
  obtain ⟨b, hb, hb'⟩ := UpperSemicontinuousOn.exists_isMaxOn ne_Y kY husc
  use a, ha, b, hb
  rw [isSaddlePointOn_iff' ha hb]
  refine le_trans (le_iInf₂ ha') ?_
  refine le_trans ?_ (iSup₂_le_iff.mpr hb')
  rw [minimax' ne_X cX kX hfy hfy' cY hfx hfx']

Goal state after: