mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha : ¬IsSuccLimit a
⊢ IsOpen[inst✝³] {a}

Tactic:
· obtain (ha | ha) := not_isSuccLimit_iff.mp ha
    · convert! isOpen_Iio (a := Order.succ a) using 1
      simp [ha.Iic_eq]
    · exact isOpen_singleton_of_not_isSuccPrelimit ha

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

Goal state before:
pp: case refine_2.refine_2
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
⊢ Set.range (enumOrd s) = s

Tactic:
range_enumOrd hs

Goal state after:
case refine_2.refine_2
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
⊢ s = s
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x y : ZFSet.{u}
h : x ≠ y
⊢ 2 = 1 + 1

Tactic:
one_add_one_eq_two

Goal state after:
x y : ZFSet.{u}
h : x ≠ y
⊢ 2 = 2
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: α : Type u
inst✝ : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{max u (v + 1), max u v} (lift.{u, v} (range f).card) ≤ lift.{max v u (v + 1), u} #α

Tactic:
lift_umax.{u, v + 1}

Goal state after:
α : Type u
inst✝ : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{max u (v + 1), max u v} (lift.{u, v} (range f).card) ≤ lift.{v + 1, u} #α
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
⊢ (mk α✝¹ A✝¹).rank = (mk α✝ A✝).rank

Tactic:
apply congr_arg sSup

Goal state after:
α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
⊢ (Set.range fun a ↦ succ (A✝¹ a).rank) = Set.range fun a ↦ succ (A✝ a).rank
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case a.inr
o a : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
⊢ ω ^ veblen o a ∈ range (veblen o)

Tactic:
· rw [← veblen_zero_apply, veblen_veblen_of_lt ho]
      simp

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

Goal state before:
pp: a x : Ordinal.{u}
⊢ veblen x.invVeblen₁ x.invVeblen₂ = veblen x.invVeblen₁ a ↔ ω ^ x = veblen x.invVeblen₁ a

Tactic:
veblen_invVeblen₁_invVeblen₂

Goal state after:
a x : Ordinal.{u}
⊢ ω ^ x = veblen x.invVeblen₁ a ↔ ω ^ x = veblen x.invVeblen₁ a
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx : y = x ∨ {x, y} = {x, y'}
hy : {x, y} = {x, y'}
⊢ y = x ∨ y = y'

Tactic:
simpa using ZFSet.ext_iff.1 hy y

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

Goal state before:
pp: a x : Ordinal.{u}
⊢ veblen x.invVeblen₁ x.invVeblen₂ < veblen x.invVeblen₁ a ↔ ω ^ x < veblen x.invVeblen₁ a

Tactic:
veblen_invVeblen₁_invVeblen₂

Goal state after:
a x : Ordinal.{u}
⊢ ω ^ x < veblen x.invVeblen₁ a ↔ ω ^ x < veblen x.invVeblen₁ a
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: a x : Ordinal.{u}
⊢ veblen x.invVeblen₁ x.invVeblen₂ ≤ veblen x.invVeblen₁ a ↔ ω ^ x ≤ veblen x.invVeblen₁ a

Tactic:
veblen_invVeblen₁_invVeblen₂

Goal state after:
a x : Ordinal.{u}
⊢ ω ^ x ≤ veblen x.invVeblen₁ a ↔ ω ^ x ≤ veblen x.invVeblen₁ a
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: a x : Ordinal.{u}
⊢ veblen x.invVeblen₁ a < veblen x.invVeblen₁ x.invVeblen₂ ↔ veblen x.invVeblen₁ a < ω ^ x

Tactic:
veblen_invVeblen₁_invVeblen₂

Goal state after:
a x : Ordinal.{u}
⊢ veblen x.invVeblen₁ a < ω ^ x ↔ veblen x.invVeblen₁ a < ω ^ x
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: a x : Ordinal.{u}
⊢ veblen x.invVeblen₁ a ≤ veblen x.invVeblen₁ x.invVeblen₂ ↔ veblen x.invVeblen₁ a ≤ ω ^ x

Tactic:
veblen_invVeblen₁_invVeblen₂

Goal state after:
a x : Ordinal.{u}
⊢ veblen x.invVeblen₁ a ≤ ω ^ x ↔ veblen x.invVeblen₁ a ≤ ω ^ x
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
en : ¬n₁ = n₂
⊢ NFBelow 0 b

Tactic:
· exact NFBelow.zero

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ deriv (fun a ↦ ω ^ a) (succ o) = nfp (fun a ↦ ω ^ a) (succ (deriv (fun a ↦ ω ^ a) o))

Tactic:
deriv_succ

Goal state after:
o : Ordinal.{u_1}
⊢ nfp (fun a ↦ ω ^ a) (succ (deriv (fun a ↦ ω ^ a) o)) = nfp (fun a ↦ ω ^ a) (succ (deriv (fun a ↦ ω ^ a) o))
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ⊆ y ∨ y ⊆ x

Tactic:
obtain h | h := mem_or_subset hx hy

Goal state after:
case inl
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x ∈ y
⊢ x ⊆ y ∨ y ⊆ x

case inr
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : y ⊆ x
⊢ x ⊆ y ∨ y ⊆ x
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg.a
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
this✝ : e₁.NF
this : e₂.NF
⊢ (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁ + e₂).repr

pp: case neg.a
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
this✝ : e₁.NF
this : e₂.NF
⊢ (e₁ + e₂).repr < e₁.repr + b₂

Tactic:
· rwa [repr_add]

Goal state after:
case neg.a
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
this✝ : e₁.NF
this : e₂.NF
⊢ (e₁ + e₂).repr < e₁.repr + b₂
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.toPSet.rank = o

Tactic:
by
  rw [toPSet, PSet.rank]
  conv_rhs => rw [← _root_.iSup_succ o]
  convert! ToType.mk.symm.iSup_comp (g := fun x ↦ Order.succ x.1.toPSet.rank)
  rw [rank_toPSet]

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

Goal state before:
pp: case refine_2
o a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
b : Ordinal.{u_1}
hb : b < a
hy : b.toZFSet ∈ a.toZFSet
c : Ordinal.{u_1}
hc : c < b
hz : c.toZFSet ∈ b.toZFSet
⊢ c.toZFSet ∈ a.toZFSet

Tactic:
exact toZFSet_mem_toZFSet_iff.2 (hc.trans hb)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s : R
b : ℕ
h : r ^ b = s
⊢ (algebraMap R A) r ^ b = (algebraMap R A) s

Tactic:
by
  rw [← map_pow, h]

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

Goal state before:
pp: ⊢ WellFormedBasis []

Tactic:
simp [WellFormedBasis]

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

Goal state before:
pp: case hb
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ 0 < exp

Tactic:
exact h_exp

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

Goal state before:
pp: case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
h_length : [].length = List.length basis_tl
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ Majorized (toFun [] basis_tl) basis_hd 0

Tactic:
simp only [toFun_nil]
    exact Majorized.const (h_basis.tendsto_atTop (by simp))

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

Goal state before:
pp: coef exp : ℝ
m : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
x : ℝ
⊢ coef * (basis_hd x ^ exp * m.toFun basis_tl x) = basis_hd x ^ exp * (coef * m.toFun basis_tl x)

Tactic:
ring

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

Goal state before:
pp: t1 t2 : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length t1.unit = List.length t2.unit
t : ℝ
⊢ t1.coef * t2.coef * (t1.unit.toFun basis t * t2.unit.toFun basis t) =
    t2.coef * (t1.coef * (t1.unit.toFun basis t * t2.unit.toFun basis t))

Tactic:
ring

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

Goal state before:
pp: t : Monomial
basis : Basis
c x : ℝ
⊢ c * t.coef * t.unit.toFun basis x = c * (t.coef * t.unit.toFun basis x)

Tactic:
ring

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

Goal state before:
pp: t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
x : ℝ
⊢ t.coef⁻¹ * (t.unit.toFun basis x)⁻¹ = (t.unit.toFun basis x)⁻¹ * t.coef⁻¹

Tactic:
ring

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
s t : Stream'.Seq α
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
base : motive s t
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
this : ∀ (n : ℕ), dist s t ≤ 2⁻¹ ^ n
⊢ dist s t = 0

Tactic:
apply eq_of_le_of_ge

Goal state after:
case a
α : Type u_1
γ : Type u_3
s t : Stream'.Seq α
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
base : motive s t
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
this : ∀ (n : ℕ), dist s t ≤ 2⁻¹ ^ n
⊢ dist s t ≤ 0

case a
α : Type u_1
γ : Type u_3
s t : Stream'.Seq α
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
base : motive s t
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
this : ∀ (n : ℕ), dist s t ≤ 2⁻¹ ^ n
⊢ 0 ≤ dist s t
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: f basis_hd✝ : ℝ → ℝ
basis_tl✝ : Basis
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ ∀ {x y z : MultiseriesExpansion (basis_hd :: basis_tl)},
    x.seq = y.seq ∧ x.toFun =ᶠ[atTop] y.toFun →
      y.seq = z.seq ∧ y.toFun =ᶠ[atTop] z.toFun → x.seq = z.seq ∧ x.toFun =ᶠ[atTop] z.toFun

Tactic:
by grind [EventuallyEq.trans]

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
x : ℚ
hx : ↑x = ↑q ^ (↑a / ↑b)
⊢ ↑q ^ a = (↑q ^ (↑a / ↑b)) ^ b

Tactic:
← Real.rpow_mul_natCast (by simpa),

Goal state after:
q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
x : ℚ
hx : ↑x = ↑q ^ (↑a / ↑b)
⊢ ↑q ^ a = ↑q ^ (↑a / ↑b * ↑b)
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: e' r : ℤ
α : Type u_1
inst✝ : Ring α
n n' : ℕ
inst : CharP α n
e : α
he : IsInt e e'
hn : IsNat n n'
h₂ : IsInt (e' % ↑n') r
⊢ ↑e' = ↑r

Tactic:
CharP.intCast_eq_intCast_mod α n,

Goal state after:
e' r : ℤ
α : Type u_1
inst✝ : Ring α
n n' : ℕ
inst : CharP α n
e : α
he : IsInt e e'
hn : IsNat n n'
h₂ : IsInt (e' % ↑n') r
⊢ ↑(e' % ↑n) = ↑r
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
h : Equicontinuous fun x ↦ ⇑↑x
hS4 : S4 = DFunLike.coe '' S1
⊢ Equicontinuous fun x ↦ ⇑↑x

Tactic:
equicontinuous_iff_range,

Goal state after:
X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
h : Equicontinuous Subtype.val
hS4 : S4 = DFunLike.coe '' S1
⊢ Equicontinuous Subtype.val
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : ContinuousMul G
H K : OpenNormalSubgroup G
h : H.toFiniteIndexNormalSubgroup = K.toFiniteIndexNormalSubgroup
⊢ (fun H ↦ ↑H.toOpenSubgroup) H = (fun H ↦ ↑H.toOpenSubgroup) K

Tactic:
exact congrArg (fun L : FiniteIndexNormalSubgroup G ↦ (L : Subgroup G)) h

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
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : F →ₗ[S] E →ₗ[S] F
f : M → F
e : E
hL : ∀ (y : F), (L y) e = y
⊢ (f ⋆[L] {1}.indicator fun x ↦ e) = f

Tactic:
by
  classical
  ext x; simp only [convolution, Set.indicator_apply]
  rw [tsum_eq_single (⟨(x, 1), by grind⟩ : mulFiber x) (by grind [LinearMap.zero_apply])]
  simp [hL]

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 : IsEmbedding (V.domRestrict ⇑f)
f_injOn : InjOn (⇑f) V
x : E
hx : x ∈ f.ker
c : 𝕜₁
hc : c • x ∈ V
c_ne : c ≠ 0
⊢ σ c • 0 = 0

Tactic:
smul_zero

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 : IsEmbedding (V.domRestrict ⇑f)
f_injOn : InjOn (⇑f) V
x : E
hx : x ∈ f.ker
c : 𝕜₁
hc : c • x ∈ V
c_ne : c ≠ 0
⊢ 0 = 0
Module: Mathlib.Topology.Convenient.Category

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y Z : ContinuousGeneratedByCat X
g : (toTopCat X).obj Y ⟶ (toTopCat X).obj Z
⊢ ContinuousGeneratedBy X (⇑WithGeneratedByTopology.equiv ∘ ⇑(TopCat.Hom.hom g) ∘ ⇑WithGeneratedByTopology.equiv.symm)

Tactic:
rw [continuousGeneratedBy_iff]
      exact g.hom.continuous

Goal state after:
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
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
claim6 : ∀ P ∈ C2, P.Nonempty
T : fsu
hT : ι T ⊆ C1
this : ⋂₀ ι T ∈ C2
⊢ (⋂₀ ι T).Nonempty

Tactic:
by exact claim6 _ 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✝ : RelCWComplex C D
I J : (n : ℕ) → Set (cell C n)
hIJ : D ∪ ⋃ n, ⋃ j, openCell n ↑j = D ∪ ⋃ n, ⋃ j, openCell n ↑j
n : ℕ
i : cell C n
hi : i ∈ I n
⊢ i ∈ J n

Tactic:
by_contra hJ

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 : ℕ
i : cell C n
hi : i ∈ I n
hJ : i ∉ J n
⊢ False
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)

pp: case right
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ IsClosed[t] (C ∩ D)

Tactic:
· intros
    rw [inter_eq_right.2 (closedCell_subset_complex _ _)]
    exact isClosed_closedCell

Goal state after:
case right
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ IsClosed[t] (C ∩ D)
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
⊢ (factors C s x).prod ∈ ↑(Submodule.span ℤ (Set.range (Products.eval (π C fun x ↦ x ∈ s))))

Tactic:
dsimp [factors]

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
⊢ (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)
        (s.sort fun x1 x2 ↦ x1 ≥ x2)).prod ∈
    ↑(Submodule.span ℤ (Set.range (Products.eval (π C fun x ↦ x ∈ s))))
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ord I i = o
⊢ true = g i

Tactic:
rw [ord_term ho] at h

Goal state after:
case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : term I ho = i
⊢ true = g i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case hf
S : Profinite
a b : ↑S.toTop
h : ι S a = ι S b
hn : ¬a = b
⊢ False

Tactic:
obtain ⟨C, hC, hh⟩ := exists_isClopen_of_totally_separated hn

Goal state after:
case hf
S : Profinite
a b : ↑S.toTop
h : ι S a = ι S b
hn : ¬a = b
C : Set ↑S.toTop
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ False
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✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h : ∀ (y : Y), (f ⁻¹' {y}).Finite
⊢ Finite (ConnectedComponents X)

Tactic:
suffices h : ∀ (y : ConnectedComponents Y), Finite (ConnectedComponents (f ⁻¹' mk ⁻¹' {y})) by
    refine .of_equiv _ (equivOfIsClopen (U := fun y ↦ f ⁻¹' mk ⁻¹' {y}) ?_ ?_ ?_).symm
    · exact fun y ↦ (isClopen_discrete {y}).preimage (continuous_coe.comp hfc)
    · exact fun i j hij ↦ (Disjoint.preimage mk (by simpa)).preimage f
    · rw [Set.iUnion_eq_univ_iff]
      exact fun x ↦ ⟨mk (f x), rfl⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h : ∀ (y : Y), (f ⁻¹' {y}).Finite
⊢ ∀ (y : ConnectedComponents Y), Finite (ConnectedComponents ↑(f ⁻¹' mk ⁻¹' {y}))
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
h : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ⊆ ⋃ i, U i → ∃ t, A ⊆ ⋃ i ∈ t, U i
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A
V : ℕ → Set E := fun n ↦ (closure[inst✝] (x '' Ici n))ᶜ
hVmono : Monotone V
hac : ∀ a ∈ A, ∃ x_1, a ∉ closure[inst✝] (x '' Ici x_1)
hAV : A ⊆ ⋃ n, V n
t : Finset ℕ
ht : A ⊆ ⋃ i ∈ t, V i
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → x b ∈ A
m : ℕ := max N (t.sup id)
j : ℕ
hjt : j ∈ t
hjV : x m ∈ V j
hxmV : x m ∈ V m
⊢ False

Tactic:
exact hxmV (subset_closure ⟨m, mem_Ici.mpr le_rfl, rfl⟩)

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

Goal state before:
pp: E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Infinite
⊢ (range x ∩ A).Infinite

Tactic:
by
        rw [eventually_iff, mem_cofinite, compl_ofPred] at hx
        exact hfin.inter_of_finite_sdiff (hx.image x |>.subset (by grind))

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : (productOfMemOpens X) x1 = (productOfMemOpens X) x2
⊢ Inseparable x1 x2

Tactic:
rw [← IsInducing.inseparable_iff (productOfMemOpens_isInducing X), h]

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

Goal state before:
pp: H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
⊢ False

Tactic:
obtain ⟨n, hn⟩ : ∃ n : ℕ, x n ∉ insert (0 : ℚ) (range x) :=
    (hxc.eventually hx0.isCompact_insert_range.compl_mem_cocompact).exists

Goal state after:
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
n : ℕ
hn : x n ∉ insert 0 (range x)
⊢ False
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case succ
x : ℝ
n : ℕ
ih : (cantorSequence x).get n = (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n
⊢ 3 *
      ((x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n -
        3 ^ n * ofDigitsTerm (cantorToTernary x).get n) =
    (x - (∑ x_1 ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get x_1 + ofDigitsTerm (cantorToTernary x).get n)) *
      3 ^ (n + 1)

Tactic:
ring

Goal state after:
Module: Mathlib.Topology.Maps.Proper.UniversallyClosed

Goal state before:
pp: case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰) (nhds (f x))
hx : ∀ t ∈ nhds (x, 𝒰.1), (t ∩ {xℱ | xℱ.2 = pure xℱ.1}).Nonempty
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ 𝒰
⊢ False

Tactic:
rcases hx (U ×ˢ {𝒢 | Uᶜ ∈ 𝒢}) (prod_mem_nhds hU (isOpen_setOfPred_mem.mem_nhds hUc)) with
      ⟨⟨z, 𝒢⟩, ⟨⟨hz : z ∈ U, hz' : Uᶜ ∈ 𝒢⟩, rfl : 𝒢 = pure z⟩⟩

Goal state after:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰) (nhds (f x))
hx : ∀ t ∈ nhds (x, 𝒰.1), (t ∩ {xℱ | xℱ.2 = pure xℱ.1}).Nonempty
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ 𝒰
z : X
hz : z ∈ U
hz' : Uᶜ ∈ pure z
⊢ False