mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
c : Submodule R M
hc : c ∈ isotypicComponents R M
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this✝² : IsSemisimpleModule R ↥c
this✝¹ : IsSemisimpleModule R ↥(c ⊓ sSup s)
this✝ : ∀ (c : ↑s), IsSemisimpleModule R ↥↑c
S : Submodule R M
le : S ≤ c ⊓ sSup s
right✝ : IsSimpleModule R ↥S
c' : Submodule R M
hc' : c' ∈ s
S' : Submodule R M
le' : S' ≤ c'
e : ↥S ≃ₗ[R] ↥S'
this : IsSimpleModule R ↥S'
⊢ c' ∈ {c}

Tactic:
rw [eq_isotypicComponent_of_le hc (le.trans inf_le_left), eq_isotypicComponent_of_le hc'.1 le']

Goal state after:
R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
c : Submodule R M
hc : c ∈ isotypicComponents R M
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this✝² : IsSemisimpleModule R ↥c
this✝¹ : IsSemisimpleModule R ↥(c ⊓ sSup s)
this✝ : ∀ (c : ↑s), IsSemisimpleModule R ↥↑c
S : Submodule R M
le : S ≤ c ⊓ sSup s
right✝ : IsSimpleModule R ↥S
c' : Submodule R M
hc' : c' ∈ s
S' : Submodule R M
le' : S' ≤ c'
e : ↥S ≃ₗ[R] ↥S'
this : IsSimpleModule R ↥S'
⊢ isotypicComponent R M ↥S' ∈ {isotypicComponent R M ↥S}
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: case cons
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
x : ι
l : List ι
ih : (∃ x ∈ l, f x ∈ I) → (List.map f l).prod ∈ I
hl : ∃ x_1 ∈ x :: l, f x_1 ∈ I
⊢ (List.map f (x :: l)).prod ∈ I

Tactic:
simp only [List.mem_cons, exists_eq_or_imp] at hl

Goal state after:
case cons
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
x : ι
l : List ι
ih : (∃ x ∈ l, f x ∈ I) → (List.map f l).prod ∈ I
hl : f x ∈ I ∨ ∃ a ∈ l, f a ∈ I
⊢ (List.map f (x :: l)).prod ∈ I
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
m : ℕ
r' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hr0 : ↑p ^ m * r' ≠ 0
n : ℕ
q' : 𝕎 k
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
hq0 : ↑p ^ n * q' ≠ 0
hrq : Localization.mk (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).1 (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).2 ≠ 0
b : 𝕎 k := frobeniusRotation p hr' hq'
⊢ φ ((algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) *
      Localization.mk (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).1 (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).2 =
    ↑p ^ (↑m - ↑n) * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b

Tactic:
exact exists_frobenius_solution_fractionRing_aux p m n r' q' hr' hq' hq

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

Goal state before:
pp: b o : Ordinal.{u_2}
h : ¬o = 0
⊢ o % b ^ log b o < o

Tactic:
decreasing_by exact mod_opow_log_lt_self b h

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

Goal state before:
pp: case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
a : Ordinal.{u_1}
H : a ∈ map Prod.fst (CNF b (o % b ^ log b o))
⊢ (log b o, o / b ^ log b o).1 > a

Tactic:
mem_map

Goal state after:
case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
a : Ordinal.{u_1}
H : ∃ a_1 ∈ CNF b (o % b ^ log b o), a_1.1 = a
⊢ (log b o, o / b ^ log b o).1 > a
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ ∀ a ∈ map Prod.toSigma (CNF b o), decide (a.snd ≠ 0) = true

Tactic:
mem_map

Goal state after:
b o : Ordinal.{u_1}
⊢ ∀ (a : (_ : Ordinal.{u_1}) × Ordinal.{u_1}), (∃ a_1 ∈ CNF b o, a_1.toSigma = a) → decide (a.snd ≠ 0) = true
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o e : Ordinal.{u_1}
h : o < b ^ e
he : e ∈ map Prod.fst (CNF b o)
⊢ False

Tactic:
mem_map

Goal state after:
b o e : Ordinal.{u_1}
h : o < b ^ e
he : ∃ a ∈ CNF b o, a.1 = e
⊢ False
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inr
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
⊢ (coeff b o) a = (single 0 o) a

Tactic:
obtain rfl | ha := eq_or_ne a 0
    · apply coeff_of_mem_CNF
      rw [CNF.of_le_one hb ho]
      simp
    · rw [single_eq_of_ne ha]
      apply coeff_of_notMem_CNF
      rw [CNF.of_le_one hb ho]
      simpa using ha

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

Goal state before:
pp: case pos
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
h : e' ∈ map Prod.fst (CNF b y)
⊢ (coeff b (b ^ e * x + y)) e' = (coeff b y) e'

Tactic:
mem_map

Goal state after:
case pos
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
h : ∃ a ∈ CNF b y, a.1 = e'
⊢ (coeff b (b ^ e * x + y)) e' = (coeff b y) e'
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case neg
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
h : e' ∉ map Prod.fst (CNF b y)
⊢ e' ∉ map Prod.fst (CNF b (b ^ e * x + y))

Tactic:
mem_map

Goal state after:
case neg
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
h : ¬∃ a ∈ CNF b y, a.1 = e'
⊢ ¬∃ a ∈ CNF b (b ^ e * x + y), a.1 = e'
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case inr
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
x✝ : a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a) := x✝
hne : (s ∩ Iic a).Nonempty
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a

Tactic:
refine ⟨hne, (isLUB_of_mem_closure ?_ h).csSup_eq hne⟩
      exact fun x hx => hx.2

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

Goal state before:
pp: case neg
b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
a : Ordinal.{u_1}
ha : a ∉ f.support
⊢ f a < b

Tactic:
rw [notMem_support_iff.1 ha]
        exact (hb 0).pos

Goal state after:
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
⊢ y.pair z ∈ map f x ↔ z = f y

Tactic:
mem_map

Goal state after:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
⊢ (∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z) ↔ z = f y
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: case refine_1
x : ZFSet.{u}
hx : IsOrdinal = IsOrdinal
y : ZFSet.{u}
hy : y.IsOrdinal
z : ZFSet.{u}
hz : ↑y z
⊢ z.IsOrdinal

pp: case refine_2
x : ZFSet.{u}
hx : IsOrdinal = IsOrdinal
y✝ z✝ w✝ : ZFSet.{u}
hyz : ↑z✝ y✝
hzw : ↑w✝ z✝
hwx : w✝.IsOrdinal
⊢ ↑w✝ y✝

Tactic:
exacts [hy.mem hz, hwx.mem_trans hyz hzw]

Goal state after:
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case add_one
o : Ordinal.{u}
ih : (V_ o).card = preBeth o
⊢ (V_ (o + 1)).card = preBeth (o + 1)

Tactic:
| add_one o ih =>

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

Goal state before:
pp: o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
fst_eq✝ : scale 1 a = o'
snd_eq✝ : n = m
⊢ ω ∣ o'.repr

Tactic:
subst o'

Goal state after:
o : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
snd_eq✝ : n = m
⊢ ω ∣ (scale 1 a).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
⊢ (ω ^ succ e.repr) ^ b ≤ (ω ^ e.repr) ^ ω

Tactic:
← opow_mul,

Goal state after:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
⊢ ω ^ (succ e.repr * b) ≤ (ω ^ e.repr) ^ ω
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g b : ℝ → ℝ
exp : ℝ
h_eq : g =ᶠ[atTop] f
h : Majorized f b exp
⊢ Majorized g b exp

Tactic:
by
  simp only [Majorized] at *
  intro exp' h_exp
  exact EventuallyEq.trans_isLittleO h_eq (h exp' h_exp)

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

Goal state before:
pp: b : ℝ → ℝ
h_tendsto : Tendsto b atTop atTop
c : ℝ
⊢ Majorized (fun x ↦ c) b 0

Tactic:
intro exp h_exp
  apply Asymptotics.isLittleO_const_left.mpr
  right
  apply tendsto_norm_atTop_atTop.comp
  exact (tendsto_rpow_atTop h_exp).comp h_tendsto

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

Goal state before:
pp: case succ.refine_1.a
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0✝ : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := ⋯
R : Ordinal.{0} := ⋯
ω0 : Ordinal.{0} := ⋯
α' : Ordinal.{0} := ⋯
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
x✝ : k + 1 ≠ 0
e0 : 0 < a0.repr
rr0 : 0 < a0.repr + a0.repr
⊢ R < ω ^ (a0.repr * succ ↑k.succ)

Tactic:
exact
        lt_of_lt_of_le Rl
          (opow_le_opow_right omega0_pos <|
            mul_le_mul_right (succ_le_succ_iff.2 (Nat.cast_le.2 (le_of_lt k.lt_succ_self))) _)

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

Goal state before:
pp: α : Type u_1
op op' : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
h' : FriendlyOperation op'
⊢ FriendlyOperation (op ∘ op')

Tactic:
rw [FriendlyOperation] at h h' ⊢

Goal state after:
α : Type u_1
op op' : Stream'.Seq α → Stream'.Seq α
h : LipschitzWith 1 op
h' : LipschitzWith 1 op'
⊢ LipschitzWith 1 (op ∘ op')
Module: Mathlib.Tactic.ModCases

Goal state before:
pp: p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ 0 ≤ (a % ↑n).toNat ∧ (a % ↑n).toNat < n ∧ a ≡ ↑(a % ↑n).toNat [ZMOD ↑n]

Tactic:
have := natCast_pos.2 <| Nat.le_of_ble_eq_true hn

Goal state after:
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
⊢ 0 ≤ (a % ↑n).toNat ∧ (a % ↑n).toNat < n ∧ a ≡ ↑(a % ↑n).toNat [ZMOD ↑n]
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
hS : S.Equicontinuous
ind : IsInducing (⇑UniformFun.ofFun ∘ Subtype.val)
f_mem : f ∈ S
h𝒢ℱ : map Subtype.val 𝒢 = map F ℱ
⊢ Tendsto id 𝒢 (𝓝 ⟨f, f_mem⟩)

Tactic:
rwa [tendsto_id', nhds_induced, ← map_le_iff_le_comap, h𝒢ℱ]

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
⊢ (∀ (a : ↑G), (ConcreteCategory.hom (eta G)) a = 1 → a = 1) ↔ Group.ResiduallyFinite ↑G

Tactic:
Group.residuallyFinite_iff_forall_finiteIndexNormalSubgroup

Goal state after:
G : GrpCat
⊢ (∀ (a : ↑G), (ConcreteCategory.hom (eta G)) a = 1 → a = 1) ↔
    ∀ (g : ↑G), (∀ (H : FiniteIndexNormalSubgroup ↑G), g ∈ H) → g = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x : M
ab : M × M
⊢ ab ∈ mulFiber x ↔ ab.1 * ab.2 = x

Tactic:
by simp [mulFiber]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
⊢ (1, 1) ∈ mulFiber 1

Tactic:
by simp [mulFiber]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsInducing (V.domRestrict ⇑f)
this✝ : IsTopologicalAddGroup E
this : ContinuousSMul 𝕜₁ E
⊢ TopologicalSpace.induced Subtype.val inst✝⁶ = TopologicalSpace.induced (V.domRestrict ⇑f) inst✝⁵

Tactic:
← H.eq_induced,

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsInducing (V.domRestrict ⇑f)
this✝ : IsTopologicalAddGroup E
this : ContinuousSMul 𝕜₁ E
⊢ TopologicalSpace.induced Subtype.val inst✝⁶ = instTopologicalSpaceSubtype
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Preperfect s ↔ ∀ (a : Ordinal.{u}), sᵈ[a] = s

Tactic:
preperfect_iff_eq_relDerivedSet,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s = relDerivedSet s ↔ ∀ (a : Ordinal.{u}), sᵈ[a] = s
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : Finite C
x✝ : ∀ (n : ℕ), _root_.Finite (cell C n)
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → IsEmpty (cell C b)
m : ℕ
j : cell C m
⊢ m < n

Tactic:
by_contra h

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : Finite C
x✝ : ∀ (n : ℕ), _root_.Finite (cell C n)
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → IsEmpty (cell C b)
m : ℕ
j : cell C m
h : ¬m < n
⊢ False
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
Q : Set X.A
hQ : Q ∈ F
q : X.A
hq1 : q ∈ Q
P : Ultrafilter X.A
hq2 : P ∈ basic A
hq3 : X.str P = q
⊢ P ∈ X.str ⁻¹' Q

Tactic:
← hq3

Goal state after:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
Q : Set X.A
hQ : Q ∈ F
q : X.A
P : Ultrafilter X.A
hq1 : X.str P ∈ Q
hq2 : P ∈ basic A
hq3 : X.str P = q
⊢ P ∈ X.str ⁻¹' Q
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
f : ↑(π C fun x ↦ x ∈ s) → ↥s → Bool := fun x j ↦ ↑x ↑j
x : I → Bool
hx : x ∈ C
y : I → Bool
hy : y ∈ C
h : f ⟨Proj (fun x ↦ x ∈ s) x, ⋯⟩ = f ⟨Proj (fun x ↦ x ∈ s) y, ⋯⟩
i : I
hi : i ∉ s
⊢ ↑⟨Proj (fun x ↦ x ∈ s) x, ⋯⟩ i = ↑⟨Proj (fun x ↦ x ∈ s) y, ⋯⟩ i

Tactic:
simp only [Proj, if_neg hi]

Goal state after:
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
⊢ Proj J ∘ Proj K = Proj J

Tactic:
by
  ext x i; dsimp [Proj]; simp_all

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
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 : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
⊢ List.IsChain (fun x1 x2 ↦ x1 > x2) as

Tactic:
rw [List.isChain_cons] at ha

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: case neg
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
i : I
hi : ¬J i
c : I → Bool
hc : c ∈ C
d : I → Bool
hd : d ∈ C
h : ↑((iso_map C J) ⟨Proj J c, ⋯⟩) = ↑((iso_map C J) ⟨Proj J d, ⋯⟩)
⊢ ↑⟨Proj J c, ⋯⟩ i = ↑⟨Proj J d, ⋯⟩ i

Tactic:
simp only [Proj, if_neg hi]

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case pos
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : ∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : ⋂ n, ⋂ m, ⋂ (_ : m ≤ n), C m = ∅
n : ℕ
g : (dissipate C n).Nonempty
⊢ dissipate C n ∈ S ∨ dissipate C n = ∅

Tactic:
simpa [or_comm] using hpi.insert_empty.dissipate_mem h1 n g

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
⊢ IsCompactSystem {s | IsCompact s ∧ IsClosed s}

Tactic:
refine IsCompactSystem.of_nonempty_iInter fun C hC_cc h_nonempty ↦ ?_
  rw [← iInter_dissipate]
  refine IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed (Set.dissipate C)
    (fun n ↦ ?_) h_nonempty ?_ (fun n ↦ isClosed_biInter (fun i _ ↦ (hC_cc i).2))
  · exact Set.antitone_dissipate (by lia)
  · simpa using (hC_cc 0).1

Goal state after:
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
⊢ ENat.card (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard

Tactic:
suffices h : ∀ {n : ℕ} (U : Fin n → Set X) (hU₁ : ∀ i, IsClopen (U i)) (hU₂ : ∀ i, (U i).Nonempty)
      (hU₃ : Pairwise (Disjoint on U)) (hU₄ : ⋃ i, U i = Set.univ),
      n ≤ (f ⁻¹' {y}).encard by
    obtain (hy | hy) := finite_or_infinite (ConnectedComponents X)
    · cases nonempty_fintype (ConnectedComponents X)
      simp only [ENat.card_eq_coe_fintype_card]
      refine h (fun i ↦ ConnectedComponents.mk ⁻¹' {(Fintype.equivFin _).symm i}) (fun i ↦ ?_)
          (fun i ↦ ?_) (fun i j hij ↦ Disjoint.preimage _ (by simp [hij])) ?_
      · exact (isClopen_discrete _).preimage continuous_coe
      · exact (Set.singleton_nonempty _).preimage surjective_coe
      · simp [← Set.preimage_iUnion]
    · simp only [ENat.card_eq_top_of_infinite, top_le_iff, ENat.eq_top_iff_forall_ge]
      intro m
      obtain ⟨U, hU1, hU2, hU3, hU4⟩ := exists_fun_isClopen_of_infinite X (m + 1) (by simp)
      exact le_trans (by simp) (h U hU1 hU2 hU3 hU4)
  intro n U hU1 hU2 hU3 hU4
  have heq : f ⁻¹' {y} = ⋃ i, (U i ∩ f ⁻¹' {y}) := by
    conv_lhs => rw [← Set.univ_inter (f ⁻¹' {y}), ← hU4, Set.iUnion_inter]
  rw [heq, Set.encard_iUnion_of_finite fun i j hij ↦ .inter_left _ (.inter_right _ <| hU3 hij)]
  trans ∑ i : Fin n, 1
  · simp
  · rw [finsum_eq_sum_of_fintype]
    refine Fintype.sum_mono fun i ↦ Set.one_le_encard_iff_nonempty.mpr (show y ∈ f '' (U i) from ?_)
    convert! Set.mem_univ y
    exact IsClopen.eq_univ ⟨hf₂ _ (hU1 i).1, hf₁ _ (hU1 i).2⟩ ((hU2 i).image f)

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: case pos
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
h : α → E := ⋯
⊢ ∀ (x : α), id x = b → (IccExtendCM f) x = (IccExtendCM g) x

Tactic:
rintro x rfl

Goal state after:
case pos
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a c : α
E : Type u_2
inst✝² : TopologicalSpace E
x : α
inst✝¹ : Fact (a ≤ id x)
inst✝ : Fact (id x ≤ c)
f : C(↑(Icc a (id x)), E)
g : C(↑(Icc (id x) c), E)
hb : f ⊤ = g ⊥
h : α → E := fun t ↦ if t ≤ id x then (IccExtendCM f) t else (IccExtendCM g) t
⊢ (IccExtendCM f) x = (IccExtendCM g) x
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F
A : Set E
f : E → F
hf : IsInducing f
⊢ IsCountablyCompact A ↔ IsCountablyCompact (f '' A)

Tactic:
refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot Fc F_le => ?_⟩
  obtain ⟨_, ⟨x, x_in : x ∈ A, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
    hs ((map_mono F_le).trans_eq map_principal)
  exact ⟨x, x_in, hf.mapClusterPt_iff.1 hx⟩

Goal state after:
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
L : X → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
⊢ ∀ ⦃x : X⦄, x ∈ ↑s → MapsTo (⇑f) (L x) (⋃₀ t)

Tactic:
exact fun x hx ↦ hLt x <| hsK x hx

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ (⨅ i, f i).lift' (Iic ∘ 𝓟) = ⨅ i, (f i).lift' (Iic ∘ 𝓟)

Tactic:
apply lift'_iInf_of_map_univ

Goal state after:
case hg
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ ∀ {s t : Set α}, (Iic ∘ 𝓟) (s ∩ t) = (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t

case hg'
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ (Iic ∘ 𝓟) univ = univ
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
⊢ some '' Metric.eball a r = Metric.eball (some a) r

Tactic:
ext x
  constructor <;> intro h
  · obtain ⟨y, yh, yx⟩ := h
    rw [← yx]
    simpa
  match x with
  | none => simp at h
  | (y : α) =>
    exact ⟨y, h, rfl⟩

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

Goal state before:
pp: θ : ↑I
⊢ 1 * (1 + ↑(1, θ).2) ≤ 2 * ↑(1, θ).1

Tactic:
dsimp only
      rw [coe_one, one_mul, mul_one, add_comm, ← one_add_one_eq_two]
      simp only [add_le_add_iff_right]
      exact le_one _

Goal state after: