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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FaithfullyFlat
⊢ Function.Injective ⇑f

Tactic:
algebraize [f]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FaithfullyFlat
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Module.FaithfullyFlat R S
⊢ Function.Injective ⇑f
Module: Mathlib.Algebra.Category.ModuleCat.Descent

Goal state before:
pp: A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.Flat
⊢ PreservesFiniteLimits (tensorLeft ((restrictScalars f).obj (of B B)))

Tactic:
algebraize [f]

Goal state after:
A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.Flat
algInst✝ : Algebra A B := f.toAlgebra
algebraizeInst✝ : Module.Flat A B
⊢ PreservesFiniteLimits (tensorLeft ((restrictScalars f).obj (of B B)))
Module: Mathlib.Algebra.Category.ModuleCat.Descent

Goal state before:
pp: A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
M N : ModuleCat A
g : M ⟶ N
h : IsIso ((extendScalars f).map g)
⊢ IsIso g

Tactic:
algebraize [f]

Goal state after:
A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
M N : ModuleCat A
g : M ⟶ N
h : IsIso ((extendScalars f).map g)
algInst✝ : Algebra A B := f.toAlgebra
algebraizeInst✝ : Module.FaithfullyFlat A B
⊢ IsIso g
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
⊢ f.Flat

Tactic:
algebraize [f]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
algInst✝ : Algebra R S := f.toAlgebra
⊢ f.Flat
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Flat
⊢ GeneralizingMap (comap f)

Tactic:
algebraize [f]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Flat
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Module.Flat R S
⊢ GeneralizingMap (comap f)
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
hf : (Hom.hom f).Flat
hg : Function.Injective ⇑(ConcreteCategory.hom g)
algInst✝¹ : Algebra ↑R ↑S := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑R ↑T := (Hom.hom g).toAlgebra
algebraizeInst✝ : Module.Flat ↑R ↑S
this : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ ⋯.isoPushout.hom = pushout.inl f g
⊢ Function.Injective ⇑(ConcreteCategory.hom (ofHom Algebra.TensorProduct.includeLeftRingHom ≫ ⋯.isoPushout.hom))

Tactic:
exact (CommRingCat.isPushout_tensorProduct R S T).isoPushout.commRingCatIsoToRingEquiv
    |>.injective.comp (Algebra.TensorProduct.includeLeft_injective (S := R) (A := S) hg)

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ ∀ A ∈ Set.range zeroLocus, ∀ B ∈ Set.range zeroLocus, A ∪ B ∈ Set.range zeroLocus

Tactic:
by
      rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩
      exact ⟨_, (union_zeroLocus s t).symm⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
⊢ Monoid.exponent Gᵐᵒᵖ = Monoid.exponent G

Tactic:
simp only [Monoid.exponent, ExponentExists]
  congr!
  all_goals exact ⟨(op_injective <| · <| op ·), (unop_injective <| · <| unop ·)⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : R
p : PrimeSpectrum R
h : (basicOpen f).carrier = {p}
⊢ f ∈ p.asIdeal.primeCompl

Tactic:
apply h ▸ Set.mem_singleton p

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
⊢ ¬ExponentExists G ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1

Tactic:
ExponentExists

Goal state after:
G : Type u
inst✝ : Monoid G
⊢ (¬∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1) ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case ofNat
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ∃ x ∈ H, x ≠ 1
x : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℕ
hk✝ : (fun x ↦ g ^ x) (Int.ofNat k) = x
hk : g ^ Int.ofNat k = x
⊢ g ^ (↑k).natAbs ∈ H

Tactic:
Int.natAbs_natCast k,

Goal state after:
case ofNat
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ∃ x ∈ H, x ≠ 1
x : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℕ
hk✝ : (fun x ↦ g ^ x) (Int.ofNat k) = x
hk : g ^ Int.ofNat k = x
⊢ g ^ k ∈ H
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:
(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.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
⊢ IsPGroup p G ↔ ∀ (g : G), ∃ k, orderOf g ∣ p ^ k

Tactic:
simp_rw [isPGroup_iff_pow_pow_eq_one, orderOf_dvd_iff_pow_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : p ≠ 0
⊢ IsPGroup p G ↔ (Nat.card G).primeFactors ⊆ p.primeFactors

Tactic:
by
  refine isPGroup_iff_card_dvd_pow.trans ⟨fun ⟨n, hn⟩ ↦ ?_, fun hG ↦ ?_⟩
  · rcases eq_or_ne n 0 with (rfl | hn0)
    · simp_all
    grw [← Nat.primeFactors_pow p hn0, Nat.primeFactors_mono hn <| pow_ne_zero n h]
  · refine ⟨Nat.card G, Nat.dvd_prod_primeFactors_pow_self NeZero.out |>.trans ?_⟩
    grw [Finset.prod_dvd_prod_of_subset _ _ (·) hG, p.prod_primeFactors_dvd]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case left
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ (fun x ↦ x ^ n) '' ↑I ⊆ ↑(I ^ n ⊔ J ^ n)

Tactic:
rintro _ ⟨x, hx, rfl⟩

Goal state after:
case left
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ ↑I
⊢ (fun x ↦ x ^ n) x ∈ ↑(I ^ n ⊔ J ^ n)
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
⊢ ∑ a, card { x // Quotient.mk'' x = a } ≡ ∑ _a, 1 [MOD p]

Tactic:
rw [← ZMod.natCast_eq_natCast_iff _ _ p, Nat.cast_sum, Nat.cast_sum]

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
⊢ ∑ x, ↑(card { x_1 // Quotient.mk'' x_1 = x }) = ∑ x, ↑1
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
k : ℕ
hk : card ↑(orbit G b) = p ^ k
hb : k ≠ 0
⊢ ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) = 0

Tactic:
simp [key, hk, hb]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case right
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ (fun x ↦ x ^ n) '' ↑J ⊆ ↑(I ^ n ⊔ J ^ n)

Tactic:
rintro _ ⟨x, hx, rfl⟩

Goal state after:
case right
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ ↑J
⊢ (fun x ↦ x ^ n) x ∈ ↑(I ^ n ⊔ J ^ n)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ¬ExponentExists (M j)
⊢ ¬ExponentExists ((i : ι) → M i)

Tactic:
ExponentExists

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ¬∃ n, 0 < n ∧ ∀ (g : M j), g ^ n = 1
⊢ ¬∃ n, 0 < n ∧ ∀ (g : (i : ι) → M i), g ^ n = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
s : Set (PrimeSpectrum S)
hs : IsClosed s
y : PrimeSpectrum R
x : PrimeSpectrum S
hx : x ∈ s
e : comap f x ⤳ y
⊢ y ∈ comap f '' s

Tactic:
algebraize [f]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
s : Set (PrimeSpectrum S)
hs : IsClosed s
y : PrimeSpectrum R
x : PrimeSpectrum S
hx : x ∈ s
e : comap f x ⤳ y
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.IsIntegral R S
⊢ y ∈ comap f '' s
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
⊢ f.IsIntegral

Tactic:
algebraize [f]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
⊢ f.IsIntegral
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
a : α
b : ↥(zpowers a)
⊢ ↑b ^ orderOf a = 1

Tactic:
by
                  let ⟨i, hi⟩ := b.2
                  rw [← hi, ← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast,
                    pow_orderOf_eq_one, one_zpow]

Goal state after:
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
⊢ ∃ k > 0, Nat.card ↥(center G) = p ^ k

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero (hGpn ▸ pow_ne_zero n (NeZero.ne p))

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
⊢ ∃ k > 0, Nat.card ↥(center G) = p ^ k
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
hinj : Function.Injective ⇑f
⊢ Function.Surjective (comap f)

Tactic:
algebraize [f]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
hinj : Function.Injective ⇑f
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.IsIntegral R S
⊢ Function.Surjective (comap f)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
p : ℕ
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p
hH : Nat.card G' = p
⊢ G ≃* G'

Tactic:
by
  have hGcyc := isCyclic_of_prime_card hG
  have hHcyc := isCyclic_of_prime_card hH
  apply mulEquivOfCyclicCardEq
  exact hG.trans hH.symm

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p G
hP : ↑P ≤ N
⊢ normalizer ↑P ⊔ N = normalizer ↑(map N.subtype ↑(P.subtype hP)) ⊔ N

Tactic:
P.coe_subtype,

Goal state after:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p G
hP : ↑P ≤ N
⊢ normalizer ↑P ⊔ N = normalizer ↑(map N.subtype ((↑P).subgroupOf N)) ⊔ N
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ annihilator R M = ⨅ x, torsionOf R M x

Tactic:
ext r
  simp [Module.mem_annihilator]

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

Goal state before:
pp: R : Type u_2
inst✝⁴ : Ring R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Module.Finite (End R M) M
s : Finset M
hs : span (End R M) ↑s = ⊤
f : End (End R M) M
r : R
hr : ∀ m ∈ s, f m = r • m
m : M
x✝ : m ∈ span (End R M) ↑s
⊢ ((toModuleEnd (End R M) M) r) m = f m

Tactic:
induction hs.ge (trivial : m ∈ ⊤) using Submodule.span_induction with

Goal state after:
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring A
a : A
inst✝⁸ : Algebra R A
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
inst✝⁴ : IsScalarTower R A M
N : Type ?u.26
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module R[X] N
inst✝ : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), f (a • m) = X • f m
p : R[X]
n : ℕ
k : R
h :
  ∀ (x : AEval R M a),
    (f ∘ₗ ↑(of R M a).symm).toFun ((C k * X ^ n) • x) = (C k * X ^ n) • (f ∘ₗ ↑(of R M a).symm).toFun x
m : AEval R M a
⊢ (f ∘ₗ ↑(of R M a).symm).toFun ((C k * X ^ (n + 1)) • m) = (C k * X ^ (n + 1)) • (f ∘ₗ ↑(of R M a).symm).toFun m

Tactic:
AddHom.toFun_eq_coe,

Goal state after:
R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring A
a : A
inst✝⁸ : Algebra R A
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
inst✝⁴ : IsScalarTower R A M
N : Type ?u.26
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module R[X] N
inst✝ : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), f (a • m) = X • f m
p : R[X]
n : ℕ
k : R
h :
  ∀ (x : AEval R M a),
    (f ∘ₗ ↑(of R M a).symm).toAddHom ((C k * X ^ n) • x) = (C k * X ^ n) • (f ∘ₗ ↑(of R M a).symm).toAddHom x
m : AEval R M a
⊢ (f ∘ₗ ↑(of R M a).symm).toAddHom ((C k * X ^ (n + 1)) • m) = (C k * X ^ (n + 1)) • (f ∘ₗ ↑(of R M a).symm).toAddHom m
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
j : ℕ
m : M
⊢ r •
      (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[i]
        (single R j m) =
    single R (i + j) (r • m)

Tactic:
induction i generalizing r j m with
  | zero =>
    rw [Function.iterate_zero, zero_add]
    exact congr(ofCoeff R $(Finsupp.smul_single r j m))
  | succ n hn =>
    rw [Function.iterate_succ, Function.comp_apply, add_assoc, ← hn]
    congr 2
    rw [Nat.one_add]
    exact congr(ofCoeff R $(Finsupp.mapDomain_single))

Goal state after:
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
q : Submodule R[X] (AEval R M a)
⊢ (fun p ↦
        let __AddSubmonoid := AddSubmonoid.map (of R M a) (↑p).toAddSubmonoid;
        { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ })
      ((fun q ↦ ⟨(Submodule.orderIsoMapComap (of R M a)).symm (Submodule.restrictScalars R q), ⋯⟩) q) =
    q

Tactic:
ext; aesop

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ ↑(Submodule.map (monomial 1) I) ⊆ ↑(reesAlgebra I)

Tactic:
rintro _ ⟨r, hr, rfl⟩

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
r : R
hr : r ∈ ↑I
⊢ (monomial 1) r ∈ ↑(reesAlgebra I)
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mp.refine_1
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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
⊢ Monotone fun n₀ ↦ Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))

Tactic:
intro n m e
      rw [Submodule.span_le, Set.iUnion₂_subset_iff]
      intro i hi
      refine Set.Subset.trans ?_ Submodule.subset_span
      refine @Set.subset_iUnion₂ _ _ _ (fun i => fun _ => ↑((single R i) '' ((N F i) : Set M))) i ?_
      exact hi.trans e

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

Goal state before:
pp: case a
R : Type u
inst✝⁴ : CommRing R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ (RingHom.ker f.toRingHom).cotangentIdeal ≤ RingHom.ker f.kerSquareLift.toRingHom

Tactic:
rintro _ ⟨x, hx, rfl⟩

Goal state after:
case a
R : Type u
inst✝⁴ : CommRing R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
x : A
hx : x ∈ ↑(RingHom.ker f.toRingHom)
⊢ (Quotient.mk (RingHom.ker f.toRingHom ^ 2)).toSemilinearMap x ∈ RingHom.ker f.kerSquareLift.toRingHom
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I✝ : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I J : Ideal R
hIJ : I = J
x : I.Cotangent
⊢ (lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq J I ⋯)) ⋯)
      ((lift (J.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I J hIJ)) ⋯).toFun x) =
    x

Tactic:
subst hIJ

Goal state after:
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I✝ : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
x : I.Cotangent
__spread✝⁻⁰ : I.Cotangent →ₗ[R] I.Cotangent := lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯
⊢ (lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯)
      ((lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯).toFun x) =
    x
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I✝ : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I J : Ideal R
hIJ : I = J
x : J.Cotangent
⊢ (lift (J.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I J hIJ)) ⋯).toFun
      ((lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq J I ⋯)) ⋯) x) =
    x

Tactic:
subst hIJ

Goal state after:
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I✝ : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
__spread✝⁻⁰ : I.Cotangent →ₗ[R] I.Cotangent := lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯
x : I.Cotangent
⊢ (lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯).toFun
      ((lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯) x) =
    x
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ X✝ Y✝ : PresheafOfModules R
f : X✝ ⟶ Y✝
X Y : Cᵒᵖ
g : X ⟶ Y
⊢ X✝.presheaf.map g ≫ AddCommGrpCat.ofHom (AddMonoidHom.mk' ⇑(ConcreteCategory.hom (f.app Y)) ⋯) =
    AddCommGrpCat.ofHom (AddMonoidHom.mk' ⇑(ConcreteCategory.hom (f.app X)) ⋯) ≫ Y✝.presheaf.map g

Tactic:
ext x; exact naturality_apply f g x

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.obj n).map ((ε F).app X) = (F.map (λ_ n).inv).app X ≫ (δ F (𝟙_ M) n).app X

Tactic:
rw [map_leftUnitor_inv]

Goal state after:
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.obj n).map ((ε F).app X) = ((λ_ (F.obj n)).inv ≫ ε F ▷ F.obj n ≫ μ F (𝟙_ M) n).app X ≫ (δ F (𝟙_ M) n).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₁ m₂ m₃ : M
X : C
inst✝ : F.Monoidal
⊢ (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₂ ⊗ m₃)).app X ≫ (δ F m₂ m₃).app ((F.obj m₁).obj X)

Tactic:
rw [map_associator]
  dsimp
  simp only [Category.id_comp, Category.assoc, μ_δ_app_assoc, μ_δ_app,
    endofunctorMonoidalCategory_tensorObj_obj, Category.comp_id]

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 ι
A B : HomologicalComplex V c
f : A.Hom B
i j : ι
⊢ f.f i ≫ B.d i j = A.d i j ≫ f.f j

Tactic:
by
  by_cases hij : c.Rel i j
  · exact f.comm' i j hij
  · rw [A.shape i j hij, B.shape i j hij, comp_zero, zero_comp]

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

Goal state before:
pp: case a.refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
⊢ x ⊗ₜ[R] y - (TensorProduct.lmul' R) (x ⊗ₜ[R] y) ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
have : x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] (1 : S) = x • ((1 : S) ⊗ₜ y - y ⊗ₜ (1 : S)) := by
        simp_rw [smul_sub, TensorProduct.smul_tmul', smul_eq_mul, mul_one]

Goal state after:
case a.refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
this : x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1)
⊢ x ⊗ₜ[R] y - (TensorProduct.lmul' R) (x ⊗ₜ[R] y) ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
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 : X ⟶ C.X 0
⊢ ((C.fromSingle₀Equiv X).symm f).f 0 = f

Tactic:
simp [fromSingle₀Equiv]

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 : X ⟶ C.X 0
hf : f ≫ C.d 0 1 = 0
⊢ ((C.fromSingle₀Equiv X).symm ⟨f, hf⟩).f 0 = f

Tactic:
simp [fromSingle₀Equiv]

Goal state after: