mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
hF : Function.Surjective ⇑(_root_.frobenius (ModP R p) p)
this : Ideal.map (fontaineTheta R p) (span {↑p}) = 𝔭
x✝ : IsHausdorff (Ideal.map (fontaineTheta R p) (span {↑p})) R
⊢ Function.Surjective ⇑(fontaineTheta R p)

Tactic:
apply surjective_of_mk_map_comp_surjective (fontaineTheta R p) (I := span {(p : 𝕎 R♭)})

Goal state after:
R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
hF : Function.Surjective ⇑(_root_.frobenius (ModP R p) p)
this : Ideal.map (fontaineTheta R p) (span {↑p}) = 𝔭
x✝ : IsHausdorff (Ideal.map (fontaineTheta R p) (span {↑p})) R
⊢ Function.Surjective ⇑((Ideal.Quotient.mk (Ideal.map (fontaineTheta R p) (span {↑p}))).comp (fontaineTheta R p))
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝³ : CommRing R
inst✝² : CharP R p
inst✝¹ : PerfectRing R p
S : Type u_2
inst✝ : CommRing S
f g : 𝕎 R →+* S
h : ∀ (x : R), f ((teichmuller p) x) = g ((teichmuller p) x)
n : ℕ
hn : ↑p ^ n = 0
x c : 𝕎 R
hc : x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i = ↑p ^ (n + 1) * c
⊢ f (↑p ^ (n + 1) * c) + f (∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i) =
    ∑ i ≤ n, f ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i))) * ↑p ^ i

Tactic:
simp [pow_succ, hn]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝³ : CommRing R
inst✝² : CharP R p
inst✝¹ : PerfectRing R p
S : Type u_2
inst✝ : CommRing S
f g : 𝕎 R →+* S
h : ∀ (x : R), f ((teichmuller p) x) = g ((teichmuller p) x)
n : ℕ
hn : ↑p ^ n = 0
x c : 𝕎 R
hc : x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i = ↑p ^ (n + 1) * c
⊢ ∑ i ≤ n, g ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i))) * ↑p ^ i =
    g (↑p ^ (n + 1) * c) + g (∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i)

Tactic:
simp [pow_succ, hn]

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 : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
⊢ ((q * (-1) ^ rootMultiplicity 1 p).hilbertPoly (d - rootMultiplicity 1 p)).natDegree = d - rootMultiplicity 1 p - 1

Tactic:
← Nat.sub_add_cancel (Nat.le_sub_of_add_le' <| add_one_le_of_lt hpd)

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
⊢ ((q * (-1) ^ rootMultiplicity 1 p).hilbertPoly (d - rootMultiplicity 1 p - 1 + 1)).natDegree =
    d - rootMultiplicity 1 p - 1
Module: Mathlib.RingTheory.Polynomial.Morse

Goal state before:
pp: case pos
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
hp : (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ p)).ncard + 1
g : G
hg : g ∈ Ideal.inertia G p
hfp : map (algebraMap R (S ⧸ p)) f = 0
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap

Tactic:
rootSet_def f (S ⧸ p),

Goal state after:
case pos
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
hp : (f.rootSet S).ncard ≤ (↑(f.aroots (S ⧸ p)).toFinset).ncard + 1
g : G
hg : g ∈ Ideal.inertia G p
hfp : map (algebraMap R (S ⧸ p)) f = 0
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
r : R
| (expand p hp) (C r * 1)

Tactic:
← smul_eq_C_mul,

Goal state after:
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
r : R
| (expand p hp) (r • 1)
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
⊢ (Set.range fun n ↦ ↑(s.equivFin.symm n)) = ↑s

Tactic:
← Function.comp_def,

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
⊢ Set.range (Subtype.val ∘ ⇑s.equivFin.symm) = ↑s
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: case inr
z : ℤ
hz : z ≠ 0
p : ℤ
⊢ Prime p ∧ 0 ≤ p ∧ p ∣ z ↔ p ∈ Finset.map Nat.castEmbedding z.natAbs.primeFactors

Tactic:
Finset.mem_map,

Goal state after:
case inr
z : ℤ
hz : z ≠ 0
p : ℤ
⊢ Prime p ∧ 0 ≤ p ∧ p ∣ z ↔ ∃ a ∈ z.natAbs.primeFactors, Nat.castEmbedding a = p
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case inr
A : Type u_1
inst✝¹ : CommRing A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsHausdorff I A
hI : I ≠ ⊤
⊢ (↑g).IsWeierstrassDivisorAt I

Tactic:
exact H.isWeierstrassDivisorAt hI

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

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = ↑r
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
⊢ ∀ (i : ℕ), (coeff i) q ∈ I ^ (k + 1)

Tactic:
rw [g.eq_X_pow_mul_shift_add_trunc (g.map (Ideal.Quotient.mk I)).order.toNat] at heq

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq :
  ((X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
          mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) +
        ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g)) *
      q =
    ↑r
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
⊢ ∀ (i : ℕ), (coeff i) q ∈ I ^ (k + 1)
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 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p ∉ {(n, 0)}
⊢ p.1 < ((map (IsLocalRing.residue A)) g).order.toNat

Tactic:
refine (Finset.HasAntidiagonal.antidiagonal.fst_le hp).lt_of_ne ?_

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 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p ∉ {(n, 0)}
⊢ p.1 ≠ n
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : ¬p = q
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)

Tactic:
have lt : q < p := lt_of_le_of_ne qle (Ne.symm eq)
    have : (comap C p).IsMaximal := by simpa [max] using maximalIdeal.isMaximal R
    obtain ⟨y, _, hy⟩ := Polynomial.exists_monic_span_sup_map_eq R p this (by simpa [max])
    have peq : p = Ideal.span (((algebraMap R R[X]) '' (maximalIdeal R).generators) ∪ {y}) := by
      simp only [Set.union_comm, Ideal.span_union, ← Ideal.map_span, algebraMap_eq, sup_comm]
      nth_rw 1 [hy, max, ← (maximalIdeal R).span_generators]
    simp only [← Localization.AtPrime.map_eq_maximalIdeal, peq, Ideal.map_span]
    rw [← maximalIdeal_height_eq_ringKrullDim, ← IsLocalization.height_under p.primeCompl,
      IsLocalization.AtPrime.under_maximalIdeal _ p]
    apply le_trans _ (WithBot.coe_le_coe.mpr (Ideal.height_add_one_le_of_lt_of_isPrime lt))
    apply le_trans _ (WithBot.coe_le_coe.mpr (add_le_add_left ht 1))
    rw [WithBot.coe_add, maximalIdeal_height_eq_ringKrullDim, WithBot.coe_one, ← reg,
      ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le]
    have fin := (fg.image (algebraMap R R[X])).union (Set.finite_singleton y)
    apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite (fin.image _))
    apply le_trans (Set.ncard_image_le fin) (le_trans (Set.ncard_union_le _ _) _)
    rw [Set.ncard_singleton, add_le_add_iff_right, ← Submodule.FG.generators_ncard fg']
    exact Set.ncard_image_le fg

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : Ring R
x✝ : IsSimpleRing R ∧ IsArtinianRing R
left✝ : IsSimpleRing R
right✝ : IsArtinianRing R
⊢ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R

pp: case refine_2
R : Type u
inst✝ : Ring R
x✝ : IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R
left✝¹ : IsSemisimpleRing R
left✝ : IsIsotypic R R
right✝ : Nontrivial R
⊢ IsSimpleRing R ∧ IsArtinianRing R

Tactic:
on_goal 1 => have := IsSimpleRing.isSemisimpleRing_iff_isArtinianRing.mpr ‹_›

Goal state after:
case refine_1
R : Type u
inst✝ : Ring R
x✝ : IsSimpleRing R ∧ IsArtinianRing R
left✝ : IsSimpleRing R
right✝ : IsArtinianRing R
this : IsSemisimpleRing R
⊢ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R

case refine_2
R : Type u
inst✝ : Ring R
x✝ : IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R
left✝¹ : IsSemisimpleRing R
left✝ : IsIsotypic R R
right✝ : Nontrivial R
⊢ IsSimpleRing R ∧ IsArtinianRing R
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
⊢ Function.Injective (comap f)

Tactic:
intro q q' hqq'

Goal state after:
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
q q' : PrimeSpectrum S
hqq' : comap f q = comap f q'
⊢ q = q'
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R Γ : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
inst✝¹ : IsDomain R
inst✝ : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible 1
x✝¹ x✝ : R
⊢ x✝¹ ≤ᵥ x✝ ↔ x✝¹ ≤ᵥ x✝

Tactic:
change _ ↔ if _ = 0 then _ else _

Goal state after:
R Γ : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
inst✝¹ : IsDomain R
inst✝ : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible 1
x✝¹ x✝ : R
⊢ x✝¹ ≤ᵥ x✝ ↔ if x✝ = 0 then x✝¹ = 0 else True
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
⊢ Function.Surjective ⇑F₀

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

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

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

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

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.FixedPointApproximants

Goal state before:
pp: α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (succ #α).ord)
⊢ False

Tactic:
have h := lift_mk_le_lift_mk_of_injective <| injOn_iff_injective.1 h_inj

Goal state after:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (succ #α).ord)
h : lift.{u, u + 1} #↑(Iio (succ #α).ord) ≤ lift.{u + 1, u} #α
⊢ False
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1.antisymm.antisymm.right
α : 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₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
a₃ : Lists α
m₃ : a₃ ∈ l₂✝.toList
⊢ a₃ ∈ l₁

Tactic:
rcases Lists'.mem_of_subset' hr₂ m₃ with ⟨a₂, m₂, e₃₂⟩

Goal state after:
case C1.antisymm.antisymm.right
α : 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₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
a₃ : Lists α
m₃ : a₃ ∈ l₂✝.toList
a₂ : Lists α
m₂ : a₂ ∈ l₂✝¹.toList
e₃₂ : a₃ ~ a₂
⊢ a₃ ∈ l₁
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α true
⊢ sizeOf l₁ + sizeOf l₂ < sizeOf ⟨true, l₁⟩ + sizeOf ⟨true, l₂⟩

Tactic:
by
          decreasing_tactic

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α true
this : Decidable (l₁ ⊆ l₂)
⊢ sizeOf l₂ + sizeOf l₁ < sizeOf ⟨true, l₁⟩ + sizeOf ⟨true, l₂⟩

Tactic:
by
          decreasing_tactic

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
this : Decidable (⟨b, a⟩ ∈ l₂)
⊢ sizeOf l₁ + sizeOf l₂ < sizeOf (a.cons' l₁) + sizeOf l₂

Tactic:
by
          decreasing_tactic

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ sizeOf a + sizeOf l₂ < sizeOf a + sizeOf (b.cons' l₂)

Tactic:
by
          decreasing_tactic

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
⊢ ↑(f.nextFixed x hx) = ⨆ a, lfpApprox f x a

Tactic:
let o := (succ #α).ord

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u} := (succ #α).ord
⊢ ↑(f.nextFixed x hx) = ⨆ a, lfpApprox f x a
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
this : OrderHom.dual g ≤ OrderHom.dual f
⊢ gfpApprox f ≤ gfpApprox g

Tactic:
exact lfpApprox_mono_left this

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

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

Tactic:
exact lt_veblen_invVeblen₁ x

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

Goal state before:
pp: p : ZFSet.{u} → Prop
x : ZFSet.{u}
⊢ Hereditarily p x ↔ p x ∧ ∀ y ∈ x, Hereditarily p y

Tactic:
rw [← Hereditarily]

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

Goal state before:
pp: case refine_1.inr
o a x : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
⊢ veblen 0 (veblen o a) = ω ^ x → x.invVeblen₁ = o ∧ x.invVeblen₂ = a

Tactic:
veblen_zero_apply,

Goal state after:
case refine_1.inr
o a x : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
⊢ ω ^ veblen o a = ω ^ x → x.invVeblen₁ = o ∧ x.invVeblen₂ = a
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u}
h : veblen o 0 ≤ o
⊢ Γ_ 0 ≤ o

Tactic:
rw [gamma_zero_eq_nfp]

Goal state after:
o : Ordinal.{u}
h : veblen o 0 ≤ o
⊢ nfp (fun x ↦ veblen x 0) 0 ≤ o
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: n : ℕ
⊢ (fun a ↦ veblen a 0)^[n] 0 < Γ_ 0

Tactic:
rw [gamma_zero_eq_nfp]

Goal state after:
n : ℕ
⊢ (fun a ↦ veblen a 0)^[n] 0 < nfp (fun x ↦ veblen x 0) 0
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u}
h : o.invVeblen₁ = o
ho : ¬o = 0
| veblen 0 o

Tactic:
veblen_zero_apply,

Goal state after:
o : Ordinal.{u}
h : o.invVeblen₁ = o
ho : ¬o = 0
| ω ^ o
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: ⊢ ∅.classToCong = ∅

Tactic:
simp [classToCong]

Goal state after:
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
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr

Tactic:
simp only [repr]

Goal state after:
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
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (ω ^ e₁.repr * ↑↑n₁ + a₁.repr) * (ω ^ e₂.repr * ↑↑n₂ + a₂.repr)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case cons.nil
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl t : Stream'.Seq α
ht : op (Seq.cons s_hd s_tl) = t
ht0 : op (Seq.cons s_hd nil) = nil
this : nil.head = t.head
⊢ t.destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s_tl))
      (match nil.destruct with
      | none => none
      | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))

Tactic:
cases t with

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

Goal state before:
pp: case cons.cons
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl t : Stream'.Seq α
ht : op (Seq.cons s_hd s_tl) = t
x✝ : α
s✝ : Stream'.Seq α
ht0 : op (Seq.cons s_hd nil) = Seq.cons x✝ s✝
this : (Seq.cons x✝ s✝).head = t.head
⊢ t.destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s_tl))
      (match (Seq.cons x✝ s✝).destruct with
      | none => none
      | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))

Tactic:
cases t with

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

Goal state before:
pp: case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : (Multiseries.cons exp coef tl).Sorted
⊢ (Multiseries.cons exp coef tl).tail.Sorted

Tactic:
simpa using h.elim_cons.right.right

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

Goal state before:
pp: left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_coef2 : { coef := coef2, unit := exps2 }.coef ≠ 0
h_lt : t1.unit < List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit
⊢ t1.toFun (left ++ right) =o[atTop] { coef := coef2, unit := exps2 }.toFun right

Tactic:
let t2' : Monomial := ⟨coef2, List.replicate left.length 0 ++ exps2⟩

Goal state after:
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_coef2 : { coef := coef2, unit := exps2 }.coef ≠ 0
h_lt : t1.unit < List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit
t2' : Monomial := { coef := coef2, unit := List.replicate (List.length left) 0 ++ exps2 }
⊢ t1.toFun (left ++ right) =o[atTop] { coef := coef2, unit := exps2 }.toFun right
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
⊢ { coef := coef2, unit := exps2 }.toFun right =o[atTop] t1.toFun (left ++ right)

Tactic:
let t2' : Monomial := ⟨coef2, List.replicate left.length 0 ++ exps2⟩

Goal state after:
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := { coef := coef2, unit := List.replicate (List.length left) 0 ++ exps2 }
⊢ { coef := coef2, unit := exps2 }.toFun right =o[atTop] t1.toFun (left ++ right)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inr
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
f : ℕ → ONote
e : b.fundamentalSequence = Sum.inr f
h1 : IsSuccLimit b.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < b ∧ (b.NF → (f i).NF)
h3 : ∀ a < b.repr, ∃ i, a < (f i).repr
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m (f i) < a.oadd m (f (i + 1)) ∧ a.oadd m (f i) < a.oadd m b ∧ ((a.oadd m b).NF → (a.oadd m (f i)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a.oadd m (f i)).repr

Tactic:
simp only [repr]

Goal state after:
case oadd.inr
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
f : ℕ → ONote
e : b.fundamentalSequence = Sum.inr f
h1 : IsSuccLimit b.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < b ∧ (b.NF → (f i).NF)
h3 : ∀ a < b.repr, ∃ i, a < (f i).repr
⊢ IsSuccLimit (ω ^ a.repr * ↑↑m + b.repr) ∧
    (∀ (i : ℕ),
        a.oadd m (f i) < a.oadd m (f (i + 1)) ∧ a.oadd m (f i) < a.oadd m b ∧ ((a.oadd m b).NF → (a.oadd m (f i)).NF)) ∧
      ∀ a_1 < ω ^ a.repr * ↑↑m + b.repr, ∃ i, a_1 < ω ^ a.repr * ↑↑m + (f i).repr
Module: Mathlib.Tactic.NormNum.IsCoprime

Goal state before:
pp: x y : ℤ
d : ℕ
hd : x.gcd y = d
h : d.beq 1 = false
⊢ ¬x.gcd y = 1

Tactic:
hd

Goal state after:
x y : ℤ
d : ℕ
hd : x.gcd y = d
h : d.beq 1 = false
⊢ ¬d = 1
Module: Mathlib.Tactic.NormNum.NatSqrt

Goal state before:
pp: x y r : ℕ
hr : y * y + r = x
hle : r.ble (y + y) = true
⊢ (y ^ 2 + r).sqrt = y

Tactic:
exact Nat.sqrt_add_eq' _ (Nat.le_of_ble_eq_true hle)

Goal state after: