mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case h
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
⊢ (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩ ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range

Tactic:
have hs₁ : QuotientGroup.mk (s := S) ∘ s = id := funext hs

Goal state after:
case h
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
⊢ (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩ ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
⊢ d • ∑ x ∈ s, c x • x ⊗ₜ[R] x = d • comul (d • a)

Tactic:
rw [← hc]; simp +contextual [(hs _ _).comul_eq_tmul_self]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Quotient

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (((↑(Algebra.TensorProduct.assoc R R R (A ⧸ I) (A ⧸ I) (A ⧸ I))).comp
            ((Algebra.TensorProduct.map (comulAlgHom I) (AlgHom.id R (A ⧸ I))).comp (comulAlgHom I))).comp
        (Ideal.Quotient.mkₐ R I)).toLinearMap =
    (((Algebra.TensorProduct.map (AlgHom.id R (A ⧸ I)) (comulAlgHom I)).comp (comulAlgHom I)).comp
        (Ideal.Quotient.mkₐ R I)).toLinearMap

Tactic:
simp only [coassoc_simps, AlgHom.comp_toLinearMap, Algebra.TensorProduct.toLinearMap_map,
      comul_comp_mkₐ, counit_comp_mkₐ]

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (↑(Algebra.TensorProduct.assoc R R R (A ⧸ I) (A ⧸ I) (A ⧸ I))).toLinearMap ∘ₗ
      map (map (Ideal.Quotient.mkₐ R I).toLinearMap (Ideal.Quotient.mkₐ R I).toLinearMap ∘ₗ comul)
          ((AlgHom.id R (A ⧸ I)).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap) ∘ₗ
        comul =
    map ((AlgHom.id R (A ⧸ I)).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap)
        (map (Ideal.Quotient.mkₐ R I).toLinearMap (Ideal.Quotient.mkₐ R I).toLinearMap ∘ₗ comul) ∘ₗ
      comul
Module: Mathlib.RingTheory.Bialgebra.Quotient

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (((Algebra.TensorProduct.map (counitAlgHom I) (AlgHom.id R (A ⧸ I))).comp (comulAlgHom I)).comp
        (Ideal.Quotient.mkₐ R I)).toLinearMap =
    ((↑(Algebra.TensorProduct.lid R (A ⧸ I)).symm).comp (Ideal.Quotient.mkₐ R I)).toLinearMap

Tactic:
simp only [coassoc_simps, AlgHom.comp_toLinearMap, Algebra.TensorProduct.toLinearMap_map,
      comul_comp_mkₐ, counit_comp_mkₐ]

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ map counit ((AlgHom.id R (A ⧸ I)).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap) ∘ₗ comul =
    (↑(Algebra.TensorProduct.lid R (A ⧸ I)).symm).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap
Module: Mathlib.RingTheory.Bialgebra.Quotient

Goal state before:
pp: case refine_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (((Algebra.TensorProduct.map (AlgHom.id R (A ⧸ I)) (counitAlgHom I)).comp (comulAlgHom I)).comp
        (Ideal.Quotient.mkₐ R I)).toLinearMap =
    ((↑(Algebra.TensorProduct.rid R R (A ⧸ I)).symm).comp (Ideal.Quotient.mkₐ R I)).toLinearMap

Tactic:
simp only [coassoc_simps, AlgHom.comp_toLinearMap, Algebra.TensorProduct.toLinearMap_map,
      comul_comp_mkₐ, counit_comp_mkₐ]

Goal state after:
case refine_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ map ((AlgHom.id R (A ⧸ I)).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap) counit ∘ₗ comul =
    (↑(Algebra.TensorProduct.rid R R (A ⧸ I)).symm).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap
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
r : R
n : ℕ
m : M
⊢ ↑(X (n, r • m)) = r ^ n • ↑(X (n, m))

Tactic:
← RingCon.coe_smul

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
n : ℕ
m : M
⊢ ↑(X (n, r • m)) = ↑(r ^ n • X (n, m))
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case pos
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : n = 0
⊢ dpow n 0 = ↑(#(∅.sym n))

pp: case neg
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ dpow n 0 = ↑(#(∅.sym n))

Tactic:
· rw [hn]
      rw [dpow_zero I.zero_mem]
      simp only [sym_zero, card_singleton, cast_one]

Goal state after:
case neg
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ dpow n 0 = ↑(#(∅.sym n))
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case insert
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec : s.Nonempty → (∀ i ∈ s, r i ∈ I) → hI.dpow n (∏ i ∈ s, r i) = n ! ^ (#s - 1) • ∏ i ∈ s, hI.dpow n (r i)
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
⊢ hI.dpow n (∏ i ∈ insert a s, r i) = n ! ^ (#(insert a s) - 1) • ∏ i ∈ insert a s, hI.dpow n (r i)

Tactic:
rw [Finset.prod_insert has]

Goal state after:
case insert
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec : s.Nonempty → (∀ i ∈ s, r i ∈ I) → hI.dpow n (∏ i ∈ s, r i) = n ! ^ (#s - 1) • ∏ i ∈ s, hI.dpow n (r i)
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
⊢ hI.dpow n (r a * ∏ x ∈ s, r x) = n ! ^ (#(insert a s) - 1) • ∏ i ∈ insert a s, hI.dpow n (r i)
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:
by
  rw [algHom_ext_iff]
  intros; simp [map_apply_dp]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
K : Ideal A
hK : hI.IsSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J

Tactic:
rintro y ⟨x, hx, rfl⟩

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
K : Ideal A
hK : hI.IsSubDPIdeal K
x : A
hx : x ∈ ↑K
⊢ f x ∈ ↑J
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ⋃ i ∈ (fun J ↦ J.carrier) '' S, ↑i ⊆ ↑I

Tactic:
rintro a ⟨-, ⟨J, rfl⟩, haJ⟩

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
a : A
J : Ideal A
haJ : a ∈ (fun i ↦ ⋃ (_ : i ∈ (fun J ↦ J.carrier) '' S), ↑i) J
⊢ a ∈ ↑I
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
h : ⋃ i ∈ (fun J ↦ J.carrier) '' S, ↑i ⊆ ↑I
n : ℕ
hn : n ≠ 0
x : A
K : hI.SubDPIdeal
hKS : K ∈ S
h' : x ∈ (fun x ↦ ↑((fun J ↦ J.carrier) K)) ⋯
⊢ hI.dpow n x ∈ ↑((fun J ↦ J.carrier) K)

Tactic:
exact K.dpow_mem _ hn x h'

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

Goal state before:
pp: case refine_3
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
x y : A
hx : x ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
⊢ y ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} →
    (∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}) →
      (∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}) →
        ∀ (n : ℕ), n ≠ 0 → hI.dpow n (x + y) ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
hy

Goal state after:
case refine_3
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
x y : A
hx : x ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hy : y ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
⊢ (∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}) →
    (∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}) →
      ∀ (n : ℕ), n ≠ 0 → hI.dpow n (x + y) ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n✝ : ℕ
a : A
ha : a ∈ I
hx : f a ∈ J
b : A
hb : b ∈ I
hy : f b ∈ J
k : ℕ × ℕ
x✝ : k ∈ Finset.antidiagonal n✝
⊢ f (hI.dpow k.1 a * hI.dpow k.2 b) = f (hI.dpow k.1 a) * dpow hI f k.2 (f b)

Tactic:
dpow_apply' hI hIf hb,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n✝ : ℕ
a : A
ha : a ∈ I
hx : f a ∈ J
b : A
hb : b ∈ I
hy : f b ∈ J
k : ℕ × ℕ
x✝ : k ∈ Finset.antidiagonal n✝
⊢ f (hI.dpow k.1 a * hI.dpow k.2 b) = f (hI.dpow k.1 a) * f (hI.dpow k.2 b)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a b : A
hb : b ∈ I
hy : f b ∈ J
⊢ dpow hI f n (f a * f b) = f a ^ n * dpow hI f n (f b)

Tactic:
dpow_apply' hI hIf hb,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a b : A
hb : b ∈ I
hy : f b ∈ J
⊢ dpow hI f n (f a * f b) = f a ^ n * f (hI.dpow n b)
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
⊢ (Ideal.Quotient.mk Q) (φ x) = 0

Tactic:
Ideal.Quotient.eq_zero_iff_mem,

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
hx : x ∈ Ideal.comap φ Q
⊢ φ x ∈ Q
Module: Mathlib.RingTheory.Grassmannian

Goal state before:
pp: case add
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
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB : Function.Surjective ⇑fAB
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
x✝ : C ⊗[R] M
hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker
hfBC_ker_eq : (map g (map f N)).toSubmodule = fBC.ker
x y : C ⊗[R] M
hx : fAC x = e (fBC x)
hy : fAC y = e (fBC y)
⊢ e (fBC x) + fAC y = e (fBC x) + e (fBC y)

Tactic:
hy

Goal state after:
case add
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
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB : Function.Surjective ⇑fAB
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
x✝ : C ⊗[R] M
hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker
hfBC_ker_eq : (map g (map f N)).toSubmodule = fBC.ker
x y : C ⊗[R] M
hx : fAC x = e (fBC x)
hy : fAC y = e (fBC y)
⊢ e (fBC x) + e (fBC y) = e (fBC x) + e (fBC y)
Module: Mathlib.RingTheory.PowerSeries.WellKnown

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

Tactic:
← mk_one_pow_eq_mk_choose_add,

Goal state after:
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
⊢ mk 1 ^ (d + 1) * (1 - X) ^ (d + 1) = 1
Module: Mathlib.RingTheory.PowerSeries.WellKnown

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

Tactic:
← mk_one_pow_eq_mk_choose_add,

Goal state after:
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
⊢ (1 - X) ^ (d + 1) * mk 1 ^ (d + 1) = 1
Module: Mathlib.RingTheory.PowerSeries.WellKnown

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

Tactic:
by
  simp [invOneSubPow_add, Units.val_mul, mul_comm, mul_assoc, ← invOneSubPow_inv_eq_one_sub_pow]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ subst ![subst ![PowerSeries.X, 0] F.toPowerSeries, 0] F.toPowerSeries = F.Xzero

Tactic:
by
      have : ![0, 0] = (0 : Fin 2 → PowerSeries R) := by
        ext x : 1; fin_cases x <;> rfl
      simp [F.assoc', this, subst_zero_of_constantCoeff_zero F.zero_constantCoeff,
        PowerSeries.HasSubst.X', PowerSeries.HasSubst]

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
y : Γ
ys : y ∈ ⋃ n, (x ^ n).support
⊢ (∀ z ∈ ⋃ n, (x ^ n).support, z < y → {a | ((fun n ↦ x ^ n) a).coeff z ≠ 0}.Finite) →
    {a | ((fun n ↦ x ^ n) a).coeff y ≠ 0}.Finite

Tactic:
hy

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
y : Γ
ys : y ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < y → {a | ((fun n ↦ x ^ n) a).coeff z ≠ 0}.Finite
⊢ {a | ((fun n ↦ x ^ n) a).coeff y ≠ 0}.Finite
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
⊢ maximalIdeal R ≤ ⊥.jacobson

Tactic:
by
    rw [Ideal.jacobson, le_sInf_iff]
    rintro I ⟨-, hI⟩
    exact (eq_maximalIdeal hI).ge

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

Goal state before:
pp: case singleton
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingUp R S
q : PrimeSpectrum R
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver (RelSeries.singleton {(a, b) | a < b} q).head.asIdeal
⊢ List.map (PrimeSpectrum.comap (algebraMap R S))
      (RelSeries.singleton {(a, b) | a < b} { asIdeal := P, isPrime := ⋯ }).toList =
    (RelSeries.singleton {(a, b) | a < b} q).toList

Tactic:
simpa [PrimeSpectrum.ext_iff] using lo.over.symm

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
⊢ q.height = 0

Tactic:
rw [← WithBot.coe_inj,
    ← IsLocalization.AtPrime.ringKrullDim_eq_height q (Localization.AtPrime q),
    WithBot.coe_zero, ← ringKrullDimZero_iff_ringKrullDim_eq_zero,
    ← isArtinianRing_iff_krullDimLE_zero, isArtinianRing_iff_isNilpotent_maximalIdeal,
    ← Localization.AtPrime.map_eq_maximalIdeal]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
⊢ IsNilpotent (map (algebraMap R (Localization.AtPrime q)) q)
Module: Mathlib.RingTheory.Ideal.UFD

Goal state before:
pp: case neg.refine_2
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : WfDvdMonoid R
x : R
hx : Prime x
p : Ideal R
inst✝³ : p.IsPrime
hxp : x ∉ p
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away x S
this : Disjoint ↑(Submonoid.powers x) ↑p
hpbot : ¬p = ⊥
hi : Function.Injective ⇑(algebraMap R S)
hpb : map (algebraMap R S) p ≠ ⊥
g : S
hg : map (algebraMap R S) p = S ∙ g
hg0 : g ≠ 0
a : R
n : ℤ
hxa : ¬x ∣ a
hag : selfZPow x S n * (algebraMap R S) a = g
hu : IsUnit (selfZPow x S n)
y : R
⊢ x * y ∈ R ∙ a → y ∈ R ∙ a

Tactic:
hy

Goal state after:
case neg.refine_2
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : WfDvdMonoid R
x : R
hx : Prime x
p : Ideal R
inst✝³ : p.IsPrime
hxp : x ∉ p
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away x S
this : Disjoint ↑(Submonoid.powers x) ↑p
hpbot : ¬p = ⊥
hi : Function.Injective ⇑(algebraMap R S)
hpb : map (algebraMap R S) p ≠ ⊥
g : S
hg : map (algebraMap R S) p = S ∙ g
hg0 : g ≠ 0
a : R
n : ℤ
hxa : ¬x ∣ a
hag : selfZPow x S n * (algebraMap R S) a = g
hu : IsUnit (selfZPow x S n)
y : R
hy : x * y ∈ R ∙ a
⊢ y ∈ R ∙ a
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: case directed
A : Type u_1
inst✝ : Ring A
F G : IdealFilter A
⊢ DirectedOn (fun x1 x2 ↦ x1 ≥ x2) {L | ∃ K ∈ G, F.IsTorsionQuot L K}

Tactic:
rintro I ⟨K, hK, hIK⟩ J ⟨L, hL, hJL⟩

Goal state after:
case directed
A : Type u_1
inst✝ : Ring A
F G : IdealFilter A
I K : Ideal A
hK : K ∈ G
hIK : F.IsTorsionQuot I K
J L : Ideal A
hL : L ∈ G
hJL : F.IsTorsionQuot J L
⊢ ∃ z ∈ {L | ∃ K ∈ G, F.IsTorsionQuot L K}, (fun x1 x2 ↦ x1 ≥ x2) I z ∧ (fun x1 x2 ↦ x1 ≥ x2) J z
Module: Mathlib.RingTheory.IdealFilter.Topology

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
s : Set (WithIdealFilter F)
⊢ s ∈ 𝓝 0 ↔ ∃ I ∈ F, idealSet I ⊆ s

Tactic:
by
  simpa [zero_vadd] using mem_nhds_iff (a := 0) (s := s)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
x : R
hx : x ∈ I
y : R
hy : y ∈ I
heq : x = x * y
this : IsUnit ((algebraMap R (Localization.AtPrime p)) (1 - y))
⊢ x ∈ RingHom.ker (algebraMap R (Localization.AtPrime p))

Tactic:
have hzero : x * (1 - y) = 0 := by simp [mul_sub, ← heq]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
x : R
hx : x ∈ I
y : R
hy : y ∈ I
heq : x = x * y
this : IsUnit ((algebraMap R (Localization.AtPrime p)) (1 - y))
hzero : x * (1 - y) = 0
⊢ x ∈ RingHom.ker (algebraMap R (Localization.AtPrime p))