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

Goal state before:
pp: n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
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 = ↑(n + 1)
h✝ : Nontrivial R
⊢ Nontrivial S

Tactic:
apply Module.nontrivial_of_rankAtStalk_pos (R := R)

Goal state after:
n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
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 = ↑(n + 1)
h✝ : Nontrivial R
⊢ 0 < Module.rankAtStalk S
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 Ω✝
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
X : FintypeCat
⊢ { obj := fun X ↦ Opposite.op (of Ω (X.obj → Ω)),
            map := fun {X Y} f ↦
              (ofHom (AlgHom.pi fun i ↦ Pi.evalAlgHom Ω (fun a ↦ Ω) ((ConcreteCategory.hom f) i))).op,
            map_id := ⋯, map_comp := ⋯ }.map
        ((NatIso.ofComponents
                (fun X ↦
                  FintypeCat.equivEquivIso
                    ((Equiv.sigmaUnique ((𝟭 FintypeCat).obj X).obj fun a ↦ PrimeSpectrum Ω).symm.trans
                      (PrimeSpectrum.sigmaToPiHomeo fun a ↦ Ω).toEquiv))
                ⋯).hom.app
          X) ≫
      (NatIso.ofComponents (fun R ↦ (isoMk (Algebra.FormallyEtale.equivPiOfIsSepClosed Ω ↑(Opposite.unop R).obj)).op)
              ⋯).hom.app
        ({ obj := fun X ↦ Opposite.op (of Ω (X.obj → Ω)),
              map := fun {X Y} f ↦
                (ofHom (AlgHom.pi fun i ↦ Pi.evalAlgHom Ω (fun a ↦ Ω) ((ConcreteCategory.hom f) i))).op,
              map_id := ⋯, map_comp := ⋯ }.obj
          X) =
    𝟙
      ({ obj := fun X ↦ Opposite.op (of Ω (X.obj → Ω)),
            map := fun {X Y} f ↦
              (ofHom (AlgHom.pi fun i ↦ Pi.evalAlgHom Ω (fun a ↦ Ω) ((ConcreteCategory.hom f) i))).op,
            map_id := ⋯, map_comp := ⋯ }.obj
        X)

Tactic:
dsimp [FiniteEtale.finiteSpec]
      apply Quiver.Hom.unop_inj
      ext x i
      dsimp
      rw [FintypeCat.equivEquivIso_apply_hom, FintypeCat.homMk_apply]
      dsimp
      rw [← Pi.coe_evalAlgHom Ω]
      simp [Algebra.FormallyEtale.equivPiOfIsSepClosed_comap,
        Algebra.FormallyEtale.equivPiOfIsSepClosed_self_apply]

Goal state after:
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
h : Infinite (R ⧸ Ideal.under R Q)
⊢ Q = ⊤

Tactic:
simpa using

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
h : Infinite (R ⧸ Ideal.under R Q)
⊢ 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
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
x : S ⧸ Q
hx : H.restrict x = 0
⊢ x = 0

Tactic:
simpa using

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
x : S ⧸ Q
hx : H.restrict x = 0
⊢ x = 0
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
x : S
hx : x ∈ Ideal.comap φ Q
⊢ x ∈ Q

Tactic:
rwa [← Ideal.Quotient.eq_zero_iff_mem, ← H.restrict_injective.eq_iff, map_zero, restrict_mk,
    Ideal.Quotient.eq_zero_iff_mem, ← Ideal.mem_comap]

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.IsSubDPIdeal (J ⊓ I)
⊢ hI.IsSubDPIdeal (RingHom.ker (Ideal.Quotient.mk J) ⊓ I)

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.IsSubDPIdeal (J ⊓ I)
⊢ hI.IsSubDPIdeal (J ⊓ I)
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: case add
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ (i : ι) ⦃x : A⦄, x ∈ s → ↑(((decompose 𝒜) x) i) ∈ s
x x✝ y✝ : A
hx✝ : x✝ ∈ Subsemiring.closure s
hy✝ : y✝ ∈ Subsemiring.closure s
h₁ : ∀ (i : ι), ↑(((decompose 𝒜) x✝) i) ∈ Subsemiring.closure s
h₂ : ∀ (i : ι), ↑(((decompose 𝒜) y✝) i) ∈ Subsemiring.closure s
i : ι
⊢ ↑(((decompose 𝒜) (x✝ + y✝)) i) ∈ Subsemiring.closure s

Tactic:
simpa using

Goal state after:
case add
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ (i : ι) ⦃x : A⦄, x ∈ s → ↑(((decompose 𝒜) x) i) ∈ s
x x✝ y✝ : A
hx✝ : x✝ ∈ Subsemiring.closure s
hy✝ : y✝ ∈ Subsemiring.closure s
h₁ : ∀ (i : ι), ↑(((decompose 𝒜) x✝) i) ∈ Subsemiring.closure s
h₂ : ∀ (i : ι), ↑(((decompose 𝒜) y✝) i) ∈ Subsemiring.closure s
i : ι
⊢ ↑(((decompose 𝒜) x✝) i) + ↑(((decompose 𝒜) y✝) i) ∈ Subsemiring.closure s
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
σ σ' : G
H : IsArithFrobAt R σ Q
H' : IsArithFrobAt R σ' Q
x : S
⊢ (σ * σ'⁻¹) • x - x ∈ Submodule.toAddSubgroup Q

Tactic:
simpa using

Goal state after:
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
σ σ' : G
H : IsArithFrobAt R σ Q
H' : IsArithFrobAt R σ' Q
x : S
⊢ σ • σ'⁻¹ • x - x ∈ Q
Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
S : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
i j : ι
x : A
hx : x ∈ ↑(𝒜 i)
y : A
hy : y ∈ ↑(𝒜 j)
⊢ (↑(Algebra.lmul S (S ⊗[R] A)) (((TensorProduct.mk R S A) 1) x)) (((TensorProduct.mk R S A) 1) y) ∈
    ↑(span S ↑(Submodule.map ((TensorProduct.mk R S A) 1) (𝒜 (i + j))))

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_3
S : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
i j : ι
x : A
hx : x ∈ ↑(𝒜 i)
y : A
hy : y ∈ ↑(𝒜 j)
⊢ 1 ⊗ₜ[R] (x * y) ∈ span S ((fun a ↦ 1 ⊗ₜ[R] a) '' ↑(𝒜 (i + j)))
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
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
this : Ideal.under R (Ideal.map ((MulSemiringAction.toRingEquiv G S) τ) Q) = Ideal.under R Q
⊢ (RingEquiv.symm ((MulSemiringAction.toRingAut G S) τ))
      ((MulSemiringAction.toAlgHom R S (τ * σ * τ⁻¹)) x -
        x ^ Nat.card (R ⧸ Ideal.under R (Ideal.comap (RingEquiv.symm ((MulSemiringAction.toRingAut G S) τ)) Q))) ∈
    Q

Tactic:
simpa using

Goal state after:
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
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
this : Ideal.under R (Ideal.map ((MulSemiringAction.toRingEquiv G S) τ) Q) = Ideal.under R Q
⊢ σ • τ⁻¹ • x - (τ⁻¹ • x) ^ Nat.card (R ⧸ Ideal.under R Q) ∈ Q
Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct

Goal state before:
pp: case tmul
ι : 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✝)
⊢ ((AlgHom.liftEquiv R S A B) ↑f).toRingHom ↑((toBaseChange S (𝒜 i✝)) (r ⊗ₜ[R] x)) ∈ ℬ i✝

Tactic:
simpa using

Goal state after:
case tmul
ι : 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✝)
⊢ r • f ↑x ∈ ℬ i✝
Module: Mathlib.RingTheory.Grassmannian

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
k : ℕ
A : Type w
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
N : G(k, A ⊗[R] M; A)
this✝ : Algebra A B := f.toAlgebra
this : IsScalarTower R A B := IsScalarTower.of_algebraMap_eq' (IsScalarTower.algebraMap_eq R A B)
equiv : (B ⊗[R] M ⧸ (baseChangeMkQ B N.toSubmodule).ker) ≃ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)
p : PrimeSpectrum B
⊢ rankAtStalk (B ⊗[R] M ⧸ (baseChangeMkQ B N.toSubmodule).ker) p = rankAtStalk (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) p

Tactic:
simpa using

Goal state after:
R : Type u
inst✝⁶ : CommRing R
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
k : ℕ
A : Type w
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
N : G(k, A ⊗[R] M; A)
this✝ : Algebra A B := f.toAlgebra
this : IsScalarTower R A B := IsScalarTower.of_algebraMap_eq' (IsScalarTower.algebraMap_eq R A B)
equiv : (B ⊗[R] M ⧸ (baseChangeMkQ B N.toSubmodule).ker) ≃ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)
p : PrimeSpectrum B
⊢ rankAtStalk (B ⊗[R] M ⧸ (baseChangeMkQ B N.toSubmodule).ker) p = rankAtStalk (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) p
Module: Mathlib.RingTheory.Grassmannian

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
k : ℕ
A : Type w
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
N : G(k, A ⊗[R] M; A)
this✝ : Algebra A B := f.toAlgebra
this : IsScalarTower R A B := IsScalarTower.of_algebraMap_eq' (IsScalarTower.algebraMap_eq R A B)
equiv : (B ⊗[R] M ⧸ (baseChangeMkQ B N.toSubmodule).ker) ≃ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)
p : PrimeSpectrum B
⊢ rankAtStalk (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) p =
    rankAtStalk (A ⊗[R] M ⧸ N.toSubmodule) (PrimeSpectrum.comap (algebraMap A B) p)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝⁶ : CommRing R
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
k : ℕ
A : Type w
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
N : G(k, A ⊗[R] M; A)
this✝ : Algebra A B := f.toAlgebra
this : IsScalarTower R A B := IsScalarTower.of_algebraMap_eq' (IsScalarTower.algebraMap_eq R A B)
equiv : (B ⊗[R] M ⧸ (baseChangeMkQ B N.toSubmodule).ker) ≃ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)
p : PrimeSpectrum B
⊢ rankAtStalk (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) p =
    rankAtStalk (A ⊗[R] M ⧸ N.toSubmodule) (PrimeSpectrum.comap (algebraMap A B) p)
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
d e : ℕ
⊢ invOneSubPow S (d + e) = invOneSubPow S d * invOneSubPow S e

Tactic:
by
  simp_rw [invOneSubPow_eq_inv_one_sub_pow, pow_add]

Goal state after:
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
  simp [sin, apply_ite f]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ binomialSeries A 0 = 1

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ binomialSeries A 0 = 1
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : 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
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
⊢ ∑ x_1 ∈ HasAntidiagonal.antidiagonal n,
      (PowerSeries.coeff x_1.1) a • (PowerSeries.coeff x_1.2) b • ((powers x) n).coeff g ≠
    0

Tactic:
simpa using

Goal state after:
Γ : 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
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
⊢ ¬∑ x_1 ∈ HasAntidiagonal.antidiagonal n, (PowerSeries.coeff x_1.1) a • (PowerSeries.coeff x_1.2) b • (x ^ n).coeff g =
      0
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : 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
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
hz : n = 0
⊢ g = 0 ∧ (PowerSeries.constantCoeff a * PowerSeries.constantCoeff b) • 1 ≠ 0

Tactic:
simpa using

Goal state after:
Γ : 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
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
hz : n = 0
⊢ g = 0 ∧ ¬(PowerSeries.constantCoeff a * PowerSeries.constantCoeff b) • 1 = 0
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case pos
Γ : 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
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
hz : n = 0
⊢ n ∈ ↑(image (fun i ↦ i.1 + i.2) (Set.Finite.toFinset ⋯))

Tactic:
have : g = 0 ∧ (a.constantCoeff * b.constantCoeff) • (1 : V) ≠ 0 := by
        simpa [hz, h] using hn
      simp only [coe_image, Set.mem_image]
      use (0, 0)
      simp [this.2, this.1, h, hz, smul_smul, mul_comm]

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

Goal state before:
pp: Γ : 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
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
i : ℕ
hi : i ∈ image (fun i ↦ i.1 + i.2) (((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support
his : i ∉ ((powerSeriesFamily x (a * b)).coeff g).support
⊢ (PowerSeries.coeff i) (a * b) • (x ^ i).coeff g = 0

Tactic:
simpa using

Goal state after:
Γ : 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
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
i : ℕ
hi : i ∈ image (fun i ↦ i.1 + i.2) (((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support
his : i ∉ ((powerSeriesFamily x (a * b)).coeff g).support
⊢ ∑ i_1 ∈ HasAntidiagonal.antidiagonal i,
      ((PowerSeries.coeff i_1.1) a * (PowerSeries.coeff i_1.2) b) • (x ^ i).coeff g =
    0
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✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
⊢ ∀ (ab : α × β), ((fun ab ↦ (of R).symm (s ab.1 • (of R) (t ab.2))) ab).support ⊆ (s ab.1).support +ᵥ (t ab.2).support

Tactic:
intro ab

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✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
ab : α × β
⊢ ((fun ab ↦ (of R).symm (s ab.1 • (of R) (t ab.2))) ab).support ⊆ (s ab.1).support +ᵥ (t ab.2).support
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✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
⊢ (⋃ a, ((fun a ↦ (of R).symm (s a.1 • (of R) (t a.2))) a).support).IsPWO

Tactic:
apply (hs.vadd ht).mono
  have hsupp : ∀ ab : α × β, support ((fun ab ↦ (of R).symm (s ab.1 • (of R) (t ab.2))) ab) ⊆
      (s ab.1).support +ᵥ (t ab.2).support := by
    intro ab
    refine Set.Subset.trans (fun x hx => ?_) (support_vaddAntidiagonal_subset_vadd fun a ↦
      Set.VAddAntidiagonal.finite_of_isPWO (s ab.1).isPWO_support (t ab.2).isPWO_support a)
    simp only [Set.mem_ofPred_eq]
    contrapose! hx
    rw [mem_support, not_not, HahnModule.coeff_smul, hx, sum_empty]
  refine Set.Subset.trans (Set.iUnion_mono fun a => (hsupp a)) ?_
  simp_all only [Set.iUnion_subset_iff, Prod.forall]
  exact fun a b => Set.vadd_subset_vadd (Set.subset_iUnion_of_subset a fun x y ↦ y)
    (Set.subset_iUnion_of_subset b fun x y ↦ y)

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

Goal state before:
pp: case h₁
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module ℚ M
inst✝ : IsOrderedModule ℚ M
strata : HahnEmbedding.ArchimedeanStrata ℚ M
f : (c : FiniteArchimedeanClass M) → ↥(strata.stratum c) →+o ℝ
hf : ∀ (c : FiniteArchimedeanClass M), Function.Injective ⇑(f c)
c : FiniteArchimedeanClass M
⊢ Monotone ⇑(f c).toRatLinearMap

Tactic:
simpa using

Goal state after:
case h₁
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module ℚ M
inst✝ : IsOrderedModule ℚ M
strata : HahnEmbedding.ArchimedeanStrata ℚ M
f : (c : FiniteArchimedeanClass M) → ↥(strata.stratum c) →+o ℝ
hf : ∀ (c : FiniteArchimedeanClass M), Function.Injective ⇑(f c)
c : FiniteArchimedeanClass M
⊢ Monotone ⇑(f c)
Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding

Goal state before:
pp: case h₂
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module ℚ M
inst✝ : IsOrderedModule ℚ M
strata : HahnEmbedding.ArchimedeanStrata ℚ M
f : (c : FiniteArchimedeanClass M) → ↥(strata.stratum c) →+o ℝ
hf : ∀ (c : FiniteArchimedeanClass M), Function.Injective ⇑(f c)
c : FiniteArchimedeanClass M
⊢ Function.Injective ⇑(f c).toRatLinearMap

Tactic:
simpa using

Goal state after:
case h₂
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module ℚ M
inst✝ : IsOrderedModule ℚ M
strata : HahnEmbedding.ArchimedeanStrata ℚ M
f : (c : FiniteArchimedeanClass M) → ↥(strata.stratum c) →+o ℝ
hf : ∀ (c : FiniteArchimedeanClass M), Function.Injective ⇑(f c)
c : FiniteArchimedeanClass M
⊢ Function.Injective ⇑(f c)
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: 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 : ¬∑ i ∈ (s.coeff x✝.1).support, (s i).coeff x✝.1 = 0 ∧ ¬t.hsum.coeff x✝.2 = 0 ∧ x✝.1 +ᵥ x✝.2 = g
h' : ∃ a ∈ (s.coeff x✝.1).support, (s a).coeff x✝.1 ≠ 0
⊢ ∃ i, ¬(s i).coeff x✝.1 = 0

Tactic:
simpa using

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 : ¬∑ i ∈ (s.coeff x✝.1).support, (s i).coeff x✝.1 = 0 ∧ ¬t.hsum.coeff x✝.2 = 0 ∧ x✝.1 +ᵥ x✝.2 = g
h' : ∃ a ∈ (s.coeff x✝.1).support, (s a).coeff x✝.1 ≠ 0
⊢ ∃ i, ¬(s i).coeff x✝.1 = 0
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h1 : IsUnit ((a * y - 1) * 1 + 1)
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
⊢ IsUnit a ∧ IsUnit y

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h1 : IsUnit ((a * y - 1) * 1 + 1)
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
⊢ IsUnit a ∧ IsUnit y
Module: Mathlib.RingTheory.HopfAlgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
ha : IsGroupLikeElem R a
⊢ (antipode R) a * a = 1

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
ha : IsGroupLikeElem R a
⊢ (antipode R) a * a = 1
Module: Mathlib.RingTheory.HopfAlgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
ha : IsGroupLikeElem R a
⊢ a * (antipode R) a = 1

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
ha : IsGroupLikeElem R a
⊢ a * (antipode R) a = 1
Module: Mathlib.RingTheory.HahnSeries.Cardinal

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x : R⟦Γ⟧
a : Γ
r : R
⊢ ((single a) r * x).cardSupp ≤ x.cardSupp

Tactic:
simpa using

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x : R⟦Γ⟧
a : Γ
r : R
⊢ ((single a) r * x).cardSupp ≤ x.cardSupp