mathlib-initiative/mathlib-tactics huggingface dataset:
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
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : (Ideal.comap f P).IsPrime
algInst✝¹ : Algebra R S := f.toAlgebra
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
algebraizeInst✝ : Module.Flat R S
⊢ (Localization.localRingHom (Ideal.comap f P) P f ⋯).Flat

Tactic:
have : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
    .of_algebraMap_eq fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : (Ideal.comap f P).IsPrime
algInst✝¹ : Algebra R S := f.toAlgebra
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
algebraizeInst✝ : Module.Flat R S
this : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ (Localization.localRingHom (Ideal.comap f P) P f ⋯).Flat
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (zeroLocus ↑I).Nonempty ∧ IsPreirreducible (zeroLocus ↑I) ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
apply and_congr

Goal state after:
case h₁
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (zeroLocus ↑I).Nonempty ↔ I ≠ ⊤

case h₂
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsPreirreducible (zeroLocus ↑I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
ι : Type u_1
f : ι → R
⊢ ⨆ i, basicOpen (f i) = ⊤ ↔ Ideal.span (Set.range f) = ⊤

Tactic:
rw [SetLike.ext'_iff, Opens.coe_iSup]
  simp only [PrimeSpectrum.basicOpen_eq_zeroLocus_compl, Opens.coe_top, ← Set.compl_iInter,
    ← PrimeSpectrum.zeroLocus_iUnion]
  rw [← PrimeSpectrum.zeroLocus_empty_iff_eq_top, compl_involutive.eq_iff]
  simp only [Set.iUnion_singleton_eq_range, Set.compl_univ, PrimeSpectrum.zeroLocus_span]

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
nc : ¬IsCyclic α
⊢ Nontrivial α

Tactic:
contrapose! nc

Goal state after:
α : Type u_1
inst✝ : Group α
nc : Subsingleton α
⊢ IsCyclic α
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
⊢ exponent G ∣ p

Tactic:
rw [exponent_dvd]
    intro g
    by_cases hg : g = 1
    · simp [hg]
    · rw [h g hg]

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

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : Finite α
inst✝ : IsCyclic α
⊢ ∃ x, ∀ (y : α), y ∈ zpowers x

Tactic:
exact IsCyclic.exists_generator

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
⊢ IsPGroup p G ↔ ∃ n, Nat.card G = p ^ n

Tactic:
isPGroup_iff_card_dvd_pow,

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
⊢ (∃ n, Nat.card G ∣ p ^ n) ↔ ∃ n, Nat.card G = p ^ n
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
⊢ orderOf t < orderOf (t ^ p ^ k * g)

Tactic:
have hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g) := by
    rw [hg, Nat.coprime_pow_right_iff (pos_of_gt hpe), Nat.coprime_comm]
    apply Or.resolve_right (Nat.coprime_or_dvd_of_prime hp _)
    nth_rw 1 [← pow_one p]
    have : 1 = (Nat.factorization (orderOf (t ^ p ^ k))) p + 1 := by
      rw [hpk', Nat.factorization_div hpk]
      simp [k, hp]
    rw [this]
    -- Porting note: convert made to_additive complain
    exact Nat.pow_succ_factorization_not_dvd (hG.orderOf_pos <| t ^ p ^ k).ne' hp

Goal state after:
case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
⊢ orderOf t < orderOf (t ^ p ^ k * g)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ zeroLocus ↑I ⊆ zeroLocus (⇑f '' ↑(Ideal.comap f I))

Tactic:
exact zeroLocus_anti_mono (Set.image_preimage_subset _ _)

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case pos
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime H.index
h1 : ¬Nat.card ↥H = 0
h2 : H.index = 0
⊢ P ≤ H ∨ Disjoint H P

Tactic:
h2,

Goal state after:
case pos
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime 0
h1 : ¬Nat.card ↥H = 0
h2 : H.index = 0
⊢ P ≤ H ∨ Disjoint H P
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime H.index
h1 : ¬Nat.card ↥H = 0
h2 : ¬H.index = 0
this : Finite G
k : ℕ
hk : Nat.card ↥P = p ^ k
⊢ ¬p ∣ Nat.card ↥H ∨ ¬p ∣ H.index

Tactic:
contrapose! h_cop

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h1 : ¬Nat.card ↥H = 0
h2 : ¬H.index = 0
this : Finite G
k : ℕ
hk : Nat.card ↥P = p ^ k
h_cop : p ∣ Nat.card ↥H ∧ p ∣ H.index
⊢ (Nat.card ↥H).gcd H.index ≠ 1
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:
let ⟨i, hi⟩ := b.2

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
a : α
b : ↥(zpowers a)
i : ℤ
hi : (fun x ↦ a ^ x) i = ↑b
⊢ ↑b ^ orderOf a = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
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
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
this : p.natDegree ≤ 1
⊢ eval r (reflect b.natDegree (map (algebraMap R S) b) * X ^ (revAt (1 + c.natDegree)) 0) = 0

Tactic:
← reflect_monomial,

Goal state after:
case refine_2
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
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
this : p.natDegree ≤ 1
⊢ eval r (reflect b.natDegree (map (algebraMap R S) b) * reflect (1 + c.natDegree) (X ^ 0)) = 0
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : H →* G
hf : IsPGroup p ↥f.ker
inst✝ : Finite (Sylow p G)
h_exists : ∀ (P : Sylow p H), ∃ Q, comap f ↑Q = ↑P := fun P ↦ exists_comap_eq_of_ker_isPGroup P hf
g : Sylow p H → Sylow p G := fun P ↦ Classical.choose ⋯
hg : ∀ (P : Sylow p H), comap f ↑(g P) = ↑P
P Q : Sylow p H
h : g P = g Q
⊢ ↑P = ↑Q

Tactic:
rw [← hg, h]

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : H →* G
hf : IsPGroup p ↥f.ker
inst✝ : Finite (Sylow p G)
h_exists : ∀ (P : Sylow p H), ∃ Q, comap f ↑Q = ↑P := fun P ↦ exists_comap_eq_of_ker_isPGroup P hf
g : Sylow p H → Sylow p G := fun P ↦ Classical.choose ⋯
hg : ∀ (P : Sylow p H), comap f ↑(g P) = ↑P
P Q : Sylow p H
h : g P = g Q
⊢ comap f ↑(g Q) = ↑Q
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
⊢ ∀ m < orderOf g, m ≠ 0 → (orderOf g).Coprime m

Tactic:
intro n hn hn0
    exact ((h n).resolve_left (Nat.not_dvd_of_pos_of_lt (Nat.pos_iff_ne_zero.mpr hn0) hn)).symm

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
x✝ : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun x_1 ↦ x * x_1) n 1
⊢ ↑((fun x_1 ↦ ⟨x, ⋯⟩ ^ n * x_1) 1) = 1

Tactic:
change _ * 1 = 1

Goal state after:
G : Type u_1
inst✝ : CommMonoid G
x✝ : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun x_1 ↦ x * x_1) n 1
⊢ ↑(⟨x, ⋯⟩ ^ n) * 1 = 1
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ (a : ι), (∃ μ, ∑ i ∈ {a}, ↑(μ i) = 1) ↔ (↑{a}).Pairwise fun i j ↦ I i ⊔ I j = ⊤

Tactic:
simp only [Finset.sum_singleton, Finset.coe_singleton, Set.pairwise_singleton, iff_true]
    refine fun a => ⟨fun i => if h : i = a then ⟨1, ?_⟩ else 0, ?_⟩
    · simp [h]
    · simp only [dif_pos, Submodule.coe_mk]

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

Goal state before:
pp: case inl
M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod 0)
h✝ : Infinite N
f : ZMod 0 →+ ZMod 2 := (ZMod.castHom ⋯ (ZMod 2)).toAddMonoidHom
hf : Function.Surjective ⇑(ZMod.castHom ⋯ (ZMod 2))
⊢ False

Tactic:
have := isAddCyclic_of_surjective (f.prodMap f) (Prod.map_surjective.mpr ⟨hf, hf⟩)

Goal state after:
case inl
M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod 0)
h✝ : Infinite N
f : ZMod 0 →+ ZMod 2 := (ZMod.castHom ⋯ (ZMod 2)).toAddMonoidHom
hf : Function.Surjective ⇑(ZMod.castHom ⋯ (ZMod 2))
this : IsAddCyclic (ZMod 2 × ZMod 2)
⊢ False
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : ⨆ i ∈ s, f i = ⊤
i : ι
hi : i ∈ s
h : IsAtomistic ↑(Iic (f i))
u : Set ↑(Iic (f i))
hu : ⊤ = sSup u
hu' : ∀ a ∈ u, IsAtom a
⊢ ∀ a ∈ Subtype.val '' u, IsAtom a

Tactic:
· rintro b ⟨⟨a, ha'⟩, ha, rfl⟩
      exact IsAtom.of_isAtom_coe_Iic (hu' _ ha)

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case mp
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
hi : ↑i < s.length
⊢ (fun i ↦ s.toFun ⟨↑i, ⋯⟩) i ≠ last s ∧ (fun i ↦ s.toFun ⟨↑i, ⋯⟩) i ∈ range s.toFun

Tactic:
simp [last, Fin.ext_iff, ne_of_lt hi, -Set.mem_range, Set.mem_range_self]

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h✝ : 0 < s.length
h : x ≠ last s ∧ x ∈ range s.toFun
⊢ x ∈ range fun i ↦ s.toFun ⟨↑i, ⋯⟩

Tactic:
exact mem_eraseLast_of_ne_of_mem h.1 h.2

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case pos
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h✝ : 0 < s.length
x : X
h : x = last s
⊢ x ∈ s ↔ ¬x = last s ∧ x ∈ s ∨ x = last s

Tactic:
simp [*, s.last_mem]

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case neg
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h✝ : 0 < s.length
x : X
h : ¬x = last s
⊢ x ∈ s ↔ ¬x = last s ∧ x ∈ s ∨ x = last s

Tactic:
simp [*, s.last_mem]

Goal state after:
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
m : M
h : torsionOf R M m = ⊤
⊢ 1 ∈ ⊤

Tactic:
exact Submodule.mem_top

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mpr
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
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))
⊢ (∀ n ≥ n₀, I • F.N n = F.N (n + 1)) →
    ∀ (i : ℕ),
      single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))

Tactic:
intro hF

Goal state after:
case mpr
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
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
⊢ ∀ (i : ℕ), single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ IsIdempotentElem I → Subsingleton I.Cotangent

Tactic:
exact fun e =>
      ⟨fun x y =>
        Quotient.inductionOn₂' x y fun x y =>
          I.toCotangent_eq.mpr <| ((pow_two I).trans e).symm ▸ I.sub_mem x.prop y.prop⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
⊢ I.cotangentEquivIdeal.symm ⟨(Submodule.mkQ (I ^ 2)) x, ⋯⟩ = I.toCotangent ⟨x, hx⟩

Tactic:
by
  simp [I.cotangentEquivIdeal.symm_apply_eq, Subtype.ext_iff]

Goal state after:
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
I : Ideal S
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ↥I →ₗ[R] M
hf : ∀ (x y : ↥I), f (x * y) = 0
r : R
x : ↥I
⊢ (↑(QuotientAddGroup.lift (I • ⊤).toAddSubgroup f.toAddMonoidHom ⋯)).toFun (r • I.toCotangent x) =
    (RingHom.id R) r • (↑(QuotientAddGroup.lift (I • ⊤).toAddSubgroup f.toAddMonoidHom ⋯)).toFun (I.toCotangent x)

Tactic:
exact map_smul f _ _

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ (∃ x, ⊤ = ResidueField R ∙ (maximalIdeal R).toCotangent x) ↔ ∃ a, maximalIdeal R = R ∙ a

Tactic:
simp_rw [← Set.image_singleton, eq_comm (a := ⊤), CotangentSpace.span_image_eq_top_iff,
    ← (map_injective_of_injective (injective_subtype _)).eq_iff, map_span, Set.image_singleton,
    Submodule.map_top, range_subtype, eq_comm (a := maximalIdeal R)]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ (∃ x, R ∙ (Submodule.subtype (maximalIdeal R)) x = maximalIdeal R) ↔ ∃ a, R ∙ a = maximalIdeal R
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : J.toCotangent x' = x
this✝ : Function.Surjective ⇑(Algebra.ofId A B)
hx : ↑x' ∈ J ^ 2 ⊔ RingHom.ker (algebraMap A B)
y : A
hy : y ∈ J ^ 2
z : A
hz : z ∈ RingHom.ker (algebraMap A B)
hyz : y + z = ↑x'
this : y + z ∈ J
zmemJ : z ∈ J
xeq : x = J.toCotangent ⟨z, zmemJ⟩
⊢ J.toCotangent ⟨z, zmemJ⟩ ∈
    Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))

Tactic:
exact Submodule.mem_map_of_mem (Submodule.mem_comap.mpr (Ideal.mem_inf.mpr ⟨hz, zmemJ⟩))

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Projective

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
P M✝ : ModuleCat R
inst✝ : Small.{v, u} R
M : ModuleCat R
e : Basis (↑M) R (↑M →₀ Shrink.{v, u} R) := { repr := Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R) }
⊢ Epi (↟((e.constr ℕ) id))

Tactic:
rw [epi_iff_range_eq_top, LinearMap.range_eq_top]

Goal state after:
R : Type u
inst✝¹ : Ring R
P M✝ : ModuleCat R
inst✝ : Small.{v, u} R
M : ModuleCat R
e : Basis (↑M) R (↑M →₀ Shrink.{v, u} R) := { repr := Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R) }
⊢ Function.Surjective ⇑(Hom.hom (↟((e.constr ℕ) id)))
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
X Y✝ : GradedObject J C
e : X ≅ Y✝
F : C ⥤ D ⥤ E
j : J
Y : D
⊢ (F.map (e.inv j ≫ e.hom j)).app Y = 𝟙 ((F.obj (Y✝ j)).obj Y)

Tactic:
inv_hom_id_eval,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
X Y✝ : GradedObject J C
e : X ≅ Y✝
F : C ⥤ D ⥤ E
j : J
Y : D
⊢ (F.map (𝟙 (Y✝ j))).app Y = 𝟙 ((F.obj (Y✝ j)).obj Y)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_3
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx✝ : x ∈ ideal R S
hx : x ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ ∀ (x y : S ⊗[R] S),
    x ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) →
      y ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) →
        (∃ (hx : x ∈ ideal R S), (fromIdeal R S) ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))) →
          (∃ (hx : y ∈ ideal R S), (fromIdeal R S) ⟨y, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))) →
            ∃ (hx : x + y ∈ ideal R S), (fromIdeal R S) ⟨x + y, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

pp: case refine_4
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx✝ : x ∈ ideal R S
hx : x ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ ∀ (a : S),
    ∀ x ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1),
      (∃ (hx : x ∈ ideal R S), (fromIdeal R S) ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))) →
        ∃ (hx : a • x ∈ ideal R S), (fromIdeal R S) ⟨a • x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
· rintro x y - - ⟨hx₁, hx₂⟩ ⟨hy₁, hy₂⟩; exact ⟨add_mem hx₁ hy₁, Submodule.add_mem _ hx₂ hy₂⟩

Goal state after:
case refine_4
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx✝ : x ∈ ideal R S
hx : x ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ ∀ (a : S),
    ∀ x ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1),
      (∃ (hx : x ∈ ideal R S), (fromIdeal R S) ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))) →
        ∃ (hx : a • x ∈ ideal R S), (fromIdeal R S) ⟨a • x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_2.refine_1
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x✝ : ↥(KaehlerDifferential.ideal R S)
hx✝ : x✝ ∈ Submodule.restrictScalars S (KaehlerDifferential.ideal R S • ⊤)
x : S ⊗[R] S
hx : (TensorProduct.lmul' R) x = 0
y : ↥(KaehlerDifferential.ideal R S)
⊢ D.tensorProductTo (x * ↑y) = 0

Tactic:
Derivation.tensorProductTo_mul,

Goal state after:
case refine_2.refine_1
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x✝ : ↥(KaehlerDifferential.ideal R S)
hx✝ : x✝ ∈ Submodule.restrictScalars S (KaehlerDifferential.ideal R S • ⊤)
x : S ⊗[R] S
hx : (TensorProduct.lmul' R) x = 0
y : ↥(KaehlerDifferential.ideal R S)
⊢ (TensorProduct.lmul' R) x • D.tensorProductTo ↑y + (TensorProduct.lmul' R) ↑y • D.tensorProductTo x = 0
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 2 = d₁

Tactic:
by
  change ite (2 = 1 + 1) (d₁ ≫ 𝟙 X₂) 0 = d₁
  rw [if_pos rfl, Category.comp_id]

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

Goal state before:
pp: case pos
C : Type u_1
ι : Type u_2
J : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
inst✝ : DecidableEq ι
j : ι
⊢ PreservesLimitsOfShape J (single C c j ⋙ eval C c j)

Tactic:
exact preservesLimitsOfShape_of_natIso (singleCompEvalIsoSelf C c j).symm

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✝¹ : AddCommMonoid A
inst✝ : HasShift C A
m₁ m₂ m₃ : A
X : C
⊢ ((shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X ≫ (shiftFunctor C m₁).map ((shiftFunctorAdd C m₂ m₃).hom.app X)) ≫
      (shiftFunctorComm C m₁ m₃).inv.app ((shiftFunctor C m₂).obj X) =
    ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X) ≫
        (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).hom.app X) ≫
          (shiftFunctorComm C m₁ m₃).hom.app ((shiftFunctor C m₂).obj X)) ≫
      (shiftFunctorComm C m₁ m₃).inv.app ((shiftFunctor C m₂).obj X)

Tactic:
← cancel_mono (((shiftFunctorComm C m₁ m₂).inv.app X)⟦m₃⟧')

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
m₁ m₂ m₃ : A
X : C
⊢ (((shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X ≫ (shiftFunctor C m₁).map ((shiftFunctorAdd C m₂ m₃).hom.app X)) ≫
        (shiftFunctorComm C m₁ m₃).inv.app ((shiftFunctor C m₂).obj X)) ≫
      (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).inv.app X) =
    (((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X) ≫
          (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).hom.app X) ≫
            (shiftFunctorComm C m₁ m₃).hom.app ((shiftFunctor C m₂).obj X)) ≫
        (shiftFunctorComm C m₁ m₃).inv.app ((shiftFunctor C m₂).obj X)) ≫
      (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).inv.app X)