mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : M →ₚₗ[R] N
r : R
x : M →ₚₗ[R] N
⊢ (r • x).ground = (RingHom.id R) r • x.ground

Tactic:
ext m

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
f : M →ₚₗ[R] N
r : R
x : M →ₚₗ[R] N
m : M
⊢ (r • x).ground m = ((RingHom.id R) r • x.ground) m
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
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
⊢ (rTensor N (h.comp φ).toLinearMap) (f.toFun' A p) = (rTensor N ψ.toLinearMap) (f.toFun' B q)

Tactic:
by
  let θ := (quotientKerEquivRangeₐ (R := R) ψ).symm.toAlgHom.comp
    (h'.comp (quotientKerEquivRangeₐ φ).toAlgHom)
  have ht : (h.comp φ.range.val).comp (quotientKerEquivRangeₐ φ).toAlgHom =
      ψ.range.val.comp ((quotientKerEquivRangeₐ ψ).toAlgHom.comp θ) := by
    simp only [θ, ← AlgHom.comp_assoc, ← hh']
    simp [AlgHom.comp_assoc]
  rw [← φ.val_comp_rangeRestrict, ← quotientKerEquivRangeₐ_comp_mkₐ φ,
    ← ψ.val_comp_rangeRestrict, ← quotientKerEquivRangeₐ_comp_mkₐ ψ,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc _, ht]
  simp only [AlgHom.comp_toLinearMap, rTensor_comp_apply]
  apply congr_arg
  rw [← rTensor_comp_apply, ← AlgHom.comp_toLinearMap, isCompat_apply',
    isCompat_apply', AlgHom.comp_toLinearMap, rTensor_comp_apply,
    isCompat_apply']
  apply congr_arg
  simp only [θ, ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap, AlgHom.comp_assoc]
  rw [quotientKerEquivRangeₐ_comp_mkₐ, comp_toLinearMap,
    rTensor_comp_apply, hpq, ← rTensor_comp_apply, ← comp_toLinearMap,
    ← quotientKerEquivRangeₐ_comp_mkₐ, ← AlgHom.comp_assoc]
  simp

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
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
h1 : ∀ (i : ℕ), (coeff i) ↑r ∈ I ^ (k + 1)
heq :
  X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat * q =
    ↑⋯.unit⁻¹ * (↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q)
i✝ i : ℕ
⊢ (coeff i) (↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q) ∈ I ^ (k + 1)

Tactic:
rw [pow_succ']

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
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
h1 : ∀ (i : ℕ), (coeff i) ↑r ∈ I ^ (k + 1)
heq :
  X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat * q =
    ↑⋯.unit⁻¹ * (↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q)
i✝ i : ℕ
⊢ (coeff i) (↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q) ∈ I * I ^ k
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
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n : ℕ
h : Module.Projective R (QuotSMulTop x ↑M)
this✝ : Free R (QuotSMulTop x ↑M)
ntr : Nontrivial (QuotSMulTop x ↑M)
this : x ∈ annihilator R (QuotSMulTop x ↑M)
⊢ False

Tactic:
simp only [annihilator_eq_bot.mpr inferInstance, Submodule.mem_bot] at this

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n : ℕ
h : Module.Projective R (QuotSMulTop x ↑M)
this✝ : Free R (QuotSMulTop x ↑M)
ntr : Nontrivial (QuotSMulTop x ↑M)
this : x = 0
⊢ False
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case inl
A : Type u_1
inst✝¹ : CommRing A
g✝ : A⟦X⟧
I✝ : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsAdicComplete I A
f : A[X] ⧸ Ideal.span {g}
h✝ : Subsingleton A
⊢ (⇑(Ideal.Quotient.mk (Ideal.span {g})) ∘ ⇑⋯.mod')
      ((↑↑(Ideal.quotientMapₐ (Ideal.span {↑g}) (Polynomial.coeToPowerSeries.algHom A) ⋯).toRingHom).toFun f) =
    f

Tactic:
have : Subsingleton A[X] := inferInstance

Goal state after:
case inl
A : Type u_1
inst✝¹ : CommRing A
g✝ : A⟦X⟧
I✝ : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsAdicComplete I A
f : A[X] ⧸ Ideal.span {g}
h✝ : Subsingleton A
this : Subsingleton A[X]
⊢ (⇑(Ideal.Quotient.mk (Ideal.span {g})) ∘ ⇑⋯.mod')
      ((↑↑(Ideal.quotientMapₐ (Ideal.span {↑g}) (Polynomial.coeToPowerSeries.algHom A) ⋯).toRingHom).toFun f) =
    f
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g✝ : A⟦X⟧
I✝ : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsAdicComplete I A
f : A[X] ⧸ Ideal.span {g}
h✝ : Nontrivial A
⊢ I ≠ ⊤

Tactic:
rintro rfl

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g✝ : A⟦X⟧
I : Ideal A
g : A[X]
f : A[X] ⧸ Ideal.span {g}
h✝ : Nontrivial A
H : g.IsDistinguishedAt ⊤
inst✝ : IsAdicComplete ⊤ A
⊢ False
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case refine_1
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
hfdeg : f.natDegree = n
i : ℕ
hi : i < n
⊢ -r.coeff i ∈ IsLocalRing.maximalIdeal A

Tactic:
neg_mem_iff

Goal state after:
case refine_1
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
hfdeg : f.natDegree = n
i : ℕ
hi : i < n
⊢ r.coeff i ∈ IsLocalRing.maximalIdeal A
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case refine_1
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
hfdeg : f.natDegree = n
i : ℕ
hi : i < n
⊢ r.coeff i ∈ IsLocalRing.maximalIdeal A

Tactic:
have := H.coeff_f_sub_r_mem hi

Goal state after:
case refine_1
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
hfdeg : f.natDegree = n
i : ℕ
hi : i < n
this : (coeff i) (X ^ n - ↑r) ∈ IsLocalRing.maximalIdeal A
⊢ r.coeff i ∈ IsLocalRing.maximalIdeal A
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsSemisimpleModule R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule R ↥S
n : ℕ
e : Nonempty (M ≃ₗ[R] Fin n → ↥S)
⊢ n ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u_2
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsSemisimpleModule R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule R ↥S
e : Nonempty (M ≃ₗ[R] Fin 0 → ↥S)
⊢ False
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
S : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R S
inst✝¹ : IsSimpleModule R S
inst✝ : IsSemisimpleModule R M
m : Submodule R M
ne : m ≠ ⊥
⊢ m = isotypicComponent R M S → IsIsotypicOfType R (↥m) S ∧ m.IsFullyInvariant

Tactic:
rintro rfl

Goal state after:
R : Type u_2
M : Type u
S : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R S
inst✝¹ : IsSimpleModule R S
inst✝ : IsSemisimpleModule R M
ne : isotypicComponent R M S ≠ ⊥
⊢ IsIsotypicOfType R (↥(isotypicComponent R M S)) S ∧ (isotypicComponent R M S).IsFullyInvariant
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
this : IsSemisimpleRing R
⊢ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R

Tactic:
isIsotypic_iff_isFullyInvariant_imp_bot_or_top,

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 ∧ (∀ (N : Submodule R R), N.IsFullyInvariant → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
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:
isIsotypic_iff_isFullyInvariant_imp_bot_or_top,

Goal state after:
case refine_2
R : Type u
inst✝ : Ring R
left✝¹ : IsSemisimpleRing R
right✝ : Nontrivial R
x✝ : IsSemisimpleRing R ∧ (∀ (N : Submodule R R), N.IsFullyInvariant → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R
left✝ : ∀ (N : Submodule R R), N.IsFullyInvariant → N = ⊥ ∨ N = ⊤
⊢ IsSimpleRing R ∧ IsArtinianRing R
Module: Mathlib.RingTheory.Valuation.Minpoly

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
hx : IsUnit x
h_alg : Algebra.IsAlgebraic K L
hx₀ : IsIntegral K x
hdeg : 0 < finrank K L / (minpoly K x).natDegree
⊢ ¬v ((minpoly K x).coeff 0) ^ (finrank K L / (minpoly K x).natDegree) = 0

Tactic:
pow_eq_zero_iff hdeg.ne.symm,

Goal state after:
K : Type u_1
inst✝⁴ : Field K
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
hx : IsUnit x
h_alg : Algebra.IsAlgebraic K L
hx₀ : IsIntegral K x
hdeg : 0 < finrank K L / (minpoly K x).natDegree
⊢ ¬v ((minpoly K x).coeff 0) = 0
Module: Mathlib.RingTheory.Valuation.Extension

Goal state before:
pp: A : Type u_2
inst✝⁴ : Ring A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst✝¹ : LinearOrderedCommGroupWithZero ΓK
inst✝ : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
h : Subring.comap (algebraMap K A) vA.integer = vK.integer
⊢ vK.IsEquiv (comap (algebraMap K A) vA)

Tactic:
rw [isEquiv_iff_val_le_one]

Goal state after:
A : Type u_2
inst✝⁴ : Ring A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst✝¹ : LinearOrderedCommGroupWithZero ΓK
inst✝ : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
h : Subring.comap (algebraMap K A) vA.integer = vK.integer
⊢ ∀ {x : K}, vK x ≤ 1 ↔ (comap (algebraMap K A) vA) x ≤ 1
Module: Mathlib.RingTheory.ZMod.Torsion

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ p - 1 ≠ 0

Tactic:
have : 2 ≤ p := Nat.Prime.two_le Fact.out

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : 2 ≤ p
⊢ p - 1 ≠ 0
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inr.inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := fun t ↦ Nat.rec a (fun x IH ↦ sSup (range fun x ↦ f x IH)) t
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
⊢ sSup (range g) ∈ t

Tactic:
apply (hs t ht).isLUB_mem (t := .range fun n ↦ f ⟨t, ht⟩ (g n)) _ (range_nonempty _)

Goal state after:
case inr.inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := ⋯
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
⊢ IsLUB (range fun n ↦ f ⟨t, ht⟩ (g n)) (sSup (range g))

α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := ⋯
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
⊢ (range fun n ↦ f ⟨t, ht⟩ (g n)) ⊆ t
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inr.inr.refine_1
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := fun t ↦ Nat.rec a (fun x IH ↦ sSup (range fun x ↦ f x IH)) t
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
n : ℕ
⊢ (fun n ↦ f ⟨t, ht⟩ (g n)) n ≤ sSup (range g)

Tactic:
apply (le_csSup (.of_not_isCofinal _) _).trans (le_csSup hg ⟨n + 1, rfl⟩)

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := ⋯
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
n : ℕ
⊢ ¬IsCofinal (range fun x ↦ f x (Nat.rec a (fun x IH ↦ sSup (range fun x ↦ f x IH)) n))

α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := ⋯
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
n : ℕ
⊢ (fun n ↦ f ⟨t, ht⟩ (g n)) n ∈ range fun x ↦ f x (Nat.rec a (fun x IH ↦ sSup (range fun x ↦ f x IH)) n)
Module: Mathlib.SetTheory.Cardinal.NatCount

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ↑(count p n) ≤ {k | p k}.encard

Tactic:
simp only [Set.encard, ENat.card, Set.coe_ofPred, Cardinal.natCast_le_toENat]
  exact Nat.count_le_cardinal n

Goal state after:
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
⊢ T = ⊥ → [] ∉ T

Tactic:
rintro rfl

Goal state after:
A : Type u_1
⊢ [] ∉ ⊥
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.lookupFinsupp.support = (map Prod.fst (CNF b o)).toFinset

Tactic:
lookupFinsupp_support,

Goal state after:
b o : Ordinal.{u_1}
⊢ (List.filter (fun x ↦ decide (x.snd ≠ 0))
          { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.entries).keys.toFinset =
    (map Prod.fst (CNF b o)).toFinset
Module: Mathlib.SetTheory.Lists

Goal state before:
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 a l IH₁ IH₂
    simpa using ⟨IH₁, IH₂⟩

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

Goal state before:
pp: b o e : Ordinal.{u_1}
h : o < b ^ e
⊢ (coeff b o) e = 0

Tactic:
by
  apply coeff_of_notMem_CNF
  intro he
  rw [mem_map] at he
  obtain ⟨⟨e, c⟩, he, rfl⟩ := he
  obtain rfl | he' := eq_or_ne e 0
  · simp_all
  · exact (opow_le_of_le_log he' (fst_le_log he)).not_gt h

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

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_lfp : ∃ y, lfp f = ↑y
y : ↑(fixedPoints ⇑f)
h_y : lfp f = ↑y
⊢ lfpApprox f ⊥ (succ #α).ord ≤ lfp f

Tactic:
h_y

Goal state after:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_lfp : ∃ y, lfp f = ↑y
y : ↑(fixedPoints ⇑f)
h_y : lfp f = ↑y
⊢ lfpApprox f ⊥ (succ #α).ord ≤ ↑y
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case single_add.inr.h
b e 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)
he' : e' < e
a : Ordinal.{u_1}
ha : a ∈ (single e' y + f).support
⊢ a ≠ e

Tactic:
rintro rfl

Goal state after:
case single_add.inr.h
b x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
a : Ordinal.{u_1}
ha : a ∈ (single e' y + f).support
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ a
a✝ : single e' y + f = f → eval b (single a x + (single e' y + f)) = b ^ a * x + eval b (single e' y + f)
he' : e' < a
⊢ False
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case pos
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
a : Ordinal.{u_1}
ha : a ∈ f.support
⊢ a ≠ e'

Tactic:
rintro rfl

Goal state after:
case pos
b x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
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 a : Ordinal.{u_1}
ha : a ∈ f.support
hf : ∀ c ∈ f.support, c < a
hb : ∀ (e' : Ordinal.{u_1}), (single a x + f) e' < b
he : ∀ e' ∈ (single a x + f).support, e' < e
he' : a ∉ f.support
⊢ False
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} := fun i ↦ (enumOrdOrderIso s hs).symm ⟨f i, ⋯⟩
⊢ ⨆ i, f i ∈ s

Tactic:
suffices enumOrd s (⨆ i, g i) = ⨆ i, f i by
      rw [← this]
      exact enumOrd_mem hs _

Goal state after:
case refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} := fun i ↦ (enumOrdOrderIso s hs).symm ⟨f i, ⋯⟩
⊢ enumOrd s (⨆ i, g i) = ⨆ i, f i
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ ⨆ i, f i ∈ s

Tactic:
let g : ι → Ordinal.{u} := fun i => (enumOrdOrderIso s hs).symm ⟨_, hf i⟩
    suffices enumOrd s (⨆ i, g i) = ⨆ i, f i by
      rw [← this]
      exact enumOrd_mem hs _
    rw [h.map_iSup bddAbove_of_small]
    congr
    ext x
    change (enumOrdOrderIso s hs _).val = f x
    rw [OrderIso.apply_symm_apply]

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

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
⊢ veblenWith f 0 = f

Tactic:
rw [veblenWith, if_pos rfl]

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

Goal state before:
pp: x y z : ZFSet.{u}
⊢ z ∈ x ∩ y ↔ z ∈ x ∧ z ∈ y

Tactic:
by simp [← sep_mem]

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

Goal state before:
pp: p : ZFSet.{u} → ZFSet.{u} → Prop
x y z : ZFSet.{u}
⊢ z ∈ pairSep p x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b

Tactic:
refine mem_sep.trans ⟨And.right, fun e => ⟨?_, e⟩⟩

Goal state after:
p : ZFSet.{u} → ZFSet.{u} → Prop
x y z : ZFSet.{u}
e : ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b
⊢ z ∈ (x ∪ y).powerset.powerset
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
⊢ y = x → y = y'

Tactic:
rintro rfl

Goal state after:
y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {y} ∨ z = {y, y} ↔ z = {y} ∨ z = {y, y'}
⊢ y = y'
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: a : Ordinal.{u}
h : a < ω ^ a
⊢ ω ^ a = veblen a.invVeblen₁ a

Tactic:
invVeblen₁_of_lt_opow h,

Goal state after:
a : Ordinal.{u}
h : a < ω ^ a
⊢ ω ^ a = veblen 0 a
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 o a = x → x.invVeblen₁ = o ∧ x.invVeblen₂ = a

Tactic:
rintro rfl

Goal state after:
case refine_1.inr
o a : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
⊢ (veblen o a).invVeblen₁ = o ∧ (veblen o a).invVeblen₂ = a
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: case mpr
x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (∃ z, x z ∧ y ∈ z) → (⋃₀ x) y

Tactic:
exact fun ⟨z, hxz, hyz⟩ => ⟨_, coe_mem.2 hxz, hyz⟩

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

Goal state before:
pp: f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
⊢ (∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z) ↔ z = f y

Tactic:
exact
      ⟨fun ⟨w, _, pr⟩ => by
        let ⟨wy, fw⟩ := ZFSet.pair_injective pr
        rw [← fw, wy], fun e => by
        subst e
        exact ⟨_, h, rfl⟩⟩

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

Goal state before:
pp: case gt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.gt
ee : Ordering.gt.Compares e₁ e₂
⊢ (match Ordering.gt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
· exact
        (Ordinal.sub_eq_of_add_eq <|
            add_of_omega0_opow_le (h₂.below_of_lt ee).repr_lt <| omega0_le_oadd _ _ _).symm

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

Goal state before:
pp: case neg.e_a
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
⊢ (if h : some x :: ↑s = some x :: ↑t then 0 else Nat.find ⋯) = Nat.find ⋯ + 1

Tactic:
split_ifs with h_if

Goal state after:
case pos
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
h_if : some x :: ↑s = some x :: ↑t
⊢ False

case neg
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
h_if : ¬some x :: ↑s = some x :: ↑t
⊢ Nat.find ⋯ = Nat.find ⋯ + 1