mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.IrreducibleRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)
hc : 1 = ∑ x ∈ Finset.antidiagonal f.natDegree, a.coeff x.1 * b.coeff x.2
⊢ IsUnit (-(a.coeff f.natDegree * b.coeff 0))

Tactic:
Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j ↦ a.coeff i * b.coeff j,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)
hc : 1 = ∑ k ∈ Finset.range f.natDegree.succ, a.coeff k * b.coeff (f.natDegree - k)
⊢ IsUnit (-(a.coeff f.natDegree * b.coeff 0))
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : IsLeftCancelMulZero R[X]
a b c : R
eq : (fun x ↦ a + x) b = (fun x ↦ a + x) c
a✝ : Nontrivial R
trinomial : R → R[X] := fun r ↦ a • X ^ 2 + r • X + C a
r : R
⊢ C a * X * X ^ 2 + C a * X ^ 2 + (C r * X * X + C r * X) + (C a * X + C a) =
    C a * X ^ 3 + (C a * X ^ 2 + C r * X ^ 2) + (C a * X + C r * X) + C a

Tactic:
noncomm_ring

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
h : p = 0
⊢ False

Tactic:
rw [h] at hh

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : hilbertPoly 0 d ≠ 0
h : p = 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p.degree ≤ 2
⊢ p = C (p.coeff 2) * X ^ 2 + C (p.coeff 1) * X + C (p.coeff 0)

Tactic:
rw [p.as_sum_range_C_mul_X_pow'
    (Nat.lt_of_le_of_lt (natDegree_le_iff_degree_le.mpr hp) (Nat.lt_add_one 2))]
  simp [Finset.sum_range_succ]
  abel

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n k : ℕ
⊢ ∑ b ∈ range (n + 1), (C ((-1) ^ b * ↑(n.choose b) * ↑((n + b).choose n)) * X ^ b).coeff k =
    (-1) ^ k * ↑(n.choose k) * ↑((n + k).choose n)

Tactic:
simp_rw [coeff_C_mul_X_pow]

Goal state after:
n k : ℕ
⊢ (∑ x ∈ range (n + 1), if k = x then (-1) ^ x * ↑(n.choose x) * ↑((n + x).choose n) else 0) =
    (-1) ^ k * ↑(n.choose k) * ↑((n + k).choose n)
Module: Mathlib.RingTheory.Polynomial.Morse

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
g : G
hg : g ∈ Ideal.inertia G p
hfp : ¬map (algebraMap R (S ⧸ p)) f = 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S, ∀ c ∈ f.rootSet S, ∀ d ∈ f.rootSet S, π a = π b → π c = π d → a ≠ b → c ≠ d → {a, b} = {c, d}
hπ : ∀ (x : S), π (g • x) = π x
x : ↑(f.rootSet S)
hx : g • x ≠ x
z : ↑(f.rootSet S)
hz : ¬z = g • x
hz' : ¬z = x
⊢ ↑(g • z) = ↑z

Tactic:
· grind [rootSet.coe_smul, SetLike.coe_eq_coe]

Goal state after:
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 t' : ↥A ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t = (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'

Tactic:
let ⟨P', hP', u', hu'⟩ := TensorProduct.exists_of_fg t'

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 t' : ↥A ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t = (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
hz : z ≠ 0
p : ℕ
x✝ : Prime ↑p ∧ 0 ≤ ↑p ∧ ↑p ∣ z
pp : Nat.Prime p
dp : p ∣ z.natAbs
⊢ p ∈ z.natAbs.primeFactors

Tactic:
by simp_all

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
H : f.IsWeierstrassDivisionAt g q r I
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
⊢ (coeff i) (f - ↑r) ∈ I

Tactic:
by
  replace H := H.2
  rw [← sub_eq_iff_eq_add] at H
  rw [H]
  refine coeff_mul_mem_ideal_of_coeff_left_mem_ideal i (fun j hj ↦ ?_) i le_rfl
  have := coeff_of_lt_order_toNat _ (lt_of_le_of_lt hj hi)
  rwa [coeff_map, ← RingHom.mem_ker, Ideal.mk_ker] at this

Goal state after:
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ Function.Surjective (π R M S)

Tactic:
by
  intro t
  obtain ⟨B : Subalgebra R S, hB : B.FG, ht : t ∈ range _⟩ := TensorProduct.Algebra.exists_of_fg t
  obtain ⟨s : Finset S, hs : (PolynomialLaw.φ R s).range = B⟩ := exists_range_φ_eq_of_fg hB
  obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor B (le_of_eq hs.symm) ht
  exact ⟨⟨s, p⟩, hp⟩

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.DivisionRing

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsSimpleModule R M
N : Type v
x✝¹ : AddCommGroup N
x✝ : Module R N
f : M →ₗ[R] N
h : f.ker = ⊤
⊢ f = 0

Tactic:
by simp_all

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
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Module.Finite R M
⊢ ∃ n S d,
    (∀ (i : Fin n), IsSimpleModule R ↥(S i)) ∧
      (∀ (i : Fin n), NeZero (d i)) ∧
        Nonempty (End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (End R ↥(S i)))

Tactic:
choose d pos S _ simple e using fun c : isotypicComponents R M ↦
    (IsIsotypic.isotypicComponents c.2).submodule_linearEquiv_fun

Goal state after:
R₀ : Type u_1
R : Type u
inst✝⁸ : CommSemiring R₀
inst✝⁷ : Ring R
inst✝⁶ : Algebra R₀ R
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Module.Finite R M
d : ↑(isotypicComponents R M) → ℕ
pos : ∀ (c : ↑(isotypicComponents R M)), NeZero (d c)
S : ↑(isotypicComponents R M) → Submodule R M
h✝ : ∀ (c : ↑(isotypicComponents R M)), S c ≤ ↑c
simple : ∀ (c : ↑(isotypicComponents R M)), IsSimpleModule R ↥(S c)
e : ∀ (c : ↑(isotypicComponents R M)), Nonempty (↥↑c ≃ₗ[R] Fin (d c) → ↥(S c))
⊢ ∃ n S d,
    (∀ (i : Fin n), IsSimpleModule R ↥(S i)) ∧
      (∀ (i : Fin n), NeZero (d i)) ∧
        Nonempty (End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (End R ↥(S i)))
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

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

Tactic:
by
  obtain hα | hα := hα.lt_or_gt
  · apply isStationary_sUnion_iff_of_cof_le_one
    rwa [← cof_lt_aleph0_iff]
  · apply isStationary_sUnion_iff hα.ne' (hα.trans_le' _)
    rwa [le_aleph0_iff_set_countable]

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂ l₃ : Lists α
h₁ : of' l₁ ~ l₂
h₂ : l₂ ~ l₃
⊢ of' l₁ ~ l₃

Tactic:
obtain - | l₂ := id h₁

Goal state after:
case C1.refl
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₃ : Lists α
h₁ : of' l₁ ~ of' l₁
h₂ : of' l₁ ~ l₃
⊢ of' l₁ ~ l₃

case C1.antisymm
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₃ : Lists α
l₂✝ : Lists' α true
l₂ : l₁.Subset l₂✝
a✝ : l₂✝.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝⟩
h₂ : ⟨true, l₂✝⟩ ~ l₃
⊢ of' l₁ ~ l₃
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (l : Lists' α true), (∀ (l' : Lists α), l' ∈ l.toList → trans l') → trans (of' l)

pp: case D0
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (l' : Lists α), l' ∈ Lists'.nil.toList → trans l'

pp: case D1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (a : Lists α) (l : Lists' α true),
    trans a → (∀ (l' : Lists α), l' ∈ l.toList → trans l') → ∀ (l' : Lists α), l' ∈ (Lists'.cons a l).toList → trans l'

Tactic:
· intro l₁ IH l₂ l₃ h₁ h₂
    obtain - | l₂ := id h₁
    · exact h₂
    obtain - | l₃ := id h₂
    · exact h₁
    obtain ⟨hl₁, hr₁⟩ := Equiv.antisymm_iff.1 h₁
    obtain ⟨hl₂, hr₂⟩ := Equiv.antisymm_iff.1 h₂
    apply Equiv.antisymm_iff.2; constructor <;> apply Lists'.subset_def.2
    · intro a₁ m₁
      rcases Lists'.mem_of_subset' hl₁ m₁ with ⟨a₂, m₂, e₁₂⟩
      rcases Lists'.mem_of_subset' hl₂ m₂ with ⟨a₃, m₃, e₂₃⟩
      exact ⟨a₃, m₃, IH _ m₁ e₁₂ e₂₃⟩
    · intro a₃ m₃
      rcases Lists'.mem_of_subset' hr₂ m₃ with ⟨a₂, m₂, e₃₂⟩
      rcases Lists'.mem_of_subset' hr₁ m₂ with ⟨a₁, m₁, e₂₁⟩
      exact ⟨a₁, m₁, (IH _ m₁ e₂₁.symm e₃₂.symm).symm⟩

Goal state after:
case D0
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (l' : Lists α), l' ∈ Lists'.nil.toList → trans l'

case D1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (a : Lists α) (l : Lists' α true),
    trans a → (∀ (l' : Lists α), l' ∈ l.toList → trans l') → ∀ (l' : Lists α), l' ∈ (Lists'.cons a l).toList → trans l'
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case single_add.inl
b x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ e'
a✝ : single e' y + f = f → eval b (single e' x + (single e' y + f)) = b ^ e' * x + eval b (single e' y + f)
⊢ eval b (single e' x + (single e' y + f)) = b ^ e' * x + eval b (single e' y + f)

Tactic:
simp only [← add_assoc, ← single_add, eval_single_add' _ hf, mul_add]

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

Goal state before:
pp: case refine_2
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : Small.{u, u + 1} ↑t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1 ⊆ s, t_1.Nonempty ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
⊢ ∀ (i : Shrink.{u, u + 1} ↑t), (Subtype.val ∘ ⇑(equivShrink ↑t).symm) i ∈ s

Tactic:
simpa [← (equivShrink t).forall_congr_left (p := (·.1 ∈ s))]

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

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

Tactic:
apply foldr_ext
    intro a ha x
    rw [coeff_of_mem_CNF ha]

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a : Ordinal.{u}
⊢ Monotone fun x ↦ veblenWith f x a

Tactic:
rw [monotone_iff_forall_lt]

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a : Ordinal.{u}
⊢ ∀ ⦃a_1 b : Ordinal.{u}⦄, a_1 < b → veblenWith f a_1 a ≤ veblenWith f b a
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: a b : Ordinal.{u}
h : a ≤ b
⊢ a = b → V_ a ⊆ V_ b

Tactic:
by simp_all

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

Goal state before:
pp: case neg
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
k0 : ¬k = 0
⊢ R < ω ^ (a0.repr * succ ↑k)

Tactic:
· rw [opow_mul]
      exact IH.1 k0

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

Goal state before:
pp: f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
this : (fun t ↦ f t ^ exp / f t ^ exp') =ᶠ[atTop] fun t ↦ f t ^ (exp - exp')
| fun t ↦ f t ^ (exp - exp')

Tactic:
show (fun t ↦ f t ^ (exp - exp')) = ((fun t ↦ t ^ (-(exp' - exp))) ∘ f) by ext; simp

Goal state after:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
this : (fun t ↦ f t ^ exp / f t ^ exp') =ᶠ[atTop] fun t ↦ f t ^ (exp - exp')
| (fun t ↦ t ^ (-(exp' - exp))) ∘ f
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
x y : α
s t : Stream'.Seq α
h : x ≠ y
⊢ dist (Seq.cons x s) (Seq.cons y t) = 1

Tactic:
by
  apply dist_eq_one_of_head
  simpa

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

Goal state before:
pp: case oadd.succ.e_a
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + ↑(k + 1)
⊢ (ω ^ a0.repr) ^ ↑k * (ω ^ a0.repr * ↑↑n + a'.repr) + (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ (k + 1)

Tactic:
← opow_natCast

Goal state after:
case oadd.succ.e_a
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + ↑(k + 1)
⊢ (ω ^ a0.repr) ^ ↑k * (ω ^ a0.repr * ↑↑n + a'.repr) + (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ ↑(k + 1)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case nil
basis : Basis
h_basis : WellFormedBasis basis
h_length : [].length = List.length basis
h_firstIsNeg : FirstNonzeroIsNeg []
⊢ Tendsto (toFun [] basis) atTop (𝓝 0)

Tactic:
simp at h_firstIsNeg

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
tl_tl : Multiseries basis_hd basis_tl
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq, x.2.Sorted
h_Pairwise✝ :
  Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq
h_all : ∀ x ∈ Multiseries.cons tl_exp tl_coef tl_tl, (exp, coef) > x
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (Multiseries.cons tl_exp tl_coef tl_tl)
x : ℝ × MultiseriesExpansion basis_tl
hx : x ∈ (mk (Multiseries.cons tl_exp tl_coef tl_tl) 0).seq
⊢ x ∈ (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq

Tactic:
by simp_all

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

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).Sorted
⊢ (Multiseries.cons exp coef tl).Sorted

Tactic:
by simpa using h

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f
h_approx : ms.Approximates
⊢ (ms.replaceFun f).Approximates

Tactic:
let motive (ms : MultiseriesExpansion (basis_hd :: basis_tl)) : Prop :=
      ∃ (ms' : MultiseriesExpansion (basis_hd :: basis_tl)) (f' : ℝ → ℝ),
      ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
  apply Approximates.coind motive ⟨ms, f, by grind⟩
  rintro _ ⟨ms, f, rfl, h_approx, h_eq⟩
  cases ms with
  | nil g =>
    simp only [nil_iff, mk_toFun, mk_replaceFun, mk_seq, true_and,
      Multiseries.nil_ne_cons, false_and, exists_const, or_false] at h_approx h_eq ⊢
    grw [← h_eq, h_approx]
  | cons exp coef tl g =>
    obtain ⟨h_coef, h_maj, h_tl⟩ := h_approx.elim_cons
    refine .inr ⟨exp, coef, tl, ?_⟩
    simp only [mk_replaceFun, mk_seq, h_coef, mk_toFun, true_and]
    simp only [mk_toFun] at h_eq
    refine ⟨h_maj.of_eventuallyEq h_eq.symm, mk tl (g - basis_hd ^ exp * coef.toFun), _, rfl,
      h_tl, ?_⟩
    grw [mk_toFun, h_eq]

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

Goal state before:
pp: b : ℕ
hb : (b / 2).beq 0 = false
⊢ jacobiSymNat 0 b = 0

Tactic:
rw [jacobiSymNat, Nat.cast_zero, jacobiSym.zero_left ?_]
  calc
    1 < 2 * 1       := by decide
    _ ≤ 2 * (b / 2) :=
      Nat.mul_le_mul_left _ (Nat.succ_le_of_lt (Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb)))
    _ ≤ b           := Nat.mul_div_le b 2

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs.length = ys.length
x y : α
i : ℕ
h₂ : xs[i]? = some x
⊢ applyId (xs.zip ys) x = y ↔ ys[i]? = some y

Tactic:
by
  induction xs generalizing ys i with
  | nil => cases h₂
  | cons x' xs xs_ih =>
    cases i
    · simp only [length_cons, lt_add_iff_pos_left, add_pos_iff, Nat.lt_add_one, or_true,
        getElem?_eq_getElem, getElem_cons_zero, Option.some.injEq] at h₂
      subst h₂
      cases ys
      · cases h₁
      · simp
    · cases ys
      · cases h₁
      · obtain - | ⟨h₀, h₁⟩ := h₀
        simp only [getElem?_cons_succ, zip_cons_cons, applyId_cons] at h₂ ⊢
        rw [if_neg]
        · apply xs_ih <;> solve_by_elim [Nat.succ.inj]
        · apply h₀; apply List.mem_of_getElem? h₂

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

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : X → Set X := fun x ↦ {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
i j : ι
hij : (i, j) ∈ ⋂ a ∈ A, {ij | (F ij.1 a, F ij.2 a) ∈ V}
x : X
⊢ (UniformFun.toFun (Prod.map F F (i, j)).1 x, UniformFun.toFun (Prod.map F F (i, j)).2 x) ∈ U

Tactic:
rw [mem_iInter₂] at hij

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : X → Set X := fun x ↦ {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
i j : ι
hij : ∀ i_1 ∈ A, (i, j) ∈ {ij | (F ij.1 i_1, F ij.2 i_1) ∈ V}
x : X
⊢ (UniformFun.toFun (Prod.map F F (i, j)).1 x, UniformFun.toFun (Prod.map F F (i, j)).2 x) ∈ U
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : X → Set X := fun x ↦ {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
this : ⋂ a ∈ A, {ij | (F ij.1 a, F ij.2 a) ∈ V} ⊆ Prod.map F F ⁻¹' UniformFun.gen X α U
⊢ Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α)

Tactic:
exact mem_of_superset
    (A.iInter_mem_sets.mpr fun x _ ↦ mem_iInf_of_mem x <| preimage_mem_comap hV) this

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

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

Tactic:
obtain ⟨y, hy⟩ : (interior (V • ({x} : Set X))).Nonempty := by
    rw [smul_assoc, interior_smul] at I
    exact smul_set_nonempty.1 I

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