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

Goal state before:
pp: R S T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.FaithfullyFlat
hg : g.FaithfullyFlat
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Module.FaithfullyFlat R S
algebraizeInst✝ : Module.FaithfullyFlat S T
⊢ (g.comp f).FaithfullyFlat

Tactic:
← algebraMap_toAlgebra (g.comp f),

Goal state after:
R S T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.FaithfullyFlat
hg : g.FaithfullyFlat
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Module.FaithfullyFlat R S
algebraizeInst✝ : Module.FaithfullyFlat S T
⊢ (algebraMap R T).FaithfullyFlat
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
hs : IsClosed s
ht : IsClosed t
⊢ vanishingIdeal t ≤ vanishingIdeal s ∧ ¬vanishingIdeal s ≤ vanishingIdeal t ↔ vanishingIdeal t < vanishingIdeal s

Tactic:
lt_iff_le_not_ge

Goal state after:
R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
hs : IsClosed s
ht : IsClosed t
⊢ vanishingIdeal t ≤ vanishingIdeal s ∧ ¬vanishingIdeal s ≤ vanishingIdeal t ↔
    vanishingIdeal t ≤ vanishingIdeal s ∧ ¬vanishingIdeal s ≤ vanishingIdeal t
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ IsIrreducible s ↔ (vanishingIdeal s).IsPrime

Tactic:
rw [← isIrreducible_iff_closure, ← zeroLocus_vanishingIdeal_eq_closure,
    isIrreducible_zeroLocus_iff_of_radical _ (isRadical_vanishingIdeal s)]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : n = 0
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

pp: case neg
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

Tactic:
· simp [hn]

Goal state after:
case neg
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
⊢ D (a ^ n) = n • a ^ (n - 1) • D a
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr.mpr
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
⊢ False

Tactic:
have h₂ : n % exponent G < exponent G := Nat.mod_lt _ (exponent_pos_of_exists n hpos hG)

Goal state after:
case inr.mpr
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ False
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf
      (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)) *
        y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)

Tactic:
rw [(h.pow_pow _ _).orderOf_mul_eq_mul_orderOf_of_coprime]

Goal state after:
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y))) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)

G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)))).Coprime
    (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))))
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : m = 0
⊢ False

Tactic:
rw [hm0, mul_zero, Fintype.card_eq_zero_iff] at hm

Goal state after:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : IsEmpty α
hm0 : m = 0
⊢ False
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
n : ℕ
hn : p.Coprime n
g : G
⊢ (hG.powEquiv hn).symm g = g ^ (orderOf g).gcdB n

Tactic:
rw [← Nat.card_zpowers]

Goal state after:
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
n : ℕ
hn : p.Coprime n
g : G
⊢ (hG.powEquiv hn).symm g = g ^ (Nat.card ↥(Subgroup.zpowers g)).gcdB n
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ϕ ↑g ^ p ^ j = ↑1
⊢ ∃ k, g ^ p ^ k = 1

Tactic:
← ϕ.map_pow

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ϕ (↑g ^ p ^ j) = ↑1
⊢ ∃ k, g ^ p ^ k = 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case H'
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
g : G
hx : x < orderOf g
hg : orderOf g = exponent G
⊢ ∃ a ∈ Set.range fun g ↦ orderOf g, x < a

Tactic:
simp_rw [Set.mem_range, exists_exists_eq_and]

Goal state after:
case H'
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
g : G
hx : x < orderOf g
hg : orderOf g = exponent G
⊢ ∃ a, x < orderOf a
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this : Finite G
⊢ ∃ k > 0, Nat.card ↥(center G) = p ^ k

Tactic:
have hcG := to_subgroup (of_card hGpn) (center G)

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this : Finite G
hcG : IsPGroup p ↥(center G)
⊢ ∃ k > 0, Nat.card ↥(center G) = p ^ k
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ a * b = y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b)

Tactic:
simp [mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ y ^ m * (y ^ n * (y ^ (-m) * a)) * (y ^ (-n) * b) = y ^ m * y ^ n * y ^ (-m) * (a * (y ^ (-n) * b))

Tactic:
simp [mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = f.ker
tH : IsMulTorsion H
tN : IsMulTorsion ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : f g ^ ngn = 1
gn : ↥N
h : ↑gn = g ^ ngn
hmem : ↑gn ∈ f.ker
nn : ℕ
nnpos : 0 < nn
hnn : gn ^ nn = 1
⊢ ↑gn ^ nn = 1

Tactic:
← Subgroup.coe_pow,

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = f.ker
tH : IsMulTorsion H
tN : IsMulTorsion ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : f g ^ ngn = 1
gn : ↥N
h : ↑gn = g ^ ngn
hmem : ↑gn ∈ f.ker
nn : ℕ
nnpos : 0 < nn
hnn : gn ^ nn = 1
⊢ ↑(gn ^ nn) = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝² : Finite α
this✝¹ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this✝ : orderOf g ∈ (p ^ 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
⊢ ?m.163

Tactic:
simpa using this

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
p k : ℕ
hp : Nat.Prime p
h : p ^ k ∣ Nat.card G
this✝ : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ k
this : ∀ g ∈ (↑H \ {1}).toFinset, p ∣ orderOf g
⊢ p ^ k ∣ ∏ i ∈ (↑H \ {1}).toFinset, orderOf i

Tactic:
← prod_dvd_prod_of_dvd _ _ this,

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
p k : ℕ
hp : Nat.Prime p
h : p ^ k ∣ Nat.card G
this✝ : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ k
this : ∀ g ∈ (↑H \ {1}).toFinset, p ∣ orderOf g
⊢ p ^ k ∣ ∏ i ∈ (↑H \ {1}).toFinset, p
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_2.refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i✝¹ : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
i✝ : Fin ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length)
i : Fin (s.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)
⊢ Iso
    (((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun i.castSucc.castSucc.castSucc,
      ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun i.castSucc.castSucc.succ)
    (((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun
        ((Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc) i.castSucc.castSucc).castSucc,
      ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun
        ((Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc) i.castSucc.castSucc).succ)

Tactic:
erw [Equiv.swap_apply_of_ne_of_ne h2 h1, snoc_castSucc, snoc_castSucc,
          snoc_castSucc, snoc_castSucc, Fin.succ_castSucc, snoc_castSucc,
          Fin.succ_castSucc, snoc_castSucc, snoc_castSucc, snoc_castSucc]

Goal state after:
case refine_2.refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i✝¹ : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
i✝ : Fin ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length)
i : Fin (s.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)
⊢ Iso (s.toFun i.castSucc, s.toFun i.succ) (s.toFun i.castSucc, s.toFun i.succ)
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : IsSemisimpleRing R
I : Ideal R
⊢ ∃ e, IsIdempotentElem e ∧ I = Ideal.span {e}

Tactic:
obtain ⟨J, h⟩ := exists_isCompl I

Goal state after:
R : Type u_2
inst✝¹ : Ring R
inst✝ : IsSemisimpleRing R
I J : Ideal R
h : IsCompl I J
⊢ ∃ e, IsIdempotentElem e ∧ I = Ideal.span {e}
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : Ring S
M : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
a : Module.End R M
a0 : a ≠ 0
⊢ (a * if h : a = 0 then 0 else ↑(LinearEquiv.ofBijective a ⋯).symm) = 1

Tactic:
simp_rw [dif_neg a0]

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : Ring S
M : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
a : Module.End R M
a0 : a ≠ 0
⊢ a * ↑(LinearEquiv.ofBijective a ⋯).symm = 1
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : R ∙ v i ⊓ Submodule.span R (Set.range fun i_1 ↦ v ↑i_1) = ⊥
this : r • v i ∈ ⊥
⊢ r ∈ torsionOf R M (v i)

Tactic:
simpa using this

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
⊢ a * ↑(μ i) ∈ p j

Tactic:
by_cases ij : j = i

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : j = i
⊢ a * ↑(μ i) ∈ p j

case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : ¬j = i
⊢ a * ↑(μ i) ∈ p j
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_5
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
x y : PolynomialModule R M
r✝ r₁ r₂ : R
m✝ m' m₁ m₂ m₁' m₂' : M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ ((s • m).coeff.sum fun i m ↦ r ^ i • m) = (RingHom.id R) s • m.coeff.sum fun i m ↦ r ^ i • m

Tactic:
refine (Finsupp.sum_smul_index' ?_).trans ?_

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_5
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
x y : PolynomialModule R M
r✝ r₁ r₂ : R
m✝ m' m₁ m₂ m₁' m₂' : M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ ∀ (i : ℕ), r ^ i • 0 = 0

case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_5
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
x y : PolynomialModule R M
r✝ r₁ r₂ : R
m✝ m' m₁ m₂ m₁' m₂' : M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ (((coeffEquiv R).toFun m).sum fun i c ↦ r ^ i • s • c) = (RingHom.id R) s • m.coeff.sum fun i m ↦ r ^ i • m
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
i j k : ℕ
⊢ I ^ (i + k) • F.N j ≤ I ^ k • F.N (i + j)

Tactic:
rw [add_comm, pow_add, mul_smul]
  exact smul_mono_right _ (F.pow_smul_le i j)

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
r : ↥(reesAlgebra I)
f : PolynomialModule R M
hf : f ∈ {f | ∀ (i : ℕ), f.coeff i ∈ F.N i}
i : ℕ
⊢ ∑ x ∈ Finset.antidiagonal i, (↑r).coeff x.1 • f.coeff x.2 ∈ F.N i

Tactic:
apply Submodule.sum_mem

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
r : ↥(reesAlgebra I)
f : PolynomialModule R M
hf : f ∈ {f | ∀ (i : ℕ), f.coeff i ∈ F.N i}
i : ℕ
⊢ ∀ c ∈ Finset.antidiagonal i, (↑r).coeff c.1 • f.coeff c.2 ∈ F.N i
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : PresheafOfModules R
f : unit R ⟶ M
⊢ (fun s ↦
        { app := fun X ↦ ModuleCat.ofHom ((ringLmapEquivSelf ↑(R.obj X) ℤ ↑(M.obj X)).symm (↑s X)), naturality := ⋯ })
      ((fun f ↦ sectionsMk (fun X ↦ (ConcreteCategory.hom (f.app X)) 1) ⋯) f) =
    f

Tactic:
ext X : 2

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : PresheafOfModules R
f : unit R ⟶ M
X : Cᵒᵖ
⊢ ModuleCat.Hom.hom
      (((fun s ↦
              { app := fun X ↦ ModuleCat.ofHom ((ringLmapEquivSelf ↑(R.obj X) ℤ ↑(M.obj X)).symm (↑s X)),
                naturality := ⋯ })
            ((fun f ↦ sectionsMk (fun X ↦ (ConcreteCategory.hom (f.app X)) 1) ⋯) f)).app
        X) =
    ModuleCat.Hom.hom (f.app X)
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n m' n' : M
f : m ⟶ m'
g : n ⟶ n'
X : C
inst✝ : F.LaxMonoidal
this :
  ((F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X)) ≫ (μ F m' n').app X =
    (μ F m n).app X ≫ (F.map (f ⊗ₘ g)).app X
⊢ (F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X) ≫ (μ F m' n').app X =
    (μ F m n).app X ≫ (F.map (f ⊗ₘ g)).app X

Tactic:
simpa using this

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (η F).app ((F.obj n).obj X) =
    (μ F n (𝟙_ M)).app X ≫ (δ F n (𝟙_ M)).app X ≫ (η F).app ((F.obj n).obj X) ≫ 𝟙 ((F.obj n).obj X)

Tactic:
simp only [Category.comp_id, μ_δ_app_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.LaxMonoidal
this :
  (F.obj m₃).map ((μ F m₁ m₂).app X) ≫ (μ F (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    𝟙 ((F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X))) ≫
      (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫ (μ F m₁ (m₂ ⊗ m₃)).app X
⊢ (F.obj m₃).map ((μ F m₁ m₂).app X) ≫ (μ F (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫ (μ F m₁ (m₂ ⊗ m₃)).app X

Tactic:
simpa using this

Goal state after:
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
hf : C.d 1 0 ≫ f = 0
⊢ ((C.toSingle₀Equiv X).symm ⟨f, hf⟩).f 0 = f

Tactic:
simp [toSingle₀Equiv]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
⊢ (shiftFunctorZero C A).hom.app X ≫ f ≫ (shiftFunctorZero C A).inv.app Y = (shiftFunctor C 0).map f

Tactic:
apply NatIso.naturality_2

Goal state after:
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
f : C.X 0 ⟶ X
⊢ ((C.toSingle₀Equiv X).symm f).f 0 = f

Tactic:
simp [toSingle₀Equiv]

Goal state after:
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
f : C₁.Hom C₂
i j : ι
w : c.Rel i j
⊢ f.prev j = (C₁.xPrevIso w).hom ≫ f.f i ≫ (C₂.xPrevIso w).inv

Tactic:
obtain rfl := c.prev_eq' w
  simp only [xPrevIso, eqToIso_refl, Iso.refl_hom, Iso.refl_inv, comp_id, id_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst✝ : K.HasHomology i
⊢ Mono (K.homologyι i)

Tactic:
by
  dsimp only [homologyι]
  infer_instance

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (kerTotal R A) ⊔
      Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
        (Submodule.span A (Set.range fun x ↦ single ((algebraMap R A) x) 1)) =
    Submodule.restrictScalars A (kerTotal R B)

Tactic:
← kerTotal_map R R A B h,

Goal state after:
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (kerTotal R A) ⊔
      Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
        (Submodule.span A (Set.range fun x ↦ single ((algebraMap R A) x) 1)) =
    Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (kerTotal R A) ⊔
      Submodule.span A (Set.range fun x ↦ single ((algebraMap R B) x) 1)
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
⊢ W.isoClosure.IsInvertedBy F → W.IsInvertedBy F

Tactic:
intro h X Y f hf

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
h : W.isoClosure.IsInvertedBy F
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (F.map f)