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

Goal state before:
pp: R✝ : Type u_1
inst✝⁶ : CommSemiring R✝
p : ℕ
hp : Fact (Nat.Prime p)
inst✝⁵ : CharP R✝ p
R : Type u₁
inst✝⁴ : CommSemiring R
inst✝³ : CharP R p
inst✝² : PerfectRing R p
S : Type u₂
inst✝¹ : CommSemiring S
inst✝ : CharP S p
f : R →+* Perfection S p
r : R
n : ℕ
⊢ (coeff S p 0) (f ((⇑(frobeniusEquiv R p).symm)^[n] r)) = (coeff S p n) (f r)

Tactic:
rw [← coeff_iterate_frobenius _ 0 n, zero_add, ← RingHom.map_iterate_frobenius,
        Function.RightInverse.iterate (frobenius_apply_frobeniusEquiv_symm R p) n]

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

Goal state before:
pp: case e'_2.e'_4
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ i + j = 0 + (i + j)

Tactic:
rw [zero_add]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x = (⇑verschiebung)^[n] (x.shift n)

Tactic:
simpa using eq_iterate_verschiebung (x := x) (n := n) h

Goal state after:
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)
⊢ Function.Surjective ⇑(fontaineTheta R p)

Tactic:
have : Ideal.map (fontaineTheta R p) (span {(p : 𝕎 R♭)}) = 𝔭 := by
    simp [map_span]

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}) = 𝔭
⊢ Function.Surjective ⇑(fontaineTheta R p)
Module: Mathlib.RingTheory.Polynomial.IrreducibleRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
hi : Irreducible (Polynomial.map φ f)
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
⊢ Irreducible f

Tactic:
rw [show φ = ψ.comp ι from rfl, ← map_map] at hi

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ψ (Polynomial.map ι f))
⊢ Irreducible f
Module: Mathlib.RingTheory.Polynomial.IrreducibleRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi✝ : Irreducible (Polynomial.map ι f)
a b : R[X]
h✝ : f = a * b
hb : IsUnit (Polynomial.map ι b)
i : ℕ
hi : i ≠ 0
w✝ : R'
left✝ : IsUnit w✝
h : C w✝ = Polynomial.map ι b
⊢ IsNilpotent (b.coeff i)

Tactic:
simpa only [coeff_map, coeff_C, hi, ite_false, ← RingHom.mem_ker,
      show RingHom.ker ι = nilradical R from Ideal.mk_ker] using! congr(coeff $(h.symm) i)

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

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

Tactic:
let p : R[X] := C a * X ^ 2 + C b * X + C c

Goal state after:
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
⊢ b = -a * (x1 + x2)
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}
⊢ c = a * x1 * x2

Tactic:
let p : R[X] := C a * X ^ 2 + C b * X + C c

Goal state after:
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
⊢ c = a * x1 * x2
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: case refine_1
n : ℕ
⊢ (shiftedLegendre n).degree ≤ ↑n

Tactic:
degree_le_iff_coeff_zero

Goal state after:
case refine_1
n : ℕ
⊢ ∀ (m : ℕ), ↑n < ↑m → (shiftedLegendre n).coeff m = 0
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
eqbot : p = ⊥
⊢ IsField (Localization.AtPrime p)

Tactic:
simp [isField_iff_maximalIdeal_eq, ← Localization.AtPrime.map_eq_maximalIdeal, eqbot]

Goal state after:
Module: Mathlib.RingTheory.PolynomialLaw.Basic

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

Tactic:
simp only [Function.comp_apply, Equiv.symm_apply_apply, j]

Goal state after:
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
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1))) → HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1 + 1))
⊢ HasProjectiveDimensionLT M (n + 1 + 1)

Tactic:
rw [hS.hasProjectiveDimensionLT_X₃_iff n inferInstance]

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
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1))) → HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1 + 1))
⊢ HasProjectiveDimensionLT S.X₁ (n + 1)
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
lt : q < p
this : (comap C p).IsMaximal
y : R[X]
left✝ : y.Monic
hy : p = Ideal.map C (comap C p) ⊔ span {y}
peq : p = span (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})
⊢ ↑(Submodule.spanFinrank
        (span
          (⇑(algebraMap R[X] (Localization.AtPrime p)) ''
            (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})))) ≤
    ↑(under R[X] (maximalIdeal (Localization.AtPrime p))).height

Tactic:
IsLocalization.AtPrime.under_maximalIdeal _ p

Goal state after:
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
lt : q < p
this : (comap C p).IsMaximal
y : R[X]
left✝ : y.Monic
hy : p = Ideal.map C (comap C p) ⊔ span {y}
peq : p = span (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})
⊢ ↑(Submodule.spanFinrank
        (span
          (⇑(algebraMap R[X] (Localization.AtPrime p)) ''
            (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})))) ≤
    ↑p.height
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
N : Submodule R M
inst✝ : IsSimpleModule R ↥N
s : Set (Submodule R M)
hs : ∀ (m : ↑s), IsSemisimpleModule R ↥↑m
hN : N ≤ sSup s
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty (↥N ≃ₗ[R] ↥S)

Tactic:
by
  rw [sSup_eq_iSup] at hN
  have e := LinearEquiv.ofInjective _ (inclusion_injective hN)
  have := IsSimpleModule.congr e.symm
  have := isSemisimpleModule_biSup_of_isSemisimpleModule_submodule fun m hm ↦ hs ⟨m, hm⟩
  obtain ⟨_, ⟨m, hm, rfl⟩, S, le, ⟨e'⟩⟩ := LinearMap.range (inclusion hN)
      |>.le_linearEquiv_of_sSup_eq_top (comap (⨆ i ∈ s, i).subtype '' s) <| by
    rw [sSup_image, biSup_comap_subtype_eq_top]
  exact ⟨m, hm, _, map_le_iff_le_comap.mpr le,
    ⟨(e.trans e').trans (equivMapOfInjective _ (subtype_injective _) _)⟩⟩

Goal state after:
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.Isotypic

Goal state before:
pp: case inl
R : Type u_2
M : Type u
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
S : Submodule R M
inst✝ : IsSimpleModule R ↥S
f : M →ₗ[R] N
inj : Function.Injective ⇑(f ∘ₗ S.subtype)
⊢ (f ∘ₗ S.subtype).range ≤ isotypicComponent R N ↥S

pp: case inr
R : Type u_2
M : Type u
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
S : Submodule R M
inst✝ : IsSimpleModule R ↥S
f : M →ₗ[R] N
eq : f ∘ₗ S.subtype = 0
⊢ (f ∘ₗ S.subtype).range ≤ isotypicComponent R N ↥S

Tactic:
· exact le_sSup ⟨.symm <| .ofInjective _ inj⟩

Goal state after:
case inr
R : Type u_2
M : Type u
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
S : Submodule R M
inst✝ : IsSimpleModule R ↥S
f : M →ₗ[R] N
eq : f ∘ₗ S.subtype = 0
⊢ (f ∘ₗ S.subtype).range ≤ isotypicComponent R N ↥S
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ (valuation R) (↑r * ↑u) = (valuation R) (↑t * ↑s)

pp: case hb
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ (valuation R) ↑s ≠ 0

pp: case hd
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ (valuation R) ↑u ≠ 0

Tactic:
this.eq_iff

Goal state after:
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ 1 (↑r * ↑u) = 1 (↑t * ↑s)

case hb
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ (valuation R) ↑s ≠ 0

case hd
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ (valuation R) ↑u ≠ 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: case inr
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
this : Subsingleton (ValueGroupWithZero R)ˣ
u : (ValueGroupWithZero R)ˣ
⊢ ↑u < 1 → ↑u ≤ 0

Tactic:
← Units.val_one,

Goal state after:
case inr
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
this : Subsingleton (ValueGroupWithZero R)ˣ
u : (ValueGroupWithZero R)ˣ
⊢ ↑u < ↑1 → ↑u ≤ 0
Module: Mathlib.RingTheory.Valuation.Extension

Goal state before:
pp: R : Type u_1
A : Type u_2
ΓR✝ : Type u_3
ΓA✝ : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring A
inst✝⁸ : LinearOrderedCommMonoidWithZero ΓR✝
inst✝⁷ : LinearOrderedCommMonoidWithZero ΓA✝
inst✝⁶ : Algebra R A
vR✝ : Valuation R ΓR✝
vA✝ : Valuation A ΓA✝
K : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Algebra K A
ΓR : Type u_6
ΓA : Type u_7
ΓK : Type u_8
inst✝³ : LinearOrderedCommGroupWithZero ΓR
inst✝² : LinearOrderedCommGroupWithZero ΓK
inst✝¹ : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vK : Valuation K ΓK
vA : Valuation A ΓA
inst✝ : vR.HasExtension vA
⊢ ∀ x ∈ vR.integer, (algebraMap R A) x ∈ vA.integer

Tactic:
by simp [Valuation.mem_integer_iff, val_map_le_one_iff vR vA]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
ΓR : Type u_6
ΓA : Type u_7
inst✝² : LinearOrderedCommGroupWithZero ΓR
inst✝¹ : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : vR.HasExtension vA
r : ↥vR.integer
a : ↥vA.integer
⊢ ↑(r • a) = ↑r • ↑a

Tactic:
by
  rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
ΓR : Type u_6
ΓA : Type u_7
inst✝² : LinearOrderedCommGroupWithZero ΓR
inst✝¹ : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : vR.HasExtension vA
r : ↥vR.integer
⊢ ↑((algebraMap ↥vR.integer ↥vA.integer) r) = (algebraMap R A) ↑r

Tactic:
by
  rfl

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

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ (Finsupp.single (0, x) (p ^ (n + 1 - x))).support ⊆ univ ×ˢ range (n + 1)

Tactic:
apply Subset.trans Finsupp.support_single_subset
      simpa using mem_range.mp hx

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

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ (Finsupp.single (1, x) (p ^ (n + 1 - x))).support ⊆ univ ×ˢ range (n + 1)

Tactic:
apply Subset.trans Finsupp.support_single_subset
      simpa using mem_range.mp hx

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l : Lists' α true
⊢ l ⊆ nil → l = nil

Tactic:
rw [← of_toList l]

Goal state after:
α : Type u_1
l : Lists' α true
⊢ ofList l.toList ⊆ nil → ofList l.toList = nil
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₂ : Lists α
m₂ : a₂ ∈ l₂✝¹.toList
e₃₂ : a₃ ~ a₂
⊢ 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₁ : Lists α
m₁ : a₁ ∈ l₁.toList
e₂₁ : a₂ ~ a₁
⊢ a₃ ∈ l₁
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1.antisymm.antisymm.right
α : 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₃
      rcases Lists'.mem_of_subset' hr₂ m₃ with ⟨a₂, m₂, e₃₂⟩
      rcases Lists'.mem_of_subset' hr₁ m₂ with ⟨a₁, m₁, e₂₁⟩
      exact ⟨a₁, m₁, (IH _ m₁ e₂₁.symm e₃₂.symm).symm⟩

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case atom
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ ⟨false, Lists'.atom a✝⟩ = ⟨false, l₂⟩ ↔ Lists'.atom a✝ = l₂

Tactic:
constructor <;> (rintro ⟨rfl⟩; rfl)

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
ha : ∃ b, b < a
⊢ (∀ i < a, ∃ x ∈ Ioc i a, x ≠ a ∧ x ∈ s) ↔ (∃ b, b < a) ∧ ∀ b < a, ∃ x, x ∈ s ∩ Ioo b a

Tactic:
mem_inter_iff

Goal state after:
case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
ha : ∃ b, b < a
⊢ (∀ i < a, ∃ x ∈ Ioc i a, x ≠ a ∧ x ∈ s) ↔ (∃ b, b < a) ∧ ∀ b < a, ∃ x ∈ s, x ∈ Ioo b a
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ ω ^ e✝.repr * ↑↑n✝ + ω ^ e✝.repr ≤ ω ^ b✝

Tactic:
grw [← mul_succ, succ_le_of_lt (natCast_lt_omega0 _), ← opow_succ, succ_le_of_lt h₃]

Goal state after:
case hc
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ 0 < ω
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
d : ω ^ b ∣ (e.oadd n a).repr
⊢ b ≤ e.repr ∧ ω ^ b ∣ a.repr

Tactic:
by
  have := mt repr_inj.1 (fun h => by injection h : ONote.oadd e n a ≠ 0)
  have L := le_of_not_gt fun l => not_le_of_gt (h.below_of_lt l).repr_lt (le_of_dvd this d)
  simp only [repr] at d
  exact ⟨L, (dvd_add_iff <| (opow_dvd_opow _ L).mul_right _).1 d⟩

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

Goal state before:
pp: case 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 : β
hb : (A a).Equiv (B 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 γ Γ
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)

Tactic:
| _ γ Γ
     => 

Goal state after:
case 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 : β
hb : (A a).Equiv (B 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 γ Γ
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.gt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
h : e.cmp e' = Ordering.gt
this : Ordering.gt.Compares e e'
⊢ (e.oadd n (e'.oadd n' a')).NFBelow b

Tactic:
exact NFBelow.oadd h₁.fst (NF.below_of_lt this ⟨⟨_, h'⟩⟩) h₁.lt

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

Goal state before:
pp: case mpr.inr
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
ha : veblenWith f o a = a
b : Ordinal.{u}
hb✝ : b < o + 1
hb : b < o
⊢ a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb✝⟩)

Tactic:
rw [← ha]
      exact veblenWith_veblenWith_of_lt hf hb _

Goal state after: