mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
isf : IsField R
⊢ IsRegularLocalRing R

pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
isf : ¬IsField R
⊢ IsRegularLocalRing R

Tactic:
· let := isf.toField
    simp [isRegularLocalRing_iff, maximalIdeal_eq_bot]

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
isf : ¬IsField R
⊢ IsRegularLocalRing R
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
⊢ projectiveDimension (of R (QuotSMulTop x ↑M)) = projectiveDimension M + 1

Tactic:
have sub : Subsingleton M ↔ Subsingleton (QuotSMulTop x M) := by
    refine ⟨fun h ↦ inferInstance, fun h ↦ ?_⟩
    contrapose! h
    exact (nontrivial_quotSMulTop_of_mem_maximalIdeal M mem)

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
⊢ projectiveDimension (of R (QuotSMulTop x ↑M)) = projectiveDimension M + 1
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝³ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝² : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this✝¹ : pS.IsPrime
this✝ : IsLocalization.AtPrime (Localization.AtPrime pS) p
this : IsRegularLocalRing (Localization.AtPrime q)
⊢ comap C pS = maximalIdeal (Localization.AtPrime q)

Tactic:
rw [← IsLocalization.map_under q.primeCompl _ (comap C pS),
      ← IsLocalization.map_under q.primeCompl _ (maximalIdeal (Localization.AtPrime q))]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝³ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝² : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this✝¹ : pS.IsPrime
this✝ : IsLocalization.AtPrime (Localization.AtPrime pS) p
this : IsRegularLocalRing (Localization.AtPrime q)
⊢ Ideal.map (algebraMap R (Localization.AtPrime q)) (under R (comap C pS)) =
    Ideal.map (algebraMap R (Localization.AtPrime q)) (under R (maximalIdeal (Localization.AtPrime q)))
Module: Mathlib.RingTheory.Valuation.Extension

Goal state before:
pp: A : Type u_2
inst✝⁴ : Ring A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst✝¹ : LinearOrderedCommGroupWithZero ΓK
inst✝ : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
h : Subring.comap (algebraMap K A) vA.integer = vK.integer
x : K
⊢ vK x ≤ 1 ↔ (comap (algebraMap K A) vA) x ≤ 1

Tactic:
← Valuation.mem_integer_iff,

Goal state after:
A : Type u_2
inst✝⁴ : Ring A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst✝¹ : LinearOrderedCommGroupWithZero ΓK
inst✝ : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
h : Subring.comap (algebraMap K A) vA.integer = vK.integer
x : K
⊢ x ∈ vK.integer ↔ x ∈ (comap (algebraMap K A) vA).integer
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (zmodEquivTrunc p n).symm.toRingHom.comp ((zmodEquivTrunc p n).toRingHom.comp (PadicInt.toZModPow n)) =
    PadicInt.toZModPow n

Tactic:
← RingHom.comp_assoc

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((zmodEquivTrunc p n).symm.toRingHom.comp (zmodEquivTrunc p n).toRingHom).comp (PadicInt.toZModPow n) =
    PadicInt.toZModPow n
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ (succNthDefiningPoly p n a₁ a₂ bs).degree ≠ 0

Tactic:
by
    simp only [succNthDefiningPoly_degree p n a₁ a₂ bs ha₁ ha₂, ne_eq, Nat.cast_eq_zero,
      hp.out.ne_zero, not_false_eq_true]

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

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o) = o

Tactic:
refine CNF.rec b ?_ ?_ o
  · rw [zero_right, foldr_nil]
  · intro o ho IH
    rw [CNF.ne_zero ho, foldr_cons, IH, div_add_mod]

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
hab : a ≤ b
hf : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ lfpApprox f x b = lfpApprox f x a

Tactic:
rw [mem_fixedPoints_iff] at hf

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
hab : a ≤ b
hf : f (lfpApprox f x a) = lfpApprox f x a
⊢ lfpApprox f x b = lfpApprox f x a
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
⊢ f e = 0

Tactic:
← notMem_support_iff

Goal state after:
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
⊢ e ∉ f.support
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: n : ℕ
⊢ (↑n).repr = ↑n

Tactic:
cases n <;> simp

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

Goal state before:
pp: x✝ y z x : ZFSet.{u}
a : PSet.{u}
f : a.Type → ↥(mk a) := fun i ↦ ⟨mk (a.Func i), ⋯⟩
⊢ Small.{u, u + 1} ↥(⟦a⟧)

Tactic:
suffices Function.Surjective f by exact small_of_surjective this

Goal state after:
x✝ y z x : ZFSet.{u}
a : PSet.{u}
f : a.Type → ↥(mk a) := fun i ↦ ⟨mk (a.Func i), ⋯⟩
⊢ Function.Surjective f
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: case mk
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
hb : (A a).Equiv (B b)
γ : Type u
Γ : γ → PSet.{u}
A_ih✝ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
x✝ : PSet.{u}
eb : B b = x✝
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)

Tactic:
induction eb : B b with

Goal state after:
case mk.mk
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
hb : (A a).Equiv (B b)
γ : Type u
Γ : γ → PSet.{u}
A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u}
⊢ ¬(o = 0 ∨ o ∈ range Γ_ ) ↔ o ≠ 0 ∧ o ∉ range Γ_

Tactic:
not_or

Goal state after:
o : Ordinal.{u}
⊢ ¬o = 0 ∧ o ∉ range Γ_ ↔ o ≠ 0 ∧ o ∉ range Γ_
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
| (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr

Tactic:
lhs
      simp [(· * ·)]

Goal state after:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
| (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: A : Type u_2
sA : CommSemiring A
a₁ a₂ b₁ b₂ : A
ha : a₁ = b₁
hb : a₂ = b₂
⊢ a₁ + a₂ = b₁ + b₂

Tactic:
by
  subst_vars
  rfl

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: A : Type u_2
e₁ e₂ a b : A
ha : e₁ = a
hb : e₂ = b
hab : a = b
⊢ e₁ = e₂

Tactic:
by
  subst_vars
  rfl

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

Goal state before:
pp: case succ.refine_2
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} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
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)
⊢ (ω ^ a0.repr) ^ ↑(k + 1) * (ω ^ a0.repr * ↑↑n + a'.repr) + R' = (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ succ ↑(k + 1)

Tactic:
calc
    (ω0 ^ (k.succ : Ordinal)) * α' + R'
    _ = (ω0 ^ succ (k : Ordinal)) * α' + ((ω0 ^ (k : Ordinal)) * α' * m + R) := by
        rw [Nat.cast_add_one, RR, ← mul_assoc, succ_eq_add_one]
    _ = ((ω0 ^ (k : Ordinal)) * α' + R) * α' + ((ω0 ^ (k : Ordinal)) * α' + R) * m := ?_
    _ = (α' + m) ^ succ (k.succ : Ordinal) := by
        rw [← mul_add, opow_succ, Nat.cast_add_one, IH.2, succ_eq_add_one]

Goal state after:
case succ.refine_2
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} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
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)
⊢ ω0 ^ succ ↑k * α' + (ω0 ^ ↑k * α' * ↑m + R) = (ω0 ^ ↑k * α' + R) * α' + (ω0 ^ ↑k * α' + R) * ↑m
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ClusterPt s (Filter.principal {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none})
n : ℕ
⊢ s n = none → s (n + 1) = none

Tactic:
hn

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ClusterPt s (Filter.principal {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none})
n : ℕ
hn : s n = none
⊢ s (n + 1) = none
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
op : Stream'.Seq α → Stream'.Seq α
h_base : motive op
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, op') => (hd, ↑op' s.tail))
              (T s.head)
s t : Stream'.Seq α
n : ℕ
⊢ dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n

Tactic:
hn

Goal state after:
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
op : Stream'.Seq α → Stream'.Seq α
h_base : motive op
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, op') => (hd, ↑op' s.tail))
              (T s.head)
s t : Stream'.Seq α
n : ℕ
hn : dist s t ≤ 2⁻¹ ^ n
⊢ dist (op s) (op t) ≤ 2⁻¹ ^ n
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons
x exp : ℝ
exps : List ℝ
ih : ∀ {basis : Basis}, WellFormedBasis basis → (∀ f ∈ basis, 0 < f x) → 0 < toFun exps basis x
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
hx : ∀ f ∈ basis_hd :: basis_tl, 0 < f x
⊢ 0 < toFun (exp :: exps) (basis_hd :: basis_tl) x

Tactic:
simp only [toFun, List.zipWith_cons_cons, List.prod_cons]

Goal state after:
case cons.cons
x exp : ℝ
exps : List ℝ
ih : ∀ {basis : Basis}, WellFormedBasis basis → (∀ f ∈ basis, 0 < f x) → 0 < toFun exps basis x
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
hx : ∀ f ∈ basis_hd :: basis_tl, 0 < f x
⊢ 0 < basis_hd x ^ exp * (List.zipWith (fun exp b ↦ b x ^ exp) exps basis_tl).prod
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: m : UnitMonomial
left right : Basis
⊢ (List.replicate (List.length left) 0 ++ m).toFun (left ++ right) = m.toFun right

Tactic:
induction left with

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
h1 : (exp1 :: m1).length = (basis_hd :: basis_tl).length
m2 : List ℝ
h2 : (exp1 :: m2).length = (basis_hd :: basis_tl).length
h : List.Lex (fun x1 x2 ↦ x1 < x2) m1 m2
⊢ m1.length = basis_tl.length

Tactic:
simpa using h1

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

Goal state before:
pp: f basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : mk Multiseries.nil f = ms
h : ms.Approximates
⊢ f =ᶠ[atTop] 0

Tactic:
cases h <;> simp at h_ms

Goal state after:
case nil
f basis_hd : ℝ → ℝ
basis_tl : Basis
f✝ : ℝ → ℝ
hf✝ : f✝ =ᶠ[atTop] 0
h_ms : f = f✝
⊢ f =ᶠ[atTop] 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : mk (Multiseries.cons exp coef tl) f = ms
h : ms.Approximates
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates

Tactic:
cases h <;> simp at h_ms

Goal state after:
case cons
f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f✝ : ℝ → ℝ
exp✝ : ℝ
h_maj✝ : Majorized f✝ basis_hd exp✝
coef✝ : MultiseriesExpansion basis_tl
h_coef✝ : coef✝.Approximates
tl✝ : Multiseries basis_hd basis_tl
h_tl✝ : (mk tl✝ (f✝ - basis_hd ^ exp✝ * coef✝.toFun)).Approximates
h_ms : (exp = exp✝ ∧ coef = coef✝ ∧ tl = tl✝) ∧ f = f✝
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: case hU
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := ⋯
F : ℕ × ↑s → Set X := ⋯
this✝ : Nonempty X
this : Encodable ↑s
⊢ ⋃ i, F i = univ

Tactic:
apply eq_univ_iff_forall.2 (fun y ↦ ?_)
      obtain ⟨h, rfl⟩ : ∃ h, h • x = y := exists_smul_eq G x y
      obtain ⟨n, hn⟩ : ∃ n, h ∈ K n := exists_mem_compactCovering h
      obtain ⟨g, gs, hg⟩ : ∃ g ∈ s, h ∈ g • V := exists_set_mem_of_union_eq_top s _ hs _
      simp only [F, smul_singleton, mem_iUnion, mem_image, mem_inter_iff, Prod.exists,
        Subtype.exists, exists_prop]
      exact ⟨n, g, gs, h, ⟨hn, hg⟩, rfl⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := ⋯
F : ℕ × ↑s → Set X := ⋯
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, ⟨g, hg⟩))).Nonempty
I : (interior ((g • V) • {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (V • {x})
⊢ x ∈ interior ((g'⁻¹ • V) • {x})

Tactic:
rwa [smul_assoc, interior_smul, mem_inv_smul_set_iff]

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

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
inst✝⁴ : CommMonoid M
inst✝³ : CommSemiring S
inst✝² : AddCommMonoid E
inst✝¹ : Module S E
inst✝ : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL : ∀ (x y : E), (L x) y = (L y) x
x : M
⊢ ∑' (ab : ↑(mulFiber x)), (L (f (↑ab).1)) (g (↑ab).2) = ∑' (ab : ↑(mulFiber x)), (L (g (↑ab).1)) (f (↑ab).2)

Tactic:
← (mulFiber_swapEquiv x).tsum_eq

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
inst✝⁴ : CommMonoid M
inst✝³ : CommSemiring S
inst✝² : AddCommMonoid E
inst✝¹ : Module S E
inst✝ : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL : ∀ (x y : E), (L x) y = (L y) x
x : M
⊢ ∑' (c : ↑(mulFiber x)), (L (f (↑((mulFiber_swapEquiv x) c)).1)) (g (↑((mulFiber_swapEquiv x) c)).2) =
    ∑' (ab : ↑(mulFiber x)), (L (g (↑ab).1)) (f (↑ab).2)
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_7
E : Type u_8
F : Type u_9
inst✝⁷ : CommRing 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd 𝕜
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ ∀ (i : F), Continuous[TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace, inst✝⁶] fun a ↦ (-B a) i

Tactic:
neg_apply,

Goal state after:
𝕜 : Type u_7
E : Type u_8
F : Type u_9
inst✝⁷ : CommRing 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd 𝕜
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ ∀ (i : F), Continuous[TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace, inst✝⁶] fun a ↦ -(B a) i
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝² : T2Space X
inst✝¹ : RelCWComplex C D
inst✝ : FiniteDimensional C
E : Subcomplex C
n : ℕ
⊢ IsEmpty (cell C n) → IsEmpty (cell (↑E) n)

Tactic:
hn

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝² : T2Space X
inst✝¹ : RelCWComplex C D
inst✝ : FiniteDimensional C
E : Subcomplex C
n : ℕ
hn : IsEmpty (cell C n)
⊢ IsEmpty (cell (↑E) n)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
I J : (n : ℕ) → Set (cell C n)
hIJ : D ∪ ⋃ n, ⋃ j, openCell n ↑j = D ∪ ⋃ n, ⋃ j, openCell n ↑j
⊢ I = J

Tactic:
ext n x

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
I J : (n : ℕ) → Set (cell C n)
hIJ : D ∪ ⋃ n, ⋃ j, openCell n ↑j = D ∪ ⋃ n, ⋃ j, openCell n ↑j
n : ℕ
x : cell C n
⊢ x ∈ I n ↔ x ∈ J n
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case left
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n✝ : ℕ
j✝ : cell C n✝
⊢ IsClosed[t] (C ∩ closedCell n✝ j✝)

Tactic:
inter_eq_right.2 (closedCell_subset_complex _ _)

Goal state after:
case left
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n✝ : ℕ
j✝ : cell C n✝
⊢ IsClosed[t] (closedCell n✝ j✝)
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}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ C0 C ho ∪ C1 C ho = C

Tactic:
ext x
  simp only [C0, C1, Set.mem_union, Set.mem_inter_iff, Set.mem_ofPred_eq,
    ← and_or_left, and_iff_left_iff_imp, Bool.dichotomy (x (term I ho)), implies_true]

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
n : ℕ
⊢ 0 < n → ∀ (j : cell C n), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)

Tactic:
hn

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
n : ℕ
hn : 0 < n
⊢ ∀ (j : cell C n), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ ↑l
h' : ¬ord I i < o
this : eval C l = 0
⊢ eval C l ∈ Submodule.span ℤ (eval C '' {m | m < l})

Tactic:
by simp [this]

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmemcell : x ∈ openCell n j
xmemD : x ∈ interior D
this : x ∈ ↑(skeletonLT C 0) ∩ openCell n j
⊢ False

Tactic:
(disjoint_skeletonLT_openCell n.cast_nonneg').inter_eq

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmemcell : x ∈ openCell n j
xmemD : x ∈ interior D
this : x ∈ ∅
⊢ False
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n : ℕ
⊢ ∀
    (j :
      match n with
      | 0 => ↑D
      | n.succ => PEmpty.{u_1 + 1}),
    ↑(match n, j with
          | 0, i => PartialEquiv.single ![] ↑i
          | n.succ, i => PEmpty.elim i) ''
        closedBall 0 1 ⊆
      D

Tactic:
cases n <;> simp

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

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : ¬(tsupport ⇑f).Nonempty
this : f = 0
⊢ ∃ x, ‖f x‖ = ‖f‖

Tactic:
by simp [this]

Goal state after:
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
hA : IsSeqCompact A
x : ℕ → F
hx : ∀ (n : ℕ), x n ∈ f '' A
⊢ ∃ a ∈ f '' A, ∃ φ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
choose y hy using hx
    obtain ⟨a, ha, ⟨φ, hφ⟩⟩ := hA (fun n => (hy n).1)
    refine ⟨f a, mem_image_of_mem f ha, φ, hφ.1, ?_⟩
    suffices f ∘ y ∘ φ = x ∘ φ from this ▸ (hf.continuous.tendsto a).comp hφ.2
    grind

Goal state after: