mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f g : End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
μ : R
hf' : MapsTo ⇑f ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
⊢ (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0

Tactic:
have hg' := f.mapsTo_maxGenEigenspace_of_comm h_comm μ

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f g : End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
μ : R
hf' : MapsTo ⇑f ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
hg' : MapsTo ⇑g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
⊢ (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ((toMatrix b b) ((id ∘ₗ f) ∘ₗ id)).trace = ((toMatrix c b) id * (toMatrix c c) f * (toMatrix b c) id).trace

Tactic:
by
        rw [LinearMap.toMatrix_comp _ c, LinearMap.toMatrix_comp _ c]

Goal state after:
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fg :
  { fg //
    (∀ (x y : A), fg.2 x * fg.2 y = 0) ∧
      (∀ (r x : A), fg.2 (r • x) = fg.1 r * fg.2 x) ∧ ∀ (r x : A), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r }
a : A
⊢ (↑fg).2 (MulOpposite.op a • 1) = (↑fg).2 (a * 1)

Tactic:
op_smul_eq_mul,

Goal state after:
R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fg :
  { fg //
    (∀ (x y : A), fg.2 x * fg.2 y = 0) ∧
      (∀ (r x : A), fg.2 (r • x) = fg.1 r * fg.2 x) ∧ ∀ (r x : A), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r }
a : A
⊢ (↑fg).2 (1 * a) = (↑fg).2 (a * 1)
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : IsProj p f
inst✝³ : Free R ↥p
inst✝² : Module.Finite R ↥p
inst✝¹ : Free R ↥f.ker
inst✝ : Module.Finite R ↥f.ker
⊢ (LinearMap.trace R M) f = ↑(finrank R ↥p)

Tactic:
by
  rw [h.eq_conj_prodMap, trace_conj', trace_prodMap', trace_id, map_zero, add_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsDomain R
inst✝³ : IsTorsionFree R M
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := fun x ↦ ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g y ⊓ g (x + y)
⊢ Disjoint (((f x + f y).genEigenspace (μ x + μ y)) (k + k)) (((f x + f y).genEigenspace (μ (x + y))) k)

Tactic:
exact disjoint_genEigenspace (f x + f y) (Ne.symm contra) _ k

Goal state after:
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ -x + ((x ^ n)⁻¹ * x + (-(x ^ n)⁻¹ + 1)) = -x + ((x ^ n)⁻¹ * x + -(x ^ n)⁻¹ + 1)

Tactic:
add_assoc _ _ 1

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ -x + ((x ^ n)⁻¹ * x + (-(x ^ n)⁻¹ + 1)) = -x + ((x ^ n)⁻¹ * x + (-(x ^ n)⁻¹ + 1))
Module: Mathlib.Algebra.Field.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : DivisionSemiring α
inst✝ : Neg β
h : Antiperiodic f c
a : α
ha : a ≠ 0
⊢ Antiperiodic (fun x ↦ f (x * a)) (c / a)

Tactic:
by
  simpa only [div_eq_mul_inv] using h.mul_const ha

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: case refine_1.left
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
a c d e f : α
⊢ Quot.mk (AssocRel α) (a * (c * (d * e * f))) = Quot.mk (AssocRel α) (a * (c * (d * (e * f))))

Tactic:
· rw [← quot_mk_assoc, quot_mk_assoc_left, quot_mk_assoc]

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
l₁ l₂ : FreeMonoid α
⊢ countP' p (l₁ * l₂) = countP' p l₁ + countP' p l₂

Tactic:
dsimp [countP']
  simp only [List.countP_append]

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Count

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ (count x) (of y) = Pi.single x 1 y

Tactic:
by
  dsimp [count]
  rw [countP_of]
  simp [Pi.single, Function.update]

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: case inr
α : Type u_1
x : FreeMonoid α
b : α
y : FreeSemigroup α
⊢ FreeMonoid.of b * toFreeMonoid y = 1 ∨ ∃ y_1, toFreeMonoid y_1 = FreeMonoid.of b * toFreeMonoid y

Tactic:
· exact Or.inr ⟨of b * y, by simp⟩

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: case one
α : Type u_1
⊢ (WithOne.lift toFreeMonoid) ((lift fun x ↦ ↑(FreeSemigroup.of x)) 1) = 1

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: case of
α : Type u_1
x✝ : α
⊢ (WithOne.lift toFreeMonoid) ((lift fun x ↦ ↑(FreeSemigroup.of x)) (of x✝)) = of x✝

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: case mul
α : Type u_1
x✝ y✝ : FreeMonoid α
a✝¹ : (WithOne.lift toFreeMonoid) ((lift fun x ↦ ↑(FreeSemigroup.of x)) x✝) = x✝
a✝ : (WithOne.lift toFreeMonoid) ((lift fun x ↦ ↑(FreeSemigroup.of x)) y✝) = y✝
⊢ (WithOne.lift toFreeMonoid) ((lift fun x ↦ ↑(FreeSemigroup.of x)) (x✝ * y✝)) = x✝ * y✝

Tactic:
simp [*]

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

Goal state before:
pp: case inl
m k : ℕ
hmn : m < m + k + 1
⊢ Δ_[1]^[k] (Δ_[1]^[1] (Δ_[1]^[m] fun x ↦ ↑(x.choose m))) 0 = 0

Tactic:
add_zero m ▸ fwdDiff_iter_choose 0 m,

Goal state after:
case inl
m k : ℕ
hmn : m < m + k + 1
⊢ Δ_[1]^[k] (Δ_[1]^[1] fun x ↦ ↑(x.choose 0)) 0 = 0
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: case inl
S : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : LinearOrder G
x✝ : SetLike S G
inst✝ : InvMemClass S G
H : S
x : G
h✝ : |x|ₘ = x
⊢ |x|ₘ ∈ H ↔ x ∈ H

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: case inr
S : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : LinearOrder G
x✝ : SetLike S G
inst✝ : InvMemClass S G
H : S
x : G
h✝ : |x|ₘ = x⁻¹
⊢ |x|ₘ ∈ H ↔ x ∈ H

Tactic:
simp [*]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x : M
⊢ x ∈ s.saturation ↔ ∃ y, y * x ∈ s

Tactic:
mem_saturation_iff,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x : M
⊢ (∃ y, x * y ∈ s) ↔ ∃ y, y * x ∈ s
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
⊢ (0 •> ∅)⁻¹ = ∅⁻¹ <• 0⁻¹

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: case inl.inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
⊢ (∅ <• 0)⁻¹ = 0⁻¹ •> ∅⁻¹

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: case inl.inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹

Tactic:
simp [*]

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

Goal state before:
pp: G₀ : Type u_1
H₀ : Type u_2
inst✝¹ : GroupWithZero G₀
inst✝ : GroupWithZero H₀
⊢ Function.Surjective ⇑(fst G₀ H₀)

Tactic:
classical
  exact Function.HasRightInverse.surjective ⟨inl .., fun _ ↦ by simp⟩

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
b : Bˣ
hb : ↑b ∈ range ⇑f
⊢ b ∈ f.valueGroup

Tactic:
suffices b ∈ valueMonoid f from Subgroup.mem_closure.mpr fun _ a ↦ a this

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : MonoidWithZero B
f : A →*₀ B
b : Bˣ
hb : ↑b ∈ range ⇑f
⊢ b ∈ f.valueMonoid
Module: Mathlib.CategoryTheory.FintypeCat

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

Tactic:
rw [Equiv.eq_symm_apply, ← uSwitchEquiv_naturality f, Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
h₁ : (LinOrd.Hom.hom f.hom) a < m
h₂ : ¬(LinOrd.Hom.hom f.hom) a ≤ m
⊢ { down := 0 } = { down := 1 }

Tactic:
exfalso
        exact h₂ (le_of_lt h₁)

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case hi
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
ij : P
hij : ij ∈ {ij | ↑ij.2 ≤ ↑ij.1}
⊢ (ij.2.castLT ⋯, ij.1.succ) ∈ {ij | ↑ij.2 ≤ ↑ij.1}ᶜ

Tactic:
Finset.compl_filter,

Goal state after:
case hi
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
ij : P
hij : ij ∈ {ij | ↑ij.2 ≤ ↑ij.1}
⊢ (ij.2.castLT ⋯, ij.1.succ) ∈ {x | ¬↑x.2 ≤ ↑x.1}
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case i_surj
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (i', j') ∈ {ij | ↑ij.2 ≤ ↑ij.1}ᶜ
⊢ ∃ a, ∃ (ha : a ∈ S), φ a ha = (i', j')

Tactic:
Finset.compl_filter,

Goal state after:
case i_surj
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (i', j') ∈ {x | ¬↑x.2 ≤ ↑x.1}
⊢ ∃ a, ∃ (ha : a ∈ S), φ a ha = (i', j')
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h_obj.h_d
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X : SimplicialObject C
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      ((alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X).d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X).d i j

pp: case h_obj.h_X
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X : SimplicialObject C
⊢ ((alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X).X =
    (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X).X

Tactic:
· rintro i j (rfl : j + 1 = i)
      dsimp only [Functor.comp_obj]
      simp only [Functor.mapHomologicalComplex_obj_d, alternatingFaceMapComplex_obj_d,
        eqToHom_refl, id_comp, comp_id, AlternatingFaceMapComplex.objD, Functor.map_sum,
        Functor.map_zsmul]
      rfl

Goal state after:
case h_obj.h_X
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X : SimplicialObject C
⊢ ((alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X).X =
    (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X).X
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 =
    (match i with
      | 0 => (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ inv ⊤.arrow
      | n.succ =>
        (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
          ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯) ≫
      (match i with
        | 0 => ⊤
        | n.succ => Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow

Tactic:
cases i <;> simp

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

Goal state before:
pp: case pos.inr
n m : ℕ
k : Fin (⦋m⦌.len + 1)
h : n + (↑k + 1) = m
hk : ↑k ≤ ↑k
⊢ 0 = ↑(Fin.predAbove 0 ((ConcreteCategory.hom (σ₀Iter ↑k ⋯)) k))

Tactic:
· grind [Fin.predAbove_of_le_castSucc, Fin.coe_castPred, σ₀Iter_coe_eq_of_ge, tsub_self]

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

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
i j : Fin (n.len + 1)
hij : i ≤ j
⊢ j.rev ≤ i.rev

Tactic:
by rwa [Fin.rev_le_rev]

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
⊢ ofSection x = range (yonedaEquiv.symm x)

Tactic:
ext U y
  simp only [ofSection_obj, Set.mem_ofPred_eq, Opposite.op_unop, range_obj,
    Set.mem_range]
  constructor
  · rintro ⟨f, rfl⟩
    exact ⟨f.unop, rfl⟩
  · rintro ⟨f, rfl⟩
    exact ⟨f.op, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : C
f : yoneda.obj X ⟶ F
⊢ range f = ofSection (yonedaEquiv f)

Tactic:
rw [ofSection_eq_range, Equiv.symm_apply_apply]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X✝ Y✝ : SSet
f : X✝ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
⊢ IsIso f

Tactic:
NatTrans.isIso_iff_isIso_app

Goal state after:
X✝ Y✝ : SSet
f : X✝ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
⊢ ∀ (X : SimplexCategoryᵒᵖ), IsIso (f.app X)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x y : X.N
⊢ x ≤ y ↔ ∃ f, ∃ (_ : Mono f), (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex

Tactic:
by
  simp only [le_iff, CategoryTheory.Subfunctor.ofSection_le_iff,
    Subcomplex.mem_ofSimplex_obj_iff]
  exact ⟨fun ⟨f, hf⟩ ↦ ⟨f, X.mono_of_nonDegenerate ⟨_, x.nonDegenerate⟩ f _ hf, hf⟩, by tauto⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ X.right.map (⦋0⦌.const ⦋0⦌ 0) = 𝟙 (Augmented.toArrow.obj X).right

Tactic:
convert! X.right.map_id _

Goal state after:
case e'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ ⦋0⦌.const ⦋0⦌ 0 = 𝟙 ⦋0⦌
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
s : X.N
d : ℕ
hd : s.dim = d
⊢ (s.cast hd).simplex ∈ X.nonDegenerate (s.cast hd).dim

Tactic:
subst hd

Goal state after:
X : SSet
s : X.N
__S✝ : X.S := s.cast ⋯
⊢ (s.cast ⋯).simplex ∈ X.nonDegenerate (s.cast ⋯).dim
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
s : X.N
d : ℕ
hd : s.dim = d
⊢ s.cast hd = s

Tactic:
subst hd

Goal state after:
X : SSet
s : X.N
⊢ s.cast ⋯ = s
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X : SSet
ι : Type u_1
inst✝ : Finite ι
A : ι → X.Subcomplex
⊢ (⨆ i, A i).toSSet.Finite ↔ ∀ (i : ι), (A i).toSSet.Finite

Tactic:
refine ⟨fun h i ↦ finite_of_mono (Subcomplex.homOfLE (le_iSup A i)), fun h ↦ ⟨?_⟩⟩
  refine Finite.of_surjective (f := fun (⟨i, s⟩ : Σ (i : ι), (A i).toSSet.N) ↦
    N.mk ((Subcomplex.homOfLE (le_iSup A i)).app _ s.simplex)
      (by simpa only [nonDegenerate_iff_of_mono] using s.nonDegenerate)) ?_
  intro s
  obtain ⟨d, ⟨⟨s, h₁⟩, h₂⟩, rfl⟩ := s.mk_surjective
  simp only [Subfunctor.iSup_obj, Set.mem_iUnion] at h₁
  obtain ⟨i, hi⟩ := h₁
  rw [Subcomplex.mem_nonDegenerate_iff] at h₂
  exact ⟨⟨i, N.mk ⟨s, hi⟩ (by rwa [Subcomplex.mem_nonDegenerate_iff])⟩, rfl⟩

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 ℕ
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

Tactic:
cases i <;> simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : Augmented C
e : X ≅ Y
ed : X.ExtraDegeneracy
⊢ ((drop.mapIso e).inv.app (op ⦋0⦌) ≫ ed.s 0 ≫ (drop.mapIso e).hom.app (op ⦋0 + 1⦌)) ≫ Y.left.δ 1 =
    Y.hom.app (op ⦋0⦌) ≫ (point.mapIso e).inv ≫ ed.s' ≫ (drop.mapIso e).hom.app (op ⦋0⦌)

Tactic:
simp [← SimplicialObject.δ_naturality, s₀_comp_δ₁_assoc, w₀_assoc]

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 ℕ
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

Tactic:
cases i <;> simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ ↑i.castSucc.succ = ↑1 + ↑i

Tactic:
by simp; grind

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

Tactic:
cases i <;> simp

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

Tactic:
cases i <;> simp

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
⊢ ∀ {i₁ i₁' : ℤ},
    (up ℤ).Rel i₁ i₁' →
      ∀ (i₂ : ℤ),
        (i₁ * i₂).negOnePow * (up ℤ).ε₁ (up ℤ) (up ℤ) (i₁, i₂) = (up ℤ).ε₂ (up ℤ) (up ℤ) (i₂, i₁) * (i₁' * i₂).negOnePow

Tactic:
rintro p _ rfl q

Goal state after:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
⊢ (p * q).negOnePow * (up ℤ).ε₁ (up ℤ) (up ℤ) (p, q) = (up ℤ).ε₂ (up ℤ) (up ℤ) (q, p) * ((p + 1) * q).negOnePow
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ K.D₁ c₁₂ i₁₂ i₁₂' =
    K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ 0

Tactic:
simp only [totalAux.ιMapObj_D₁, comp_zero]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂' = 0