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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
hroots : (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}
⊢ b = -a * (x1 + x2)

Tactic:
let p : R[X] := C a * X ^ 2 + C b * X + C c
  have hp_natDegree : p.natDegree = 2 := le_antisymm natDegree_quadratic_le
    (by convert! p.card_roots'; rw [hroots, Multiset.card_pair])
  have hp_roots_card : p.roots.card = p.natDegree := by
    rw [hp_natDegree, hroots, Multiset.card_pair]
  simpa [leadingCoeff, hp_natDegree, p, hroots, mul_assoc, add_comm x1] using
    coeff_eq_esymm_roots_of_card hp_roots_card (k := 1) (by simp [hp_natDegree])

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

Goal state before:
pp: n : ℕ
⊢ (coeff n) catalanSeries = catalan n

Tactic:
by
  simp [catalanSeries]

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

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
c : ℝ
f : R⟦X⟧
⊢ Tendsto (fun t ↦ ‖(MvPowerSeries.coeff t) f‖ * t.prod fun x1 x2 ↦ c ^ x2) cofinite (𝓝 0) ↔
    Tendsto (fun t ↦ ‖(coeff t) f‖ * c ^ t) cofinite (𝓝 0)

Tactic:
isRestricted_comp_uniqueEquiv

Goal state after:
R : Type u_1
inst✝ : NormedRing R
c : ℝ
f : R⟦X⟧
⊢ Tendsto ((fun n ↦ ‖(coeff n) f‖ * c ^ n) ∘ ⇑(Finsupp.uniqueEquiv ())) cofinite (𝓝 0) ↔
    Tendsto (fun t ↦ ‖(coeff t) f‖ * c ^ t) cofinite (𝓝 0)
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
x : ℕ
a : x < n
h : ¬0 < x
⊢ (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder = 0

Tactic:
simp_all only [not_lt, nonpos_iff_eq_zero, coeff_zero_eq_constantCoeff, map_mul,
      constantCoeff_X, constantCoeff_largeSchroderSeries, mul_one, tsub_zero, zero_mul]

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: case inr
z : ℤ
hz : z ≠ 0
⊢ primeFactors z = Finset.map Nat.castEmbedding z.natAbs.primeFactors

Tactic:
ext p

Goal state after:
case inr
z : ℤ
hz : z ≠ 0
p : ℤ
⊢ p ∈ primeFactors z ↔ p ∈ Finset.map Nat.castEmbedding z.natAbs.primeFactors
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case eq_mul_add
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
inst✝ : IsAdicComplete I A
hI : I ≠ ⊤
i : ℕ
⊢ (coeff i) (f - g * H.div f) = (coeff i) ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) (f - g * H.div f))

Tactic:
rw [Polynomial.coeff_coe, coeff_trunc]

Goal state after:
case eq_mul_add
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
inst✝ : IsAdicComplete I A
hI : I ≠ ⊤
i : ℕ
⊢ (coeff i) (f - g * H.div f) =
    if i < ((map (Ideal.Quotient.mk I)) g).order.toNat then (coeff i) (f - g * H.div f) else 0
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
inst✝ : IsAdicComplete I A
hI : I ≠ ⊤
i : ℕ
hi : ¬i < ((map (Ideal.Quotient.mk I)) g).order.toNat
k : ℕ
⊢ (coeff i) (f - g * H.div f) ≡ 0 [SMOD I ^ k • ⊤]

Tactic:
rw [SModEq.zero, smul_eq_mul, Ideal.mul_top, show f - g * H.div f =
      f - g * (H.seq f k) - g * (H.div f - (H.seq f k)) by ring, map_sub]

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
inst✝ : IsAdicComplete I A
hI : I ≠ ⊤
i : ℕ
hi : ¬i < ((map (Ideal.Quotient.mk I)) g).order.toNat
k : ℕ
⊢ (coeff i) (f - g * H.seq f k) - (coeff i) (g * (H.div f - H.seq f k)) ∈ I ^ k
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
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
S : Type v
inst✝³ : CommSemiring S
inst✝² : Algebra R S
f : M →ₚₗ[R] N
T : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
h' : ↥(φ R s).range →ₐ[R] ↥(φ R s').range := (h.comp (φ R s).range.val).codRestrict (φ R s').range ⋯
j : Fin s.card → Fin s'.card :=
  ⇑s'.equivFin ∘
    (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨h x, ⋯⟩) ∘
      ⇑s.equivFin.symm
⊢ (φ R s').comp (rename j) = h.comp (φ R s)

Tactic:
ext p

Goal state after:
R : Type u
inst✝⁸ : CommSemiring R
M : Type u_1
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
S : Type v
inst✝³ : CommSemiring S
inst✝² : Algebra R S
f : M →ₚₗ[R] N
T : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p✝ : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p✝⟩ = t
s' : Finset T := Finset.image (⇑h) s
h' : ↥(φ R s).range →ₐ[R] ↥(φ R s').range := (h.comp (φ R s).range.val).codRestrict (φ R s').range ⋯
j : Fin s.card → Fin s'.card :=
  ⇑s'.equivFin ∘
    (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨h x, ⋯⟩) ∘
      ⇑s.equivFin.symm
p : Fin s.card
⊢ ((φ R s').comp (rename j)) (X p) = (h.comp (φ R s)) (X p)
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
hx : x ∈ f.ker ⊓ I • ⊤
y : TensorProduct R (↥I) M
hy : (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) y = x
inj : Function.Injective ⇑(↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I))
comm1 :
  (↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I)) ∘ₗ lTensor (↥I) f =
    f ∘ₗ ↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)
eq0 : (lTensor (↥I) f) y = 0
z : TensorProduct R ↥I ↥f.ker
hz : (lTensor (↥I) f.ker.subtype) z = y
comm2 :
  (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) ∘ₗ lTensor (↥I) f.ker.subtype =
    f.ker.subtype ∘ₗ ↑(TensorProduct.lid R ↥f.ker) ∘ₗ rTensor (↥f.ker) (Submodule.subtype I)
⊢ ⟨x, ⋯⟩ ∈ I • ⊤

Tactic:
← Ideal.subtype_rTensor_range

Goal state after:
case refine_1
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
hx : x ∈ f.ker ⊓ I • ⊤
y : TensorProduct R (↥I) M
hy : (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) y = x
inj : Function.Injective ⇑(↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I))
comm1 :
  (↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I)) ∘ₗ lTensor (↥I) f =
    f ∘ₗ ↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)
eq0 : (lTensor (↥I) f) y = 0
z : TensorProduct R ↥I ↥f.ker
hz : (lTensor (↥I) f.ker.subtype) z = y
comm2 :
  (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) ∘ₗ lTensor (↥I) f.ker.subtype =
    f.ker.subtype ∘ₗ ↑(TensorProduct.lid R ↥f.ker) ∘ₗ rTensor (↥f.ker) (Submodule.subtype I)
⊢ ⟨x, ⋯⟩ ∈ (↑(TensorProduct.lid R ↥f.ker) ∘ₗ rTensor (↥f.ker) (Submodule.subtype I)).range
Module: Mathlib.RingTheory.Valuation.Quotient

Goal state before:
pp: case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ Ideal.map (Ideal.Quotient.mk J) v.supp ≤ (v.onQuot hJ).supp

Tactic:
rw [Ideal.map_le_iff_le_comap]
    intro x hx
    exact hx

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

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ (v.onQuot ⋯).supp = 0

Tactic:
by
  rw [supp_quot]
  exact Ideal.map_quotient_self _

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
x : 𝕎 k
hx : x.coeff 0 ≠ 0
y : kˣ := Units.mk0 (x.coeff 0) hx
hy : x.coeff 0 = ↑y
⊢ IsUnit x

Tactic:
exact (mkUnit hy).isUnit

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

Goal state before:
pp: case refine_1.ind
o : Ordinal.{u_1}
ih : ∀ y < o, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
h : o₁ + o₂ = o
⊢ ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂

Tactic:
| ind o ih
     => 

Goal state after:
case refine_1.ind
o : Ordinal.{u_1}
ih : ∀ y < o, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
h : o₁ + o₂ = o
⊢ ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
Module: Mathlib.SetTheory.Ordinal.Commute

Goal state before:
pp: case refine_1
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
⊢ ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂

Tactic:
induction h : o₁ + o₂ using WellFoundedLT.induction generalizing o₁ o₂ with | ind o ih

Goal state after:
case refine_1.ind
o : Ordinal.{u_1}
ih : ∀ y < o, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
h : o₁ + o₂ = o
⊢ ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_1
b o : Ordinal.{u_1}
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b 0))

pp: case refine_2
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
· rw [zero_right]
    exact .nil

Goal state after:
case refine_2
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1.antisymm.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' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
⊢ of' l₁ ~ ⟨true, l₂✝⟩

Tactic:
obtain ⟨hl₁, hr₁⟩ := Equiv.antisymm_iff.1 h₁

Goal state after:
case C1.antisymm.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' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
⊢ of' l₁ ~ ⟨true, l₂✝⟩
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
a : Ordinal.{u_1}
H : a ∈ map Prod.fst (CNF b (o % b ^ log b o))
⊢ (log b o, o / b ^ log b o).1 > a

Tactic:
rw [mem_map] at H

Goal state after:
case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
a : Ordinal.{u_1}
H : ∃ a_1 ∈ CNF b (o % b ^ log b o), a_1.1 = a
⊢ (log b o, o / b ^ log b o).1 > a
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ ∀ (e' : Ordinal.{u_1}), f e' < b

Tactic:
intro a
      by_cases ha : a ∈ f.support
      · apply (hb a).trans_eq'
        rw [add_apply, single_eq_of_ne, zero_add]
        rintro rfl
        contradiction
      · rw [notMem_support_iff.1 ha]
        exact (hb 0).pos

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

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

Tactic:
← veblen_zero_apply,

Goal state after:
case a.inr
o a : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
⊢ veblen 0 (veblen o a) ∈ range (veblen o)
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
← veblen_zero_apply,

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

Goal state before:
pp: o a : Ordinal.{u}
ho : o ≠ 0
h : a < veblen o a
⊢ ω ^ veblen o a = veblen o a

Tactic:
← veblen_zero_apply,

Goal state after:
o a : Ordinal.{u}
ho : o ≠ 0
h : a < veblen o a
⊢ veblen 0 (veblen o a) = veblen o a
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: x y : ZFSet.{u}
h : ↑x = ↑y
z : ZFSet.{u}
⊢ z ∈ x ↔ z ∈ y

Tactic:
by
    change (x : Class.{u}) z ↔ (y : Class.{u}) z
    rw [h]

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

Goal state before:
pp: x : ZFSet.{u}
⊢ x.IsTransitive ↔ ⋃₀ x ⊆ x

Tactic:
by
  constructor <;>
  intro h y hy
  · obtain ⟨z, hz, hz'⟩ := mem_sUnion.1 hy
    exact h.mem_trans hz' hz
  · exact fun z hz ↦ h <| mem_sUnion_of_mem hz hy

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

Goal state before:
pp: A : Type u_2
sA : CommSemiring A
a₁ a₂ b₁ b₂ : A
ha₁ : a₁ = 0
ha₂ : a₂ = b₁ + b₂
⊢ a₁ + a₂ = b₁ + b₂

Tactic:
by
  subst_vars
  simp

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

Goal state before:
pp: A : Type u_2
sA : CommSemiring A
a₁ a₂ b₁ b₂ : A
hb₁ : b₁ = 0
ha : a₁ + a₂ = b₂
⊢ a₁ + a₂ = b₁ + b₂

Tactic:
by
  subst_vars
  simp

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

Goal state before:
pp: e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ b ≤ (ω ^ e.repr) ^ ω

Tactic:
apply (opow_le_opow_left b <| this.le).trans

Goal state after:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
⊢ (ω ^ succ e.repr) ^ b ≤ (ω ^ e.repr) ^ ω
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
s t : Stream'.Seq α
h : dist s t ≤ 2⁻¹
⊢ s = nil ∧ t = nil ∨ ∃ hd s' t', s = Seq.cons hd s' ∧ t = Seq.cons hd t'

Tactic:
cases s <;> cases t <;> norm_num at h

Goal state after:
case nil.nil
α : Type u_1
h : True
⊢ nil = nil ∧ nil = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ nil = Seq.cons hd t'

case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) ≤ 1 / 2
⊢ Seq.cons x✝¹ s✝¹ = nil ∧ Seq.cons x✝ s✝ = nil ∨
    ∃ hd s' t', Seq.cons x✝¹ s✝¹ = Seq.cons hd s' ∧ Seq.cons x✝ s✝ = Seq.cons hd t'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: case insert
basis basis✝ : Basis
f✝ : ℝ → ℝ
ex : BasisExtension basis✝
ih : List.Sublist basis✝ ex.getBasis
⊢ List.Sublist basis✝ (insert f✝ ex).getBasis

Tactic:
exact List.Sublist.cons _ ih

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

Goal state before:
pp: basis : Basis
⊢ toFun [] basis = 1

Tactic:
by
  ext x
  simp [toFun]

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

Goal state before:
pp: m : UnitMonomial
⊢ m.toFun [] = 1

Tactic:
by
  ext x
  simp [toFun]

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

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

Tactic:
by
  ext x
  simp [toFun]

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

Goal state before:
pp: m1 m2 : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length m1 = List.length m2
x : ℝ
h_pos : ∀ f ∈ basis, 0 < f x
⊢ (m1.mul m2).toFun basis x = (m1.toFun basis * m2.toFun basis) x

Tactic:
simp only [toFun, mul, Pi.mul_apply]

Goal state after:
m1 m2 : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length m1 = List.length m2
x : ℝ
h_pos : ∀ f ∈ basis, 0 < f x
⊢ (List.zipWith (fun exp b ↦ b x ^ exp) (List.zipWith (fun x1 x2 ↦ x1 + x2) m1 m2) basis).prod =
    (List.zipWith (fun exp b ↦ b x ^ exp) m1 basis).prod * (List.zipWith (fun exp b ↦ b x ^ exp) m2 basis).prod
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
exp : ℝ
coef : MultiseriesExpansion basis_tl
c : γ
next : β
h : F b = some (exp, coef, c, next)
⊢ Seq.cons ?m.36
      (op ?m.37
        (Seq.gcorec
          (fun a ↦
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, c, next) => ((exp, coef), c, next))
              (F a))
          op ?m.38)) =
    cons exp coef
      (op c
        (Seq.gcorec
          (fun a ↦
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, c, next) => ((exp, coef), c, next))
              (F a))
          op next))

Tactic:
simp [cons]

Goal state after:
β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
exp : ℝ
coef : MultiseriesExpansion basis_tl
c : γ
next : β
h : F b = some (exp, coef, c, next)
⊢ Seq.cons ?m.36 (op ?m.37 (Seq.gcorec (fun a ↦ Option.map (fun x ↦ ((x.1, x.2.1), x.2.2)) (F a)) op ?m.38)) =
    Seq.cons (exp, coef) (op c (Seq.gcorec (fun a ↦ Option.map (fun x ↦ ((x.1, x.2.1), x.2.2)) (F a)) op next))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
basis : Basis
⊢ { coef := coef, unit := [] }.toFun basis = fun x ↦ coef

Tactic:
by
  ext x
  simp [toFun]

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ ms.Approximates

Tactic:
by
  apply coinduct fun {basis} ms =>
    ms.Approximates ∨ ∃ (h_basis : basis = basis_hd :: basis_tl), (motive (h_basis ▸ ms))
  · rintro basis ms (h_ms | ⟨rfl, h_ms⟩)
    · cases h_ms <;> grind
    simp only [reduceCtorEq, List.cons.injEq, ↓existsAndEq, and_true, heq_eq_eq, ms_eq_mk_iff,
      true_and, exists_eq_right_right', exists_and_left, false_or] at h_ms ⊢
    rcases h_step _ h_ms with h_step | ⟨exp, coef, tl, h_seq, h_coef, h_maj, h_tl⟩
    · grind
    · refine .inr ⟨basis_hd, ms.toFun, basis_tl, exp, coef, by simpa, ‹_›, tl, ?_⟩
      simp
      grind
  · grind

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

Goal state before:
pp: a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
⊢ a = y

Tactic:
apply Nat.dvd_antisymm
  · exact eq_of_mul_eq_mul_of_coprime_aux hab h
  · exact eq_of_mul_eq_mul_of_coprime_aux (x := b) hxy.symm (by rw [mul_comm, ← h, mul_comm])

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

Goal state before:
pp: a b ab : ℕ
r : ℤ
hab : a % b = ab
hr : jacobiSymNat ab b = r
⊢ jacobiSymNat a b = r

Tactic:
rw [← hr, jacobiSymNat, jacobiSymNat, _root_.jacobiSym.mod_left a b, ← hab]; rfl

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

Goal state before:
pp: a m : ℕ
⊢ (a.pow 1).mod m = a.mod m

Tactic:
rw [natPow_one]

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

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

Tactic:
symm; rw [h]
      rw [← List.applyId_zip_eq] <;> assumption

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
⊢ Injective (mapToSelf xs hperm hnodup).apply

Tactic:
generalize h₁ : xs.map (@id ((Σ _ : α, α) → α) <| @Sigma.snd α fun _ : α => α) = xs₁

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map (id Sigma.snd) xs = xs₁
⊢ Injective (mapToSelf xs hperm hnodup).apply
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}
this✝ : Nonempty X
this : Encodable ↑s
h : G
n : ℕ
hn : h ∈ K n
g : G
gs : g ∈ s
hg : h ∈ g • V
⊢ h • x ∈ ⋃ i, F i

Tactic:
simp only [F, smul_singleton, mem_iUnion, mem_image, mem_inter_iff, Prod.exists,
        Subtype.exists, exists_prop]

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}
this✝ : Nonempty X
this : Encodable ↑s
h : G
n : ℕ
hn : h ∈ K n
g : G
gs : g ∈ s
hg : h ∈ g • V
⊢ ∃ a, ∃ a_1 ∈ s, ∃ x_1, (x_1 ∈ K a ∧ x_1 ∈ a_1 • V) ∧ x_1 • x = h • x
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
⊢ Continuous ⇑WithGeneratedByTopology.equiv.symm

Tactic:
by
    rw [continuous_def]
    intro U hU
    rw [WithGeneratedByTopology.isOpen_iff] at hU ⊢
    intro i f
    refine hU ⟨WithGeneratedByTopology.equiv.symm ∘ f, ?_⟩
    rw [continuous_iff X]
    intro j g
    rw [Function.comp_assoc, 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)
a b : ↑C
i : ι
h : (π_app C fun x ↦ x ∈ {i}) a = (π_app C fun x ↦ x ∈ {i}) b
⊢ ↑a i = ↑b i

Tactic:
Subtype.ext_iff

Goal state after:
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : ↑C
i : ι
h : ↑((π_app C fun x ↦ x ∈ {i}) a) = ↑((π_app C fun x ↦ x ∈ {i}) b)
⊢ ↑a i = ↑b i