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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
⊢ IsNilpotent x ↔ IsNilpotent x.fst

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
⊢ IsNilpotent x → IsNilpotent x.fst

case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
⊢ IsNilpotent x.fst → IsNilpotent x
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ (x ^ n) ^ 2 = 0

Tactic:
ext

Goal state after:
case mpr.h1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ ((x ^ n) ^ 2).fst = fst 0

case mpr.h2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ ((x ^ n) ^ 2).snd = snd 0
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case inl
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
h✝ : IsEmpty ι
⊢ hI.IsSubDPIdeal (I ⊓ ⨅ i, J i)

Tactic:
simp only [iInf_of_empty, le_top, inf_of_le_left]
    exact IsSubDPIdeal.self hI

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : ε * r ∈ I
hx0 : ε * r ≠ 0
⊢ ε * r = fst r • ε

Tactic:
ext

Goal state after:
case h1
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : ε * r ∈ I
hx0 : ε * r ≠ 0
⊢ fst (ε * r) = fst (fst r • ε)

case h2
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : ε * r ∈ I
hx0 : ε * r ≠ 0
⊢ snd (ε * r) = snd (fst r • ε)
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
inst✝ : IsFiniteSplit k R
f : R →ₐ[k] k
⊢ (fun p ↦ (↑(AlgEquiv.ofBijective (ofId k (R ⧸ p.asIdeal)) ⋯).symm).comp (Ideal.Quotient.mkₐ k p.asIdeal))
      ((fun f ↦ { asIdeal := RingHom.ker f, isPrime := ⋯ }) f) =
    f

Tactic:
ext

Goal state after:
k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
inst✝ : IsFiniteSplit k R
f : R →ₐ[k] k
x✝ : R
⊢ ((fun p ↦ (↑(AlgEquiv.ofBijective (ofId k (R ⧸ p.asIdeal)) ⋯).symm).comp (Ideal.Quotient.mkₐ k p.asIdeal))
        ((fun f ↦ { asIdeal := RingHom.ker f, isPrime := ⋯ }) f))
      x✝ =
    f x✝
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = 0
e : R ⊗[R] S ≃ₐ[R] S := TensorProduct.lid R S
⊢ IsFiniteSplit R S

Tactic:
Module.rankAtStalk_eq_zero_iff_subsingleton

Goal state after:
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Subsingleton S
e : R ⊗[R] S ≃ₐ[R] S := TensorProduct.lid R S
⊢ IsFiniteSplit R S
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)
⊢ TensorProduct.lmul' T = (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R)).comp ↑e

Tactic:
ext

Goal state after:
case ha
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)
x✝ : S
⊢ ((AlgHom.restrictScalars R ((TensorProduct.lmul' T).comp TensorProduct.includeLeft)).comp TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            (((TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R)).comp ↑e).comp TensorProduct.includeLeft)).comp
        TensorProduct.includeRight)
      x✝

case hb
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)
x✝ : S
⊢ ((AlgHom.restrictScalars R ((AlgHom.restrictScalars T (TensorProduct.lmul' T)).comp TensorProduct.includeRight)).comp
        TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((AlgHom.restrictScalars T ((TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R)).comp ↑e)).comp
              TensorProduct.includeRight)).comp
        TensorProduct.includeRight)
      x✝
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u₃
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst✝ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
⊢ TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R) =
    (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S))).comp
      (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
        (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T))

Tactic:
ext

Goal state after:
case ha
R : Type u₁
S : Type u₂
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u₃
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst✝ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
x✝ : ULift.{max u₁ u₂ u₃, u₃} T
⊢ (((TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R)).comp TensorProduct.includeLeft) x✝).down =
    ((((AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S))).comp
              (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
                (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T))).comp
          TensorProduct.includeLeft)
        x✝).down

case hb
R : Type u₁
S : Type u₂
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u₃
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst✝ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
x✝ : ULift.{max u₁ u₂ u₃, u₃} T
⊢ (((AlgHom.restrictScalars (ULift.{max (max u₁ u₂) u₃, u₁} R)
              (TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R))).comp
          TensorProduct.includeRight)
        x✝).down =
    (((AlgHom.restrictScalars (ULift.{max (max u₁ u₂) u₃, u₁} R)
              ((AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R)
                    (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S))).comp
                (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
                  (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T)))).comp
          TensorProduct.includeRight)
        x✝).down
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✝
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (IsScalarTower.toAlgHom R P.Ring S).comp (IsScalarTower.toAlgHom R P.Ring P.Ring) =
    (IsScalarTower.toAlgHom R S S).comp (IsScalarTower.toAlgHom R P.Ring S)

Tactic:
ext

Goal state after:
R✝ : Type u
S✝ : Type v
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
inst✝³ : Algebra R✝ S✝
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x✝ : P.Ring
⊢ ((IsScalarTower.toAlgHom R P.Ring S).comp (IsScalarTower.toAlgHom R P.Ring P.Ring)) x✝ =
    ((IsScalarTower.toAlgHom R S S).comp (IsScalarTower.toAlgHom R P.Ring S)) x✝
Module: Mathlib.RingTheory.Etale.Finite

Goal state before:
pp: R : Type u
inst✝⁷ : CommRing R
k : Type u
inst✝⁶ : Field k
Ω : Type w
inst✝⁵ : Field Ω
inst✝⁴ : Algebra R Ω
S : Type w
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra S Ω
inst✝ : IsScalarTower R S Ω
A B : FiniteEtale R
f : A ⟶ B
⊢ ofHom (Algebra.TensorProduct.map (AlgHom.id R R) (Hom.hom f.hom)) ≫ (isoMk (Algebra.TensorProduct.lid R ↑B.obj)).hom =
    (isoMk (Algebra.TensorProduct.lid R ↑A.obj)).hom ≫ f

Tactic:
ext

Goal state after:
R : Type u
inst✝⁷ : CommRing R
k : Type u
inst✝⁶ : Field k
Ω : Type w
inst✝⁵ : Field Ω
inst✝⁴ : Algebra R Ω
S : Type w
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra S Ω
inst✝ : IsScalarTower R S Ω
A B : FiniteEtale R
f : A ⟶ B
x✝ : ↑A.obj
⊢ ((AlgHom.restrictScalars R
            (Hom.hom
              (ofHom (Algebra.TensorProduct.map (AlgHom.id R R) (Hom.hom f.hom)) ≫
                  (isoMk (Algebra.TensorProduct.lid R ↑B.obj)).hom).hom)).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R (Hom.hom ((isoMk (Algebra.TensorProduct.lid R ↑A.obj)).hom ≫ f).hom)).comp
        Algebra.TensorProduct.includeRight)
      x✝
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
⊢ Submodule.comap P.cotangentComplex.ker.subtype (Cotangent.map P.toExtendScalars).ker = ⊥

Tactic:
← cotangentExtendScalarsEquiv_symm_toLinearMap,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Submodule.comap P.cotangentComplex.ker.subtype (↑P.cotangentExtendScalarsEquiv.symm).ker = ⊥
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✝
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (IsScalarTower.toAlgHom P.Ring (Generators.self P.Ring S).toExtension.Ring S).comp
      (ofId P.Ring (Generators.self P.Ring S).toExtension.Ring) =
    (IsScalarTower.toAlgHom P.Ring S S).comp (IsScalarTower.toAlgHom P.Ring P.extendScalars.Ring S)

Tactic:
ext

Goal state after:
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
⊢ Function.Surjective ⇑(map (defaultHom R S P))

Tactic:
rw [← LinearMap.range_eq_top,
    ← (Submodule.map_injective_of_injective h1Cotangentι_injective).eq_iff,
    ← LinearMap.range_comp, ← P.h1CotangentEquivCotangent_comp_map, LinearMap.range_comp,
    ← (Algebra.H1Cotangent.exact_map_δ R P.Ring S).linearMap_ker_eq, Submodule.map_top,
    ← exact_hCotangentι_cotangentComplex.linearMap_ker_eq, Submodule.map_equiv_eq_comap_symm,
    LinearMap.ker, LinearMap.ker, ← Submodule.comap_comp]
  congr
  rw [LinearEquiv.comp_toLinearMap_symm_eq, P.cotangentComplex_comp_h1CotangentEquivCotangent]

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
a b : A
ha : a ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
hb : b ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
⊢ a + b ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}

Tactic:
by
    apply And.intro (I.add_mem ha.1 hb.1) (fun n ↦ ?_)
    rw [hI.dpow_add ha.1 hb.1, hI'.dpow_add ha.1 hb.1]
    exact Finset.sum_congr rfl (fun k _ ↦ by rw [ha.2, hb.2])

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.AlgHom

Goal state before:
pp: R : Type u_1
A : Type u_6
ι : Type u_10
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : 𝒜 →ₐᵍ[R] 𝒜
n : ℕ
⊢ ⇑(f ^ Nat.zero) = (⇑f)^[Nat.zero]

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_6
ι : Type u_10
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : 𝒜 →ₐᵍ[R] 𝒜
n : ℕ
x✝ : A
⊢ (f ^ Nat.zero) x✝ = (⇑f)^[Nat.zero] x✝
Module: Mathlib.RingTheory.GradedAlgebra.AlgHom

Goal state before:
pp: R : Type u_1
A : Type u_6
ι : Type u_10
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : 𝒜 →ₐᵍ[R] 𝒜
n x✝ : ℕ
ih : ⇑(f ^ x✝) = (⇑f)^[x✝]
⊢ ⇑(f ^ x✝.succ) = (⇑f)^[x✝.succ]

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_6
ι : Type u_10
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : 𝒜 →ₐᵍ[R] 𝒜
n x✝¹ : ℕ
ih : ⇑(f ^ x✝¹) = (⇑f)^[x✝¹]
x✝ : A
⊢ (f ^ x✝¹.succ) x✝ = (⇑f)^[x✝¹.succ] x✝
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✝ : Q.IsPrime
⊢ H.localize.IsArithFrobAt (maximalIdeal (Localization.AtPrime Q))

Tactic:
have h : Nat.card (R ⧸ (maximalIdeal _).comap (algebraMap R (Localization.AtPrime Q))) =
      Nat.card (R ⧸ Q.under R) := by
    congr 2
    rw [← Ideal.under_def, ← Ideal.under_under (B := S), Localization.AtPrime.under_maximalIdeal]

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✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
⊢ H.localize.IsArithFrobAt (maximalIdeal (Localization.AtPrime Q))
Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst✝¹² : DecidableEq ι
inst✝¹¹ : AddMonoid ι
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : 𝒜 →ₐᵍ[R] fun x ↦ Submodule.restrictScalars R (ℬ x)
i✝ : ι
r : S
x : ↥(𝒜 i✝)
hx : ↑((toBaseChange S (𝒜 i✝)) (r ⊗ₜ[R] x)) ∈ baseChange S (𝒜 i✝)
⊢ f ↑x ∈ ℬ i✝

Tactic:
exact f.map_mem x.2

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
⊢ (map f) (invUnitsSub u) = invUnitsSub ((Units.map ↑f) u)

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
n✝ : ℕ
⊢ (coeff n✝) ((map f) (invUnitsSub u)) = (coeff n✝) (invUnitsSub ((Units.map ↑f) u))
Module: Mathlib.RingTheory.PowerSeries.WellKnown

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

Tactic:
ext

Goal state after:
case zero
S : Type u_1
inst✝ : CommRing S
d n✝ : ℕ
⊢ (coeff n✝) (mk 1 ^ (0 + 1)) = (coeff n✝) (mk fun n ↦ ↑((0 + n).choose 0))
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
⊢ (map f) (sin A) = sin A'

Tactic:
ext

Goal state after:
A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
n✝ : ℕ
⊢ (coeff n✝) ((map f) (sin A)) = (coeff n✝) (sin A')
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
⊢ (map f) (cos A) = cos A'

Tactic:
ext

Goal state after:
A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
n✝ : ℕ
⊢ (coeff n✝) ((map f) (cos A)) = (coeff n✝) (cos A')
Module: Mathlib.RingTheory.HahnSeries.Binomial

Goal state before:
pp: case inr
Γ : 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 ∧ (binomialFamily x r).hsum.leadingCoeff = 1

Tactic:
constructor

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

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
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
⊢ hsum 0 = 0

Tactic:
ext

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
x✝ : Γ
⊢ (hsum 0).coeff x✝ = HahnSeries.coeff 0 x✝
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
hs : s.hsum ≠ 0
this : ⋯.min ⋯ = g
⊢ ∑ᶠ (i : α), (s i).coeff g = (s a).coeff g

Tactic:
finsum_eq_single (fun i ↦ (s i).coeff g) a hna

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
hs : s.hsum ≠ 0
this : ⋯.min ⋯ = g
⊢ (s a).coeff g = (s a).coeff g
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : d 1 = 0
hd₀ : d 0 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0

Tactic:
simp [hd₀, hd₁]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
x : Fin (Nat.succ 0).succ
⊢ ![0, 0] x = 0 x

Tactic:
fin_cases x

Goal state after:
case «0»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ ![0, 0] ((fun i ↦ i) ⟨0, ⋯⟩) = 0 ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ ![0, 0] ((fun i ↦ i) ⟨1, ⋯⟩) = 0 ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 1 1
hd₁ : d 0 = 0
hd₀ : d 1 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![0, PowerSeries.X] s ^ e) = 0

Tactic:
simp [hd₀, hd₁]

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

Goal state before:
pp: case refine_1
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
x✝ : Γ × Γ'
hgh : ¬s.hsum.coeff x✝.1 = 0 ∧ ¬t.hsum.coeff x✝.2 = 0 ∧ x✝.1 +ᵥ x✝.2 = g
⊢ (∃ i, ¬(s i).coeff x✝.1 = 0) ∧ ∃ i, ¬(t i).coeff x✝.2 = 0

Tactic:
constructor

Goal state after:
case refine_1.left
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
x✝ : Γ × Γ'
hgh : ¬s.hsum.coeff x✝.1 = 0 ∧ ¬t.hsum.coeff x✝.2 = 0 ∧ x✝.1 +ᵥ x✝.2 = g
⊢ ∃ i, ¬(s i).coeff x✝.1 = 0

case refine_1.right
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
x✝ : Γ × Γ'
hgh : ¬s.hsum.coeff x✝.1 = 0 ∧ ¬t.hsum.coeff x✝.2 = 0 ∧ x✝.1 +ᵥ x✝.2 = g
⊢ ∃ i, ¬(t i).coeff x✝.2 = 0
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : R⟦ℕ⟧
⊢ (fun f ↦ { coeff := fun n ↦ (PowerSeries.coeff n) f, isPWO_support' := ⋯ }) ((fun f ↦ PowerSeries.mk f.coeff) f) = f

Tactic:
ext

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : R⟦ℕ⟧
x✝ : ℕ
⊢ ((fun f ↦ { coeff := fun n ↦ (PowerSeries.coeff n) f, isPWO_support' := ⋯ })
          ((fun f ↦ PowerSeries.mk f.coeff) f)).coeff
      x✝ =
    f.coeff x✝
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : PowerSeries R
⊢ (fun f ↦ PowerSeries.mk f.coeff) ((fun f ↦ { coeff := fun n ↦ (PowerSeries.coeff n) f, isPWO_support' := ⋯ }) f) = f

Tactic:
ext

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : PowerSeries R
n✝ : ℕ
⊢ (PowerSeries.coeff n✝)
      ((fun f ↦ PowerSeries.mk f.coeff)
        ((fun f ↦ { coeff := fun n ↦ (PowerSeries.coeff n) f, isPWO_support' := ⋯ }) f)) =
    (PowerSeries.coeff n✝) f
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝ : Semiring R
f g : R⟦ℕ⟧
⊢ PowerSeries.mk (f + g).coeff = PowerSeries.mk f.coeff + PowerSeries.mk g.coeff

Tactic:
ext

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝ : Semiring R
f g : R⟦ℕ⟧
n✝ : ℕ
⊢ (PowerSeries.coeff n✝) (PowerSeries.mk (f + g).coeff) =
    (PowerSeries.coeff n✝) (PowerSeries.mk f.coeff + PowerSeries.mk g.coeff)
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 Γ
n : Γ
hn : ¬n = 1
⊢ (embDomain Nat.castOrderEmbedding (toPowerSeries.symm PowerSeries.X)).coeff n = 0

Tactic:
rw [embDomain_notin_image_support]
    simp only [not_exists, Set.mem_image, toPowerSeries_symm_apply_coeff, mem_support,
      PowerSeries.coeff_X]
    intro
    simp +contextual [Ne.symm hn]

Goal state after: