mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : InvolutiveStar R
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
inst✝³ : StarAddMonoid E
inst✝² : StarModule R E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousStar E
x✝ : E
⊢ (star (toConv (ContinuousLinearMap.id R E))).ofConv x✝ = (toConv (ContinuousLinearMap.id R E)).ofConv x✝

Tactic:
;

Goal state after:
R : Type u_1
E : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : InvolutiveStar R
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
inst✝³ : StarAddMonoid E
inst✝² : StarModule R E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousStar E
x✝ : E
⊢ (star (toConv (ContinuousLinearMap.id R E))).ofConv x✝ = (toConv (ContinuousLinearMap.id R E)).ofConv x✝
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousStar E
inst✝ : ContinuousStar F
x✝ : E
⊢ (star (toConv 0)).ofConv x✝ = (toConv 0).ofConv x✝

Tactic:
;

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousStar E
inst✝ : ContinuousStar F
x✝ : E
⊢ (star (toConv 0)).ofConv x✝ = (toConv 0).ofConv x✝
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: E : Type u_2
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : StarAddMonoid E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : ContinuousStar E
S : Type u_4
inst✝⁷ : Semiring S
inst✝⁶ : StarAddMonoid S
inst✝⁵ : StarModule S S
inst✝⁴ : Module S E
inst✝³ : StarModule S E
inst✝² : TopologicalSpace S
inst✝¹ : ContinuousStar S
inst✝ : ContinuousSMul S E
a : E
⊢ (star (toConv (toSpanSingleton S a))).ofConv 1 = (toConv (toSpanSingleton S (star a))).ofConv 1

Tactic:
;

Goal state after:
E : Type u_2
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : StarAddMonoid E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : ContinuousStar E
S : Type u_4
inst✝⁷ : Semiring S
inst✝⁶ : StarAddMonoid S
inst✝⁵ : StarModule S S
inst✝⁴ : Module S E
inst✝³ : StarModule S E
inst✝² : TopologicalSpace S
inst✝¹ : ContinuousStar S
inst✝ : ContinuousSMul S E
a : E
⊢ (star (toConv (toSpanSingleton S a))).ofConv 1 = (toConv (toSpanSingleton S (star a))).ofConv 1
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹⁷ : AddCommMonoid E
inst✝¹⁶ : StarAddMonoid E
inst✝¹⁵ : AddCommMonoid F
inst✝¹⁴ : StarAddMonoid F
inst✝¹³ : TopologicalSpace E
inst✝¹² : TopologicalSpace F
inst✝¹¹ : ContinuousStar E
inst✝¹⁰ : ContinuousStar F
S : Type u_4
inst✝⁹ : Semiring S
inst✝⁸ : StarAddMonoid S
inst✝⁷ : StarModule S S
inst✝⁶ : Module S E
inst✝⁵ : StarModule S E
inst✝⁴ : TopologicalSpace S
inst✝³ : ContinuousStar S
inst✝² : Module S F
inst✝¹ : StarModule S F
inst✝ : ContinuousSMul S F
f : WithConv (E →L[S] S)
x : F
x✝ : E
⊢ (star (toConv (f.ofConv.smulRight x))).ofConv x✝ = (toConv ((star f).ofConv.smulRight (star x))).ofConv x✝

Tactic:
;

Goal state after:
E : Type u_2
F : Type u_3
inst✝¹⁷ : AddCommMonoid E
inst✝¹⁶ : StarAddMonoid E
inst✝¹⁵ : AddCommMonoid F
inst✝¹⁴ : StarAddMonoid F
inst✝¹³ : TopologicalSpace E
inst✝¹² : TopologicalSpace F
inst✝¹¹ : ContinuousStar E
inst✝¹⁰ : ContinuousStar F
S : Type u_4
inst✝⁹ : Semiring S
inst✝⁸ : StarAddMonoid S
inst✝⁷ : StarModule S S
inst✝⁶ : Module S E
inst✝⁵ : StarModule S E
inst✝⁴ : TopologicalSpace S
inst✝³ : ContinuousStar S
inst✝² : Module S F
inst✝¹ : StarModule S F
inst✝ : ContinuousSMul S F
f : WithConv (E →L[S] S)
x : F
x✝ : E
⊢ (star (toConv (f.ofConv.smulRight x))).ofConv x✝ = (toConv ((star f).ofConv.smulRight (star x))).ofConv x✝
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁵ : Semiring R
inst✝¹⁴ : InvolutiveStar R
inst✝¹³ : AddCommMonoid E
inst✝¹² : Module R E
inst✝¹¹ : StarAddMonoid E
inst✝¹⁰ : StarModule R E
inst✝⁹ : AddCommMonoid F
inst✝⁸ : Module R F
inst✝⁷ : StarAddMonoid F
inst✝⁶ : StarModule R F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : ContinuousStar E
inst✝² : ContinuousStar F
inst✝¹ : SMulCommClass R R F
inst✝ : ContinuousConstSMul R F
x✝² : R
x✝¹ : WithConv (E →L[R] F)
x✝ : E
⊢ (star (x✝² • x✝¹)).ofConv x✝ = (star x✝² • star x✝¹).ofConv x✝

Tactic:
;

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁵ : Semiring R
inst✝¹⁴ : InvolutiveStar R
inst✝¹³ : AddCommMonoid E
inst✝¹² : Module R E
inst✝¹¹ : StarAddMonoid E
inst✝¹⁰ : StarModule R E
inst✝⁹ : AddCommMonoid F
inst✝⁸ : Module R F
inst✝⁷ : StarAddMonoid F
inst✝⁶ : StarModule R F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : ContinuousStar E
inst✝² : ContinuousStar F
inst✝¹ : SMulCommClass R R F
inst✝ : ContinuousConstSMul R F
x✝² : R
x✝¹ : WithConv (E →L[R] F)
x✝ : E
⊢ (star (x✝² • x✝¹)).ofConv x✝ = (star x✝² • star x✝¹).ofConv x✝
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 y : cell C 0
⊢ cellFrontier 1 e = {↑(map 0 x) ![]} ∪ {↑(map 0 y) ![]} ↔ cellFrontier 1 e = {↑(map 0 x) ![], ↑(map 0 y) ![]}

Tactic:
singleton_union

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
x y : cell C 0
⊢ cellFrontier 1 e = {↑(map 0 x) ![], ↑(map 0 y) ![]} ↔ cellFrontier 1 e = {↑(map 0 x) ![], ↑(map 0 y) ![]}
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
a : Ordinal.{u}
⊢ sᵈ[a + 1] = relDerivedSet sᵈ[a]

Tactic:
by
  simpa [iteratedDerivedSet] using
    gfpApprox_add_one relDerivedSet relDerivedSet_subset a

Goal state after:
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
g : WithGeneratedByTopology X Y → Z
i : ι
f : C(X i, Y)
⊢ Continuous[inferInstance, inst✝] (g ∘ ⇑f) ↔ Continuous[inst✝¹ i, inst✝] (g ∘ ⇑equiv.symm ∘ ⇑f)

Tactic:
;

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
g : WithGeneratedByTopology X Y → Z
i : ι
f : C(X i, Y)
⊢ Continuous[inferInstance, inst✝] (g ∘ ⇑f) ↔ Continuous[inst✝¹ i, inst✝] (g ∘ ⇑equiv.symm ∘ ⇑f)
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
inst✝ : IsGeneratedBy X Y
⊢ Continuous[_, tY] ⇑WithGeneratedByTopology.equiv

Tactic:
;

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
inst✝ : IsGeneratedBy X Y
⊢ Continuous[_, tY] ⇑WithGeneratedByTopology.equiv
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
inst✝ : IsGeneratedBy X Y
⊢ Continuous[tY, _] ⇑WithGeneratedByTopology.equiv.symm

Tactic:
;

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
inst✝ : IsGeneratedBy X Y
⊢ Continuous[tY, _] ⇑WithGeneratedByTopology.equiv.symm
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
inst✝ : IsGeneratedBy X Y
g : Y → Z
⊢ Continuous[tY, inst✝¹] g ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, inst✝¹] (g ∘ ⇑f)

Tactic:
(homeomorph (X := X)).isQuotientMap.continuous_iff,

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
inst✝ : IsGeneratedBy X Y
g : Y → Z
⊢ Continuous[_, inst✝¹] (g ∘ ⇑homeomorph) ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, inst✝¹] (g ∘ ⇑f)
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₂✝
x : ↑X✝
⊢ (ConcreteCategory.hom a₁✝) x = (ConcreteCategory.hom a₂✝) x

Tactic:
;

Goal state after:
ι : 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₂✝
x : ↑X✝
⊢ (ConcreteCategory.hom a₁✝) x = (ConcreteCategory.hom a₂✝) x
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₂✝
x : ↑X✝
⊢ (ConcreteCategory.hom a₁✝) x = (ConcreteCategory.hom a₂✝) x

Tactic:
;

Goal state after:
ι : 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₂✝
x : ↑X✝
⊢ (ConcreteCategory.hom a₁✝) x = (ConcreteCategory.hom a₂✝) x
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
J : (Finset ι)ᵒᵖ
⊢ IsCompact (obj C fun x ↦ x ∈ unop J)

Tactic:
;

Goal state after:
ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
J : (Finset ι)ᵒᵖ
⊢ IsCompact (obj C fun x ↦ x ∈ unop J)
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
⊢ CompactSpace ↑C

Tactic:
rwa [← isCompact_iff_compactSpace]

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
⊢ Fintype ↑(π C fun x ↦ x ∈ s)

Tactic:
let f : π C (· ∈ s) → (s → Bool) := fun x j ↦ x.val j.val

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : ↑(π C fun x ↦ x ∈ s) → ↥s → Bool := fun x j ↦ ↑x ↑j
⊢ Fintype ↑(π C fun x ↦ x ∈ s)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y = x
b : I
left✝ : b ∈ s.sort fun x1 x2 ↦ x1 ≥ x2
hh : ¬↑x b = true
⊢ LocallyConstant.toFun 1 x - 0 = 1

Tactic:
simp only [LocallyConstant.toFun_eq_coe, LocallyConstant.coe_one, Pi.one_apply, sub_zero]

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : ∀ (a : I), ↑y a = ↑x a
⊢ y = x

Tactic:
;

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : ∀ (a : I), ↑y a = ↑x a
⊢ y = x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : ∀ (a : I), ↑y a = ↑x a
x✝ : I
⊢ ↑y x✝ = ↑x x✝

Tactic:
;

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : ∀ (a : I), ↑y a = ↑x a
x✝ : I
⊢ ↑y x✝ = ↑x x✝
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_1.h
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
⊢ ∀ (i : I), y i ≠ false → J i

Tactic:
;

Goal state after:
case refine_1.h
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
⊢ ∀ (i : I), y i ≠ false → J i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_2.h
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
⊢ ∀ (i : I), x i ≠ false → J i

Tactic:
;

Goal state after:
case refine_2.h
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
⊢ ∀ (i : I), x i ≠ false → J i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : I → Bool
i : I
⊢ (Proj J ∘ Proj K) x i = Proj J x i

Tactic:
;

Goal state after:
I : Type u
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : I → Bool
i : I
⊢ (Proj J ∘ Proj K) x i = Proj J x i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : I → Bool
i : I
⊢ (if J i then if K i then x i else false else false) = if J i then x i else false

Tactic:
;

Goal state after:
I : Type u
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : I → Bool
i : I
⊢ (if J i then if K i then x i else false else false) = if J i then x i else false
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: 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
ih :
  List.IsChain (fun x1 x2 ↦ x1 > x2) as →
    (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 ≤ as})
ha : (∀ y ∈ as.head?, a > y) ∧ List.IsChain (fun x1 x2 ↦ x1 > x2) as
⊢ List.IsChain (fun x1 x2 ↦ x1 > x2) as

Tactic:
;

Goal state after:
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
ih :
  List.IsChain (fun x1 x2 ↦ x1 > x2) as →
    (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 ≤ as})
ha : (∀ y ∈ as.head?, a > y) ∧ List.IsChain (fun x1 x2 ↦ x1 > x2) as
⊢ List.IsChain (fun x1 x2 ↦ x1 > x2) as
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
s : (Finset I)ᵒᵖ
⊢ IsCompact (π C fun x ↦ x ∈ unop s)

Tactic:
;

Goal state after:
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
s : (Finset I)ᵒᵖ
⊢ IsCompact (π C fun x ↦ x ∈ unop s)
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
J : (Finset I)ᵒᵖ
⊢ CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := id, continuous_toFun := ⋯ } =
    𝟙 (of ↑(π C fun x ↦ x ∈ unop J))

Tactic:
;

Goal state after:
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
J : (Finset I)ᵒᵖ
⊢ CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := id, continuous_toFun := ⋯ } =
    𝟙 (of ↑(π C fun x ↦ x ∈ unop J))
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✝ Z✝ : (Finset I)ᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ } =
    CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X)
      ({ toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ }.comp { toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ })

Tactic:
;

Goal state after:
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✝ Z✝ : (Finset I)ᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ } =
    CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X)
      ({ toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ }.comp { toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ })
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✝ Z✝ : (Finset I)ᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ProjRestricts C ⋯ =
    ⇑{ toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ } ∘ ⇑{ toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ }

Tactic:
;

Goal state after:
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✝ Z✝ : (Finset I)ᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ProjRestricts C ⋯ =
    ⇑{ toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ } ∘ ⇑{ toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ }
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✝ Z✝ : (Finset I)ᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ProjRestricts C ⋯ = ProjRestricts C ⋯ ∘ ProjRestricts C ⋯

Tactic:
;

Goal state after:
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✝ Z✝ : (Finset I)ᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ProjRestricts C ⋯ = ProjRestricts C ⋯ ∘ ProjRestricts C ⋯
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) *
      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})

Tactic:
;

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: 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
⊢ CompactSpace ↑C

Tactic:
rwa [← isCompact_iff_compactSpace]

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
s t : Finset I
f : unop (op t) ⊆ unop (op s)
x : ↑((spanFunctor hC).obj (op s)).toTop
x✝ : ↑(π C (Membership.mem (unop (op s))))
i : ↥t
⊢ ↑((⇑(iso_map C fun x ↦ x ∈ t) ∘ ProjRestricts C f) x✝) i =
    ↑((⇑(IndexFunctor.map C f) ∘ ⇑(iso_map C fun x ↦ x ∈ s)) x✝) i

Tactic:
;

Goal state after:
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
s t : Finset I
f : unop (op t) ⊆ unop (op s)
x : ↑((spanFunctor hC).obj (op s)).toTop
x✝ : ↑(π C (Membership.mem (unop (op s))))
i : ↥t
⊢ ↑((⇑(iso_map C fun x ↦ x ∈ t) ∘ ProjRestricts C f) x✝) i =
    ↑((⇑(IndexFunctor.map C f) ∘ ⇑(iso_map C fun x ↦ x ∈ s)) x✝) i
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✝¹ : (Finset I)ᵒᵖ
s : Finset I
a✝ : ↑(((Functor.const (Finset I)ᵒᵖ).obj (indexCone hC).pt).obj (op s)).toTop
x✝ : ↑C
i : ↥s
⊢ ↑((⇑(iso_map C fun x ↦ x ∈ s) ∘ ProjRestrict C fun x ↦ x ∈ s) x✝) i = ↑((IndexFunctor.π_app C fun x ↦ x ∈ s) x✝) i

Tactic:
;

Goal state after:
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✝¹ : (Finset I)ᵒᵖ
s : Finset I
a✝ : ↑(((Functor.const (Finset I)ᵒᵖ).obj (indexCone hC).pt).obj (op s)).toTop
x✝ : ↑C
i : ↥s
⊢ ↑((⇑(iso_map C fun x ↦ x ∈ s) ∘ ProjRestrict C fun x ↦ x ∈ s) x✝) i = ↑((IndexFunctor.π_app C fun x ↦ x ∈ s) x✝) i