mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A'.val.toLinearMap) t'
hj : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t = (rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'

Tactic:
have hj' : (A ⊔ A').val.comp (Subalgebra.inclusion le_sup_right) = A'.val := by ext; rfl

Goal state after:
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A'.val.toLinearMap) t'
hj : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
hj' : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A'.val
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t = (rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
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
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n✝ n : ℕ
S : ShortComplex (ModuleCat R) := M.smulShortComplex x
hS : S.ShortExact
⊢ HasProjectiveDimensionLE (of R (QuotSMulTop x ↑M)) (n + 1) ↔ HasProjectiveDimensionLE M n

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ hS.hasProjectiveDimensionLT_X₃ (n + 1) h
        (hasProjectiveDimensionLT_of_ge M (n + 1) (n + 2) (Nat.le_add_right _ 1))⟩

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)
n✝ n : ℕ
S : ShortComplex (ModuleCat R) := M.smulShortComplex x
hS : S.ShortExact
h : HasProjectiveDimensionLE (of R (QuotSMulTop x ↑M)) (n + 1)
⊢ HasProjectiveDimensionLE M n
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 : 1 = (coeff n) ((map (IsLocalRing.residue A)) g * (map (IsLocalRing.residue A)) q)
⊢ IsUnit q

Tactic:
isUnit_iff_constantCoeff,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 : 1 = (coeff n) ((map (IsLocalRing.residue A)) g * (map (IsLocalRing.residue A)) q)
⊢ IsUnit (constantCoeff q)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
this : f.degree = ↑n
⊢ f.natDegree = n

Tactic:
rw [Polynomial.natDegree, this]; rfl

Goal state after:
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
⊢ False

Tactic:
have ⟨S, le, _⟩ := (IsSemisimpleModule.eq_bot_or_exists_simple_le _).resolve_left ne

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
⊢ False
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : IsSimpleRing R
tfae_1_to_2 : IsSemisimpleRing R → IsArtinianRing R
tfae_2_to_3 : IsArtinianRing R → ∃ I, IsAtom I
x✝ : ∃ I, IsAtom I
I : Ideal R
hI : IsAtom I
⊢ IsSemisimpleRing R

Tactic:
have ⟨_, h⟩ := isSimpleRing_iff_isTwoSided_imp.mp ‹IsSimpleRing R›
    simp_rw [← isFullyInvariant_iff_isTwoSided] at h
    have := isSimpleModule_iff_isAtom.mpr hI
    obtain eq | eq := h _ (.isotypicComponent R R I)
    · exact (hI.bot_lt.not_ge <| (le_sSup <| by exact ⟨.refl ..⟩).trans_eq eq).elim
    exact .congr (.symm <| .trans (.ofEq _ _ eq) Submodule.topEquiv)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
⊢ IsStationary Set.univ ↔ Nonempty α

Tactic:
by
  simp [IsStationary, ← not_imp_not (b := IsClub _), not_nonempty_iff_eq_empty,
    isClub_empty_iff]

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

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
h : (e.oadd n a).NFBelow b
⊢ a.NFBelow e.repr

Tactic:
by
  obtain - | ⟨h₁, h₂, h₃⟩ := h; exact h₂

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

Goal state before:
pp: e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a + o).repr = a.repr + o.repr
| (a + o).repr

Tactic:
simp [HAdd.hAdd, Add.add]

Goal state after:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a + o).repr = a.repr + o.repr
| (a.add o).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: 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
nf : (a + o).NF
| (a + o).NF

Tactic:
simp [HAdd.hAdd, Add.add]

Goal state after:
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
nf : (a + o).NF
| (a.add o).NF
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: 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
nf : (a.add o).NF
| e.oadd n a + o

Tactic:
simp [HAdd.hAdd, Add.add]

Goal state after:
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
nf : (a.add o).NF
| (e.oadd n a).add o
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: 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 : β
γ : 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}
hb : (PSet.mk γ Γ).Equiv (PSet.mk δ Δ)
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)

Tactic:
obtain ⟨γδ, δγ⟩ := hb

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 : β
γ : 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 δ Δ
γδ : ∀ (a : γ), ∃ b, (Γ a).Equiv (Δ b)
δγ : ∀ (b : δ), ∃ a, (Γ a).Equiv (Δ b)
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: 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 : β
γ : 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 δ Δ
γδ : ∀ (a : γ), ∃ b, (Γ a).Equiv (Δ b)
δγ : ∀ (b : δ), ∃ a, (Γ a).Equiv (Δ b)
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)

Tactic:
let c : (A a).Type := c

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 : β
γ : 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 δ Δ
γδ : ∀ (a : γ), ∃ b, (Γ a).Equiv (Δ b)
δγ : ∀ (b : δ), ∃ a, (Γ a).Equiv (Δ b)
c : (A a).Type := c✝
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
⊢ f a < veblenWith f o (f a) ↔ a < veblenWith f o a

Tactic:
simpa using veblenWith_lt_veblenWith_veblenWith_iff hf zero_le

Goal state after:
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 : True ∧ y = x ∨ True ↔ True ∧ y = x ∨ {x, y} = {x, y'}
⊢ x = x ∧ y = y'

Tactic:
true_and,

Goal state after:
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 ∨ True ↔ y = x ∨ {x, y} = {x, y'}
⊢ x = x ∧ y = y'
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}
⊢ ↑(map f x) (y.pair z) ↔ z = f y

Tactic:
Class.coe_apply,

Goal state after:
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
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (⋃ (i : α), f i).rank ≤ ⨆ i, (f i).rank

Tactic:
simp_rw [rank_le_iff, mem_iUnion]
    intro y ⟨i, hy⟩
    exact (rank_lt_of_mem hy).trans_le (Ordinal.le_iSup _ _)

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

Goal state before:
pp: o : Ordinal.{u}
x : ZFSet.{u}
⊢ x ∈ V_ o ↔ x.rank < o

Tactic:
simp_rw [mem_vonNeumann', subset_vonNeumann]

Goal state after:
o : Ordinal.{u}
x : ZFSet.{u}
⊢ (∃ a < o, x.rank ≤ a) ↔ x.rank < o
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
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
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : ¬e₂ = 0
this✝ : e₁.NF
this : e₂.NF
⊢ ω ^ e₁.repr * ω ^ e₂.repr * ↑↑n₂ + (ω ^ e₁.repr * ↑↑n₁ + a₁.repr) * a₂.repr =
    (ω ^ e₁.repr * ↑↑n₁ + a₁.repr) * ω ^ e₂.repr * ↑↑n₂ + (ω ^ e₁.repr * ↑↑n₁ + a₁.repr) * a₂.repr

Tactic:
congr 2

Goal state after:
case neg.e_a.e_a
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
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : ¬e₂ = 0
this✝ : e₁.NF
this : e₂.NF
⊢ ω ^ e₁.repr * ω ^ e₂.repr = (ω ^ e₁.repr * ↑↑n₁ + a₁.repr) * ω ^ e₂.repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: basis : Basis
ex : BasisExtension basis
⊢ List.Sublist basis ex.getBasis

Tactic:
by
  induction ex with
  | nil => simp
  | keep _ ex ih => simpa [getBasis] using ih
  | insert _ ex ih => exact List.Sublist.cons _ ih

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

Goal state before:
pp: ⊢ ¬FirstNonzeroIsPos []

Tactic:
by simp [FirstNonzeroIsPos, sign]

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

Goal state before:
pp: case nil
exps_hd : ℝ
basis_hd : ℝ → ℝ
h_nonzero : exps_hd ≠ 0
basis_tl : Basis
hlo : ∀ b ∈ basis_tl, (log ∘ b) =o[atTop] (log ∘ basis_hd)
⊢ toLogFun [] basis_tl =o[atTop] (log ∘ basis_hd)

Tactic:
simp only [toLogFun_nil]
    exact Asymptotics.isLittleO_zero _ _

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

Goal state before:
pp: case seq.h_Pairwise.nil
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
h_comp : Multiseries.nil.leadingExp < ↑exp
h_tl_coef : ∀ x ∈ (mk Multiseries.nil 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk Multiseries.nil 0).seq
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef Multiseries.nil) 0).seq

pp: case seq.h_Pairwise.cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl
tl✝ : Multiseries basis_hd basis_tl
h_comp : (Multiseries.cons exp✝ coef✝ tl✝).leadingExp < ↑exp
h_tl_coef : ∀ x ∈ (mk (Multiseries.cons exp✝ coef✝ tl✝) 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp✝ coef✝ tl✝) 0).seq
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef (Multiseries.cons exp✝ coef✝ tl✝)) 0).seq

Tactic:
· exact Seq.Pairwise_cons_nil

Goal state after:
case seq.h_Pairwise.cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl
tl✝ : Multiseries basis_hd basis_tl
h_comp : (Multiseries.cons exp✝ coef✝ tl✝).leadingExp < ↑exp
h_tl_coef : ∀ x ∈ (mk (Multiseries.cons exp✝ coef✝ tl✝) 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp✝ coef✝ tl✝) 0).seq
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef (Multiseries.cons exp✝ coef✝ tl✝)) 0).seq
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_coef : 0 < t.coef
⊢ ∀ᶠ (x : ℝ) in atTop, 0 < t.toFun basis x

Tactic:
simp only [Monomial.toFun]

Goal state after:
t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_coef : 0 < t.coef
⊢ ∀ᶠ (x : ℝ) in atTop, 0 < (t.coef • t.unit.toFun basis) x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f : ℝ → ℝ
h : (mk (Multiseries.cons exp coef tl) f).Trimmed
⊢ coef.Trimmed ∧ ¬coef.IsZero

Tactic:
by
  simp only [trimmed_iff_seq_trimmed, mk_seq] at h
  exact h.elim_cons

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

Goal state before:
pp: case h
a : ℚ
n d : ℕ
ha : IsNNRat a (n * n) (d * d)
⊢ a = ↑n / ↑d * (↑n / ↑d)

Tactic:
simp [ha.to_eq, div_mul_div_comm]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: case inr.mpr
ι : 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 (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f))

Tactic:
have H' : Tendsto id 𝒢 (𝓝 ⟨f, f_mem⟩) := by
      rwa [tendsto_id', nhds_induced, ← map_le_iff_le_comap, h𝒢ℱ]

Goal state after:
case inr.mpr
ι : 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 ℱ
H' : Tendsto id 𝒢 (𝓝 ⟨f, f_mem⟩)
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f))
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
⊢ Function.Injective toFiniteIndexNormalSubgroup

Tactic:
intro H K h
  apply toSubgroup_injective
  exact congrArg (fun L : FiniteIndexNormalSubgroup G ↦ (L : Subgroup G)) h

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

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f g : completion G ⟶ P
h : eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map f = eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map g
x : ↑(completion G).toProfinite.toTop
y : ↑G
⊢ (⇑(Hom.hom f) ∘ etaFn G) y = (⇑(Hom.hom g) ∘ etaFn G) y

Tactic:
simpa [GrpCat.comp_apply] using! (ConcreteCategory.congr_hom h y)

Goal state after:
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, Pi.topologicalSpace] ((fun x1 x2 ↦ (B x1) x2) ∘ fun p ↦ p.1 • p.2)

Tactic:
simp only [Function.comp_def, map_smul, smul_apply]

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, Pi.topologicalSpace] fun x x2 ↦ x.1 • (B x.2) x2
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
V_mem : V ∈ 𝓝 0
H : 𝓝 0 ⊓ 𝓟 V = 𝓝 0 ⊓ 𝓟 V
⊢ t₁ = t₂

Tactic:
by
  classical
  -- For `i = 1, 2`, denote by `𝓕ᵢ` the filter of neighborhoods of `0` for the topology `tᵢ`.
  set 𝓕₁ := @nhds E t₁ 0
  set 𝓕₂ := @nhds E t₂ 0
  -- Note that, because `V ∈ 𝓕₁`, `H` may be rewritten as `𝓕₁ = 𝓕₂ ⊓ 𝓟 V`.
  replace H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V := by simpa [← H]
  -- Because both `t₁` and `t₂` are additive group topologies, it is enough to show `𝓕₁ = 𝓕₂`.
  suffices 𝓕₁ = 𝓕₂ by rwa [IsTopologicalAddGroup.ext_iff] <;> infer_instance
  -- If we can show that `V ∈ 𝓕₂` we are done, because then `𝓕₁ = 𝓕₂ ⊓ 𝓟 V = 𝓕₂`.
  suffices V ∈ 𝓕₂ by simpa [H]
  -- Hence, let us show that `V ∈ 𝓕₂`. Fix a scalar `c` with `0 < ‖c‖ < 1`.
  obtain ⟨c, hc₀, hc₁⟩ := NormedField.exists_norm_lt_one 𝕜₁
  have c_ne : c ≠ 0 := norm_pos_iff.mp hc₀
  -- We know that `c • V ∈ 𝓕₁ = 𝓕₂ ⊓ 𝓟 V`.
  have cV_mem : c • V ∈ 𝓕₂ ⊓ 𝓟 V := by
    simpa [← H, 𝓕₁, set_smul_mem_nhds_zero_iff c_ne]
  -- Furthermore, we know that `𝓕₂` has a basis of balanced sets
  have basis_𝓕₂ : HasBasis 𝓕₂ (fun (s : Set E) ↦ s ∈ 𝓕₂ ∧ Balanced 𝕜₁ s) id :=
    let := t₂; nhds_basis_balanced 𝕜₁ E
  -- Hence, we get a balanced set `W ∈ 𝓕₂` such that `W ∩ V ⊆ c • V`.
  obtain ⟨W, ⟨W_mem_𝓕₂, W_bal⟩, hW⟩ := basis_𝓕₂.inf_principal V |>.mem_iff.mp cV_mem
  -- We claim that `W ⊆ V`. This will conclude the proof, since `W ∈ 𝓕₂`.
  suffices W ⊆ V from mem_of_superset W_mem_𝓕₂ this
  -- Let `w ∈ W` be arbitrary.
  intro w w_in_W
  -- Because `V` is a `t₁`-neighborhood of `0`, we have `c ^ n • w ∈ V` for some natural number `n`.
  obtain ⟨n, hn⟩ : ∃ n : ℕ, c ^ n • w ∈ V :=
    let := t₁
    tendsto_pow_atTop_nhds_zero_of_norm_lt_one hc₁ |>.zero_smul_const w
      |>.eventually_mem V_mem |>.exists
  -- We will conclude by reducing `c ^ n • w ∈ V` to `w = c ^ 0 • w ∈ V` inductively.
  suffices c ^ 0 • w ∈ V by simpa
  apply Nat.decreasingInduction (motive := fun (k : ℕ) _ ↦ c^k • w ∈ V) ?_ hn n.zero_le
  -- To do so, we show that if `k : ℕ` is such that `c ^ (k + 1) • w ∈ V` then `c ^ k • w ∈ V`.
  intro k _ (hk : c ^ (k + 1) • w ∈ V)
  -- Indeed, because `W` is balanced, we have `c ^ (k + 1) • w ∈ W ∩ V ⊆ c • V`
  have : c ^ (k + 1) • w ∈ c • V :=
    hW ⟨W_bal.smul_mem (by grw [norm_pow, hc₁.le, one_pow]) w_in_W, hk⟩
  -- Cancelling `c`, we get `c ^ k • w ∈ V` as we claimed.
  rwa [pow_add, pow_one, mul_comm, mul_smul, smul_mem_smul_set_iff₀ c_ne V] at this

Goal state after:
Module: Mathlib.Topology.Baire.BaireMeasurable

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : IsOpen[inst✝] s
⊢ BaireMeasurableSet s

Tactic:
by
  borelize α
  exact h.measurableSet.baireMeasurableSet

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

Goal state before:
pp: X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D✝ : Set X✝
inst✝¹ : RelCWComplex C✝ D✝
X : Type u
inst✝ : TopologicalSpace X
C D : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
closed' :
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) ∧ IsClosed[inst✝] (A ∩ D) →
      IsClosed[inst✝] A
isClosedBase : IsClosed[inst✝] D
union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
n : ℕ
i : cell n
⊢ ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)

Tactic:
use fun m ↦ finite_univ.toFinset (s := (univ : Set (cell m)))
    simp only [Finite.mem_toFinset, mem_univ, iUnion_true]
    exact mapsTo n i

Goal state after: