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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ ∀ (s : Set (PrimeSpectrum R)), (∃ s_1, s = zeroLocus s_1) → ∃ s_1, comap f ⁻¹' s = zeroLocus s_1

Tactic:
rintro _ ⟨s, rfl⟩

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
s : Set R
⊢ ∃ s_1, comap f ⁻¹' zeroLocus s = zeroLocus s_1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ TopologicalSpace.IsTopologicalBasis (Set.range fun r ↦ ↑(basicOpen r))

Tactic:
apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds

Goal state after:
case h_open
R : Type u
inst✝ : CommSemiring R
⊢ ∀ u ∈ Set.range fun r ↦ ↑(basicOpen r), IsOpen u

case h_nhds
R : Type u
inst✝ : CommSemiring R
⊢ ∀ (a : PrimeSpectrum R) (u : Set (PrimeSpectrum R)),
    a ∈ u → IsOpen u → ∃ v ∈ Set.range fun r ↦ ↑(basicOpen r), a ∈ v ∧ v ⊆ u
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ IsCyclic ↥H ↔ ∃ g, zpowers g = H

Tactic:
isCyclic_iff_exists_zpowers_eq_top

Goal state after:
α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ (∃ g, zpowers g = ⊤) ↔ ∃ g, zpowers g = H
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
intro hG
    by_contra h
    rw [Nat.dvd_iff_mod_eq_zero, ← Ne, ← pos_iff_ne_zero] at h
    have h₂ : n % exponent G < exponent G := Nat.mod_lt _ (exponent_pos_of_exists n hpos hG)
    have h₃ : exponent G ≤ n % exponent G := by
      apply exponent_min' _ h
      simp_rw [← pow_eq_mod_exponent]
      exact hG
    exact h₂.not_ge h₃

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
⊢ ∃ g, g ^ (exponent G / p) ≠ 1

Tactic:
suffices key : ¬exponent G ∣ exponent G / p by
      rwa [exponent_dvd_iff_forall_pow_eq_one, not_forall] at key

Goal state after:
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
⊢ ¬exponent G ∣ exponent G / p
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case negSucc
α : 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.negSucc k) = x
hk : g ^ Int.negSucc k = x
⊢ g ^ (Int.negSucc k).natAbs ∈ H

Tactic:
rw [Int.natAbs_negSucc, ← Subgroup.inv_mem_iff H]

Goal state after:
case negSucc
α : 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.negSucc k) = x
hk : g ^ Int.negSucc k = x
⊢ (g ^ k.succ)⁻¹ ∈ H
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (comap f '' zeroLocus ↑I)
⊢ comap f '' zeroLocus ↑I ⊆ zeroLocus ↑(Ideal.comap f I)

Tactic:
rintro _ ⟨q, hq, rfl⟩

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (comap f '' zeroLocus ↑I)
q : PrimeSpectrum S
hq : q ∈ zeroLocus ↑I
⊢ comap f q ∈ zeroLocus ↑(Ideal.comap f I)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case refine_1.inr
G : Type u_2
inst✝ : Group G
g : G
n : ℕ
h : zpowers (g ^ (-↑n)) ≤ zpowers g
⊢ ∃ n_1, zpowers (g ^ (-↑n)) = zpowers (g ^ n_1)

Tactic:
exact ⟨n, by simp⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
by
  refine ⟨fun hG g hg ↦ ?_, fun h ↦ dvd_antisymm ?_ ?_⟩
  · rw [Ne, ← orderOf_eq_one_iff] at hg
    exact Eq.symm <| (hp.dvd_iff_eq hg).mp <| hG ▸ Monoid.order_dvd_exponent g
  · rw [exponent_dvd]
    intro g
    by_cases hg : g = 1
    · simp [hg]
    · rw [h g hg]
  · obtain ⟨g, hg⟩ := exists_ne (1 : G)
    simpa [h g hg] using Monoid.order_dvd_exponent g

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : IsPGroup p G
g : G
hg : g ≠ 1
k : ℕ
hk : orderOf g = p ^ k
hk0 : k = 0
⊢ g = 1

Tactic:
← orderOf_eq_one_iff,

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : IsPGroup p G
g : G
hg : g ≠ 1
k : ℕ
hk : orderOf g = p ^ k
hk0 : k = 0
⊢ orderOf g = 1
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
s : Set G
inst✝ : Finite ↑s
this : Fintype ↑s
⊢ rank ↥(closure ↑s.toFinset) ≤ s.toFinset.card

Tactic:
exact rank_closure_finset_le_card s.toFinset

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ False

Tactic:
have hQ : IsPGroup p Q := by
    apply h.comap_of_ker_isPGroup
    rw [QuotientGroup.ker_mk']
    exact P.2

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p ↥Q
⊢ False
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ ¬p ∣ (↑P).index

Tactic:
have := P.finite_of_finiteIndex

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
this : Finite (Sylow p G)
⊢ ¬p ∣ (↑P).index
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
⊢ (∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a) ↔ ∀ ⦃x : G⦄, x ∈ torsion G → x ∈ ⊥

Tactic:
simp [not_imp_not, CommGroup.mem_torsion]

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

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : ∀ (x : G'), x ∈ zpowers g'
h : orderOf g = orderOf g'
⊢ (monoidHomOfForallMemZpowers hg' ⋯).comp (monoidHomOfForallMemZpowers hg ⋯) = MonoidHom.id G

Tactic:
simp [MonoidHom.eq_iff_eq_on_generator hg]

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx✝ : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : ↑s → ↑(Iic a) := fun y ↦ ⟨↑y, ⋯⟩
⊢ ∃ s_1, (∀ x ∈ s_1, IsCompactElement x) ∧ sSup s_1 = ⟨sSup s, hx✝⟩

Tactic:
refine ⟨range f, ?_, ?_⟩

Goal state after:
case refine_1
ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx✝ : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : ↑s → ↑(Iic a) := fun y ↦ ⟨↑y, ⋯⟩
⊢ ∀ x ∈ range f, IsCompactElement x

case refine_2
ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx✝ : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : ↑s → ↑(Iic a) := fun y ↦ ⟨↑y, ⋯⟩
⊢ sSup (range f) = ⟨sSup s, hx✝⟩
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Group M
inst✝² : Group N
cyc : IsCyclic (M × N)
inst✝¹ : Finite M
inst✝ : Finite N
hM : IsCyclic M
hN : IsCyclic N
x✝² : CommGroup (M × N) := IsCyclic.commGroup
x✝¹ : CommGroup M := IsCyclic.commGroup
x✝ : CommGroup N := IsCyclic.commGroup
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
IsCyclic.iff_exponent_eq_card,

Goal state after:
M : Type u_4
N : Type u_5
inst✝³ : Group M
inst✝² : Group N
cyc✝ : IsCyclic (M × N)
inst✝¹ : Finite M
inst✝ : Finite N
hM✝ : IsCyclic M
hN✝ : IsCyclic N
x✝² : CommGroup (M × N) := IsCyclic.commGroup
cyc : Monoid.exponent (M × N) = Nat.card (M × N)
x✝¹ : CommGroup M := IsCyclic.commGroup
hM : Monoid.exponent M = Nat.card M
x✝ : CommGroup N := IsCyclic.commGroup
hN : Monoid.exponent N = Nat.card N
⊢ (Nat.card M).Coprime (Nat.card N)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_1.inr.inl.inr
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (N × M)
h✝² : Finite M
h✝¹ : Infinite N
h✝ : Nontrivial M
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
exact (not_isCyclic_prod_of_infinite_nontrivial N M h).elim

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

Goal state before:
pp: case refine_2.mpr
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
⊢ (((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤) →
    ∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1

Tactic:
rintro ⟨hs, Hb⟩

Goal state after:
case refine_2.mpr
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
⊢ ∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1
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
s : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
this : Ideal.span s ≤ Ideal.torsionOf R M x
⊢ ∀ (a : ↑↑(Ideal.span s)), ↑a • x = 0

Tactic:
by
    rintro ⟨a, ha⟩
    exact this ha

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

Goal state before:
pp: R : Type u_1
A : Type u_3
M : Type u_2
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
r : R
f : R[X]
m : AEval R M a
⊢ (r • f) • m = r • f • m

Tactic:
apply (of R M a).symm.injective

Goal state after:
R : Type u_1
A : Type u_3
M : Type u_2
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
r : R
f : R[X]
m : AEval R M a
⊢ (of R M a).symm ((r • f) • m) = (of R M a).symm (r • f • m)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case zero
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
j : ℕ
m : M
⊢ r • id (single R j m) = single R (0 + j) (r • m)

Tactic:
zero_add

Goal state after:
case zero
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
j : ℕ
m : M
⊢ r • id (single R j m) = single R j (r • m)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case refine_2.e_g
ι : 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 : ℕ
c : M
⊢ r ^ i • s • c = s • r ^ i • c

Tactic:
smul_comm

Goal state after:
case refine_2.e_g
ι : 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 : ℕ
c : M
⊢ s • r ^ i • c = s • r ^ i • c
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
D : M.Derivation f
b : ↑B
⊢ (ConcreteCategory.hom D.desc) (CommRingCat.KaehlerDifferential.d b) = D.d b

Tactic:
by
  let := f.hom.toAlgebra
  let := Module.compHom M f.hom
  apply D.liftKaehlerDifferential_comp_D

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

Goal state before:
pp: 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
⊢ 2 ≠ 0

Tactic:
omega

Goal state after:
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
app : (X : Cᵒᵖ) → M₁.obj X ≅ M₂.obj X
naturality :
  ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
    M₁.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app Y).hom = (app X).hom ≫ M₂.map f
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ M₁.map f = (app X).hom ≫ (app X).inv ≫ M₁.map f

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
app : (X : Cᵒᵖ) → M₁.obj X ≅ M₂.obj X
naturality :
  ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
    M₁.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app Y).hom = (app X).hom ≫ M₂.map f
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ M₁.map f = M₁.map f
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
⊢ (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:
by
  have := congr_app (associativity F m₁ m₂ m₃) X
  dsimp at this
  simpa using this

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

Tactic:
zero_add

Goal state after:
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)
n : A
X : C
⊢ (F n).obj X = (F n).obj X
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : ¬c.Rel i j
⊢ C.d i j ≫ C.d j k = 0

Tactic:
C.shape i j hij,

Goal state after:
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : ¬c.Rel i j
⊢ 0 ≫ C.d j k = 0
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 (0 + n)).obj X

Tactic:
zero_add

Goal state after:
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).obj X
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ⊆ ↑(Submodule.restrictScalars S (ideal R S))

Tactic:
rintro _ ⟨s, rfl⟩

Goal state after:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
⊢ (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) s ∈ ↑(Submodule.restrictScalars S (ideal R S))
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
i j : A
⊢ shiftFunctorAdd' C i j (i + j) ⋯ = shiftFunctorAdd C i j

Tactic:
ext1
  apply Category.id_comp

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

Tactic:
zero_add

Goal state after:
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).obj X
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ⊆ ↑(ideal R S)

Tactic:
rintro _ ⟨s, rfl⟩

Goal state after:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
⊢ (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) s ∈ ↑(ideal R S)
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 (0 + a)).obj X

Tactic:
zero_add

Goal state after:
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).obj X
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 : HomologicalComplex V c
i : ι
h : ¬c.Rel i (c.next i)
⊢ c.next i = i

Tactic:
dsimp [ComplexShape.next]
        rw [dif_neg]; rintro ⟨j, hj⟩
        have : c.next i = j := c.next_eq' hj
        rw [this] at h; contradiction

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹⁰ : Category.{v, u} V
inst✝⁹ : Preadditive V
W : Type u_2
inst✝⁸ : Category.{v_1, u_2} W
inst✝⁷ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁶ : Category.{v_2, u_3} W₁
inst✝⁵ : Category.{v_3, u_4} W₂
inst✝⁴ : HasZeroMorphisms W₁
inst✝³ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f✝ : C ⟶ D
i : ι
F : W₁ ⥤ W₂
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.ReflectsIsomorphisms
c : ComplexShape ι
A✝ B✝ : HomologicalComplex W₁ c
f : A✝ ⟶ B✝
inst✝ : IsIso ((F.mapHomologicalComplex c).map f)
this✝ : ∀ (n : ι), IsIso (F.map (f.f n))
this : ∀ (n : ι), IsIso (f.f n)
⊢ IsIso f

Tactic:
exact HomologicalComplex.Hom.isIso_of_components f

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁹ : Category.{v, u} V
inst✝⁸ : Preadditive V
W : Type u_2
inst✝⁷ : Category.{v_1, u_2} W
inst✝⁶ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁵ : Category.{v_2, u_3} W₁
inst✝⁴ : Category.{v_3, u_4} W₂
inst✝³ : HasZeroMorphisms W₁
inst✝² : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f : C ⟶ D
i : ι
F : V ⥤ W
inst✝¹ : F.Additive
c : ComplexShape ι
inst✝ : F.Faithful
K L : HomologicalComplex V c
f₁ f₂ : K ⟶ L
h : (F.mapHomologicalComplex c).map f₁ = (F.mapHomologicalComplex c).map f₂
⊢ f₁ = f₂

Tactic:
by
    ext
    exact F.map_injective ((HomologicalComplex.eval W c _).congr_map h)

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✝¹ : AddGroup A
inst✝ : HasShift C A
n m : A
h : n + m = 0
X : C
⊢ 0 + n = n

Tactic:
zero_add

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n m : A
h : n + m = 0
X : C
⊢ n = n
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₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
n : ℕ
⊢ mkAux X₀ X₁ X₂ d₀ d₁ s succ n =
    { X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2), X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1),
      X₃ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X n, f := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1),
      g := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }

Tactic:
rw [show n + 2 = n + 1 + 1 from rfl]

Goal state after:
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₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
n : ℕ
⊢ mkAux X₀ X₁ X₂ d₀ d₁ s succ n =
    { X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1 + 1), X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1),
      X₃ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X n, f := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1 + 1) (n + 1),
      g := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }
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)
⊢ 0 + 0 = 0

Tactic:
zero_add

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)
⊢ 0 = 0