mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: 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 ^ p ^ k)).Coprime (orderOf g)

Tactic:
rw [hg, Nat.coprime_pow_right_iff (pos_of_gt hpe), Nat.coprime_comm]

Goal state after:
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
⊢ p.Coprime (orderOf (t ^ p ^ k))
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
simp_rw [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]

Goal state after:
case H
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ (a : G), orderOf a ≤ exponent G
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)

Tactic:
by
  cases subsingleton_or_nontrivial R
  · refine ⟨0, 0, ?_, ?_, ?_, ?_⟩ <;> apply Subsingleton.elim
  obtain ⟨I, hI, hI'⟩ := isCompact_isOpen_iff_ideal.mp ⟨hs.1.isCompact, hs.2⟩
  obtain ⟨J, hJ, hJ'⟩ := isCompact_isOpen_iff_ideal.mp
    ⟨hs.2.isClosed_compl.isCompact, hs.1.isOpen_compl⟩
  simp only [compl_eq_iff_isCompl, ← eq_compl_iff_isCompl, compl_compl] at hI' hJ'
  have : I * J ≤ nilradical R := by
    refine Ideal.radical_le_radical_iff.mp (le_of_eq ?_)
    rw [← zeroLocus_eq_iff, Ideal.zero_eq_bot, zeroLocus_bot,
      zeroLocus_mul, hI', hJ', Set.compl_union_self]
  obtain ⟨n, hn⟩ := Ideal.exists_pow_le_of_le_radical_of_fg this (Submodule.FG.mul hI hJ)
  have hnz : n ≠ 0 := by rintro rfl; simp at hn
  rw [mul_pow, Ideal.zero_eq_bot] at hn
  have : I ^ n ⊔ J ^ n = ⊤ := by
    rw [eq_top_iff, ← Ideal.span_pow_eq_top (I ∪ J : Set R) _ n, Ideal.span_le, Set.image_union,
      Set.union_subset_iff]
    constructor
    · rintro _ ⟨x, hx, rfl⟩; exact Ideal.mem_sup_left (Ideal.pow_mem_pow hx n)
    · rintro _ ⟨x, hx, rfl⟩; exact Ideal.mem_sup_right (Ideal.pow_mem_pow hx n)
    · rw [Ideal.span_union, Ideal.span_eq, Ideal.span_eq, ← zeroLocus_empty_iff_eq_top,
        zeroLocus_sup, hI', hJ', Set.compl_inter_self]
  rw [Ideal.eq_top_iff_one, Submodule.mem_sup] at this
  obtain ⟨x, hx, y, hy, add⟩ := this
  have mul : x * y = 0 := hn (Ideal.mul_mem_mul hx hy)
  have : s = basicOpen x := by
    refine subset_antisymm ?_ ?_
    · rw [← hJ', basicOpen_eq_zeroLocus_of_mul_add _ _ mul add]
      exact zeroLocus_anti_mono (Set.singleton_subset_iff.mpr <| Ideal.pow_le_self hnz hy)
    · rw [basicOpen_eq_zeroLocus_compl, Set.compl_subset_comm, ← hI']
      exact zeroLocus_anti_mono (Set.singleton_subset_iff.mpr <| Ideal.pow_le_self hnz hx)
  refine ⟨x, y, mul, add, this, ?_⟩
  rw [this, basicOpen_eq_zeroLocus_of_mul_add _ _ mul add, basicOpen_eq_zeroLocus_compl]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ IsClopen s ↔ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e)

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Goal state after:
case refine_1
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
h : IsClopen s
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e)

case refine_2
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e)) → IsClopen s
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
⊢ exponent (M₁ × M₂) ∣ GCDMonoid.lcm (exponent M₁) (exponent M₂)

Tactic:
refine exponent_dvd_of_forall_pow_eq_one fun g ↦ ?_

Goal state after:
case refine_1
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ g ^ GCDMonoid.lcm (exponent M₁) (exponent M₂) = 1
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ Finite (Sylow p G)

Tactic:
by
  apply finite_of_ker_is_pGroup (f := QuotientGroup.mk' P.normalCore)
  rw [QuotientGroup.ker_mk']
  exact P.isPGroup'.to_le P.normalCore_le

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
⊢ Nat.card (Sylow p G) ≡ 1 [MOD p]

Tactic:
refine Sylow.nonempty.elim fun P : Sylow p G => ?_
  have : fixedPoints P.1 (Sylow p G) = {P} :=
    Set.ext fun Q : Sylow p G =>
      calc
        Q ∈ fixedPoints P (Sylow p G) ↔ P.1 ≤ Q := P.2.sylow_mem_fixedPoints_iff
        _ ↔ Q.1 = P.1 := ⟨P.3 Q.2, ge_of_eq⟩
        _ ↔ Q ∈ {P} := Sylow.ext_iff.symm.trans Set.mem_singleton_iff.symm
  have : Nat.card (fixedPoints P.1 (Sylow p G)) = 1 := by simp [this]
  exact (P.2.card_modEq_card_fixedPoints (Sylow p G)).trans (by rw [this])

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

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

Tactic:
by group

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f ↑P) := ⋯.some
Q : Subgroup G := map (comap f ↑P).subtype ↑Q₀
hPQ : map f Q ≤ ↑P
hpQ : IsPGroup p ↥Q
hQ : ¬p ∣ Q.index
⊢ ∃ a, mapSurjective hf a = P

Tactic:
use hpQ.toSylow hQ

Goal state after:
case h
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f ↑P) := ⋯
Q : Subgroup G := ⋯
hPQ : map f Q ≤ ↑P
hpQ : IsPGroup p ↥Q
hQ : ¬p ∣ Q.index
⊢ mapSurjective hf (hpQ.toSylow hQ) = P
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:
rw [IsCyclic.iff_exponent_eq_card, Monoid.exponent_prod, Nat.card_prod, lcm_eq_nat_lcm] at *

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).lcm (Monoid.exponent N) = Nat.card M * Nat.card 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 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 (Nat.card N))
h✝ : Infinite N
⊢ False

Tactic:
rw [Nat.card_eq_zero_of_infinite] at hMN

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
⊢ False
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case refine_2.right
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Nat.card ((i : ↥ps) → ↥↑(P ↑i)) = Nat.card G

Tactic:
calc
      Nat.card (∀ p : ps, P p) = ∏ p : ps, Nat.card (P p) := Nat.card_pi
      _ = ∏ p : ps, p.1 ^ (Nat.card G).factorization p.1 := by
        congr 1 with ⟨p, hp⟩
        exact @card_eq_multiplicity _ _ _ p ⟨Nat.prime_of_mem_primeFactors hp⟩ (P p)
      _ = ∏ p ∈ ps, p ^ (Nat.card G).factorization p :=
        (Finset.prod_finset_coe (fun p => p ^ (Nat.card G).factorization p) _)
      _ = (Nat.card G).factorization.prod (· ^ ·) := rfl
      _ = Nat.card G := Nat.prod_factorization_pow_eq_self Nat.card_pos.ne'

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
⊢ ↑i ≠ s.length

Tactic:
simpa [last, s.inj, Fin.ext_iff] using hx

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
⊢ (∀ (b : ↑s) (a : M), ↑b • a = 0) ↔ ∀ x ∈ s, ∀ (m : M), x • m = 0

Tactic:
SetCoe.forall

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 : R) (h : x ∈ s) (a : M), ↑⟨x, h⟩ • a = 0) ↔ ∀ x ∈ s, ∀ (m : M), x • m = 0
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case monomial
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ ((monomial f_n) f_a • g).coeff n = ∑ x ∈ Finset.antidiagonal n, ((monomial f_n) f_a).coeff x.1 • g.coeff x.2

Tactic:
| monomial f_n f_a =>

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf : a✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
hg : b✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
i : ℕ
⊢ (a✝ + b✝).coeff i ∈ I ^ i

Tactic:
rw [coeff_add]
    exact Ideal.add_mem _ (hf i) (hg i)

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
M : Submodule R ↥(maximalIdeal R)
H : Submodule.map (maximalIdeal R).toCotangent M = ⊤
⊢ maximalIdeal R ≤ Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ maximalIdeal R • maximalIdeal R

Tactic:
rw [smul_eq_mul, ← pow_two, ← Ideal.map_toCotangent_ker, ← Submodule.map_sup,
    ← Submodule.comap_map_eq, H, Submodule.comap_top, Submodule.map_top, Submodule.range_subtype]

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsNoetherianRing R
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
hx' : x ∉ ⊥
this : x ∈ ⨅ i, I ^ i • ⊤ ↔ ∃ r, ↑r • x = x
⊢ False

Tactic:
obtain ⟨r, hr⟩ := this.mp hx

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsNoetherianRing R
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
hx' : x ∉ ⊥
this : x ∈ ⨅ i, I ^ i • ⊤ ↔ ∃ r, ↑r • x = x
r : ↥I
hr : ↑r • x = x
⊢ False
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 : (algebraMap A B) ↑x' ∈ map (algebraMap A B) J ^ 2
⊢ x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))

Tactic:
rw [← Ideal.map_pow, ← Ideal.mem_comap, Ideal.comap_map_of_surjective' _ surj] at hx

Goal state after:
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)
⊢ x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))
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
X : Cᵒᵖ
hX : Limits.IsInitial X
M : PresheafOfModules R
Y Z : Cᵒᵖ
f : Y ⟶ Z
r : ↑(R.obj X)
x : ↑(forgetToPresheafModuleCatObjObj X hX M Y)
⊢ (ConcreteCategory.hom (R.map (hX.to Y) ≫ R.map f)) r • (ConcreteCategory.hom (M.map f)) x =
    (RingCat.Hom.hom (R.map (hX.to Z))) r • (ConcreteCategory.hom (M.map f)) x

Tactic:
← R.map_comp

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
X : Cᵒᵖ
hX : Limits.IsInitial X
M : PresheafOfModules R
Y Z : Cᵒᵖ
f : Y ⟶ Z
r : ↑(R.obj X)
x : ↑(forgetToPresheafModuleCatObjObj X hX M Y)
⊢ (ConcreteCategory.hom (R.map (hX.to Y ≫ f))) r • (ConcreteCategory.hom (M.map f)) x =
    (RingCat.Hom.hom (R.map (hX.to Z))) r • (ConcreteCategory.hom (M.map f)) x
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_2
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 y : S ⊗[R] S
⊢ ∀ (x y_1 : S),
    D.tensorProductTo (x ⊗ₜ[R] y_1 * y) =
      (TensorProduct.lmul' R) (x ⊗ₜ[R] y_1) • D.tensorProductTo y +
        (TensorProduct.lmul' R) y • D.tensorProductTo (x ⊗ₜ[R] y_1)

Tactic:
intro x₁ x₂

Goal state after:
case refine_2
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 y : S ⊗[R] S
x₁ x₂ : S
⊢ D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * y) =
    (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo y +
      (TensorProduct.lmul' R) y • D.tensorProductTo (x₁ ⊗ₜ[R] 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 ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ }.d i j
i j : ι
hij : ¬c.Rel i j
⊢ 0 = d₂ i j

Tactic:
s₂ i j hij

Goal state after:
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ }.d i j
i j : ι
hij : ¬c.Rel i j
⊢ 0 = 0
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
i j : A
h : i + j = 0
⊢ j + i = 0

Tactic:
← add_left_inj j,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
i j : A
h : i + j = 0
⊢ j + i + j = 0 + j
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
i j : A
h : i + j = 0
X : C
⊢ j + i = 0

Tactic:
← add_left_inj j,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
i j : A
h : i + j = 0
X : C
⊢ j + i + j = 0 + j
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: 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
a b : S
this : LinearMap.CompatibleSMul ↥(ideal R S) Ω[S⁄R] S (S ⊗[R] S)
⊢ ↑⟨1 ⊗ₜ[R] (a * b) - (a * b) ⊗ₜ[R] 1, ⋯⟩ - ↑(a • ⟨1 ⊗ₜ[R] b - b ⊗ₜ[R] 1, ⋯⟩ + b • ⟨1 ⊗ₜ[R] a - a ⊗ₜ[R] 1, ⋯⟩) =
    (1 ⊗ₜ[R] a - a ⊗ₜ[R] 1) * (1 ⊗ₜ[R] b - b ⊗ₜ[R] 1)

Tactic:
simp only [Submodule.coe_add,
        TensorProduct.tmul_mul_tmul, mul_sub, sub_mul, mul_comm b, Submodule.coe_smul_of_tower,
        smul_sub, TensorProduct.smul_tmul', smul_eq_mul, mul_one]

Goal state after:
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
a b : S
this : LinearMap.CompatibleSMul ↥(ideal R S) Ω[S⁄R] S (S ⊗[R] S)
⊢ 1 ⊗ₜ[R] (a * b) - (a * b) ⊗ₜ[R] 1 - (a ⊗ₜ[R] b - (a * b) ⊗ₜ[R] 1 + ((1 * b) ⊗ₜ[R] a - (a * b) ⊗ₜ[R] 1)) =
    1 ⊗ₜ[R] (a * b) - a ⊗ₜ[R] (1 * b) - ((1 * b) ⊗ₜ[R] a - (a * b) ⊗ₜ[R] 1)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: 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
⊢ D.liftKaehlerDifferential.compDer (KaehlerDifferential.D R S) = D

Tactic:
ext a
  dsimp [KaehlerDifferential.D_apply]
  refine (D.liftKaehlerDifferential_apply _).trans ?_
  rw [Subtype.coe_mk, map_sub, Derivation.tensorProductTo_tmul, Derivation.tensorProductTo_tmul,
    one_smul, D.map_one_eq_zero, smul_zero, sub_zero]

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

Goal state before:
pp: 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✝¹ : HasFiniteLimits C
K L : HomologicalComplex C c
φ : K ⟶ L
inst✝ : Mono φ
n : ι
⊢ Mono (φ.f n)

Tactic:
by
  change Mono ((HomologicalComplex.eval C c n).map φ)
  infer_instance

Goal state after:
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
⊢ (linearCombination S ⇑(D R S)).ker ≤ (kerTotal R S).mkQ.ker

Tactic:
← KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination

Goal state after:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (linearCombination S ⇑(D R S)).ker ≤
    ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S)).ker
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a.tmul
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
r : B
s : Ω[A⁄R]
⊢ (mapBaseChange R A B) (r ⊗ₜ[A] s) ∈ (map R A B B).ker

Tactic:
| tmul r s =>

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 K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ (-z₁).comp z₂ h = -z₁.comp z₂ h

Tactic:
by
  ext p q hpq
  simp only [comp_v _ _ h p _ q rfl (by lia), neg_v, neg_comp]

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
H : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
⊢ (mapArrowHom φ φ H (𝟙 (Arrow.mk φ))).f i = 𝟙 (X φ i)

Tactic:
by_cases hi : c.Rel i (c.next i)

Goal state after:
case pos
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
H : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
hi : c.Rel i (c.next i)
⊢ (mapArrowHom φ φ H (𝟙 (Arrow.mk φ))).f i = 𝟙 (X φ i)

case neg
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
H : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
hi : ¬c.Rel i (c.next i)
⊢ (mapArrowHom φ φ H (𝟙 (Arrow.mk φ))).f i = 𝟙 (X φ i)
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
F' F'' G' G'' : HomologicalComplex C c
φ' : F' ⟶ G'
φ'' : F'' ⟶ G''
inst✝¹ : HasHomotopyCofiber φ'
inst✝ : HasHomotopyCofiber φ''
H : ∀ (j : ι), ∃ i, c.Rel i j
α : Arrow.mk φ ⟶ Arrow.mk φ'
β : Arrow.mk φ' ⟶ Arrow.mk φ''
i : ι
⊢ (mapArrowHom φ φ'' H (α ≫ β)).f i = (mapArrowHom φ φ' H α).f i ≫ (mapArrowHom φ' φ'' H β).f i

Tactic:
by_cases hi : c.Rel i (c.next i)

Goal state after:
case pos
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
F' F'' G' G'' : HomologicalComplex C c
φ' : F' ⟶ G'
φ'' : F'' ⟶ G''
inst✝¹ : HasHomotopyCofiber φ'
inst✝ : HasHomotopyCofiber φ''
H : ∀ (j : ι), ∃ i, c.Rel i j
α : Arrow.mk φ ⟶ Arrow.mk φ'
β : Arrow.mk φ' ⟶ Arrow.mk φ''
i : ι
hi : c.Rel i (c.next i)
⊢ (mapArrowHom φ φ'' H (α ≫ β)).f i = (mapArrowHom φ φ' H α).f i ≫ (mapArrowHom φ' φ'' H β).f i

case neg
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
F' F'' G' G'' : HomologicalComplex C c
φ' : F' ⟶ G'
φ'' : F'' ⟶ G''
inst✝¹ : HasHomotopyCofiber φ'
inst✝ : HasHomotopyCofiber φ''
H : ∀ (j : ι), ∃ i, c.Rel i j
α : Arrow.mk φ ⟶ Arrow.mk φ'
β : Arrow.mk φ' ⟶ Arrow.mk φ''
i : ι
hi : ¬c.Rel i (c.next i)
⊢ (mapArrowHom φ φ'' H (α ≫ β)).f i = (mapArrowHom φ φ' H α).f i ≫ (mapArrowHom φ' φ'' H β).f i