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}
p : R[X] := C a * X ^ 2 + C b * X + C c
hp_natDegree : p.natDegree = 2
hp_roots_card : p.roots.card = p.natDegree
⊢ 0 ≤ p.natDegree

Tactic:
simp [hp_natDegree]

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

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

Tactic:
simp [hπ]

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

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

Tactic:
simp [hπ]

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

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

Tactic:
rw [IsRestricted, MvPowerSeries.IsRestricted, isRestricted_comp_uniqueEquiv]
  exact ⟨fun H ↦ (H.comp (Finsupp.uniqueEquiv ()).symm.injective.tendsto_cofinite).congr fun n ↦
    by simp, fun H ↦ H.comp (Finsupp.uniqueEquiv ()).injective.tendsto_cofinite⟩

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: case h
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
u : M ⊗[R] N
P : { P // P.FG }
t : ↥↑P ⊗[R] N
ht :
  (Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun ⦃P Q⦄ h ↦ rTensor N (inclusion h)) P) t =
    (FG.rTensor.directLimit R M N).symm u
⊢ (FG.rTensor.directLimit R M N) ((FG.rTensor.directLimit R M N).symm u) = u

Tactic:
LinearEquiv.apply_symm_apply

Goal state after:
case h
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
u : M ⊗[R] N
P : { P // P.FG }
t : ↥↑P ⊗[R] N
ht :
  (Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun ⦃P Q⦄ h ↦ rTensor N (inclusion h)) P) t =
    (FG.rTensor.directLimit R M N).symm u
⊢ u = u
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: case pos
n : ℕ
hn : n = 0
⊢ (coeff n) largeSchroderSeries = (coeff n) (1 + X * largeSchroderSeries + X * largeSchroderSeries ^ 2)

Tactic:
aesop

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

Goal state before:
pp: n : ℕ
⊢ radical n ≤ n → n ≠ 0

Tactic:
aesop

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
⊢ IsRegular N (List.map (⇑(algebraMap R S)) rs)

Tactic:
by
  have : IsLocalRing S := IsLocalization.AtPrime.isLocalRing S p
  refine (IsLocalRing.isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal (fun _ hr ↦ ?_)).mpr <|
    reg.of_isLocalizedModule S p.primeCompl f
  rcases List.mem_map.mp hr with ⟨r, hr, eq⟩
  simpa only [← eq, IsLocalization.AtPrime.to_map_mem_maximal_iff S p] using mem r hr

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
kerf : f.ker = x • ⊤
fg : g.ker.FG
⊢ g.ker = ⊥

Tactic:
apply Submodule.eq_bot_of_le_smul_of_le_jacobson_bot (Ideal.span {x}) _ fg _ lejac

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 := ⋯
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) := ⋯
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := ⋯
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ⋯
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 • ⊤
fg : g.ker.FG
⊢ g.ker ≤ Ideal.span {x} • g.ker
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
f : A⟦X⟧
k : ℕ
hq : ∀ {i : ℕ}, i ≥ ((map (Ideal.Quotient.mk I)) g).order.toNat → (coeff i) (f - g * H.seq f k) ∈ I ^ k
i : ℕ
hi : i ≥ ((map (Ideal.Quotient.mk I)) g).order.toNat
⊢ (coeff i) (f - g * H.seq f (k + 1)) ∈ I ^ (k + 1)

Tactic:
rw [seq]
    set q := H.seq f k
    set s := f - g * q
    set n := (g.map (Ideal.Quotient.mk I)).order.toNat
    have hs := s.eq_X_pow_mul_shift_add_trunc n
    set s₀ := s.trunc n
    set s₁ := PowerSeries.mk fun i ↦ coeff (i + n) s
    set q' := q + s₁ * H.isUnit_shift.unit⁻¹
    have key : f - g * q' = (s₀ : A⟦X⟧) - (g.trunc n : A⟦X⟧) * s₁ * H.isUnit_shift.unit⁻¹ := by
      trans s + g * (q - q')
      · simp_rw [s]; ring
      simp_rw [q']
      rw [sub_add_cancel_left, mul_neg, ← mul_assoc, mul_right_comm]
      nth_rw 1 [g.eq_X_pow_mul_shift_add_trunc n]
      rw [add_mul, mul_assoc, IsUnit.mul_val_inv, hs]
      ring
    rw [key, map_sub, Polynomial.coeff_coe, coeff_trunc, if_neg hi.not_gt, zero_sub, neg_mem_iff,
      pow_succ']
    refine coeff_mul_mem_ideal_of_coeff_left_mem_ideal' (fun i ↦ ?_) i
    refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal'
      (by simp [n, g.coeff_trunc_order_mem]) (fun i ↦ ?_) i
    rw [coeff_mk]
    exact hq (by simp)

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

Goal state before:
pp: case inl
A : Type u_1
inst✝¹ : CommRing A
g f : A⟦X⟧
H : g.IsWeierstrassDivisorAt ⊤
inst✝ : IsAdicComplete ⊤ A
this : Subsingleton A
⊢ IsWeierstrassDivisionAt 0 g (H.div 0) (H.mod 0) ⊤

Tactic:
Subsingleton.elim (H.div 0) 0,

Goal state after:
case inl
A : Type u_1
inst✝¹ : CommRing A
g f : A⟦X⟧
H : g.IsWeierstrassDivisorAt ⊤
inst✝ : IsAdicComplete ⊤ A
this : Subsingleton A
⊢ IsWeierstrassDivisionAt 0 g 0 (H.mod 0) ⊤
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ (rTensor M A.val.toLinearMap).range
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (rTensor M (φ R gen).toLinearMap) p = t
hs : s ∈ (φ R gen).range
⊢ ∃ n ψ p q, (rTensor M ψ.toLinearMap) p = t ∧ ψ q = s

Tactic:
use gen.card, φ R gen, p, hs.choose, hp, hs.choose_spec

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

Tactic:
← eq_sub_iff_add_eq

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 :
  (mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) *
        X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
      q =
    ↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
h1 : ∀ (i : ℕ), (coeff i) ↑r ∈ I ^ (k + 1)
⊢ ∀ (i : ℕ), (coeff i) q ∈ I ^ (k + 1)
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 q' : A⟦X⟧
r r' : A[X]
hr : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hr' : r'.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q + ↑r = g * q' + ↑r'
⊢ g * (q - q') = ↑(r' - r)

Tactic:
← eq_sub_iff_add_eq

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q q' : A⟦X⟧
r r' : A[X]
hr : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hr' : r'.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = g * q' + ↑r' - ↑r
⊢ g * (q - q') = ↑(r' - r)
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✝ : Nontrivial M
h : IsIsotypic R M
⊢ ∃ ι, ∃ (_ : Nonempty ι), ∃ S, IsSimpleModule R ↥S ∧ Nonempty (M ≃ₗ[R] ι →₀ ↥S)

Tactic:
by
  have ⟨S, hS⟩ := IsAtomic.exists_atom (Submodule R M)
  rw [← isSimpleModule_iff_isAtom] at hS
  have ⟨ι, e⟩ := (h S).linearEquiv_finsupp
  exact ⟨ι, (isEmpty_or_nonempty ι).resolve_left fun _ ↦ not_subsingleton _ (e.some.subsingleton),
    S, hS, e⟩

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i ≤ n
hpi : ↑p ^ i = 0
⊢ i = n

Tactic:
contrapose! hpi

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i ≤ n
hpi : i ≠ n
⊢ ↑p ^ i ≠ 0
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: case succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hA : A.coeff 0 = ↑a
n : ℕ
a✝ : (A * { coeff := inverseCoeff a A }).coeff n = coeff 1 n
H_coeff : k :=
  A.coeff (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i ↦ inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
⊢ (A * { coeff := inverseCoeff a A }).coeff (n + 1) = coeff 1 (n + 1)

Tactic:
linear_combination (norm := skip) -H_coeff * H

Goal state after:
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hA : A.coeff 0 = ↑a
n : ℕ
a✝ : (A * { coeff := inverseCoeff a A }).coeff n = coeff 1 n
H_coeff : k := ⋯
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
⊢ (A * { coeff := inverseCoeff a A }).coeff (n + 1) + -H_coeff * 1 -
      (coeff 1 (n + 1) + -H_coeff * (↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹)) =
    0
Module: Mathlib.RingTheory.WittVector.Isocrystal

Goal state before:
pp: case refine_1
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.Injective ⇑F₀

Tactic:
rw [← LinearMap.ker_eq_bot]
      exact LinearMap.ker_toSpanSingleton K(p, k) hx

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a ≤ b
⊢ lfpApprox f x a ≤ lfpApprox f x b

Tactic:
rw [lfpApprox, lfpApprox]

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a ≤ b
⊢ x ⊔ ⨆ b, ⨆ (_ : b < a), f (lfpApprox f x b) ≤ x ⊔ ⨆ b_1, ⨆ (_ : b_1 < b), f (lfpApprox f x b_1)
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case ind
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ lfpApprox g x y
⊢ lfpApprox f x i ≤ lfpApprox g x i

Tactic:
rw [lfpApprox, lfpApprox]

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

Goal state before:
pp: case ofList.cons
α : Type u_1
l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : (∀ (a : Lists α), a ∈ t → a ∈ l₂) → ofList t ⊆ l₂
H : h ∈ l₂ ∧ ∀ (a : Lists α), a ∈ t → a ∈ l₂
⊢ cons h (ofList t) ⊆ l₂

Tactic:
exact cons_subset.2 ⟨H.1, t_ih H.2⟩

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

Goal state before:
pp: case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x₁ x₂ : α
h : x₁ ≤ x₂
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x₁ y ≤ lfpApprox f x₂ y
⊢ lfpApprox f x₁ i ≤ lfpApprox f x₂ i

Tactic:
rw [lfpApprox, lfpApprox]

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x₁ x₂ : α
h : x₁ ≤ x₂
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x₁ y ≤ lfpApprox f x₂ y
⊢ x₁ ⊔ ⨆ b, ⨆ (_ : b < i), f (lfpApprox f x₁ b) ≤ x₂ ⊔ ⨆ b, ⨆ (_ : b < i), f (lfpApprox f x₂ b)
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
this :
  {b : Bool} →
    (l : Lists' α b) →
      C ⟨b, l⟩ ×'
        match b, l with
        | true, l => D l
        | false, x => PUnit
⊢ ((l : Lists α) → C l) ×' ((l : Lists' α true) → D l)

Tactic:
exact ⟨fun ⟨b, l⟩ => (this _).1, fun l => (this l).2⟩

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case antisymm
α : Type u_1
l₁✝ l₂✝ : Lists' α true
h₁ : l₁✝.Subset l₂✝
h₂ : l₂✝.Subset l₁✝
⊢ ⟨true, l₂✝⟩ ~ ⟨true, l₁✝⟩

Tactic:
exact Equiv.antisymm h₂ h₁

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
hx : x ≤ f x
hab : a < b
hac : a ≤ c
hf : lfpApprox f x a = lfpApprox f x b
H : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ lfpApprox f x c ∈ fixedPoints ⇑f

Tactic:
lfpApprox_eq_of_mem_fixedPoints f hac H

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
hx : x ≤ f x
hab : a < b
hac : a ≤ c
hf : lfpApprox f x a = lfpApprox f x b
H : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ lfpApprox f x a ∈ fixedPoints ⇑f
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1.antisymm.antisymm.left
α : Type u_1
trans : Lists α → Prop := ⋯
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 α), a ∈ l₁.toList → a ∈ l₂✝

Tactic:
intro a₁ m₁

Goal state after:
case C1.antisymm.antisymm.left
α : 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₂✝
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1.antisymm.antisymm.left
α : 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₂✝

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

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

Goal state before:
pp: case inr.e_a.e_a
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
e' : Ordinal.{u_1}
he' : e' ∈ f.support.sort fun x1 x2 ↦ x1 ≥ x2
b✝ : Ordinal.{u_1}
⊢ e' ≠ e

Tactic:
aesop

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

Goal state before:
pp: n : ℕ
⊢ (↑n).repr = ↑n

Tactic:
by cases n <;> simp

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

Goal state before:
pp: case single_add
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
⊢ b ^ e₁ * x + eval b (f₁ + f₂) = eval b (single e₁ x + f₁) + eval b f₂

pp: case single_add.h
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
⊢ ∀ e' ∈ (f₁ + f₂).support, e' ≤ e₁

Tactic:
eval_single_add' _ hf₁,

Goal state after:
case single_add
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
⊢ b ^ e₁ * x + eval b (f₁ + f₂) = b ^ e₁ * x + eval b f₁ + eval b f₂

case single_add.h
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
⊢ ∀ e' ∈ (f₁ + f₂).support, e' ≤ e₁
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case single_add
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
⊢ eval b (single e' x + f) < b ^ e

Tactic:
have he' : e' ∉ f.support := fun h ↦ (hf _ h).false

Goal state after:
case single_add
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
⊢ eval b (single e' x + f) < b ^ e
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e o₁ o₂ : ONote
n₁ n₂ : ℕ+
h₁ : (e.oadd n₁ o₁).NF
h : ↑n₁ < ↑n₂
⊢ succ ↑↑n₁ ≤ ↑↑n₂

Tactic:
succ_le_iff,

Goal state after:
e o₁ o₂ : ONote
n₁ n₂ : ℕ+
h₁ : (e.oadd n₁ o₁).NF
h : ↑n₁ < ↑n₂
⊢ ↑↑n₁ < ↑↑n₂