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

Goal state before:
pp: case h.mul_X
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
h_C : ∀ (a : R), P ↑(C a)
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
g : MvPolynomial (ℕ × M) R
nm : ℕ × M
h : P ↑g
⊢ P ↑(g * X nm)

Tactic:
RingCon.coe_mul

Goal state after:
case h.mul_X
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
h_C : ∀ (a : R), P ↑(C a)
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
g : MvPolynomial (ℕ × M) R
nm : ℕ × M
h : P ↑g
⊢ P (↑g * ↑(X nm))
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ map R (g ∘ₗ f) = (map R g).comp (map R f)

Tactic:
rw [algHom_ext_iff]
  intros; simp [map_apply_dp]

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
S : Type u_4
inst✝⁷ : CommSemiring S
N : Type u_5
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Module S N
f : M →ₗ[R] N
inst✝³ : Algebra R S
inst✝² : IsScalarTower R S N
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g : M ≃ₗ[R] N
⊢ (map R ↑g).comp (map R ↑g.symm) = AlgHom.id R (DividedPowerAlgebra R N)

Tactic:
simp [← map_comp, map_id]

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
S : Type u_4
inst✝⁷ : CommSemiring S
N : Type u_5
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Module S N
f : M →ₗ[R] N
inst✝³ : Algebra R S
inst✝² : IsScalarTower R S N
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g : M ≃ₗ[R] N
⊢ (map R ↑g.symm).comp (map R ↑g) = AlgHom.id R (DividedPowerAlgebra R M)

Tactic:
simp [← map_comp, map_id]

Goal state after:
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] (S ⊗[R] S) :=
  (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S).trans (TensorProduct.assoc R R T T S S)
this : TensorProduct.lmul' T = (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R)).comp ↑e
⊢ ((TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R)).comp ↑e).Flat

Tactic:
refine .comp (.of_bijective e.bijective) (.tensorProductMap ?_ ?_)

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] (S ⊗[R] S) :=
  (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S).trans (TensorProduct.assoc R R T T S S)
this : TensorProduct.lmul' T = (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R)).comp ↑e
⊢ (AlgHom.id T T).Flat

case refine_2
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] (S ⊗[R] S) :=
  (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S).trans (TensorProduct.assoc R R T T S S)
this : TensorProduct.lmul' T = (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R)).comp ↑e
⊢ (TensorProduct.lmul' R).Flat
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ P.cotangentComplex ∘ₗ ↑P.cotangentExtendScalarsEquiv ∘ₗ h1Cotangentι ∘ₗ ↑P.h1CotangentExtendScalarsEquiv.symm =
    H1Cotangent.δ R P.Ring S

Tactic:
← LinearMap.comp_assoc,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (P.cotangentComplex ∘ₗ ↑P.cotangentExtendScalarsEquiv) ∘ₗ h1Cotangentι ∘ₗ ↑P.h1CotangentExtendScalarsEquiv.symm =
    H1Cotangent.δ R P.Ring S
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (P.cotangentComplex ∘ₗ ↑P.cotangentExtendScalarsEquiv) ∘ₗ h1Cotangentι ∘ₗ ↑P.h1CotangentExtendScalarsEquiv.symm =
    H1Cotangent.δ R P.Ring S

Tactic:
← LinearMap.comp_assoc,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ ((P.cotangentComplex ∘ₗ ↑P.cotangentExtendScalarsEquiv) ∘ₗ h1Cotangentι) ∘ₗ ↑P.h1CotangentExtendScalarsEquiv.symm =
    H1Cotangent.δ R P.Ring S
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Cotangent.map P.toExtendScalars ∘ₗ h1Cotangentι ∘ₗ H1Cotangent.map (defaultHom R S P) =
    h1Cotangentι ∘ₗ
      H1Cotangent.map
        ((defaultHom P.Ring S P.extendScalars).comp
          ((Generators.self R S).defaultHom (Generators.self P.Ring S)).toExtensionHom)

Tactic:
← LinearMap.comp_assoc,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (Cotangent.map P.toExtendScalars ∘ₗ h1Cotangentι) ∘ₗ H1Cotangent.map (defaultHom R S P) =
    h1Cotangentι ∘ₗ
      H1Cotangent.map
        ((defaultHom P.Ring S P.extendScalars).comp
          ((Generators.self R S).defaultHom (Generators.self P.Ring S)).toExtensionHom)
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
j : ℕ
⊢ ζ ^ (i * j) - ζ ^ (q * j) ∈ Q

Tactic:
pow_mul,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
j : ℕ
⊢ (ζ ^ i) ^ j - ζ ^ (q * j) ∈ Q
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
⊢ ∃ σ, IsArithFrobAt R σ Q

Tactic:
let P := Q.under R
  have := Algebra.IsInvariant.isIntegral R S G
  have : Q.IsMaximal := Ideal.Quotient.maximal_of_isField _ (Finite.isField_of_domain (S ⧸ Q))
  obtain ⟨p, hc⟩ := CharP.exists (R ⧸ P)
  have : Finite (R ⧸ P) := .of_injective _ Ideal.algebraMap_quotient_injective
  cases nonempty_fintype (R ⧸ P)
  obtain ⟨k, hp, hk⟩ := FiniteField.card (R ⧸ P) p
  have := CharP.of_ringHom_of_ne_zero (algebraMap (R ⧸ P) (S ⧸ Q)) p hp.ne_zero
  have : ExpChar (S ⧸ Q) p := .prime hp
  let l : (S ⧸ Q) ≃ₐ[R ⧸ P] S ⧸ Q :=
    { __ := iterateFrobeniusEquiv (S ⧸ Q) p k,
      commutes' r := by
        dsimp [iterateFrobenius_def]
        rw [← map_pow, ← hk, FiniteField.pow_card] }
  obtain ⟨σ, hσ⟩ := Ideal.Quotient.stabilizerHom_surjective G P Q l
  refine ⟨σ, fun x ↦ ?_⟩
  rw [← Ideal.Quotient.eq, Nat.card_eq_fintype_card, hk]
  exact DFunLike.congr_fun hσ (Ideal.Quotient.mk Q x)

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

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
d : ℕ
⊢ mk 1 ^ (d + 1) = mk fun n ↦ ↑((d + n).choose d)

Tactic:
by
  induction d with
  | zero => ext; simp
  | succ d hd =>
      ext n
      rw [pow_add, hd, pow_one, mul_comm, coeff_mul]
      simp_rw [coeff_mk, Pi.one_apply, one_mul]
      norm_cast
      rw [Finset.sum_antidiagonal_choose_add, add_right_comm]

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

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
⊢ (invOneSubPow S 0).inv = 1

Tactic:
delta invOneSubPow
  simp only [Units.inv_eq_val_inv, inv_one, Units.val_one]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
f : PowerSeries R
g : Γ
hg : ¬g = 0
⊢ (powerSeriesFamily 0 f).hsum.coeff g = (PowerSeries.constantCoeff f • 1).coeff g

Tactic:
coeff_hsum,

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
f : PowerSeries R
g : Γ
hg : ¬g = 0
⊢ ∑ᶠ (i : ℕ), ((powerSeriesFamily 0 f) i).coeff g = (PowerSeries.constantCoeff f • 1).coeff g
Module: Mathlib.RingTheory.HahnSeries.Binomial

Goal state before:
pp: case inr.left
Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
h✝ : Nontrivial A
⊢ (binomialFamily x r).hsum.orderTop = 0

pp: case inr.right
Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
h✝ : Nontrivial A
⊢ (binomialFamily x r).hsum.leadingCoeff = 1

Tactic:
· exact hsum_orderTop_of_le (by simp [hx]) (fun b g hg => binomialFamily_mem_support
        hx r b hg) fun b hb => coeff_eq_zero_of_lt_orderTop <| binomialFamily_orderTop_pos hx r <|
        Nat.zero_lt_of_ne_zero hb

Goal state after:
case inr.right
Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
h✝ : Nontrivial A
⊢ (binomialFamily x r).hsum.leadingCoeff = 1
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
x y : SummableFamily Γ R α
⊢ ⋃ a, ((⇑x + ⇑y) a).support ⊆ (⋃ a, (x a).support) ∪ ⋃ a, (y a).support

Tactic:
rw [← Set.iUnion_union_distrib]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
x y : SummableFamily Γ R α
⊢ ⋃ a, ((⇑x + ⇑y) a).support ⊆ ⋃ i, (x i).support ∪ (y i).support
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
hg : s.hsum.coeff g ≠ 0
⊢ g ∈ ⋃ a, (s a).support

Tactic:
coeff_hsum,

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
hg : ∑ᶠ (i : α), (s i).coeff g ≠ 0
⊢ g ∈ ⋃ a, (s a).support
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddCommMonoid R
ι : Type u_7
inst✝ : DecidableEq ι
i : ι
x : R⟦Γ⟧
g : Γ
⊢ (single i x).hsum.coeff g = x.coeff g

Tactic:
coeff_hsum,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddCommMonoid R
ι : Type u_7
inst✝ : DecidableEq ι
i : ι
x : R⟦Γ⟧
g : Γ
⊢ ∑ᶠ (i_1 : ι), ((single i x) i_1).coeff g = x.coeff g
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
a : α
ha : ↑g = (s a).orderTop
hg : ∀ (b : α), ∀ g' ∈ (s b).support, g ≤ g'
hna : ∀ (b : α), b ≠ a → (s b).coeff g = 0
⊢ s.hsum.coeff g = (s a).coeff g

Tactic:
coeff_hsum,

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
a : α
ha : ↑g = (s a).orderTop
hg : ∀ (b : α), ∀ g' ∈ (s b).support, g ≤ g'
hna : ∀ (b : α), b ≠ a → (s b).coeff g = 0
⊢ ∑ᶠ (i : α), (s i).coeff g = (s a).coeff g
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
⊢ { toFun := fun a ↦ if a = 1 then x ^ a else 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }.hsum.coeff g =
    x.coeff g

Tactic:
coeff_hsum,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
⊢ ∑ᶠ (i : ℕ),
      ({ toFun := fun a ↦ if a = 1 then x ^ a else 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } i).coeff g =
    x.coeff g
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommGroup R
s✝ t : SummableFamily Γ R α
a : α
s s' : SummableFamily Γ R α
⊢ (⋃ a, ((⇑s - ⇑s') a).support).IsPWO

Tactic:
by
        simp_rw [sub_eq_add_neg]
        exact (s + -s').isPWO_iUnion_support

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case refine_1
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal g ⋯
⊢ gh ∈ VAddAntidiagonal g ⋯

Tactic:
simp_all only [mem_vaddAntidiagonal, Function.mem_support, Set.mem_iUnion, mem_support]

Goal state after:
case refine_1
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh : (s a.1).coeff gh.1 ≠ 0 ∧ (t a.2).coeff gh.2 ≠ 0 ∧ gh.1 +ᵥ gh.2 = g
⊢ (∃ i, (s.toFun i).coeff gh.1 ≠ 0) ∧ (∃ i, (t.toFun i).coeff gh.2 ≠ 0) ∧ True
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ PowerSeries.constantCoeff F.zeroX = 0

Tactic:
simp [PowerSeries.constantCoeff, zeroX, PowerSeries.X, MvPowerSeries.constantCoeff_subst_eq_zero
    HasSubst.zero_X _ F.zero_constantCoeff]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ subst ![0, f] F.toPowerSeries = f

Tactic:
calc
    _ = PowerSeries.subst f (F.toPowerSeries.subst ![0, PowerSeries.X (R := R)]) := by
      rw [PowerSeries.subst, subst_comp_subst_apply _ hf.const]
      · congr! 2 with s
        fin_cases s
        · simp [subst, eval₂]
        · simp [PowerSeries.X, subst]
      · exact HasSubst.zero_X
    _ = _ := by
      simp [zeroX_eq_X, PowerSeries.subst_X hf]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding

Goal state before:
pp: M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
hf₁ : Function.Injective ⇑f₁
hf₁class :
  ∀ (a : M), ArchimedeanClass.mk a = (DivisibleHull.archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (f₁ a))
f₂' : DivisibleHull M →ₗ[ℚ] Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
hf₂' : StrictMono ⇑f₂'
hf₂class' :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂' a)).orderTop
f₂ : DivisibleHull M →+o Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ :=
  { toAddMonoidHom := f₂'.toAddMonoidHom, monotone' := ⋯ }
hf₂ : Function.Injective ⇑f₂
hf₂class :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂ a)).orderTop
f₃ : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ →+o Lex ℝ⟦FiniteArchimedeanClass M⟧ :=
  embDomainOrderAddMonoidHom
    (RelIso.toRelEmbedding (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M).symm))
hf₃ : Function.Injective ⇑f₃
hf₃class :
  ∀ (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧),
    (ofLex a).orderTop =
      (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M)).withTopCongr
        (ofLex (f₃ a)).orderTop
a : M
⊢ ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex ((f₃.comp (f₂.comp f₁)) a)).orderTop

Tactic:
hf₁class,

Goal state after:
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
hf₁ : Function.Injective ⇑f₁
hf₁class :
  ∀ (a : M), ArchimedeanClass.mk a = (DivisibleHull.archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (f₁ a))
f₂' : DivisibleHull M →ₗ[ℚ] Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
hf₂' : StrictMono ⇑f₂'
hf₂class' :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂' a)).orderTop
f₂ : DivisibleHull M →+o Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ :=
  { toAddMonoidHom := f₂'.toAddMonoidHom, monotone' := ⋯ }
hf₂ : Function.Injective ⇑f₂
hf₂class :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂ a)).orderTop
f₃ : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ →+o Lex ℝ⟦FiniteArchimedeanClass M⟧ :=
  embDomainOrderAddMonoidHom
    (RelIso.toRelEmbedding (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M).symm))
hf₃ : Function.Injective ⇑f₃
hf₃class :
  ∀ (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧),
    (ofLex a).orderTop =
      (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M)).withTopCongr
        (ofLex (f₃ a)).orderTop
a : M
⊢ (DivisibleHull.archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (f₁ a)) =
    (FiniteArchimedeanClass.withTopOrderIso M) (ofLex ((f₃.comp (f₂.comp f₁)) a)).orderTop
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
r : R
n : Γ
hn : ¬n = 0
⊢ n ∉ ⇑Nat.castOrderEmbedding '' (toPowerSeries.symm (PowerSeries.C r)).support

Tactic:
simp only [not_exists, Set.mem_image, toPowerSeries_symm_apply_coeff, mem_support,
      PowerSeries.coeff_C]

Goal state after:
case neg
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
r : R
n : Γ
hn : ¬n = 0
⊢ ∀ (x : ℕ), ¬((if x = 0 then r else 0) ≠ 0 ∧ Nat.castOrderEmbedding x = n)
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K[X]
x✝¹ : f.Monic
a₀ : K
h₁ : Polynomial.eval a₀ f ∈ maximalIdeal K
x✝ : IsUnit (Polynomial.eval a₀ (derivative f))
⊢ ∃ a, f.IsRoot a ∧ a - a₀ ∈ maximalIdeal K

Tactic:
simp only [(maximalIdeal K).eq_bot_of_prime, Ideal.mem_bot] at h₁ ⊢
    exact ⟨a₀, h₁, sub_self _⟩

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
⊢ IsUnit x

Tactic:
let ⟨⟨u, i, ui, iu⟩, h⟩ := hx
  rw [Units.val_mk] at h
  rw [h] at iu
  have h' := SummableFamily.one_sub_self_mul_hsum_powers (unit_aux x iu _ hxo.addUnit.neg_add)
  rw [sub_sub_cancel] at h'
  exact isUnit_of_mul_isUnit_right (.of_mul_eq_one _ h')

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ Polynomial.eval (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ((taylor (c n)) f) ∈ I ^ (n + 1 + 1)

Tactic:
eval_eq_sum,

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ (((taylor (c n)) f).sum fun e a ↦ a * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ e) ∈
    I ^ (n + 1 + 1)
Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
n : ℤ
⊢ (antipode R) (C a * T n) = C ((antipode R) a) * T (-n)

Tactic:
simp [← single_eq_C_mul_T]

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
⊢ 0 * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ i = 0

Tactic:
rw [zero_mul]

Goal state after:
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingUp R S
inst✝ : HasGoingUp S T
⊢ HasGoingUp R T

Tactic:
by
  rw [iff_specializingMap_primeSpectrumComap, IsScalarTower.algebraMap_eq R S T]
  simp only [PrimeSpectrum.comap_comp]
  apply SpecializingMap.comp
  · rwa [← iff_specializingMap_primeSpectrumComap]
  · rwa [← iff_specializingMap_primeSpectrumComap]

Goal state after: