mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f f' : A⟦X⟧
inst✝ : IsAdicComplete I A
⊢ H.mod (f + f') = H.mod f + H.mod f'

Tactic:
have H1 := (H.isWeierstrassDivisionAt_div_mod f).add (H.isWeierstrassDivisionAt_div_mod f')

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f f' : A⟦X⟧
inst✝ : IsAdicComplete I A
H1 : (f + f').IsWeierstrassDivisionAt g (H.div f + H.div f') (H.mod f + H.mod f') I
⊢ H.mod (f + f') = H.mod f + H.mod f'
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case degree_lt
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ := ⋯
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ (Polynomial.X ^ n - f).degree < ↑((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) g).order.toNat

Tactic:
refine (Polynomial.degree_sub_lt_left ?_ (Polynomial.monic_X_pow n).ne_zero ?_).trans_eq
      (by simpa)

Goal state after:
case degree_lt.refine_1
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ (Polynomial.X ^ n).degree = f.degree

case degree_lt.refine_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ (Polynomial.X ^ n).leadingCoeff = f.leadingCoeff
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst✝⁹ : CommSemiring R₀
inst✝⁸ : Ring R
inst✝⁷ : Algebra R₀ R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R S
inst✝ : IsSimpleModule R S
s : Set ↑(isotypicComponents R M)
c : ↑(isotypicComponents R M)
hc : c ∈ {c | ↑c ≤ ↑(⨆ c ∈ s, ⟨↑c, ⋯⟩)}
hcs : c ∉ s
⊢ ∀ i ∈ s, ↑i ≤ sSup (isotypicComponents R M \ {↑c})

Tactic:
exact fun c hc ↦ le_sSup ⟨c.2, Subtype.coe_ne_coe.mpr (ne_of_mem_of_not_mem hc hcs)⟩

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
n : ℕ
hn : NeZero n
S : Submodule R R
hS : IsSimpleModule R ↥S
e : R ≃ₗ[R] Fin n → ↥S
⊢ Rᵐᵒᵖ ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥S)

Tactic:
exact .trans (.moduleEndSelf R₀) <| .trans (e.conjAlgEquiv R₀) (endVecAlgEquivMatrixEnd ..)

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : CommRing R
f : R[X]
xli : PrimeSpectrum R[X]
complement : xli ∈ (zeroLocus {f})ᶜ
⊢ PrimeSpectrum.comap C xli ∈ imageOfDf f

Tactic:
exact comap_C_mem_imageOfDf complement

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ (Multiset.map f s).sum ∈ I

Tactic:
rw [mem_iff, ← Multiset.sum_map_zero]
  exact I.ringCon.multisetSum s hs

Goal state after:
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k₁ k₂ : ℕ
hk : k₁ ≤ k₂
⊢ (TruncatedWittVector.truncate hk).comp ((zmodEquivTrunc p k₂).toRingHom.comp (PadicInt.toZModPow k₂)) =
    (zmodEquivTrunc p k₁).toRingHom.comp (PadicInt.toZModPow k₁)

Tactic:
by
  rw [← RingHom.comp_assoc, commutes, RingHom.comp_assoc,
    PadicInt.zmod_cast_comp_toZModPow _ _ hk]

Goal state after:
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ (toPadicInt p).comp (fromPadicInt p) = RingHom.id ℤ_[p]

Tactic:
rw [← PadicInt.toZModPow_eq_iff_ext]
  intro n
  rw [← RingHom.comp_assoc, toPadicInt, PadicInt.lift_spec]
  simp only [fromPadicInt, toZModPow, RingHom.comp_id]
  rw [RingHom.comp_assoc, truncate_comp_lift, ← RingHom.comp_assoc]
  simp only [RingEquiv.symm_toRingHom_comp_toRingHom, RingHom.id_comp]

Goal state after:
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    (rename (Prod.mk 0)) (C (↑p ^ (n + 1)) * X (n + 1) ^ 1)

Tactic:
pow_one,

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    (rename (Prod.mk 0)) (C (↑p ^ (n + 1)) * X (n + 1))
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    (rename (Prod.mk 1)) (C (↑p ^ (n + 1)) * X (n + 1) ^ 1)

Tactic:
pow_one,

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    (rename (Prod.mk 1)) (C (↑p ^ (n + 1)) * X (n + 1))
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ↑p ^ (n + 1) * X (0, n + 1) *
    ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))

Tactic:
2

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ↑p ^ (n + 1) * X (1, n + 1) *
    ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))

Tactic:
2

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (remainder p n).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
apply remainder_vars

Goal state after:
Module: Mathlib.RingTheory.WittVector.Isocrystal

Goal state before:
pp: case refine_2
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
⊢ F₀.range = ⊤

Tactic:
rw [← (finrank_eq_one_iff_of_nonzero x hx).mp h_dim]

Goal state after:
case refine_2
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
⊢ F₀.range = K(p, k) ∙ x
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
s : Set (Set α)
inst✝ : OrderTop α
hs : ∀ x ∈ s, IsClub x
⊢ IsClub (⋂₀ s)

Tactic:
refine ⟨.sInter fun x hx ↦ (hs x hx).dirSupClosed, ?_⟩
  rw [isCofinal_iff_top_mem, mem_sInter]
  exact fun x hx ↦ (hs x hx).isCofinal.top_mem

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

Goal state before:
pp: case inr.refine_2.inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
a : α
h : NoTopOrder α
⊢ ∃ y ∈ Function.fixedPoints f, a ≤ y

Tactic:
rw [noTopOrder_iff_noMaxOrder] at h

Goal state after:
case inr.refine_2.inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
a : α
h : NoMaxOrder α
⊢ ∃ y ∈ Function.fixedPoints f, a ≤ y
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x : List A
⊢ pullSub (subAt T x) x ≤ T

Tactic:
by
  intro y (h : y ∈ pullSub _ x); rcases le_total y.length x.length with h' | h'
  · rw [mem_pullSub_short h'] at h; exact mem_of_prefix h.1 (by simpa using h.2)
  · rw [mem_pullSub_long h'] at h; obtain ⟨_, h, rfl⟩ := h; exact h

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

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
h : ∀ x ∈ s, ¬IsStationary x
⊢ ¬IsStationary (⋃₀ s)

Tactic:
simp_rw [not_isStationary_iff] at h ⊢

Goal state after:
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
h : ∀ x ∈ s, ∃ t, IsClub t ∧ Disjoint x t
⊢ ∃ t, IsClub t ∧ Disjoint (⋃₀ s) t
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
h : ∀ x ∈ s, ¬IsStationary x
⊢ ¬IsStationary (⋃₀ s)

Tactic:
simp_rw [not_isStationary_iff] at h ⊢

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
h : ∀ x ∈ s, ∃ t, IsClub t ∧ Disjoint x t
⊢ ∃ t, IsClub t ∧ Disjoint (⋃₀ s) t
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inl
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hα : cof α < ℵ₀
⊢ IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x

pp: case inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hα : ℵ₀ < cof α
⊢ IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x

Tactic:
· apply isStationary_sUnion_iff_of_cof_le_one
    rwa [← cof_lt_aleph0_iff]

Goal state after:
case inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hα : ℵ₀ < cof α
⊢ IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
⊢ Monotone (lfpApprox f x)

Tactic:
by
  intro a b h
  rw [lfpApprox, lfpApprox]
  apply sup_le_sup_left (iSup₂_mono' _)
  grind

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

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

pp: case refine_2
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : f x = x ∨ o = 0
⊢ lfpApprox f x o = x

Tactic:
· rcases eq_or_ne o 0 with (rfl | ho)
    · exact Or.inr rfl
    · have hpos : (0 : Ordinal) < o :=
        zero_lt_one.trans_le (one_le_iff_ne_zero.mpr ho)
      have hmem : lfpApprox f x 0 ∈ fixedPoints f :=
        lfpApprox_mem_fixedPoints_of_eq f hx hpos (le_refl _)
          ((lfpApprox_zero f).trans h.symm)
      have hfx : f x = x :=
        (mem_fixedPoints_iff.mp (by simpa [lfpApprox_zero] using hmem))
      exact Or.inl hfx

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

Goal state before:
pp: case zero
b : ONote
⊢ Decidable (b.TopBelow zero)

Tactic:
delta TopBelow

Goal state after:
case zero
b : ONote
⊢ Decidable
    (match zero with
    | zero => True
    | e.oadd a a_1 => e.cmp b = Ordering.lt)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd
b a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ Decidable (b.TopBelow (a✝².oadd a✝¹ a✝))

Tactic:
delta TopBelow

Goal state after:
case oadd
b a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ Decidable
    (match a✝².oadd a✝¹ a✝ with
    | zero => True
    | e.oadd a a_1 => e.cmp b = Ordering.lt)
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: ⊢ ∅.card = 0

Tactic:
← lift_inj,

Goal state after:
⊢ lift.{?u.9, u_1} ∅.card = lift.{?u.9, u_1} 0
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case inl
o a : Ordinal.{u}
h : o < a.invVeblen₁
⊢ a < veblen o a ↔ a.invVeblen₁ ≤ o

Tactic:
veblen_eq_of_lt_invVeblen₁ h

Goal state after:
case inl
o a : Ordinal.{u}
h : o < a.invVeblen₁
⊢ a < a ↔ a.invVeblen₁ ≤ o
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: x : Ordinal.{u_1}
h : 0 < x.invVeblen₁
⊢ x = veblen 0 x

Tactic:
veblen_eq_of_lt_invVeblen₁ h

Goal state after:
x : Ordinal.{u_1}
h : 0 < x.invVeblen₁
⊢ x = x
Module: Mathlib.SetTheory.ZFC.Class

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

Tactic:
← mk_out x,

Goal state after:
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
⊢ mk (Quotient.out x) ∈ mk (PSet.mk (Shrink.{u, u + 1} ↑s) fun x ↦ Quotient.out ↑((equivShrink ↑s).symm x)) ↔
    mk (Quotient.out x) ∈ s
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ⊆ y ∧ y.rank ≤ x.rank ↔ x ⊆ y ∧ y ⊆ x

Tactic:
rank_le_iff_subset hy hx

Goal state after:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ⊆ y ∧ 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₁ + e₂).repr < e₁.repr + b₂

Tactic:
grw [repr_add, h₂.lt]

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

Goal state before:
pp: case refine_1
x : ZFSet.{u}
h : x.IsOrdinal
⊢ x.rank.toZFSet ∈ Set.range toZFSet

Tactic:
exact Set.mem_range_self _

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

Goal state before:
pp: basis : Basis
f : ℝ → ℝ
h : WellFormedBasis basis
h_comp : ∀ (g : ℝ → ℝ), List.getLast? basis = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
⊢ ∀ g ∈ basis, (Real.log ∘ f) =o[atTop] (Real.log ∘ g)

Tactic:
by
  intro g hg
  rcases basis.eq_nil_or_concat with rfl | ⟨basis_begin, basis_end, rfl⟩
  · simp at hg
  simp only [List.concat_eq_append, List.mem_append, List.mem_cons, List.not_mem_nil, or_false,
    List.getLast?_append, List.getLast?_singleton, Option.some_or, Option.some.injEq,
    forall_eq'] at hg h_comp
  rcases hg with hg | hg
  · simp only [WellFormedBasis, List.concat_eq_append, List.mem_append, List.mem_cons,
      List.not_mem_nil, or_false] at h
    exact h_comp.trans (by grind)
  · grind

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

Goal state before:
pp: case h.nil
α : Type u_1
op✝ : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
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, opf, op') => (hd, ↑opf (↑op' s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = opf ∘ op' ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
s : Stream'.Seq α
hT :
  nil.destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
      (T s.head)
⊢ (opf nil).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match T s.head with
      | none => Option.map (fun x ↦ (x.1, ⟨(fun x_1 ↦ ↑x.2 nil) ∘ op, ⋯⟩)) (h_opf.unfold none)
      | some (hd, opf', op') => Option.map (fun x ↦ (x.1, ⟨(↑x.2 ∘ ↑opf') ∘ ↑op', ⋯⟩)) (h_opf.unfold (some hd)))

Tactic:
symm at hT

Goal state after:
case h.nil
α : Type u_1
op✝ : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
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, opf, op') => (hd, ↑opf (↑op' s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = opf ∘ op' ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
s : Stream'.Seq α
hT :
  Option.map
      (fun x ↦
        match x with
        | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
      (T s.head) =
    nil.destruct
⊢ (opf nil).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match T s.head with
      | none => Option.map (fun x ↦ (x.1, ⟨(fun x_1 ↦ ↑x.2 nil) ∘ op, ⋯⟩)) (h_opf.unfold none)
      | some (hd, opf', op') => Option.map (fun x ↦ (x.1, ⟨(↑x.2 ∘ ↑opf') ∘ ↑op', ⋯⟩)) (h_opf.unfold (some hd)))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
⊢ ms = mk s f ↔ ms.seq = s ∧ ms.toFun = f

Tactic:
conv => lhs; lhs; rw [eq_mk ms]

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
⊢ mk ms.seq ms.toFun = mk s f ↔ ms.seq = s ∧ ms.toFun = f
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ ¬(IsSquare (↑↑n / ↑↑d).num ∧ IsSquare (↑↑n / ↑↑d).den)

Tactic:
Rat.num_div_eq_of_coprime

Goal state after:
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ ¬(IsSquare ↑n ∧ IsSquare (↑↑n / ↑↑d).den)

case hb0
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ 0 < ↑d

case h
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ (↑n).natAbs.Coprime (↑d).natAbs
Module: Mathlib.Tactic.NormNum.PowMod

Goal state before:
pp: a b m : ℕ
⊢ a ^ b * a ^ b * a ^ 1 % m = a ^ b % m * (a ^ b % m * a % m) % m

Tactic:
pow_one,

Goal state after:
a b m : ℕ
⊢ a ^ b * a ^ b * a % m = a ^ b % m * (a ^ b % m * a % m) % m
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous[inst✝⁸, inst✝³] ⇑f
A : MulAction G H := MulAction.compHom H f
this✝ : ContinuousSMul G H
this : IsPretransitive G H
⊢ ⇑f = fun g ↦ g • 1

Tactic:
simp [A, MulAction.compHom_smul_def]

Goal state after:
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
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
c : 𝕜₁
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
c_ne : c ≠ 0
cV_mem : c • V ∈ 𝓕₂ ⊓ 𝓟 V
basis_𝓕₂ : 𝓕₂.HasBasis (fun s ↦ s ∈ 𝓕₂ ∧ Balanced 𝕜₁ s) id
W : Set E
hW : id W ∩ V ⊆ c • V
W_mem_𝓕₂ : W ∈ 𝓕₂
W_bal : Balanced 𝕜₁ W
w : E
w_in_W : w ∈ W
n : ℕ
hn : c ^ n • w ∈ V
k : ℕ
h✝ : k < n
hk : c ^ (k + 1) • w ∈ V
this : (c ^ k * c ^ 1) • w ∈ c • V
⊢ c ^ k • w ∈ V

Tactic:
pow_one,

Goal state after:
𝕜₁ : 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
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
c : 𝕜₁
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
c_ne : c ≠ 0
cV_mem : c • V ∈ 𝓕₂ ⊓ 𝓟 V
basis_𝓕₂ : 𝓕₂.HasBasis (fun s ↦ s ∈ 𝓕₂ ∧ Balanced 𝕜₁ s) id
W : Set E
hW : id W ∩ V ⊆ c • V
W_mem_𝓕₂ : W ∈ 𝓕₂
W_bal : Balanced 𝕜₁ W
w : E
w_in_W : w ∈ W
n : ℕ
hn : c ^ n • w ∈ V
k : ℕ
h✝ : k < n
hk : c ^ (k + 1) • w ∈ V
this : (c ^ k * c) • w ∈ c • V
⊢ c ^ k • w ∈ V
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ (ConcreteCategory.hom f) (X.str xs) = Y.str (Ultrafilter.map (⇑(ConcreteCategory.hom f)) xs)

Tactic:
change (X.a ≫ f.f) _ = _
  rw [← f.h]
  rfl

Goal state after:
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[tY, _] (⇑WithGeneratedByTopology.equiv.symm ∘ g) ↔ Continuous[tY, inst✝¹] g

Tactic:
refine ⟨fun hg ↦ WithGeneratedByTopology.continuous_equiv.comp hg, fun hg ↦ ?_⟩
  rw [continuous_iff (X := X)]
  intro i f
  rw [continuous_def]
  intro U hU
  rw [WithGeneratedByTopology.isOpen_iff] at hU
  exact hU (ContinuousMap.comp ⟨g, hg⟩ f)

Goal state after:
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
⊢ ContinuousGeneratedBy X ⇑equiv.symm

Tactic:
by
    rw [continuousGeneratedBy_def]
    intro i f
    rw [IsGeneratedBy.equiv_symm_comp_continuous_iff]
    fun_prop

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J : ι → Prop
x : ↑(obj C J)
⊢ ∃ a, (π_app C J) a = x

Tactic:
obtain ⟨y, hy⟩ := x.prop

Goal state after:
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J : ι → Prop
x : ↑(obj C J)
y : (i : ι) → X i
hy : y ∈ C ∧ (precomp Subtype.val) y = ↑x
⊢ ∃ a, (π_app C J) a = x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u_1
C : Set (I → Bool)
x : ↑C
l : List (LocallyConstant ↑C ℤ)
⊢ l.prod x = (LocallyConstant.evalMonoidHom x) l.prod

Tactic:
LocallyConstant.evalMonoidHom_apply

Goal state after:
I : Type u_1
C : Set (I → Bool)
x : ↑C
l : List (LocallyConstant ↑C ℤ)
⊢ l.prod x = l.prod x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y = x
⊢ ∀ (x_1 : ℤ),
    (∃ a,
        (∃ a_1 ∈ s.sort fun x1 x2 ↦ x1 ≥ x2,
            (if ↑x a_1 = true then e (π C fun x ↦ x ∈ s) a_1 else 1 - e (π C fun x ↦ x ∈ s) a_1) = a) ∧
          ((Pi.evalMonoidHom (fun a ↦ ℤ) x).comp LocallyConstant.coeFnMonoidHom) a = x_1) →
      x_1 = 1

Tactic:
rintro _ ⟨a, ⟨b, _, rfl⟩, rfl⟩

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y = x
b : I
left✝ : b ∈ s.sort fun x1 x2 ↦ x1 ≥ x2
⊢ ((Pi.evalMonoidHom (fun a ↦ ℤ) x).comp LocallyConstant.coeFnMonoidHom)
      (if ↑x b = true then e (π C fun x ↦ x ∈ s) b else 1 - e (π C fun x ↦ x ∈ s) b) =
    1