mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I

Tactic:
simp_rw [or_iff_not_imp_left, SetLike.not_le_iff_exists]

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ {x y : R}, x * y ∈ I → x ∉ I → y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → (∃ x_1 ∈ x, x_1 ∉ I) → y ≤ I
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
⊢ a • D (a * b) = 0

Tactic:
by rw [h, map_one_eq_zero, smul_zero]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ exponent G = 1

Tactic:
exponent,

Goal state after:
case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ (g ^ if h : ExponentExists G then Nat.find h else 0) = 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
G : Type u
inst✝ : Monoid G
g : G
h : ¬ExponentExists G
⊢ g ^ exponent G = 1

Tactic:
exponent,

Goal state after:
case neg
G : Type u
inst✝ : Monoid G
g : G
h : ¬ExponentExists G
⊢ (g ^ if h : ExponentExists G then Nat.find h else 0) = 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ exponent G ≤ n

Tactic:
exponent,

Goal state after:
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ (if h : ExponentExists G then Nat.find h else 0) ≤ n
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x ↦ h ^ x) m = σ h
n : ℤ
⊢ σ ((fun x ↦ h ^ x) n) = (fun x ↦ h ^ x) n ^ m

Tactic:
rw [map_zpow, ← hm, ← zpow_mul, ← zpow_mul']

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case le
G : Type u
inst✝ : Monoid G
h : Subsingleton G
⊢ exponent G ≤ 1

Tactic:
apply exponent_min' _ Nat.one_pos

Goal state after:
case le
G : Type u
inst✝ : Monoid G
h : Subsingleton G
⊢ ∀ (g : G), g ^ 1 = 1
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: α : Type u_3
inst✝ : Group α
a : α
this : Nat.card ↑(MulAction.orbit (↥(zpowers a)) 1) = Function.minimalPeriod (fun x ↦ a • x) 1
⊢ Nat.card ↥(zpowers a) = orderOf a

Tactic:
orbit_subgroup_one_eq_self

Goal state after:
α : Type u_3
inst✝ : Group α
a : α
this : Nat.card ↑↑(zpowers a) = Function.minimalPeriod (fun x ↦ a • x) 1
⊢ Nat.card ↥(zpowers a) = orderOf a
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : G →* H
hϕ : Function.Surjective ⇑ϕ
h : H
g : G
hg : ϕ g = h
k : ℕ
hk : g ^ p ^ k = 1
⊢ h ^ p ^ k = 1

Tactic:
rw [← hg, ← ϕ.map_pow, hk, ϕ.map_one]

Goal state after:
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)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : p ∣ Nat.card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b ∈ ↑(Subgroup.center G), a ≠ b
⊢ Nontrivial ↥(Subgroup.center G)

Tactic:
have dvd : p ∣ Nat.card G := by
    obtain ⟨n, hn0, hn⟩ := hG.nontrivial_iff_card.mp inferInstance
    exact hn.symm ▸ dvd_pow_self _ (ne_of_gt hn0)

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : p ∣ Nat.card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b ∈ ↑(Subgroup.center G), a ≠ b
dvd : p ∣ Nat.card G
⊢ Nontrivial ↥(Subgroup.center G)
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:
obtain ⟨k, hk⟩ := hϕ ⟨g.1 ^ p ^ j, hj⟩

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 : ℕ
hk : ⟨↑g ^ p ^ j, hj⟩ ^ p ^ k = 1
⊢ ∃ k, g ^ p ^ k = 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h.h
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1
n : ℕ
hn : 0 < n
m : M j
hm : m ^ n ≠ 1
⊢ ∃ g, g ^ n ≠ 1

Tactic:
refine ⟨Pi.mulSingle j m, fun h ↦ hm ?_⟩

Goal state after:
case h.h
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1
n : ℕ
hn : 0 < n
m : M j
hm : m ^ n ≠ 1
h : Pi.mulSingle j m ^ n = 1
⊢ m ^ n = 1
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Finite ↥H₁
inst✝ : Finite ↥H₂
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
n₁ n₂ : ℕ
heq₂ : Nat.card ↥H₂ = p₂ ^ n₂
⊢ (p₁ ^ n₁).Coprime (p₂ ^ n₂)

Tactic:
clear heq₂

Goal state after:
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Finite ↥H₁
inst✝ : Finite ↥H₂
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
n₁ n₂ : ℕ
⊢ (p₁ ^ n₁).Coprime (p₂ ^ n₂)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
a b : { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
h : basicOpen ((↑a).1 * (↑b).1) = basicOpen (↑a).1
⊢ a ≤ b

Tactic:
rw [← inf_eq_left]

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
a b : { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
h : basicOpen ((↑a).1 * (↑b).1) = basicOpen (↑a).1
⊢ a ⊓ b = a
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
a b : { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
⊢ basicOpen (↑a).1 ≤ basicOpen (↑b).1 ↔ a ≤ b

Tactic:
rw [← inf_eq_left, ← basicOpen_mul]
    refine ⟨fun h ↦ ?_, (by rw [·])⟩
    rw [← inf_eq_left]
    have := (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1
    exact mul_eq_zero_add_eq_one_ext_left (basicOpen_injOn_isIdempotentElem
      (this.mul (IsIdempotentElem.of_mul_add b.2.1 b.2.2).1) this h)

Goal state after:
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
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
⊢ x ∈ closure (comap f '' zeroLocus ↑I)

Tactic:
obtain ⟨q, hq₁, hq₂⟩ := Ideal.exists_minimalPrimes_le hx

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
q : Ideal R
hq₁ : q ∈ (Ideal.comap f I).minimalPrimes
hq₂ : q ≤ x.asIdeal
⊢ x ∈ closure (comap f '' zeroLocus ↑I)
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 = 1
h1 : ¬Nat.card ↥H = 0
h2 : H.index = 0
⊢ P ≤ H ∨ Disjoint H P

Tactic:
Subgroup.card_eq_one

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 : H = ⊥
h1 : ¬Nat.card ↥H = 0
h2 : H.index = 0
⊢ P ≤ H ∨ Disjoint H P
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p✝ : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
p : ℕ
inst✝ : Fact (Nat.Prime p)
H : Subgroup G
card_eq : Nat.card ↥H = p ^ (Nat.card G).factorization p
⊢ ¬Nat.card ↥H * p ∣ Nat.card ↥H * H.index

Tactic:
card_mul_index,

Goal state after:
p✝ : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
p : ℕ
inst✝ : Fact (Nat.Prime p)
H : Subgroup G
card_eq : Nat.card ↥H = p ^ (Nat.card G).factorization p
⊢ ¬Nat.card ↥H * p ∣ Nat.card G
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : FG G
inst✝ : FG H
f : G →* H
hf : Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ Subgroup.closure ↑(Finset.image (⇑f) S) = ⊤

Tactic:
rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]

Goal state after:
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 + 1) (C r * X) - reflect (b.natDegree + 1) 1) * eval r (reflect c.natDegree c) = 0

Tactic:
reflect_mul _ _ (by simp) (by simp)

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 (C r) * reflect 1 X - reflect (b.natDegree + 1) 1) * eval r (reflect c.natDegree c) = 0
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
tG : IsMulTorsion G
h : H
⊢ IsOfFinOrder h

Tactic:
obtain ⟨g, rfl⟩ := hf h
  exact f.isOfFinOrder (tG g)

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'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ g ^ Classical.choose ⋯ = g

Tactic:
exact Classical.choose_spec <| mem_zpowers_iff.mp <| hg g

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
_hp✝ : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
hnm✝ : n ≤ m
hnm : n < m
h0m : 0 < m
hnm1 : n ≤ m - 1
K : Subgroup G
hK : Nat.card ↥K = p ^ (m - 1) ∧ H ≤ K
⊢ p ^ (m - 1 + 1) ∣ Nat.card G

Tactic:
by rwa [tsub_add_cancel_of_le h0m.nat_succ_le]

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
s : Set R
⊢ (∀ ⦃x : M⦄ ⦃a : ↑s⦄, ↑a • x = 0) ↔ ∀ x ∈ s, x ∈ ↑(annihilator R M)

Tactic:
SetLike.mem_coe,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
⊢ (∀ ⦃x : M⦄ ⦃a : ↑s⦄, ↑a • x = 0) ↔ ∀ x ∈ s, x ∈ annihilator R M
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case neg
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : ¬(eraseLast s).last = x
⊢ ∃ t, head t = head s ∧ t.length + 1 = n + 1 ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)

Tactic:
have imxs : IsMaximal (x ⊓ s.eraseLast.last) s.eraseLast.last :=
        isMaximal_of_eq_inf x s.last rfl (Ne.symm hetx) hm (isMaximal_eraseLast_last h0s)
      have := ih _ _ imxs (le_inf (by simpa) (le_last_of_mem s.eraseLast.head_mem)) (by simp [hn])
      rcases this with ⟨t, htb, htl, htt, hteqv⟩
      have hmtx : IsMaximal t.last x :=
        isMaximal_of_eq_inf s.eraseLast.last s.last (by rw [inf_comm, htt]) hetx
          (isMaximal_eraseLast_last h0s) hm
      use snoc t x hmtx
      refine ⟨by simp [htb], by simp [htl], by simp, ?_⟩
      have : s.Equivalent ((snoc t s.eraseLast.last <| show IsMaximal t.last _ from
        htt.symm ▸ imxs).snoc s.last
          (by simpa using isMaximal_eraseLast_last h0s)) := by
        conv_lhs => rw [eq_snoc_eraseLast h0s]
        exact Equivalent.snoc hteqv (by simpa using iso_refl)
      refine this.trans <| Equivalent.snoc_snoc_swap
        (iso_symm
            (second_iso_of_eq hm
              (sup_eq_of_isMaximal hm (isMaximal_eraseLast_last h0s) (Ne.symm hetx)) htt.symm))
        (second_iso_of_eq (isMaximal_eraseLast_last h0s)
            (sup_eq_of_isMaximal (isMaximal_eraseLast_last h0s) hm hetx) (by rw [inf_comm, htt]))

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
hM : IsTorsionBySet R M ↑I
b : R ⧸ I
⊢ Submodule.toAddSubgroup I ≤ (smulAddHom R M).ker

Tactic:
rwa [isTorsionBySet_iff_subset_annihilator] at hM

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ∏ i ∈ S, ↑⋯.choose ∈ ↑⊤.annihilator

Tactic:
SetLike.mem_coe,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ∏ i ∈ S, ↑⋯.choose ∈ ⊤.annihilator
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case h.succ
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₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n✝ : ℕ
ih : F.N (n₀ + n✝) = I ^ n✝ • F.N n₀
⊢ F.N (n₀ + (n✝ + 1)) = I ^ (n✝ + 1) • F.N n₀

Tactic:
rw [← add_assoc, ← hn, ih, add_comm, pow_add, mul_smul, pow_one]

Goal state after:
case h.succ.a
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₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n✝ : ℕ
ih : F.N (n₀ + n✝) = I ^ n✝ • F.N n₀
⊢ n₀ + n✝ ≥ n₀
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
y : ↑B
⊢ (_root_.KaehlerDifferential.D ↑A ↑B) y ∈ ↑(ModuleCat.Hom.hom (α - β)).ker

Tactic:
SetLike.mem_coe,

Goal state after:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
y : ↑B
⊢ (_root_.KaehlerDifferential.D ↑A ↑B) y ∈ (ModuleCat.Hom.hom (α - β)).ker
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ I.cotangentToQuotientSquare.range = Submodule.map I.cotangentToQuotientSquare ⊤

Tactic:
Submodule.map_top

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ I.cotangentToQuotientSquare.range = I.cotangentToQuotientSquare.range
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
⊢ IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤

Tactic:
constructor
  · intro H
    by_cases I = ⊤; · exact Or.inr ‹_›
    refine Or.inl (eq_bot_iff.mpr ?_)
    rw [← Ideal.iInf_pow_eq_bot_of_isLocalRing I ‹_›]
    apply le_iInf
    rintro (_ | n) <;> simp [H.pow_succ_eq]
  · rintro (rfl | rfl) <;> simp [IsIdempotentElem]

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
F : A → C ⥤ C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  ∀ (m₁ m₂ m₃ : A) (X : C),
    (add (m₁ + m₂) m₃).hom.app X ≫ (F m₃).map ((add m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ (add m₁ (m₂ + m₃)).hom.app X ≫ (add m₂ m₃).hom.app ((F m₁).obj X)
zero_add_hom_app : ∀ (n : A) (X : C), (add 0 n).hom.app X = eqToHom ⋯ ≫ (F n).map (zero.inv.app X)
n : A
X : C
⊢ (F (n + 0)).obj X = (F n).obj X

Tactic:
rw [add_zero]

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
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f : A ⟶ B
⊢ ((single V c j).map f).f j = (singleObjXSelf c j A).hom ≫ f ≫ (singleObjXSelf c j B).inv

Tactic:
by
  dsimp [single]
  rw [dif_pos rfl]
  rfl

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
h : ShiftMkCore C A
n : A
X : C
⊢ (h.F n).obj X = (h.F (n + 0)).obj X

Tactic:
rw [add_zero]

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
A B : V
f : A ⟶ B
⊢ ((single₀ V).map f).f 0 = f

Tactic:
HomologicalComplex.single_map_f_self

Goal state after:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
A B : V
f : A ⟶ B
⊢ (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 A).hom ≫
      f ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 B).inv =
    f
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
a : A
X : C
⊢ (shiftFunctor C (a + 0)).obj X = (shiftFunctor C a).obj X

Tactic:
rw [add_zero]

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
a : A
X : C
⊢ (shiftFunctor C a).obj X = (shiftFunctor C (a + 0)).obj X

Tactic:
rw [add_zero]

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
A B : V
f : A ⟶ B
⊢ ((single₀ V).map f).f 0 = f

Tactic:
HomologicalComplex.single_map_f_self

Goal state after:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
A B : V
f : A ⟶ B
⊢ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 A).hom ≫
      f ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 B).inv =
    f
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i : A
⊢ (shiftFunctor C i).IsEquivalence

Tactic:
by
  change (shiftEquiv C i).functor.IsEquivalence
  infer_instance

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ homologyMap (φ - ψ) i = homologyMap φ i - homologyMap ψ i

Tactic:
by
  dsimp [homologyMap]
  rw [← ShortComplex.homologyMap_sub]
  rfl

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
⊢ d φ i j ≫ sndX φ j = fstX φ i j hij ≫ φ.f j + sndX φ i ≫ G.d i j

Tactic:
dsimp [d]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
⊢ (if hij : c.Rel i j then
        (if hj : c.Rel j (c.next j) then -fstX φ i j hij ≫ F.d j (c.next j) ≫ inlX φ (c.next j) j hj else 0) +
            fstX φ i j hij ≫ φ.f j ≫ inrX φ j +
          sndX φ i ≫ G.d i j ≫ inrX φ j
      else 0) ≫
      sndX φ j =
    fstX φ i j hij ≫ φ.f j + sndX φ i ≫ G.d i j
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K 0
m₁ : ℤ
h₁ : n₁ + 1 = m₁
⊢ δ n₁ m₁ (z₁.comp z₂ ⋯) = z₁.comp (δ 0 1 z₂) h₁ + (δ n₁ m₁ z₁).comp z₂ ⋯

Tactic:
simp only [δ_comp z₁ z₂ (add_zero n₁) m₁ 1 m₁ h₁ h₁ (zero_add 1), one_smul,
    Int.negOnePow_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
z : Cochain F G (-1)
⊢ δ (-1) 0 z = Cochain.ofHom (Homotopy.nullHomotopicMap' fun i j hij ↦ z.v i j ⋯)

Tactic:
ext p
  rw [δ_v (-1) 0 (neg_add_cancel 1) _ p p (add_zero p) (p - 1) (p + 1) rfl rfl]
  simp only [one_smul, Cochain.ofHom_v, Int.negOnePow_zero]
  rw [Homotopy.nullHomotopicMap'_f (show (ComplexShape.up ℤ).Rel (p - 1) p by simp)
    (show (ComplexShape.up ℤ).Rel p (p + 1) by simp)]
  abel

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
⊢ (dNext j) f = P.d j (j + 1) ≫ f (j + 1) j

Tactic:
by
  dsimp [dNext]
  have : (ComplexShape.up ℕ).next j = j + 1 := CochainComplex.next ℕ j
  congr 2

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n : ℤ
z₁ : Cochain F G n
z₂ : Cocycle G K 0
m : ℤ
hnm : n + 1 = m
⊢ δ n m (z₁.comp ↑z₂ ⋯) = (δ n m z₁).comp ↑z₂ ⋯

pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n : ℤ
z₁ : Cochain F G n
z₂ : Cocycle G K 0
m : ℤ
hnm : ¬n + 1 = m
⊢ δ n m (z₁.comp ↑z₂ ⋯) = (δ n m z₁).comp ↑z₂ ⋯

Tactic:
· simp [δ_comp_zero_cochain _ _ _ hnm]

Goal state after:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n : ℤ
z₁ : Cochain F G n
z₂ : Cocycle G K 0
m : ℤ
hnm : ¬n + 1 = m
⊢ δ n m (z₁.comp ↑z₂ ⋯) = (δ n m z₁).comp ↑z₂ ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
K : CochainComplex C ℤ
i j : ℤ
hij : ¬(ComplexShape.up ℤ).Rel i j
⊢ ¬(ComplexShape.up ℤ).Rel (i + n) (j + n)

Tactic:
intro hij'

Goal state after:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
K : CochainComplex C ℤ
i j : ℤ
hij : ¬(ComplexShape.up ℤ).Rel i j
hij' : (ComplexShape.up ℤ).Rel (i + n) (j + n)
⊢ False
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
n : ℤ
⊢ n = n + 0

Tactic:
rw [add_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
n : ℤ
⊢ n + 0 = n

Tactic:
rw [add_zero]

Goal state after: