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

Goal state before:
pp: case neg
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
m n k : ℕ
hk : (coeff k) (f + g) ≠ 0
hm : (Perfection.coeff (ModP O p) p (max (max m n) k)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max (max m n) k)) g ≠ 0
⊢ valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)

Tactic:
replace hk := coeff_ne_zero_of_le hk (le_max_right (max m n) k)

Goal state after:
case neg
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
m n k : ℕ
hm : (Perfection.coeff (ModP O p) p (max (max m n) k)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max (max m n) k)) g ≠ 0
hk : (Perfection.coeff (ModP O p) p (max (max m n) k)) (f + g) ≠ 0
⊢ valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case succ.zero
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
hnk : Odd (n + 1 + 0)
⊢ (hermite (n + 1)).coeff 0 = 0

Tactic:
rw [Nat.succ_add_eq_add_succ] at hnk
      rw [coeff_hermite_succ_zero, ih hnk, neg_zero]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Semiring A
I : Ideal A
f g : A⟦X⟧
n : ℕ
inst✝ : I.IsTwoSided
hf : ∀ i ≤ n, (coeff i) f ∈ I
⊢ ∀ i ≤ n, (coeff i) (f * g) ∈ I

Tactic:
by
  simpa only [Ideal.IsTwoSided.mul_one] using
    coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal (J := 1) (g := g) n hf (by simp)

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

Goal state before:
pp: n k : ℕ
hk : k ≠ 0
⊢ radical n ∣ k ↔ n.primeFactors ⊆ k.primeFactors

Tactic:
rw [radical_eq_prod_primeFactors, prod_primeFactors_dvd_iff hk]

Goal state after:
Module: Mathlib.RingTheory.Regular.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : Module S N
inst✝⁵ : IsScalarTower R S N
p : Ideal R
inst✝⁴ : p.IsPrime
inst✝³ : IsLocalization.AtPrime S p
inst✝² : Nontrivial N
inst✝¹ : Module.Finite S N
f : M →ₗ[R] N
inst✝ : IsLocalizedModule.AtPrime p f
rs : List R
reg : IsWeaklyRegular M rs
mem : ∀ r ∈ rs, r ∈ p
this : IsLocalRing S
x✝ : S
hr✝ : x✝ ∈ List.map (⇑(algebraMap R S)) rs
r : R
hr : r ∈ rs
eq : (algebraMap R S) r = x✝
⊢ x✝ ∈ IsLocalRing.maximalIdeal S

Tactic:
simpa only [← eq, IsLocalization.AtPrime.to_map_mem_maximal_iff S p] using mem r hr

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
a : A
⊢ a • f = g * a • q + ↑(a • r)

Tactic:
simp [H.eq_mul_add, Algebra.smul_def, mul_add, mul_left_comm]

Goal state after:
Module: Mathlib.RingTheory.Regular.Free

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
⊢ Free R M

Tactic:
have kerf : LinearMap.ker f = x • (⊤ : Submodule R (I →₀ R)) := by
    simp only [LinearEquiv.ker_comp, f]
    rw [Finsupp.ker_mapRange, Submodule.ker_mkQ, ← (Ideal.span {x}).mul_top, ← smul_eq_mul,
      Finsupp.submodule_smul]
    simp [Submodule.ideal_span_singleton_smul]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
kerf : f.ker = x • ⊤
⊢ Free R M
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
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) ↑r ∈ I ^ (k + 1)

Tactic:
rcases lt_or_ge i (g.map (Ideal.Quotient.mk I)).order.toNat with hi | hi

Goal state after:
case inl
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 : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
⊢ (coeff i) ↑r ∈ I ^ (k + 1)

case inr
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 : ℕ
hi : ((map (Ideal.Quotient.mk I)) g).order.toNat ≤ i
⊢ (coeff i) ↑r ∈ I ^ (k + 1)
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
w✝⁴ : Type v
w✝³ : AddCommGroup w✝⁴
w✝² : Module R w✝⁴
w✝¹ : Free R w✝⁴
w✝ : Module.Finite R w✝⁴
f : w✝⁴ →ₗ[R] ↑M
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := f.shortComplexKer
hS : S.ShortExact
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L 0)) → HasProjectiveDimensionLT M 0
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (0 + 1))
⊢ HasProjectiveDimensionLT M (0 + 1)

Tactic:
simp only [zero_add, ← projective_iff_hasProjectiveDimensionLT_one]

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
w✝⁴ : Type v
w✝³ : AddCommGroup w✝⁴
w✝² : Module R w✝⁴
w✝¹ : Free R w✝⁴
w✝ : Module.Finite R w✝⁴
f : w✝⁴ →ₗ[R] ↑M
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := f.shortComplexKer
hS : S.ShortExact
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L 0)) → HasProjectiveDimensionLT M 0
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (0 + 1))
⊢ CategoryTheory.Projective M
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Small.{v, u} R
inst✝³ : IsLocalRing R
inst✝² : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Nontrivial ↑M] [Module.Finite R ↑M] (rs : List R),
    IsWeaklyRegular (↑M) rs →
      (∀ r ∈ rs, r ∈ maximalIdeal R) →
        rs.length = n → projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑n
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : Module.Finite R ↑M
rs : List R
x : R
rs' : List R
reg : IsWeaklyRegular (↑M) (x :: rs')
mem : ∀ r ∈ x :: rs', r ∈ maximalIdeal R
len : (x :: rs').length = n + 1
⊢ projectiveDimension (of R (↑M ⧸ Ideal.ofList (x :: rs') • ⊤)) = projectiveDimension M + ↑(n + 1)

Tactic:
simp only [List.mem_cons, forall_eq_or_imp] at mem
      simp only [isWeaklyRegular_cons_iff] at reg
      have := nontrivial_quotSMulTop_of_mem_maximalIdeal M mem.1
      simp only [List.length_cons, Nat.add_right_cancel_iff] at len
      rw [Nat.cast_add, Nat.cast_one, projectiveDimension_eq_of_iso
        (Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner M x rs').toModuleIso, add_comm _ 1,
        ← add_assoc, ← projectiveDimension_quotSMulTop_eq_succ_of_isSMulRegular M x reg.1 mem.1,
        ← hn (ModuleCat.of R (QuotSMulTop x M)) rs' reg.2 mem.2 len]

Goal state after:
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)}
⊢ 0 * (coeff p.2) ((map (IsLocalRing.residue A)) q) = 0

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

Tactic:
· rw [zero_mul]

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 < ((map (IsLocalRing.residue A)) g).order
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: 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))) *
      ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, 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)) +
        ↑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)) +
      remainder p n

Tactic:
conv_lhs =>
    arg 1
    rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]

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)) +
        ↑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)) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, 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)) +
        ↑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)) +
      remainder p n
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

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

Tactic:
by
  cases isEmpty_or_nonempty α; · simp
  cases topOrderOrNoTopOrder α
  · exact .sInter_of_orderTop hs
  · cases one_lt_cof.not_ge hα

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

Goal state before:
pp: case inr.refine_1
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
s : Set α
hs : s ⊆ Function.fixedPoints f
hs₀ : s.Nonempty
x✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
⊢ IsLUB ((fun a ↦ a) '' s) a

Tactic:
image_id'

Goal state after:
case inr.refine_1
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
s : Set α
hs : s ⊆ Function.fixedPoints f
hs₀ : s.Nonempty
x✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
⊢ IsLUB s a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case refine_1
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ IsClub (⋂ x, f ↑x ⋯)

pp: case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ Disjoint (⋃₀ s) (⋂ x, f ↑x ⋯)

Tactic:
· apply IsClub.iInter_of_cof_le_one hα
      simpa

Goal state after:
case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ Disjoint (⋃₀ s) (⋂ x, f ↑x ⋯)
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b✝ : Ordinal.{u}
hf : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, a ≤ y → lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
⊢ x ⊔ ⨆ b_1, ⨆ (_ : b_1 < b), f (lfpApprox f x b_1) ≤ lfpApprox f x a

Tactic:
apply sup_le (le_lfpApprox ..)

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b✝ : Ordinal.{u}
hf : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, a ≤ y → lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
⊢ ⨆ b_1, ⨆ (_ : b_1 < b), f (lfpApprox f x b_1) ≤ lfpApprox f x a
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C0
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : α
l₂ l₃ : Lists α
h₁ : atom a ~ l₂
⊢ l₂ ~ l₃ → atom a ~ l₃

Tactic:
h₂

Goal state after:
case C0
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : α
l₂ l₃ : Lists α
h₁ : atom a ~ l₂
h₂ : l₂ ~ l₃
⊢ atom a ~ l₃
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₂
⊢ l₂ ~ l₃ → of' l₁ ~ l₃

Tactic:
h₂

Goal state after:
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₃
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case h.right
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ lfpApprox f x ↑a = lfpApprox f x ↑b

Tactic:
exact h_fab

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

Goal state before:
pp: b o e : Ordinal.{u_1}
h : e ∉ map Prod.fst (CNF b o)
⊢ e ∉ (map Prod.fst (CNF b o)).toFinset

Tactic:
mem_toFinset

Goal state after:
b o e : Ordinal.{u_1}
h : e ∉ map Prod.fst (CNF b o)
⊢ e ∉ map Prod.fst (CNF b o)
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
  have hfix : lfpApprox f x o ∈ fixedPoints f :=
    lfpApprox_ord_mem_fixedPoint f hx
  rw [iSup_lfpApprox_eq_of_mem_fixedPoints f hfix]
  apply le_antisymm
  · exact f.nextFixed_le hx (y := ⟨lfpApprox f x o, hfix⟩) (le_lfpApprox f)
  · exact lfpApprox_le_of_mem_fixedPoints f (f.nextFixed x hx).2 (f.le_nextFixed hx) o

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

Goal state before:
pp: case refine_3
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, (Subtype.val ∘ ⇑(equivShrink ↑t).symm) i = sSup t

Tactic:
simp [(equivShrink t).symm.iSup_comp, ← sSup_eq_iSup']

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

Goal state before:
pp: x y : ZFSet.{u}
⊢ (x ∪ y).card ≤ x.card + y.card

Tactic:
by
  rw [← lift_le.{u + 1}]
  simpa [← cardinalMk_coe_sort] using! mk_union_le (x : Set ZFSet) y

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

Goal state before:
pp: case mk.mk
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c✝ : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, (Γ a).Equiv (Δ b)
δγ : ∀ (b : δ), ∃ a, (Γ a).Equiv (Δ b)
c : (A a).Type := c✝
d : δ
hd : (Γ (⋯.mp c)).Equiv (Δ d)
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)

Tactic:
use ⟨b, Eq.ndrec d (Eq.symm eb)⟩

Goal state after:
case h
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c✝ : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, (Γ a).Equiv (Δ b)
δγ : ∀ (b : δ), ∃ a, (Γ a).Equiv (Δ b)
c : (A a).Type := c✝
d : δ
hd : (Γ (⋯.mp c)).Equiv (Δ d)
⊢ ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func ⟨b, ⋯ ▸ d⟩)
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (range f).rank = ⨆ i, succ (f i).rank

Tactic:
apply (Ordinal.iSup_le _).antisymm'

Goal state after:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (range f).rank ≤ ⨆ i, succ (f i).rank

α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ∀ (i : α), succ (f i).rank ≤ (range f).rank
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: x y z : Class.{u_1}
hy : y ∈ ⋂₀ x
hz : z ∈ x
⊢ y ∈ z

Tactic:
obtain ⟨w, rfl, hw⟩ := hy
  exact coe_mem.2 (hw z hz)

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

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

Tactic:
← ZFSet.eq,

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a.toZFSet ⊆ b.toZFSet ↔ a ≤ b

Tactic:
by
  refine ⟨?_, fun h ↦ toZFSet_monotone h⟩
  contrapose!
  exact fun h ↦ not_subset_of_mem (toZFSet_mem_toZFSet_of_lt h)

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

Goal state before:
pp: case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
⊢ (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m → e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m

Tactic:
have := h.fst

Goal state after:
case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this : e.NF
⊢ (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m → e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝ : e.NF
this : a.NF
⊢ (1 + (e - 1)).repr = e.repr

Tactic:
simp only [repr_add, repr_one, Nat.cast_one, repr_sub]

Goal state after:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝ : e.NF
this : a.NF
⊢ 1 + (e.repr - 1) = e.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
⊢ (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m → o'.NF ∧ ω ^ e.repr * ↑↑n + a.repr = ω * o'.repr + ↑m

Tactic:
have := h.fst

Goal state after:
case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this : e.NF
⊢ (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m → o'.NF ∧ ω ^ e.repr * ↑↑n + a.repr = ω * o'.repr + ↑m
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: n : ℕ
R : Type u_3
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : n.AtLeastTwo
a : A
⊢ OfNat.ofNat n • a = OfNat.ofNat n * a

Tactic:
by
  simp_rw [← nat_rawCast_2]
  simp [Nat.cast_smul_eq_nsmul]

Goal state after: