mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inl.inr.refine_1
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
⊢ i.castSucc < min x hd

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin (d + 1)
hi : min x hd < i
⊢ (min x hd).castSucc < i.castSucc

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin (d + 1)
hi : min x hd < i
⊢ (min x hd).castSucc < i.succ

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin (d + 1)
hi : min x hd < i
⊢ i.castSucc.pred ⋯ < i.succ.pred ⋯

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
y : Fin (d + 1)
hy : (x.cast hd).simplex.1 (l.castSucc.succAbove y) = k.succ
this : y < l
⊢ y.castSucc < l.castSucc

Tactic:
grind

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

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ zero) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y zero))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) zero x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) zero x)
      zero (𝟙 zero) =
    𝟙 (WalkingIso.rec X Y zero)

Tactic:
rfl

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

Goal state before:
pp: case one
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ one) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y one))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) one x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) one x)
      one (𝟙 one) =
    𝟙 (WalkingIso.rec X Y one)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
d✝ : ℕ
⊢ ∀ (hd_1 : hl.δ.dim = d✝) (l_1 : Fin (d✝ + 1)), ¬IsIndex hl.δ hd_1 l_1

Tactic:
rfl

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
⊢ ∀ (l_1 : Fin (hl.δ.dim + 1)), ¬IsIndex hl.δ ⋯ l_1
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
hi : i < l.castSucc
⊢ l ≠ 0

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
l : Fin u.dim
hl : IsIndex x hd l.succ.succ
hi : i < l.succ.castSucc
⊢ i < l.succ.succ

Tactic:
grind

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

Goal state before:
pp: case false
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).obj { as := { down := false } } =
    F.obj { as := { down := false } }

Tactic:
rfl

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

Goal state before:
pp: case true
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).obj { as := { down := true } } =
    F.obj { as := { down := true } }

Tactic:
rfl

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

Goal state before:
pp: case zero.one
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : zero ⟶ one
⊢ F.map iso.hom = F.map f

Tactic:
rfl

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

Goal state before:
pp: case one.zero
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : one ⟶ zero
⊢ F.map iso.inv = F.map f

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
hi✝ : l.castSucc < i
hi : l.succ < i
⊢ l ≠ Fin.last u.dim

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
l : Fin u.dim
hl : IsIndex x hd l.castSucc.succ
hi✝ : l.castSucc.castSucc < i
hi : l.castSucc.succ < i
⊢ l.castSucc.castSucc < i

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
l : Fin u.dim
hl : IsIndex x hd l.castSucc.succ
hi✝ : l.castSucc.castSucc < i
hi : l.castSucc.succ < i
⊢ l.succ.castSucc < i

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case pos.fst
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
⊢ (s.x.cast ⋯).simplex.1 s.index.castSucc = (s.x.cast ⋯).simplex.1 s.index.castSucc

Tactic:
rfl

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h✝¹ : j₁.castSucc < i
h✝ : j₂.castSucc < i
⊢ 0 ≤ 0

Tactic:
grind

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h✝¹ : j₁.castSucc < i
h✝ : ¬j₂.castSucc < i
⊢ 0 ≤ 1

Tactic:
grind

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h✝¹ : ¬j₁.castSucc < i
h✝ : j₂.castSucc < i
⊢ 1 ≤ 0

Tactic:
grind

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h✝¹ : ¬j₁.castSucc < i
h✝ : ¬j₂.castSucc < i
⊢ 1 ≤ 1

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
this : Ss.card = Sδ.card ∧ St.card = Sδ.card + 1
⊢ (finset { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs }.x ⋯).card <
    (finset { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }.x ⋯).card

Tactic:
grind

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

Goal state before:
pp: case pos
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : j ≤ i.castSucc
⊢ ↑((stdSimplex.objEquiv.symm (SimplexCategory.σ i)) j) + ↑((objMk₁ i.castSucc.succ) j) = ↑j

Tactic:
rw [objMk₁_of_castSucc_lt _ _ (by simpa),
          Fin.coe_ofNat_eq_mod, Nat.zero_mod, add_zero]

Goal state after:
case pos
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : j ≤ i.castSucc
⊢ ↑((stdSimplex.objEquiv.symm (SimplexCategory.σ i)) j) = ↑j
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
k : Fin (n + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n] 0)) (stdSimplex.objEquiv.symm (SimplexCategory.σ 0)))).op))
            x,
          stdSimplex.objMk₁ (Fin.pred 1 ⋯)).2
      k =
    ((ConcreteCategory.hom (ι₁.app (op ⦋n⦌))) x).2 k

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n⦌
⊢ X.ιChainComplex x ≫ (X.toNormalizedChainComplex R).f n = X.ιNormalizedChainComplex x

Tactic:
rfl

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

Goal state before:
pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ i.succ)))).op))
            x,
          stdSimplex.objMk₁ (i.castSucc.succ.succ.pred ⋯)).2
      k =
    ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ i.castSucc)))).op))
            x,
          stdSimplex.objMk₁ (i.castSucc.castSucc.succ.castPred ⋯)).2
      k

Tactic:
rfl

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

Goal state before:
pp: case fst
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
x : X _⦋n + 1⦌
⊢ (ConcreteCategory.hom (X.map (SimplexCategory.σ j).op)) ((ConcreteCategory.hom (X.map (SimplexCategory.δ i).op)) x) =
    (ConcreteCategory.hom (X.map (SimplexCategory.σ j).op)) ((ConcreteCategory.hom (δ X i)) x)

Tactic:
rfl

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

Goal state before:
pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ j.castSucc)))).op))
            x,
          stdSimplex.objMk₁ (j.castSucc.castSucc.succ.castPred ⋯)).2
      k =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (δ X i)) x)).app (op ⦋n + 1⦌)))
            (stdSimplex.objEquiv.symm (SimplexCategory.σ j)),
          stdSimplex.objMk₁ j.castSucc.succ).2
      k

Tactic:
rfl

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

Goal state before:
pp: case fst
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (X.map (SimplexCategory.σ j.succ).op))
      ((ConcreteCategory.hom (X.map (SimplexCategory.σ i).op)) x) =
    (ConcreteCategory.hom (X.map (SimplexCategory.σ j.succ).op)) ((ConcreteCategory.hom (σ X i)) x)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
⊢ ¬k.castSucc = Fin.last (m + 1)

Tactic:
grind

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

Goal state before:
pp: case fst
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (X.map (SimplexCategory.σ j.castSucc).op))
      ((ConcreteCategory.hom (X.map (SimplexCategory.σ i).op)) x) =
    (ConcreteCategory.hom (X.map (SimplexCategory.σ j.castSucc).op)) ((ConcreteCategory.hom (σ X i)) x)

Tactic:
rfl

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

Goal state before:
pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
x : X _⦋n⦌
k : Fin (n + 1 + 1 + 1)
⊢ ((ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n + 1 + 1⦌)))
            ((ConcreteCategory.hom (σ Δ[n] i.succ)) (stdSimplex.objEquiv.symm (SimplexCategory.σ j))),
          stdSimplex.objMk₁ j.castSucc.succ.castSucc).2
      k =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (σ X i)) x)).app (op ⦋n + 1 + 1⦌)))
            (stdSimplex.objEquiv.symm (SimplexCategory.σ j.castSucc)),
          stdSimplex.objMk₁ j.castSucc.castSucc.succ).2
      k

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
j : Fin (n + 2)
i : Fin n
hj : j < i.succ.castSucc
⊢ j ≠ Fin.last (n + 1)

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
x : X _⦋0⦌
n : ℕ
f : X.PtSimplex (n + 1) x
i : Fin (n + 1)
j : Fin (n + 1 + 1)
hj : j.castSucc < i.succ.castSucc
⊢ j ≤ i.castSucc

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin (n + 1)
j : Fin (n + 2)
hj : i.succ < j
⊢ i ≠ Fin.last n

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
x : X _⦋0⦌
n : ℕ
f : X.PtSimplex (n + 1) x
i : Fin (n + 1)
j : Fin (n + 1 + 1)
hj : i.castSucc.succ < j.succ
⊢ i.castSucc < j

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : k < j.castSucc.castSucc
⊢ i.succ.succ < k.rev

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : j.succ.succ < k
⊢ k.rev < i.castSucc.castSucc

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : g.op.MulStruct f.op fg.op i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : k < j.castSucc.castSucc
⊢ i.succ.succ < k.rev

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : g.op.MulStruct f.op fg.op i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : j.succ.succ < k
⊢ k.rev < i.castSucc.castSucc

Tactic:
grind

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

Goal state before:
pp: X : TopCat
x✝ : C(↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))), ↑X)
⊢ ((fun x ↦ { toFun := fun x_1 ↦ x, continuous_toFun := ⋯ }) ((fun f ↦ f.toFun default) x✝)) default = x✝ default

Tactic:
rfl

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

Goal state before:
pp: X : TopCat
f : SSet.toTop.obj Δ[0] ⟶ X
this : sSetTopAdj.unit.app Δ[0] = SSet.const (TopCat.toSSetObj₀Equiv.symm default)
⊢ SSet.const (TopCat.toSSetObj₀Equiv.symm default) ≫ TopCat.toSSet.map f =
    SSet.const
      ((X.toSSetObjEquiv (op ⦋0⦌)).symm { toFun := fun x ↦ (ConcreteCategory.hom f) default, continuous_toFun := ⋯ })

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
R : C
⊢ Sigma.ι (fun x ↦ R)
      ((ConcreteCategory.hom ((TopCat.toSSet.map (toTopSimplex.hom.app ⦋n⦌)).app (Opposite.op ⦋n⦌)))
        ((ConcreteCategory.hom ((sSetTopAdj.unit.app Δ[n]).app (Opposite.op ⦋n⦌)))
          (stdSimplex.objEquiv.symm (𝟙 ⦋n⦌)))) =
    Sigma.ι (fun x ↦ R)
      ((ConcreteCategory.hom
          ((sSetTopAdj.unit.app Δ[n]).app (Opposite.op ⦋n⦌) ≫
            (TopCat.toSSet.map (toTopSimplex.hom.app ⦋n⦌)).app (Opposite.op ⦋n⦌)))
        (stdSimplex.objEquiv.symm (𝟙 ⦋n⦌)))

Tactic:
rfl

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

Goal state before:
pp: case e_6
⊢ stdSimplex.vertex ((ConcreteCategory.hom (SimplexCategory.δ 1)) 0) = ⟨Pi.single 0 1, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: case e_6
⊢ stdSimplex.vertex ((ConcreteCategory.hom (SimplexCategory.δ 0)) 0) = ⟨Pi.single 1 1, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: case inr
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
⊢ JoinedIn sᶜ a b

Tactic:
let x := (2 : ℝ)⁻¹ • (b - a)

Goal state after:
case inr
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
⊢ JoinedIn sᶜ a b
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι✝ : Type u_3
inst✝ : Finite ι✝
v✝ : ι✝ → AbsoluteValue R S
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc : card ι ≠ 2
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) a ∧
    ∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) a < 1
b : R
hb :
  1 < (restrict (fun k ↦ k = i ∨ k = j) v ⟨i, ⋯⟩) b ∧
    ∀ (j_1 : { k // k = i ∨ k = j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k = i ∨ k = j) v j_1) b < 1
ha₁ : (v j) a = 1
⊢ ⟨j, ⋯⟩ ≠ ⟨i, ⋯⟩

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι✝ : Type u_3
inst✝ : Finite ι✝
v✝ : ι✝ → AbsoluteValue R S
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h✝ : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc✝ : card ι ≠ 2
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) a ∧
    ∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) a < 1
b : R
hb :
  1 < (restrict (fun k ↦ k = i ∨ k = j) v ⟨i, ⋯⟩) b ∧
    ∀ (j_1 : { k // k = i ∨ k = j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k = i ∨ k = j) v j_1) b < 1
ha₁ : (v j) a = 1
c : R
hc :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) c ∧
    (∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) c < 1) ∧ (v j) c < 1
k : ι
hk : k ≠ i
h : k ≠ j
⊢ ⟨k, h⟩ ≠ ⟨i, ⋯⟩

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι✝ : Type u_3
inst✝ : Finite ι✝
v✝ : ι✝ → AbsoluteValue R S
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h✝ : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc : card ι ≠ 2
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) a ∧
    ∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) a < 1
b : R
hb :
  1 < (restrict (fun k ↦ k = i ∨ k = j) v ⟨i, ⋯⟩) b ∧
    ∀ (j_1 : { k // k = i ∨ k = j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k = i ∨ k = j) v j_1) b < 1
ha₁ : (v j) a ≠ 1
ha_lt : (v j) a < 1
k : ι
hk : k ≠ i
h : k ≠ j
⊢ ⟨k, h⟩ ≠ ⟨i, ⋯⟩

Tactic:
grind

Goal state after: