mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
B : Type u_3
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
inj : Function.Injective ⇑(algebraMap R B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ y, (algebraMap R B) y = x
x✝ : A
hx : IsIntegral R x✝
⊢ ∃ y, (algebraMap R A) y = x✝

Tactic:
obtain ⟨y, fx_eq⟩ := cl.mp ((isIntegral_algHom_iff f hf).mpr hx)

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
B : Type u_3
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
inj : Function.Injective ⇑(algebraMap R B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ y, (algebraMap R B) y = x
x✝ : A
hx : IsIntegral R x✝
y : R
fx_eq : (algebraMap R B) y = f x✝
⊢ ∃ y, (algebraMap R A) y = x✝
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
y : K := (algebraMap R K) b / (algebraMap R K) a
⊢ IsIntegral R y

Tactic:
refine ⟨X ^ n - C x, monic_X_pow_sub_C _ hn, ?_⟩

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
y : K := (algebraMap R K) b / (algebraMap R K) a
⊢ eval₂ (algebraMap R K) y (X ^ n - C x) = 0
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
⊢ IsIntegrallyClosed S

Tactic:
by
  let K := FractionRing R
  let g : S →+* K := IsLocalization.map _ (T := R⁰) (RingHom.id R) hM
  let := g.toAlgebra
  have : IsScalarTower R S K := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
  have := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M S K
  refine (isIntegrallyClosed_iff_isIntegralClosure (K := K)).mpr
    ⟨IsFractionRing.injective _ _, fun {x} ↦ ⟨?_, fun e ↦ e.choose_spec ▸ isIntegral_algebraMap⟩⟩
  intro hx
  obtain ⟨⟨y, y_mem⟩, hy⟩ := hx.exists_multiple_integral_of_isLocalization M _
  obtain ⟨z, hz⟩ := (isIntegrallyClosed_iff _).mp ‹_› hy
  refine ⟨IsLocalization.mk' S z ⟨y, y_mem⟩, (IsLocalization.lift_mk'_spec _ _ _ _).mpr ?_⟩
  rw [RingHom.comp_id, hz, ← Algebra.smul_def, Submonoid.mk_smul]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ a + star a = ↑(2 * a.re + c₂ * a.imI)

Tactic:
by ext <;> simp [two_mul]; ring

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommGroup G
h : M
R : Type u_3
inst✝¹ : Ring R
inst✝ : Module R G
f : M → R
g : M → G
⊢ Δ_[h] (f • g) = Δ_[h] f • g + f • Δ_[h] g + Δ_[h] f • Δ_[h] g

Tactic:
by
  ext y
  simp only [fwdDiff, Pi.smul_apply', Pi.add_apply, smul_sub, sub_smul]
  abel

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x₁ x₂ : M
hxy✝ : x₁ * x₂ ∈ s.saturation
ih : ∃ y, x₁ * x₂ * y ∈ s
y : M
h : x₁ * x₂ * y ∈ s
⊢ x₂ * (x₁ * y) ∈ s

Tactic:
mul_left_comm,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x₁ x₂ : M
hxy✝ : x₁ * x₂ ∈ s.saturation
ih : ∃ y, x₁ * x₂ * y ∈ s
y : M
h : x₁ * x₂ * y ∈ s
⊢ x₁ * (x₂ * y) ∈ s
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
⊢ univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}

Tactic:
ext i

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
i : ι
⊢ i ∈ univ ↔ i ∈ {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
⊢ SemigroupWithZero α

Tactic:
by
  let mul := e.mul
  let zero := e.zero
  apply e.injective.semigroupWithZero _ <;> intros <;> exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : MonoidWithZero B
f : A →*₀ B
a✝ b✝ : Bˣ
hb : a✝ ∈ Units.val ⁻¹' range ⇑f
hb' : b✝ ∈ Units.val ⁻¹' range ⇑f
⊢ a✝ * b✝ ∈ Units.val ⁻¹' range ⇑f

Tactic:
obtain ⟨y, hy⟩ := hb
    obtain ⟨y', hy'⟩ := hb'
    use y * y'
    rw [map_mul, hy, hy', Units.val_mul]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ ↑f.valueMonoid = ↑f.valueGroup

Tactic:
by
  rw [valueMonoid_eq_valueGroup, coe_toSubmonoid]

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X Y : FintypeCat
f : X ⟶ Y
x : (uSwitch.obj X).obj
⊢ (ConcreteCategory.hom f) (X.uSwitchEquiv x) = Y.uSwitchEquiv ((ConcreteCategory.hom (uSwitch.map f)) x)

Tactic:
simp only [uSwitch, uSwitchEquiv, Equiv.trans_apply, Equiv.ulift_apply]
  rw [homMk_apply]
  aesop

Goal state after:
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ (kernelSubobject (X.δ i.succ)).Factors ((objX X (n + 1 + 1)).arrow ≫ X.δ 0)

Tactic:
apply kernelSubobject_factors

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ ((objX X (n + 1 + 1)).arrow ≫ X.δ 0) ≫ X.δ i.succ = 0
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ HasEqualizer (𝟙 X) p

Tactic:
exact
      ⟨Nonempty.intro
          { cone := Fork.ofι i (show i ≫ 𝟙 X = i ≫ p by rw [comp_id, ← h₂, ← assoc, h₁, id_comp])
            isLimit := by
              apply Fork.IsLimit.mk'
              intro s
              refine ⟨s.ι ≫ e, ?_⟩
              constructor
              · simp [h₂, ← Limits.Fork.condition s]
              · intro m hm
                rw [Fork.ι_ofι] at hm
                rw [← hm]
                simp only [assoc, h₁]
                exact (comp_id m).symm }⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : SimplexCategory
f g : ⦋0⦌ ⟶ n
h0 : (toOrderHom f) 0 = (toOrderHom g) 0
⊢ f = g

Tactic:
ext i

Goal state after:
n : SimplexCategory
f g : ⦋0⦌ ⟶ n
h0 : (toOrderHom f) 0 = (toOrderHom g) 0
i : Fin (⦋0⦌.len + 1)
⊢ ↑((toOrderHom f) i) = ↑((toOrderHom g) i)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : SimplexCategory
f g : ⦋1⦌ ⟶ n
h0 : (toOrderHom f) 0 = (toOrderHom g) 0
h1 : (toOrderHom f) 1 = (toOrderHom g) 1
⊢ f = g

Tactic:
ext i

Goal state after:
n : SimplexCategory
f g : ⦋1⦌ ⟶ n
h0 : (toOrderHom f) 0 = (toOrderHom g) 0
h1 : (toOrderHom f) 1 = (toOrderHom g) 1
i : Fin (⦋1⦌.len + 1)
⊢ ↑((toOrderHom f) i) = ↑((toOrderHom g) i)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ δ i.castSucc ≫ σ j.succ = σ j ≫ δ i

Tactic:
ext k : 3

Goal state after:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
⊢ (Hom.toOrderHom (δ i.castSucc ≫ σ j.succ)) k = (Hom.toOrderHom (σ j ≫ δ i)) k
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ δ i.succ ≫ σ j.castSucc = σ j ≫ δ i

Tactic:
ext k : 3

Goal state after:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
⊢ (Hom.toOrderHom (δ i.succ ≫ σ j.castSucc)) k = (Hom.toOrderHom (σ j ≫ δ i)) k
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ σ i.castSucc ≫ σ j = σ j.succ ≫ σ i

Tactic:
ext k : 3

Goal state after:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (⦋n + 1 + 1⦌.len + 1)
⊢ (Hom.toOrderHom (σ i.castSucc ≫ σ j)) k = (Hom.toOrderHom (σ j.succ ≫ σ i)) k
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
j : Fin (n + 2)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f) k ≠ j
⊢ factor_δ f j ≫ δ j = f

Tactic:
ext k : 3

Goal state after:
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
j : Fin (n + 2)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f) k ≠ j
k : Fin (⦋m⦌.len + 1)
⊢ (Hom.toOrderHom (factor_δ f j ≫ δ j)) k = (Hom.toOrderHom f) k
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasPullbacks C
X✝ Y✝ : SimplicialObject C
x✝² : X✝ ⟶ Y✝
x✝¹ : Mono x✝²
x✝ : ℕ
⊢ Mono (((alternatingFaceMapComplex C).map x✝²).f x✝)

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
j✝ : Fin ((Opposite.unop y).len + 1)
⊢ (X.left.map f ≫
        WidePullback.lift (X.hom.app y ≫ Arrow.Hom.right G)
          (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop y) i).op ≫ Arrow.Hom.left G) ⋯) ≫
      WidePullback.π (fun x ↦ F.hom) j✝ =
    (WidePullback.lift (X.hom.app x ≫ Arrow.Hom.right G)
          (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop x) i).op ≫ Arrow.Hom.left G) ⋯ ≫
        WidePullback.lift (WidePullback.base fun x ↦ F.hom)
          (fun i ↦ WidePullback.π (fun x ↦ F.hom) ((SimplexCategory.Hom.toOrderHom f.unop) i)) ⋯) ≫
      WidePullback.π (fun x ↦ F.hom) j✝

pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
⊢ ((X.left.map f ≫
        WidePullback.lift (X.hom.app y ≫ Arrow.Hom.right G)
          (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop y) i).op ≫ Arrow.Hom.left G) ⋯) ≫
      WidePullback.base fun x ↦ F.hom) =
    (WidePullback.lift (X.hom.app x ≫ Arrow.Hom.right G)
          (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop x) i).op ≫ Arrow.Hom.left G) ⋯ ≫
        WidePullback.lift (WidePullback.base fun x ↦ F.hom)
          (fun i ↦ WidePullback.π (fun x ↦ F.hom) ((SimplexCategory.Hom.toOrderHom f.unop) i)) ⋯) ≫
      WidePullback.base fun x ↦ F.hom

Tactic:
· simp only [WidePullback.lift_π, Category.assoc, ← X.left.map_comp_assoc]
          rfl

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
⊢ ((X.left.map f ≫
        WidePullback.lift (X.hom.app y ≫ Arrow.Hom.right G)
          (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop y) i).op ≫ Arrow.Hom.left G) ⋯) ≫
      WidePullback.base fun x ↦ F.hom) =
    (WidePullback.lift (X.hom.app x ≫ Arrow.Hom.right G)
          (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop x) i).op ≫ Arrow.Hom.left G) ⋯ ≫
        WidePullback.lift (WidePullback.base fun x ↦ F.hom)
          (fun i ↦ WidePullback.π (fun x ↦ F.hom) ((SimplexCategory.Hom.toOrderHom f.unop) i)) ⋯) ≫
      WidePullback.base fun x ↦ F.hom
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
⊢ Mono (g hf₁ f₂)

Tactic:
have := isIso_factorThruImage_g hf₁ hy₁ hy₂

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
this : IsIso (factorThruImage (g hf₁ f₂))
⊢ Mono (g hf₁ f₂)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: case e'_3
C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) := ⋯
x✝ : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1✝ : ComposableArrows C 1 = (fun X ↦ X) (nerve C _⦋1⦌)
⊢ ComposableArrows.arrowEquiv.symm (Arrow.mk f₀₂) = (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) h.simplex

Tactic:
exact (h.d₁).symm

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ {
        f := fun x ↦
          match x with
          | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
          | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1)),
        comm' := ⋯ } ≫
      {
        f := fun x ↦
          match x with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)),
        comm' := ⋯ } =
    𝟙 ((truncate.obj C).augment (C.d 1 0) ⋯)

Tactic:
ext i

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ ({
            f := fun x ↦
              match x with
              | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
              | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1)),
            comm' := ⋯ } ≫
          {
            f := fun x ↦
              match x with
              | 0 => 𝟙 (C.X 0)
              | n.succ => 𝟙 (C.X (n + 1)),
            comm' := ⋯ }).f
      i =
    (𝟙 ((truncate.obj C).augment (C.d 1 0) ⋯)).f i
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ {
        f := fun x ↦
          match x with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)),
        comm' := ⋯ } ≫
      {
        f := fun x ↦
          match x with
          | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
          | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1)),
        comm' := ⋯ } =
    𝟙 C

Tactic:
ext i

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ ({
            f := fun x ↦
              match x with
              | 0 => 𝟙 (C.X 0)
              | n.succ => 𝟙 (C.X (n + 1)),
            comm' := ⋯ } ≫
          {
            f := fun x ↦
              match x with
              | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
              | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1)),
            comm' := ⋯ }).f
      i =
    (𝟙 C).f i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
⊢ ∀ {a b : Fin (d + 1)},
    (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) a ≤ (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) b ↔ a ≤ b

Tactic:
by
    have := (mem_nonDegenerate_iff_mono x.val).1 x.property
    rw [SimplexCategory.mono_iff_injective] at this
    intro a b
    dsimp
    simp only [Subtype.mk_le_mk]
    constructor
    · rw [← not_lt, ← not_lt]
      intro h h'
      apply h
      obtain h'' | h'' := (monotone_apply x.val h'.le).lt_or_eq
      · assumption
      · simp only [this h'', lt_self_iff_false] at h'
    · intro h
      exact monotone_apply _ h

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
⊢ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } =
    𝟙 (truncate.obj (C.augment f w))

Tactic:
ext i

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
⊢ ({ f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ }).f i =
    (𝟙 (truncate.obj (C.augment f w))).f i
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
⊢ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } = 𝟙 C

Tactic:
ext i

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
⊢ ({ f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ }).f i =
    (𝟙 C).f i
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
⊢ (mapTrifunctorObj F X₁ I₂ I₃).map ψ ≫
      { app := fun X₃ x ↦ ((F.map (φ x.1)).app (Y₂ x.2.1)).app (X₃ x.2.2), naturality := ⋯ } =
    { app := fun X₃ x ↦ ((F.map (φ x.1)).app (X₂ x.2.1)).app (X₃ x.2.2), naturality := ⋯ } ≫
      (mapTrifunctorObj F Y₁ I₂ I₃).map ψ

Tactic:
ext X₃ x
        dsimp
        simp only [← NatTrans.comp_app]
        congr 1
        rw [NatTrans.naturality]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
i₁ i₁' : I₁
h : ¬c₁.Rel i₁ i₁'
i₂ : I₂
⊢ (K.d i₁ i₁').f i₂ = 0

Tactic:
K.shape _ _ h,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
i₁ i₁' : I₁
h : ¬c₁.Rel i₁ i₁'
i₂ : I₂
⊢ Hom.f 0 i₂ = 0
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁶ : TotalComplexShape c₁ c₂ c
inst✝⁵ : TotalComplexShape c₂ c₁ c
inst✝⁴ : TotalComplexShapeSymmetry c₁ c₂ c
inst✝³ : K.HasTotal c
inst✝² : DecidableEq J
inst✝¹ : TotalComplexShapeSymmetry c₂ c₁ c
inst✝ : TotalComplexShapeSymmetrySymmetry c₁ c₂ c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
⊢ K.flip.flip.ιTotal c i₁ i₂ j h ≫ (K.flip.totalFlipIso c).hom.f j =
    K.flip.flip.ιTotal c i₁ i₂ j h ≫ (K.totalFlipIso c).symm.hom.f j

Tactic:
rw [Iso.symm_hom, ιTotal_totalFlipIso_f_hom]

Goal state after:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁶ : TotalComplexShape c₁ c₂ c
inst✝⁵ : TotalComplexShape c₂ c₁ c
inst✝⁴ : TotalComplexShapeSymmetry c₁ c₂ c
inst✝³ : K.HasTotal c
inst✝² : DecidableEq J
inst✝¹ : TotalComplexShapeSymmetry c₂ c₁ c
inst✝ : TotalComplexShapeSymmetrySymmetry c₁ c₂ c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
⊢ c₂.σ c₁ c i₂ i₁ • K.flip.ιTotal c i₂ i₁ j ⋯ = K.flip.flip.ιTotal c i₁ i₂ j h ≫ (K.totalFlipIso c).inv.f j
Module: Mathlib.CategoryTheory.Shift.CommShiftTwo

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₁'
inst✝⁹ : Category.{v_3, u_3} C₂
inst✝⁸ : Category.{v_4, u_4} C₂'
inst✝⁷ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₁' M
inst✝³ : HasShift C₂ M
inst✝² : HasShift D M
F : C₁' ⥤ C₁
inst✝¹ : F.CommShift M
G : C₁ ⥤ C₂ ⥤ D
h : CommShift₂Setup D M
inst✝ : G.CommShift₂ h
X₁' Y₁' : C₁'
f : X₁' ⟶ Y₁'
⊢ NatTrans.CommShift ((F ⋙ G).map f) M

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Shift.CommShiftTwo

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₁'
inst✝⁹ : Category.{v_3, u_3} C₂
inst✝⁸ : Category.{v_4, u_4} C₂'
inst✝⁷ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₂' M
inst✝³ : HasShift C₂ M
inst✝² : HasShift D M
F : C₂' ⥤ C₂
inst✝¹ : F.CommShift M
G : C₁ ⥤ C₂ ⥤ D
h : CommShift₂Setup D M
inst✝ : G.CommShift₂ h
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
⊢ NatTrans.CommShift ((G ⋙ (whiskeringLeft C₂' C₂ D).obj F).map f) M

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Shift.CommShiftTwo

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₁'
inst✝⁹ : Category.{v_3, u_3} C₂
inst✝⁸ : Category.{v_4, u_4} C₂'
inst✝⁷ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₂ M
inst✝³ : HasShift D M
G₁ G₂ G₃ : C₁ ⥤ C₂ ⥤ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup D M
inst✝² : G₁.CommShift₂ h
inst✝¹ : G₂.CommShift₂ h
inst✝ : G₃.CommShift₂ h
x✝ : C₁
⊢ CommShift ((𝟙 G₁).app x✝) M

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Shift.CommShiftTwo

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst✝¹³ : Category.{v_1, u_1} C₁
inst✝¹² : Category.{v_2, u_2} C₁'
inst✝¹¹ : Category.{v_3, u_3} C₂
inst✝¹⁰ : Category.{v_4, u_4} C₂'
inst✝⁹ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁸ : AddCommMonoid M
inst✝⁷ : HasShift C₁ M
inst✝⁶ : HasShift C₂ M
inst✝⁵ : HasShift D M
G₁ G₂ G₃ : C₁ ⥤ C₂ ⥤ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup D M
inst✝⁴ : G₁.CommShift₂ h
inst✝³ : G₂.CommShift₂ h
inst✝² : G₃.CommShift₂ h
inst✝¹ : CommShift₂ τ h
inst✝ : CommShift₂ τ' h
x✝ : C₁
⊢ CommShift ((τ ≫ τ').app x✝) M

Tactic:
dsimp; infer_instance

Goal state after: