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

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
⊢ ∃ g, orderOf g = exponent G

Tactic:
by
  have he := hG.exponent_ne_zero
  have hne : (Set.range (orderOf : G → ℕ)).Nonempty := ⟨1, 1, orderOf_one⟩
  have hfin : (Set.range (orderOf : G → ℕ)).Finite := by
    rwa [← exponent_ne_zero_iff_range_orderOf_finite hG.orderOf_pos]
  obtain ⟨t, ht⟩ := hne.csSup_mem hfin
  use t
  apply Nat.dvd_antisymm (order_dvd_exponent _)
  refine Nat.dvd_of_primeFactorsList_subperm he ?_
  rw [List.subperm_ext_iff]
  by_contra! ⟨p, hp, hpe⟩
  replace hp := Nat.prime_of_mem_primeFactorsList hp
  simp only [Nat.primeFactorsList_count_eq] at hpe
  set k := (orderOf t).factorization p with hk
  obtain ⟨g, hg⟩ := hp.exists_orderOf_eq_pow_factorization_exponent G
  suffices orderOf t < orderOf (t ^ p ^ k * g) by
    rw [ht] at this
    exact this.not_ge (le_csSup hfin.bddAbove <| Set.mem_range_self _)
  have hpk : p ^ k ∣ orderOf t := Nat.ordProj_dvd _ _
  have hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k := by
    rw [orderOf_pow' t (pow_ne_zero k hp.ne_zero), Nat.gcd_eq_right hpk]
  obtain ⟨a, ha⟩ := Nat.exists_eq_add_of_lt hpe
  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
  rw [(Commute.all _ g).orderOf_mul_eq_mul_orderOf_of_coprime hcoprime, hpk',
    hg, ha, hk, pow_add, pow_add, pow_one, ← mul_assoc, ← mul_assoc,
    Nat.div_mul_cancel, mul_assoc, lt_mul_iff_one_lt_right <| hG.orderOf_pos t, ← pow_succ]
  · exact one_lt_pow₀ hp.one_lt a.succ_ne_zero
  · exact hpk

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ exponent G = sSup ↑(Finset.image orderOf Finset.univ)

Tactic:
Finset.coe_image,

Goal state after:
G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ exponent G = sSup (orderOf '' ↑Finset.univ)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
and_congr_right

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
e f : R
⊢ (e * f = 0 ∧ e + f = 1) ∧ ?m.63 ↔ (e * f = 0 ∧ e + f = 1) ∧ s = zeroLocus {e}

R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
e f : R
⊢ e * f = 0 ∧ e + f = 1 → (s = ↑(basicOpen f) ↔ ?m.63)

R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
e f : R
⊢ Prop
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:
Finset.coe_image,

Goal state after:
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 (⇑f '' ↑S) = ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝² : Finite α
this✝¹ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this✝ : orderOf g ∈ (p ^ 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
⊢ ?m.163

Tactic:
by simpa using this

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this✝ : Fact (Nat.Prime p)
this : Finite G
⊢ ∃ H, Nat.card ↥H = p ^ n

Tactic:
obtain ⟨m, hm⟩ := h.exists_card_eq

Goal state after:
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this✝ : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hm : Nat.card G = p ^ m
⊢ ∃ H, Nat.card ↥H = p ^ n
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
m : M
h : m ≠ 0
r : R
hr : r ∈ torsionOf R M m
⊢ r = 0

Tactic:
mem_torsionOf_iff,

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
m : M
h : m ≠ 0
r : R
hr : r • m = 0
⊢ r = 0
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✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
I : Ideal R
hbot : I ≠ ⊥
⊢ IsTorsion R ↥(torsionBySet R M ↑I)

Tactic:
aesop (add norm Submodule.eq_bot_iff)

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case succ
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
⊢ ∃ t, head t = head s ∧ t.length + 1 = n + 1 ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case succ
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), head s₁ = head s₂ → last s₁ = last s₂ → s₁.length = n → s₁.Equivalent s₂
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hle : s₁.length = n + 1
⊢ s₁.Equivalent s₂

Tactic:
| succ n ih =>

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

Goal state before:
pp: G : Type u_3
inst✝ : AddCommGroup G
⊢ (torsion ℤ G).toAddSubgroup = AddCommGroup.torsion G

Tactic:
ext x
  refine ((isOfFinAddOrder_iff_zsmul_eq_zero (x := x)).trans ?_).symm
  simp [mem_nonZeroDivisors_iff_ne_zero]

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
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R ↑s = F.N i
⊢ Submodule.span ↥(reesAlgebra I) ↑(Finset.image (⇑(lsingle R i)) s) =
    Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))

Tactic:
Finset.coe_image,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R ↑s = F.N i
⊢ Submodule.span (↥(reesAlgebra I)) (⇑(lsingle R i) '' ↑s) = Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
d : M.Derivation φ
f : M ⟶ N
X Y : Dᵒᵖ
g : X ⟶ Y
x : ↑(R.obj X)
⊢ ((ModuleCat.Hom.hom (f.app Y)).toAddMonoidHom.comp d.d) ((ConcreteCategory.hom (R.map g)) x) =
    (ConcreteCategory.hom (N.map g)) (((ModuleCat.Hom.hom (f.app X)).toAddMonoidHom.comp d.d) x)

Tactic:
simpa using naturality_apply f g (d.d x)

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

Goal state before:
pp: case neg
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i✝ : ι
h : ¬i✝ = j
⊢ 0 = 𝟙 (if i✝ = j then A else 0)

Tactic:
· #adaptation_note /-- nightly-2024-03-07
      previously was `rw [if_neg h]; simp`, but that fails with "motive not type correct"
      This is because dsimp does not simplify numerals;
      this note should be removable once https://github.com/leanprover/lean4/pull/8433 lands. -/
      convert! (id_zero (C := V)).symm
      all_goals simp [if_neg h]

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

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

Tactic:
· intro x y hx hy
      rw [map_add, TensorProduct.add_tmul, ← sub_add_sub_comm]
      exact add_mem hx hy

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : c.Rel i j
⊢ C.dTo j = (C.xPrevIso r).hom ≫ C.d i j

Tactic:
obtain rfl := c.prev_eq' r
  exact (Category.id_comp _).symm

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

Goal state before:
pp: case h.a
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
⊢ Ideal.span ↑(Finset.image (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S)) ≤ ideal R S

Tactic:
Finset.coe_image,

Goal state after:
case h.a
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
⊢ Ideal.span ((fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) '' ↑(EssFiniteType.finset R S)) ≤ ideal R S
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
inst✝ : EssFiniteType R S
⊢ Module.Finite S Ω[S⁄R]

Tactic:
let s := (EssFiniteType.finset R S).image (fun s ↦ D R S s)
  refine ⟨⟨s, top_le_iff.mp ?_⟩⟩
  rw [← span_range_derivation, Submodule.span_le]
  rintro _ ⟨x, rfl⟩
  have : ∀ x ∈ adjoin R (EssFiniteType.finset R S : Set S),
      .D _ _ x ∈ Submodule.span S (s : Set Ω[S⁄R]) := by
    intro x hx
    refine adjoin_induction ?_ ?_ ?_ ?_ hx
    · exact fun x hx ↦ Submodule.subset_span (Finset.mem_image_of_mem _ hx)
    · simp
    · exact fun x y _ _ hx hy ↦ (D R S).map_add x y ▸ add_mem hx hy
    · intro x y _ _ hx hy
      simp only [Derivation.leibniz]
      exact add_mem (Submodule.smul_mem _ _ hy) (Submodule.smul_mem _ _ hx)
  obtain ⟨t, ht, ht', hxt⟩ := (essFiniteType_cond_iff R S (EssFiniteType.finset R S)).mp
    EssFiniteType.cond.choose_spec x
  rw [show D R S x =
    ht'.unit⁻¹ • (D R S (x * t) - x • D R S t) by simp [smul_smul, Units.smul_def]]
  exact Submodule.smul_mem _ _ (sub_mem (this _ hxt) (Submodule.smul_mem _ _ (this _ ht)))

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
⊢ W.IsInvertedBy F₁ ↔ W.IsInvertedBy F₂

Tactic:
dsimp [IsInvertedBy]
  simp only [NatIso.isIso_map_iff e]

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
⊢ (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

Tactic:
split_ifs with hij

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
i j : ι
hij✝ : c.Rel i j
hij : c.Rel j (c.next j)
⊢ (-fstX φ i j hij✝ ≫ F.d j (c.next j) ≫ inlX φ (c.next j) j hij + fstX φ i j hij✝ ≫ φ.f j ≫ inrX φ j +
        sndX φ i ≫ G.d i j ≫ inrX φ j) ≫
      sndX φ j =
    fstX φ i j hij✝ ≫ φ.f j + sndX φ i ≫ G.d i j

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
i j : ι
hij✝ : c.Rel i j
hij : ¬c.Rel j (c.next j)
⊢ (0 + fstX φ i j hij✝ ≫ φ.f j ≫ inrX φ j + sndX φ i ≫ G.d i j ≫ inrX φ j) ≫ 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₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ z₂' : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ z₁.comp (z₂ - z₂') h = z₁.comp z₂ h - z₁.comp z₂' h

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

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
ι : Type u_3
inst✝² : AddRightCancelSemigroup ι
inst✝¹ : One ι
F G : CochainComplex C ι
φ : F ⟶ G
inst✝ : ∀ (p : ι), HasBinaryBiproduct (F.X (p + 1)) (G.X p)
⊢ ∀ (i j : ι), (ComplexShape.up ι).Rel i j → HasBinaryBiproduct (F.X j) (G.X i)

Tactic:
rintro i _ rfl
    infer_instance

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
X✝ Y✝ Z✝ : HomologicalComplex V c
g : Y✝ ⟶ Z✝
f : HomotopyEquiv X✝ Y✝
e : HomotopyEquiv X✝ Z✝
he : e.hom = f.hom ≫ g
⊢ Homotopy ((f.inv ≫ f.hom) ≫ g) g

Tactic:
exact f.homotopyInvHomId.compRightId g

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

Goal state before:
pp: ι✝ : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι✝
C✝ D E : HomologicalComplex V c✝
f✝ g✝ : C✝ ⟶ D
h✝ k : D ⟶ E
i✝ : ι✝
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝² : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
h : HomotopyEquiv K L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ homologyMap (𝟙 K) i = 𝟙 (K.homology i)

Tactic:
homologyMap_id

Goal state after:
ι✝ : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι✝
C✝ D E : HomologicalComplex V c✝
f✝ g✝ : C✝ ⟶ D
h✝ k : D ⟶ E
i✝ : ι✝
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝² : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
h : HomotopyEquiv K L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ 𝟙 (K.homology i) = 𝟙 (K.homology i)
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι✝ : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι✝
C✝ D E : HomologicalComplex V c✝
f✝ g✝ : C✝ ⟶ D
h✝ k : D ⟶ E
i✝ : ι✝
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝² : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
h : HomotopyEquiv K L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ homologyMap (𝟙 L) i = 𝟙 (L.homology i)

Tactic:
homologyMap_id

Goal state after:
ι✝ : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι✝
C✝ D E : HomologicalComplex V c✝
f✝ g✝ : C✝ ⟶ D
h✝ k : D ⟶ E
i✝ : ι✝
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝² : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
h : HomotopyEquiv K L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ 𝟙 (L.homology i) = 𝟙 (L.homology i)
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f g✝ : X ⟶ Y
f₁ f₂ g : X.as ⟶ Y.as
h₁₂ : HomRel.CompClosure r f₁ f₂
⊢ Quot.mk (HomRel.CompClosure r) (f₁ + g) = Quot.mk (HomRel.CompClosure r) (f₂ + g)

Tactic:
simp only [HomRel.compClosure_iff_self] at h₁₂
      erw [functor_map_eq_iff]
      exact hr _ _ _ _ h₁₂ (Congruence.equivalence.refl g)

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

Goal state before:
pp: ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
K L : HomologicalComplex V c
f : K ⟶ L
⊢ IsIso ((quotient V c).map f) ↔ homotopyEquivalences V c f

Tactic:
refine ⟨fun _ ↦ ?_, fun hf ↦ quotient_inverts_homotopyEquivalences _ _ _ hf⟩

Goal state after:
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
K L : HomologicalComplex V c
f : K ⟶ L
x✝ : IsIso ((quotient V c).map f)
⊢ homotopyEquivalences V c f
Module: Mathlib.Algebra.Homology.HomotopyCategory

Goal state before:
pp: ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
K L : HomologicalComplex V c
f : K ⟶ L
x✝ : IsIso ((quotient V c).map f)
⊢ homotopyEquivalences V c f

Tactic:
obtain ⟨g, hg⟩ := (quotient V c).map_surjective (inv ((quotient _ _).map f))

Goal state after:
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
K L : HomologicalComplex V c
f : K ⟶ L
x✝ : IsIso ((quotient V c).map f)
g : L ⟶ K
hg : (quotient V c).map g = inv ((quotient V c).map f)
⊢ homotopyEquivalences V c f
Module: Mathlib.CategoryTheory.Shift.Induced

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
⊢ (i (m₁ + m₂ + m₃)).hom.app X ≫
      F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
        (i m₃).inv.app ((shiftFunctor C (m₁ + m₂)).obj X) ≫
          (s m₃).map ((i (m₁ + m₂)).inv.app X) ≫
            (s m₃).map ((i (m₁ + m₂)).hom.app X) ≫
              (s m₃).map (F.map ((shiftFunctorAdd C m₁ m₂).hom.app X)) ≫
                (s m₃).map ((i m₂).inv.app ((shiftFunctor C m₁).obj X)) ≫
                  (s m₃).map ((s m₂).map ((i m₁).inv.app X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.app X)) =
    (eqToHom ⋯).app (F.obj X) ≫
      (i (m₁ + (m₂ + m₃))).hom.app X ≫
        F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
          (i (m₂ + m₃)).inv.app ((shiftFunctor C m₁).obj X) ≫
            (s (m₂ + m₃)).map ((i m₁).inv.app X) ≫
              (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.app X))

Tactic:
slice_lhs 4 5 =>
          erw [← Functor.map_comp, Iso.inv_hom_id_app, Functor.map_id]

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
⊢ (i (m₁ + m₂ + m₃)).hom.app X ≫
      F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
        (i m₃).inv.app ((shiftFunctor C (m₁ + m₂)).obj X) ≫
          (((𝟙 ((s m₃).obj (F.obj ((shiftFunctor C (m₁ + m₂)).obj X))) ≫
                  (s m₃).map (F.map ((shiftFunctorAdd C m₁ m₂).hom.app X))) ≫
                (s m₃).map ((i m₂).inv.app ((shiftFunctor C m₁).obj X))) ≫
              (s m₃).map ((s m₂).map ((i m₁).inv.app X))) ≫
            (s m₃).map ((s m₂).map ((i m₁).hom.app X)) =
    (eqToHom ⋯).app (F.obj X) ≫
      (i (m₁ + (m₂ + m₃))).hom.app X ≫
        F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
          (i (m₂ + m₃)).inv.app ((shiftFunctor C m₁).obj X) ≫
            (s (m₂ + m₃)).map ((i m₁).inv.app X) ≫
              (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.app X))
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : G.CommShift A
inst✝ : H.CommShift A
a : A
X : C
⊢ G.map ((iso e a).inv.app X) =
    (commShiftIso G a).hom.app (F.obj X) ≫
      (shiftFunctor E a).map (e.hom.app X) ≫ (commShiftIso H a).inv.app X ≫ e.inv.app ((shiftFunctor C a).obj X)

Tactic:
have h : ((whiskeringRight C D E).obj G).map (iso e a).inv = _ :=
    Functor.map_preimage _ _
  simpa using congr_app h X

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case ofNat.succ
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
H : ℤ → Prop := fun n ↦ ∀ T ∈ distinguishedTriangles, (shiftFunctor C n).obj T ∈ distinguishedTriangles
H_zero : H 0
H_one : H 1
H_neg_one : H (-1)
H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c
n : ℕ
hn : H (Int.ofNat n)
⊢ H (Int.ofNat (n + 1))

Tactic:
exact H_add hn H_one rfl

Goal state after: