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

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝ : MulOneClass M
c : Con M
f g : ι → M
x : ι
xs : List ι
ih : (∀ x ∈ xs, c (f x) (g x)) → c (List.map f xs).prod (List.map g xs).prod
h : ∀ x_1 ∈ x :: xs, c (f x_1) (g x_1)
⊢ c (List.map f (x :: xs)).prod (List.map g (x :: xs)).prod

Tactic:
rw [List.map_cons, List.map_cons, List.prod_cons, List.prod_cons]

Goal state after:
case cons
ι : Type u_1
M : Type u_2
inst✝ : MulOneClass M
c : Con M
f g : ι → M
x : ι
xs : List ι
ih : (∀ x ∈ xs, c (f x) (g x)) → c (List.map f xs).prod (List.map g xs).prod
h : ∀ x_1 ∈ x :: xs, c (f x_1) (g x_1)
⊢ c (f x * (List.map f xs).prod) (g x * (List.map g xs).prod)
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h h' : (i : ι) → β i →+ M
f g : Π₀ (i : ι), β i
H : ∀ (i : ι), c ((h i) (f i)) ((h' i) (g i))
⊢ c ((DFinsupp.sumAddHom h) f) ((DFinsupp.sumAddHom h') g)

Tactic:
simp_rw [DFinsupp.sumAddHom_apply]
  exact c.dfinsuppSum _ _
    (bot_le (a := c) <| map_zero <| h ·) (bot_le (a := c) <| map_zero <| h' ·) H

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
le : matrix n I ≤ matrix n J
x : R
xI : x ∈ I
⊢ (of fun x_1 x_2 ↦ x) ∈ matrix n I

Tactic:
by simp [xI]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
hef : ∀ (i : I), e i ∈ f.range
⊢ ∃ e', (CompleteOrthogonalIdempotents fun t ↦ Option.rec e₀ e' t) ∧ e = ⇑f ∘ e'

Tactic:
choose e' he' using hef

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
⊢ ∃ e', (CompleteOrthogonalIdempotents fun t ↦ Option.rec e₀ e' t) ∧ e = ⇑f ∘ e'
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
⊢ ∀ {a b : R},
    (a ∈ Set.range fun x ↦ e * x * e) → (b ∈ Set.range fun x ↦ e * x * e) → a * b ∈ Set.range fun x ↦ e * x * e

Tactic:
by rintro _ _ ⟨a, rfl⟩ ⟨b, rfl⟩; exact ⟨a * e * e * b, by simp_rw [mul_assoc]⟩

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e r : R
he : IsIdempotentElem e
I : Ideal R
H : (1 - e) * r ∈ I
⊢ e ∣ (1 - e) * r - r

Tactic:
by simp [sub_mul]

Goal state after:
Module: Mathlib.Algebra.Divisibility.Prod

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Semigroup (G i)
x y : (i : ι) → G i
⊢ x ∣ y ↔ ∀ (i : ι), x i ∣ y i

Tactic:
dvd_def,

Goal state after:
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Semigroup (G i)
x y : (i : ι) → G i
⊢ (∃ c, y = x * c) ↔ ∀ (i : ι), ∃ c, y i = x i * c
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
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
⊢ trace R (M × N) ∘ₗ prodMapLinear R M N M N R = id.coprod id ∘ₗ (trace R M).prodMap (trace R N)

Tactic:
by
  let e := (dualTensorHomEquiv R M M).prodCongr (dualTensorHomEquiv R N N)
  have h : Function.Surjective e.toLinearMap := e.surjective
  refine (cancel_right h).1 ?_
  ext <;> simp [e]

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: K : Type u_6
m : Type u_7
F : Type u_8
inst✝⁴ : Field K
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : FunLike F (Matrix m m K) (Matrix m m K)
inst✝ : AlgHomClass F K (Matrix m m K) (Matrix m m K)
f : F
x : Matrix m m K
⊢ (f x).trace = x.trace

Tactic:
by
  by_cases! Nonempty m
  · exact Matrix.trace_map (AlgEquiv.ofBijective _ (AlgHomClass.toAlgHom f).bijective) x
  · simp

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

Goal state before:
pp: K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
n : ℕ
⊢ Submodule.map ((f - (algebraMap K (End K V)) μ) ^ n) (LinearMap.range f) ≤ f.genEigenrange μ ↑n

Tactic:
rw [genEigenrange_nat]; apply LinearMap.map_le_range

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 - 1)⁻¹ * (x - x⁻¹ ^ n * x) * (x⁻¹ - 1) = x⁻¹ ^ n - 1

Tactic:
← mul_right_inj' h₃,

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 - 1) * ((x - 1)⁻¹ * (x - x⁻¹ ^ n * x) * (x⁻¹ - 1)) = (x - 1) * (x⁻¹ ^ n - 1)
Module: Mathlib.Algebra.Free

Goal state before:
pp: case refine_2
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
⊢ ∀ (a₁ a₂ b : α), AssocRel α a₁ a₂ → Quot.mk (AssocRel α) (a₁ * b) = Quot.mk (AssocRel α) (a₂ * b)

Tactic:
· rintro a₁ a₂ b (⟨c, d, e⟩ | ⟨c, d, e, f⟩)
      · simp only [quot_mk_assoc, quot_mk_assoc_left]
      · rw [quot_mk_assoc, quot_mk_assoc, quot_mk_assoc_left, quot_mk_assoc_left,
          quot_mk_assoc_left, ← quot_mk_assoc c d, ← quot_mk_assoc c d, quot_mk_assoc_left]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : reduce L = L
⊢ IsReduced L

Tactic:
rw [IsReduced, List.isChain_iff_forall_rel_of_append_cons_cons]
  rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ l₁ l₂ hl rfl
  rw [eq_comm, ← Bool.ne_not]
  rintro rfl
  exact reduce.not (h.trans hl)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case a
α : Type u
inst✝ : Nonempty α
⊢ max #α ℵ₀ ≤ #(FreeGroup α)

Tactic:
apply max_le

Goal state after:
case a.h₁
α : Type u
inst✝ : Nonempty α
⊢ #α ≤ #(FreeGroup α)

case h₂
α : Type u
inst✝ : Nonempty α
⊢ ℵ₀ ≤ #(FreeGroup α)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: case inr
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
h₂ : f.natDegree < n
⊢ f.coeff n ∈ 𝓟

Tactic:
rw [coeff_eq_zero_of_natDegree_lt h₂]
    exact Ideal.zero_mem _

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ≥0
⊢ ↑↑x✝.num / ↑↑x✝.den = ↑x✝.num / ↑x✝.den

Tactic:
coe_natCast,

Goal state after:
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ≥0
⊢ ↑x✝.num / ↑↑x✝.den = ↑x✝.num / ↑x✝.den
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case succ
R : Type u_3
inst✝ : CommRing R
n : ℕ
IH : (Δ_[1]^[n] fun r ↦ r ^ n) = ↑n !
this : (Δ_[1] fun r ↦ r ^ (n + 1)) = ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i
⊢ Δ_[1]^[n] (∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i) = ↑(n + 1)!

Tactic:
fwdDiff_iter_finsetSum,

Goal state after:
case succ
R : Type u_3
inst✝ : CommRing R
n : ℕ
IH : (Δ_[1]^[n] fun r ↦ r ^ n) = ↑n !
this : (Δ_[1] fun r ↦ r ^ (n + 1)) = ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i
⊢ ∑ k ∈ range (n + 1), Δ_[1]^[n] ((n + 1).choose k • fun r ↦ r ^ k) = ↑(n + 1)!
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ Δ_[1]^[P.natDegree] (fun x ↦ (∑ c ∈ range (P.natDegree + 1), fun x ↦ P.coeff c * x ^ c) x) x =
    (P.leadingCoeff • ↑P.natDegree !) x

Tactic:
fwdDiff_iter_finsetSum,

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ (∑ k ∈ range (P.natDegree + 1), Δ_[1]^[P.natDegree] fun x ↦ P.coeff k * x ^ k) x = (P.leadingCoeff • ↑P.natDegree !) x
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
P : ℕ → R
⊢ (Δ_[1]^[n] fun r ↦ (∑ c ∈ range n, fun x ↦ P c * x ^ c) r) = 0

Tactic:
fwdDiff_iter_finsetSum,

Goal state after:
R : Type u_3
inst✝ : CommRing R
n : ℕ
P : ℕ → R
⊢ (∑ k ∈ range n, Δ_[1]^[n] fun x ↦ P k * x ^ k) = 0
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 ↔ ∃ m ∈ s, x ∣ m

Tactic:
dvd_def,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x : M
⊢ x ∈ s.saturation ↔ ∃ m ∈ s, ∃ c, m = x * c
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁶ : GroupWithZero M₀
inst✝⁵ : MulZeroOneClass N₀
inst✝⁴ : Nontrivial N₀
inst✝³ : NoZeroDivisors N₀
inst✝² : MulZeroOneClass G₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
f : M₀ →*₀ N₀
x : M₀
⊢ 1 (f x) = 1 x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inl
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁶ : GroupWithZero M₀
inst✝⁵ : MulZeroOneClass N₀
inst✝⁴ : Nontrivial N₀
inst✝³ : NoZeroDivisors N₀
inst✝² : MulZeroOneClass G₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
f : M₀ →*₀ N₀
⊢ 1 (f 0) = 1 0

case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁶ : GroupWithZero M₀
inst✝⁵ : MulZeroOneClass N₀
inst✝⁴ : Nontrivial N₀
inst✝³ : NoZeroDivisors N₀
inst✝² : MulZeroOneClass G₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
f : M₀ →*₀ N₀
x : M₀
hx : x ≠ 0
⊢ 1 (f x) = 1 x
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case h₁
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ ↑f.valueMonoid ∪ (↑f.valueMonoid)⁻¹ ⊆ ↑f.valueMonoid

Tactic:
simp only [union_subset_iff, subset_refl, true_and]
    intro _ ⟨y, hy⟩
    use y⁻¹
    simp [hy]

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

Goal state before:
pp: case none
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
⊢ none = 0 ∨ ∃ r s, ∃ (hr : f r ≠ 0) (hs : f s ≠ 0), none = ↑(valueGroup.mk f r s hr hs)

pp: case some
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
x : Bˣ
hx : x ∈ f.valueGroup
⊢ some ⟨x, hx⟩ = 0 ∨ ∃ r s, ∃ (hr : f r ≠ 0) (hs : f s ≠ 0), some ⟨x, hx⟩ = ↑(valueGroup.mk f r s hr hs)

Tactic:
· left; rfl

Goal state after:
case some
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
x : Bˣ
hx : x ∈ f.valueGroup
⊢ some ⟨x, hx⟩ = 0 ∨ ∃ r s, ∃ (hr : f r ≠ 0) (hs : f s ≠ 0), some ⟨x, hx⟩ = ↑(valueGroup.mk f r s hr hs)
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
  match i with
  | 0 => exact h0 ▸ rfl
  | 1 => exact h1 ▸ rfl

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
P✝ Q✝ : Karoubi (J ⥤ C)
f✝ : P✝ ⟶ Q✝
X : J
P Q : Karoubi (J ⥤ C)
f : (karoubiFunctorCategoryEmbedding J C).obj P ⟶ (karoubiFunctorCategoryEmbedding J C).obj Q
j j' : J
φ : j ⟶ j'
h : (P.p.app j ≫ P.X.map φ) ≫ (f.app j').f = (f.app j).f ≫ Q.p.app j ≫ Q.X.map φ
⊢ P.X.map φ ≫ (f.app j').f = P.p.app j ≫ P.X.map φ ≫ (f.app j').f

Tactic:
rw [← P.p.naturality_assoc]

Goal state after:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
P✝ Q✝ : Karoubi (J ⥤ C)
f✝ : P✝ ⟶ Q✝
X : J
P Q : Karoubi (J ⥤ C)
f : (karoubiFunctorCategoryEmbedding J C).obj P ⟶ (karoubiFunctorCategoryEmbedding J C).obj Q
j j' : J
φ : j ⟶ j'
h : (P.p.app j ≫ P.X.map φ) ≫ (f.app j').f = (f.app j).f ≫ Q.p.app j ≫ Q.X.map φ
⊢ P.X.map φ ≫ (f.app j').f = P.X.map φ ≫ P.p.app j' ≫ (f.app j').f
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case cast.succ.inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)

Tactic:
simp_rw [Fin.predAbove_of_castSucc_lt i.castSucc _ (Fin.castSucc_lt_castSucc_iff.mpr
        (Fin.castSucc_lt_succ_iff.mpr h)), ← Fin.succ_castSucc, Fin.pred_succ,
        Fin.succ_predAbove_succ]

Goal state after:
case cast.succ.inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ j.predAbove k.castSucc = i.predAbove (j.predAbove k.castSucc).succ
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ i.castSucc).op = 𝟙 (X _⦋n⦌)

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_self, op_id, X.map_id]

Goal state after:
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

Goal state after:
case zero
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
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 =
    (match 0 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 0 with
        | 0 => ⊤
        | n.succ => Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow

case succ
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
n✝ : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 =
    (match n✝ + 1 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 n✝ + 1 with
        | 0 => ⊤
        | n.succ => Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: X : NonemptyFinLinOrd
aux : Fintype.card ↑X.toLinOrd = Fintype.card ↑X.toLinOrd - 1 + 1
f : Fin (Fintype.card ↑X.toLinOrd - 1 + 1) ≃o ↑X.toLinOrd := monoEquivOfFin (↑X.toLinOrd) aux
hf : StrictMono ⇑(Finset.univ.orderEmbOfFin aux)
⊢ InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f.symm, monotone' := ?m.113 }) ≫
      InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f, monotone' := ⋯ }) =
    𝟙 X

Tactic:
by ext; apply f.apply_symm_apply

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

Goal state before:
pp: X : NonemptyFinLinOrd
aux : Fintype.card ↑X.toLinOrd = Fintype.card ↑X.toLinOrd - 1 + 1
f : Fin (Fintype.card ↑X.toLinOrd - 1 + 1) ≃o ↑X.toLinOrd := monoEquivOfFin (↑X.toLinOrd) aux
hf : StrictMono ⇑(Finset.univ.orderEmbOfFin aux)
i j : ↑X.1
h : i ≤ j
⊢ f.symm i ≤ f.symm j

Tactic:
rw [← hf.le_iff_le]

Goal state after:
X : NonemptyFinLinOrd
aux : Fintype.card ↑X.toLinOrd = Fintype.card ↑X.toLinOrd - 1 + 1
f : Fin (Fintype.card ↑X.toLinOrd - 1 + 1) ≃o ↑X.toLinOrd := monoEquivOfFin (↑X.toLinOrd) aux
hf : StrictMono ⇑(Finset.univ.orderEmbOfFin aux)
i j : ↑X.1
h : i ≤ j
⊢ (Finset.univ.orderEmbOfFin aux) (f.symm i) ≤ (Finset.univ.orderEmbOfFin aux) (f.symm j)
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case h₁
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
A : X ⟶ F.augmentedCechNerve
x : SimplexCategoryᵒᵖ
⊢ (equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).left.app x = A.left.app x

pp: case h₂
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
A : X ⟶ F.augmentedCechNerve
⊢ (equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).right = A.right

Tactic:
· refine WidePullback.hom_ext _ _ _ (fun j => ?_) ?_
      · simp
      · simpa using congr_app A.w.symm x

Goal state after:
case h₂
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
A : X ⟶ F.augmentedCechNerve
⊢ (equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).right = A.right
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f
x : X _⦋m⦌
⊢ ofSimplex ((ConcreteCategory.hom (X.map f.op)) x) = ofSimplex x

Tactic:
by
  refine le_antisymm (ofSimplex_map_le f x) ?_
  simp only [Subfunctor.ofSection_le_iff]
  have := isSplitEpi_of_epi f
  exact ⟨(section_ f).op, by simp [← Functor.map_comp_apply, ← op_comp]⟩

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝ : Epi f
⊢ range f = ⊤

Tactic:
by
  rwa [range_eq_top_iff]

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case id
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
i : WidePullbackShape ι
⊢ (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).map (WidePullbackShape.Hom.id i) ≫
      Option.casesOn i (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
        limit.π (Discrete.functor fun x ↦ X) { as := i }) =
    (Option.casesOn i (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
        limit.π (Discrete.functor fun x ↦ X) { as := i }) ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.id i)

Tactic:
cases i

Goal state after:
case id.none
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
⊢ (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).map (WidePullbackShape.Hom.id none) ≫
      Option.casesOn none (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
        limit.π (Discrete.functor fun x ↦ X) { as := i }) =
    (Option.casesOn none (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
        limit.π (Discrete.functor fun x ↦ X) { as := i }) ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.id none)

case id.some
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
val✝ : ι
⊢ (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).map (WidePullbackShape.Hom.id (some val✝)) ≫
      Option.casesOn (some val✝) (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none))
        fun i ↦ limit.π (Discrete.functor fun x ↦ X) { as := i }) =
    (Option.casesOn (some val✝) (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none))
        fun i ↦ limit.π (Discrete.functor fun x ↦ X) { as := i }) ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.id (some val✝))
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₂
this : IsIso (factorThruImage (g hf₁ f₂))
⊢ Mono (g hf₁ f₂)

Tactic:
rw [← image.fac (g hf₁ f₂)]

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 (factorThruImage (g hf₁ f₂) ≫ image.ι (g hf₁ f₂))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
B : Y.Subcomplex
inst✝ : IsIso f
⊢ B ≤ (B.preimage f).image f

Tactic:
· intro n y hy
    exact ⟨(inv f).app _ y, by simpa [← NatIso.isIso_inv_app, ← NatTrans.comp_app_apply]⟩

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

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x y : X.N
⊢ { toFun := fun x ↦ mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex) ⋯,
          invFun := fun y ↦ mk ((ConcreteCategory.hom (e.inv.app (Opposite.op ⦋y.dim⦌))) y.simplex) ⋯, left_inv := ⋯,
          right_inv := ⋯ }
        x ≤
      { toFun := fun x ↦ mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex) ⋯,
          invFun := fun y ↦ mk ((ConcreteCategory.hom (e.inv.app (Opposite.op ⦋y.dim⦌))) y.simplex) ⋯, left_inv := ⋯,
          right_inv := ⋯ }
        y ↔
    x ≤ y

Tactic:
dsimp
    simp only [le_iff, Subcomplex.ofSimplex_le_iff, Subcomplex.mem_ofSimplex_obj_iff]
    refine exists_congr (fun f ↦ ?_)
    dsimp at f ⊢
    rw [← NatTrans.naturality_apply e.hom f.op]
    exact (e.app _).toEquiv.apply_eq_iff_eq

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

Goal state before:
pp: case mpr.mk
X : SSet
A B : X.Subcomplex
h : ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (op ⦋n⦌) → ↑x ∈ B.obj (op ⦋n⦌)
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
a : A.toSSet _⦋m⦌
ha : ↑a ∈ X.nonDegenerate m
hx : ↑((ConcreteCategory.hom (↾fun x ↦ ⟨(ConcreteCategory.hom (X.map f.op)) ↑x, ⋯⟩)) a) ∈ A.obj (op ⦋n⦌)
⊢ ↑((ConcreteCategory.hom (↾fun x ↦ ⟨(ConcreteCategory.hom (X.map f.op)) ↑x, ⋯⟩)) a) ∈ B.obj (op ⦋n⦌)

Tactic:
exact B.map f.op (h _ ⟨_, ha⟩ a.prop)

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

Goal state before:
pp: X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
⊢ s ∈ Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i)) ↔ s.obj i.castSucc = s.obj i.succ

Tactic:
by
  constructor
  · rintro ⟨s, rfl⟩
    simp [-nerve_obj, nerve.σ_obj]
  · intro h
    refine ⟨(nerve X).δ i.castSucc s, ?_⟩
    ext j
    rw [nerve.σ_obj, nerve.δ_obj]
    by_cases h₁ : i.castSucc < j
    · obtain ⟨j, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h₁)
      rw [Fin.predAbove_of_castSucc_lt _ _ h₁, Fin.pred_succ,
        Fin.succAbove_of_le_castSucc _ _ (Fin.le_castSucc_iff.2 h₁)]
    · simp only [not_lt] at h₁
      grind [→ Fin.succAbove_of_castSucc_lt,
        → Fin.predAbove_of_le_castSucc, Fin.castSucc_castPred, Fin.castPred_castSucc,
        Fin.succAbove_castSucc_self, → LE.le.lt_or_eq]

Goal state after: