mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
⊢ toFun S (g.comp f) t = (toFun S g ∘ toFun S f) t

Tactic:
obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t

Goal state after:
R : Type u
inst✝⁸ : CommSemiring R
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
⊢ toFun S (g.comp f) t = (toFun S g ∘ toFun S f) t
Module: Mathlib.RingTheory.Spectrum.Maximal.Topology

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ range toPrimeSpectrum = {x | IsClosed {x}}

Tactic:
simp only [isClosed_singleton_iff_isMaximal]
  ext ⟨x, _⟩
  exact ⟨fun ⟨y, hy⟩ => hy ▸ y.isMaximal, fun hx => ⟨⟨x, hx⟩, rfl⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Valuation.Extension

Goal state before:
pp: R : Type u_1
A : Type u_2
ΓR : Type u_3
ΓA : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : LinearOrderedCommMonoidWithZero ΓR
inst✝² : LinearOrderedCommMonoidWithZero ΓA
inst✝¹ : Algebra R A
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : vR.HasExtension vA
x y : R
⊢ vA ((algebraMap R A) x) < vA ((algebraMap R A) y) ↔ vR x < vR y

Tactic:
by
  simpa only [not_le] using ((val_map_le_iff vR vA _ _).not)

Goal state after:
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x y z : List A
hl : z.length ≤ x.length
⊢ z.length ≤ (x ++ y).length

Tactic:
simp; lia

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

Goal state before:
pp: b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → x.1 ≤ log b o

Tactic:
by
  refine CNF.rec b ?_ (fun o ho H ↦ ?_) o
  · simp
  · rw [CNF.ne_zero ho, mem_cons]
    rintro (rfl | h)
    · rfl
    · exact (H h).trans (log_mono_right _ (mod_opow_log_lt_self b ho).le)

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
this : (∀ (l₁ : Lists α), trans l₁) ×' ∀ (l : Lists' α true) (l' : Lists α), l' ∈ l.toList → trans l'
⊢ ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃

Tactic:
exact this.1

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : f x = x
o : Ordinal.{u}
⊢ lfpApprox f x 0 ∈ fixedPoints ⇑f

Tactic:
mem_fixedPoints_iff,

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : f x = x
o : Ordinal.{u}
⊢ f (lfpApprox f x 0) = lfpApprox f x 0
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

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

Tactic:
mem_fixedPoints_iff,

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
⊢ Decidable (a ∈ b.cons' l₂)

Tactic:
haveI :=
        have : sizeOf (⟨_, b⟩ : Lists α) < 1 + 1 + sizeOf b + sizeOf l₂ := by simp [sizeof_pos]
        Equiv.decidable a ⟨_, b⟩

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Decidable (a ∈ b.cons' l₂)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.inr.inr
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
⊢ (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)

Tactic:
have IHa := @cmp_compares _ _ h₁.snd h₂.snd

Goal state after:
case eq.inr.inr
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
IHa : (a₁.cmp a₂).Compares a₁ a₂
⊢ (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case mpr.inl
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a b : Ordinal.{u}
ha : veblenWith f b a = a
hb : b < b + 1
⊢ a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb⟩)

pp: case mpr.inr
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
ha : veblenWith f o a = a
b : Ordinal.{u}
hb✝ : b < o + 1
hb : b < o
⊢ a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb✝⟩)

Tactic:
· rw [Function.mem_fixedPoints_iff, ha]

Goal state after:
case mpr.inr
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
ha : veblenWith f o a = a
b : Ordinal.{u}
hb✝ : b < o + 1
hb : b < o
⊢ a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb✝⟩)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.eq
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝¹ : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
he : e.cmp e' = Ordering.eq
ee : e = e'
⊢ ω ^ e'.repr * (↑↑n + ↑↑n') + a'.repr = ω ^ e'.repr * ↑↑n + ω ^ e'.repr * ↑↑n' + a'.repr

Tactic:
← mul_add

Goal state after:
case oadd.eq
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝¹ : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
he : e.cmp e' = Ordering.eq
ee : e = e'
⊢ ω ^ e'.repr * (↑↑n + ↑↑n') + a'.repr = ω ^ e'.repr * (↑↑n + ↑↑n') + a'.repr
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: x : Ordinal.{u_1}
⊢ x.invVeblen₂ < ω ^ x

Tactic:
rw [invVeblen₂_lt_iff, opow_lt_veblen_opow_iff]

Goal state after:
x : Ordinal.{u_1}
⊢ x < veblen x.invVeblen₁ x
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u}
⊢ o < nfp (fun a ↦ ω ^ a) 0 ↔ ∃ n, o < (fun a ↦ ω ^ a)^[n] 0

Tactic:
lt_nfp_iff

Goal state after:
o : Ordinal.{u}
⊢ (∃ n, o < (fun a ↦ ω ^ a)^[n] 0) ↔ ∃ n, o < (fun a ↦ ω ^ a)^[n] 0
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
this : a₁.NF
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
have := h₂.snd

Goal state after:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u}
⊢ o < nfp (fun x ↦ veblen x 0) 0 ↔ ∃ n, o < (fun a ↦ veblen a 0)^[n] 0

Tactic:
lt_nfp_iff

Goal state after:
o : Ordinal.{u}
⊢ (∃ n, o < (fun x ↦ veblen x 0)^[n] 0) ↔ ∃ n, o < (fun a ↦ veblen a 0)^[n] 0
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: case refine_2
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
xs : x ∈ s
⊢ (Quotient.out x).Equiv
    ((PSet.mk (Shrink.{u, u + 1} ↑s) fun x ↦ Quotient.out ↑((equivShrink ↑s).symm x)).Func ((equivShrink ↑s) ⟨x, xs⟩))

Tactic:
· simp [PSet.Equiv.refl]

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

Goal state before:
pp: o : Ordinal.{u_1}
z : ZFSet.{u_1}
⊢ z.rank < o + 1 ↔ z ⊆ V_ o

Tactic:
subset_vonNeumann,

Goal state after:
o : Ordinal.{u_1}
z : ZFSet.{u_1}
⊢ z.rank < o + 1 ↔ z.rank ≤ o
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: 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)
αd : ω ∣ α'
⊢ ¬IsMin α'

Tactic:
isMin_iff_eq_bot

Goal state after:
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)
αd : ω ∣ α'
⊢ ¬α' = ⊥
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case neg
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
h_if : ¬some x :: ↑s = some x :: ↑t
⊢ Nat.find ⋯ = Nat.find ⋯ + 1

Tactic:
convert! Nat.find_comp_succ _ _ _
    simp [Stream'.cons]

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

Goal state before:
pp: hd : ℝ → ℝ
tl : Basis
h : WellFormedBasis (hd :: tl)
f : ℝ → ℝ
hf : f ∈ tl
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)

Tactic:
by
  rw [WellFormedBasis, List.pairwise_cons] at h
  exact h.left.left _ hf

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
γ : Type u_1
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
h : ∀ (c : γ), FriendlyOperation (op c)
⊢ FriendlyOperationClass op

Tactic:
suffices Seq.FriendlyOperationClass op by constructor
  exact ⟨h⟩

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

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

Tactic:
by
  generalize h_ms : (mk .nil f) = ms at h
  cases h <;> simp at h_ms; grind

Goal state after:
Module: Mathlib.Tactic.LinearCombinationPrime

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝ : AddGroup α
p : a - b = 0
H : a' - b' - (a - b) = 0
⊢ a' - b' = 0

Tactic:
sub_eq_zero,

Goal state after:
α : Type u_1
a a' b b' : α
inst✝ : AddGroup α
p : a - b = 0
H : a' - b' = a - b
⊢ a' - b' = 0
Module: Mathlib.Tactic.LinearCombinationPrime

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : IsReduced α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n - (a - b) = 0
⊢ (a' - b') ^ n = 0

Tactic:
sub_eq_zero,

Goal state after:
α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : IsReduced α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n = a - b
⊢ (a' - b') ^ n = 0
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)
⊢ ↑b ≠ 0

Tactic:
simp; lia

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

Goal state before:
pp: case neg
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
h : ↑a / ↑b = (↑↑x / ↑y) ^ d
hx' : x' = ↑x
⊢ False

Tactic:
simp only [Int.cast_natCast, div_pow] at h

Goal state after:
case neg
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : ↑a / ↑b = ↑x ^ d / ↑y ^ d
⊢ False
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
this : NeZero c
⊢ jacobiSym (↑a) (2 * c) = r

Tactic:
jacobiSym.mul_right,

Goal state after:
case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
this : NeZero c
⊢ jacobiSym (↑a) 2 * jacobiSym (↑a) c = r
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
b : α
a : ℕ
a' : α
p : IsNat (↑n - 1) a
pa : ↑a = a'
⊢ -b = (↑n - 1) * b

Tactic:
← neg_one_mul

Goal state after:
α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
b : α
a : ℕ
a' : α
p : IsNat (↑n - 1) a
pa : ↑a = a'
⊢ -1 * b = (↑n - 1) * b
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
a b : α
na : ℕ
na' : α
p : IsNat ((↑n - 1) * a) na
pa : ↑na = na'
⊢ -(a * b) = (↑n - 1) * a * b

Tactic:
← neg_one_mul

Goal state after:
α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
a b : α
na : ℕ
na' : α
p : IsNat ((↑n - 1) * a) na
pa : ↑na = na'
⊢ -1 * (a * b) = (↑n - 1) * a * b
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hs : Icc m n = s
⊢ Ico m (n + 1) = Icc m n

Tactic:
Ico_add_one_right_eq_Icc

Goal state after:
m n : ℕ
s : Finset ℕ
hs : Icc m n = s
⊢ Icc m n = Icc m n
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = some val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs

Tactic:
· obtain - | ⟨h₀, h₅⟩ := h₀
        obtain - | ⟨h₂, h₄⟩ := h₂
        have h₆ := Nat.succ.inj h₁
        specialize xs_ih h₅ h₃ h₄ h₆
        simp only [Ne.symm h, xs_ih, List.mem_cons]
        suffices val ∈ ys by tauto
        rw [← Option.mem_def, List.mem_dlookup_iff] at h₃
        · simp only [Prod.toSigma, List.mem_map, Prod.exists] at h₃
          rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩
          apply (List.of_mem_zip h₃).2
        simp only [List.NodupKeys, List.keys, comp_def, Prod.fst_toSigma, List.map_map]
        rwa [List.map_fst_zip (le_of_eq h₆)]

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

Goal state before:
pp: G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
⊢ (U ∩ Set.range (etaFn G)).Nonempty

Tactic:
have hM : M.Normal := Subgroup.normal_iInf_normal fun j => inferInstance

Goal state after:
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
⊢ (U ∩ Set.range (etaFn G)).Nonempty
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ IsInducing (⇑(UniformOnFun.ofFun ?m.83) ∘ Subtype.val ∘ ⇑(Equiv.Set.image DFunLike.coe S ⋯))

Tactic:
exact ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact.isInducing.comp .subtypeVal

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝ :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
⊢ (fun y ↦ 1 + y) '' ↑(I ^ n) ⊆ s

Tactic:
rintro _ ⟨x, hx, rfl⟩

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝ :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
x : R
hx : x ∈ ↑(I ^ n)
⊢ (fun y ↦ 1 + y) x ∈ s
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝ : ContinuousAdd 𝕜
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ Continuous[instTopologicalSpaceProd, inst] fun p ↦ p.1 + p.2

Tactic:
hB.eq_induced,

Goal state after:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝ : ContinuousAdd 𝕜
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace] fun p ↦
    p.1 + p.2
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝ : ContinuousSMul 𝕜 𝕜
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ Continuous[instTopologicalSpaceProd, inst] fun p ↦ p.1 • p.2

Tactic:
hB.eq_induced,

Goal state after:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝ : ContinuousSMul 𝕜 𝕜
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace] fun p ↦
    p.1 • p.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
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ -a

Tactic:
hB.eq_induced,

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
⊢ Continuous[TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace,
      TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace]
    fun a ↦ -a
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
⊢ IsClosed[inst✝¹] (derivedSet A)

Tactic:
rw [← derivedSet_closure, isClosed_iff_derivedSet_subset]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
⊢ derivedSet (derivedSet (closure[inst✝¹] A)) ⊆ derivedSet (closure[inst✝¹] A)
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
⊢ Perfect (perfectKernel s)

Tactic:
obtain ⟨a, ha⟩ := iteratedDerivedSet_mem_fixedPoints s

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
a : Ordinal.{u}
ha : sᵈ[a] ∈ fixedPoints ⇑relDerivedSet
⊢ Perfect (perfectKernel s)
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[_, inst✝¹] (g ∘ ⇑homeomorph) ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, inst✝¹] (g ∘ ⇑f)

Tactic:
WithGeneratedByTopology.continuous_from_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
⊢ (∀ ⦃i : ι⦄ (f : C(X i, Y)),
      Continuous[inst✝² i, inst✝¹] ((g ∘ ⇑homeomorph) ∘ ⇑WithGeneratedByTopology.equiv.symm ∘ ⇑f)) ↔
    ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, inst✝¹] (g ∘ ⇑f)
Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : Y → Z
⊢ ContinuousGeneratedBy X g ↔ Continuous[_, inst✝] (g ∘ ⇑WithGeneratedByTopology.equiv)

Tactic:
WithGeneratedByTopology.continuous_from_iff

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : Y → Z
⊢ ContinuousGeneratedBy X g ↔
    ∀ ⦃i : ι⦄ (f : C(X i, Y)),
      Continuous[inst✝² i, inst✝] ((g ∘ ⇑WithGeneratedByTopology.equiv) ∘ ⇑WithGeneratedByTopology.equiv.symm ∘ ⇑f)