mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
⊢ M = 0 → ∀ (i j : n), M i j = 0

Tactic:
intro H; simp [H]

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
⊢ ∃ z, z * M * single p q x + z - 1 ∈ matrix n I

Tactic:
let N : Matrix n n R := 1 - ∑ i, single i q (if i = q then 1 - z else (M i p) * x * z)

Goal state after:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i, single i q (if i = q then 1 - z else M i p * x * z)
⊢ ∃ z, z * M * single p q x + z - 1 ∈ matrix n I
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
x y : R
i j : n
⊢ c.ofMatrix x y ↔ c (single i j x) (single i j y)

Tactic:
by
  refine ⟨fun h ↦ h i j, fun h i' j' ↦ ?_⟩
  simpa using c.mul (c.mul (c.refl <| single i' i 1) h) (c.refl <| single j j' 1)

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
f g : End R M
μ : R
k : ℕ∞
x : M
l : ℕ
hl : ↑l ≤ k
hx : ((f - μ • 1) ^ l) x = 0
h : Commute ((f - μ • 1) ^ l) g
⊢ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) (g x) = 0

Tactic:
use l, hl

Goal state after:
case right
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
x : M
l : ℕ
hl : ↑l ≤ k
hx : ((f - μ • 1) ^ l) x = 0
h : Commute ((f - μ • 1) ^ l) g
⊢ ((f - μ • 1) ^ l) (g x) = 0
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
⊢ (trace R M) (g ∘ₗ f) = 0

Tactic:
by
  have hfg : ∀ μ,
      MapsTo (g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ) :=
    fun μ ↦ (f.mapsTo_maxGenEigenspace_of_comm h_comm μ).comp
      (f.mapsTo_maxGenEigenspace_of_comm rfl μ)
  suffices ∀ μ, trace R _ ((g ∘ₗ f).restrict (hfg μ)) = 0 by
    classical
    have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
      f.independent_maxGenEigenspace hf
    have h_fin : {μ | f.maxGenEigenspace μ ≠ ⊥}.Finite :=
      WellFoundedGT.finite_ne_bot_of_iSupIndep f.independent_maxGenEigenspace
    simp [trace_eq_sum_trace_restrict' hds h_fin hfg, this]
  intro μ
  have hf' := f.mapsTo_maxGenEigenspace_of_comm (Commute.refl _) μ
  have hg' := f.mapsTo_maxGenEigenspace_of_comm h_comm μ
  replace h_comm : Commute (g.restrict (f.mapsTo_maxGenEigenspace_of_comm h_comm μ))
      (f.restrict (f.mapsTo_maxGenEigenspace_of_comm rfl μ)) :=
    restrict_commute h_comm.symm _ _
  have := f.isNilpotent_restrict_maxGenEigenspace_sub_algebraMap μ
  rw [restrict_comp hf' hg', trace_comp_eq_mul_of_commute_of_isNilpotent μ h_comm this,
    hg, mul_zero]

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
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
⊢ (↑fe).1 1 * (↑fe).2 = (↑fe).2

Tactic:
map_one,

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
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
⊢ 1 * (↑fe).2 = (↑fe).2
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case refine_2
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ ((f - μ₂ • 1) ^ l).ker
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
⊢ (g ^ l) (y + z) ∈ ↑(s.sup fun μ ↦ (f.genEigenspace μ) k)

Tactic:
· rw [SetLike.mem_coe, map_add, hl, zero_add]
      suffices (s.sup fun μ ↦ f.genEigenspace μ k).map (g ^ l) ≤
          s.sup fun μ ↦ f.genEigenspace μ k by exact this (Submodule.mem_map_of_mem hz)
      simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := R), Submodule.map_iSup (ι := _ ∈ s)]
      refine iSup₂_mono fun μ _ ↦ ?_
      rintro - ⟨u, hu, rfl⟩
      refine f.mapsTo_genEigenspace_of_comm ?_ μ k hu
      exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l

Goal state after:
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
P : Type u_4
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
⊢ (trace R P) ((g ∘ₗ f) ∘ₗ h) = (trace R M) ((h ∘ₗ g) ∘ₗ f)

Tactic:
rw [trace_comp_comm', ← comp_assoc]

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
f : End R M
μ ρ : R
⊢ (f + ρ • LinearMap.id).HasEigenvalue μ ↔ f.HasEigenvalue (μ - ρ)

Tactic:
by
  have aux : f + ρ • .id - μ • 1 = f - (μ - ρ) • 1 := by module
  simp only [hasEigenvalue_iff, eigenspace_def, aux]

Goal state after:
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
V₁ : Type u₁
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
V₂ : Type u₂
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
V₃ : Type u₃
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
V₄ : Type u₄
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
V₅ : Type u₅
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
W₀ : Type (max u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₀} V₀
W₁ : Type (max u₁ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₁} V₁
W₂ : Type (max u₂ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₂} V₂
W₃ : Type (max u₃ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₃} V₃
W₄ : Type (max u₄ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₄} V₄
W₅ : Type (max u₅ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₅} V₅
g₀ : W₀ →ₗ[k] W₁ := ↑ULift.moduleEquiv.symm ∘ₗ f₀ ∘ₗ ↑ULift.moduleEquiv
⊢ ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0

Tactic:
let g₁ : W₁ →ₗ[k] W₂ := ULift.moduleEquiv.symm.toLinearMap ∘ₗ f₁ ∘ₗ ULift.moduleEquiv.toLinearMap

Goal state after:
k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
V₁ : Type u₁
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
V₂ : Type u₂
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
V₃ : Type u₃
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
V₄ : Type u₄
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
V₅ : Type u₅
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
W₀ : Type (max u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₀} V₀
W₁ : Type (max u₁ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₁} V₁
W₂ : Type (max u₂ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₂} V₂
W₃ : Type (max u₃ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₃} V₃
W₄ : Type (max u₄ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₄} V₄
W₅ : Type (max u₅ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₅} V₅
g₀ : W₀ →ₗ[k] W₁ := ↑ULift.moduleEquiv.symm ∘ₗ f₀ ∘ₗ ↑ULift.moduleEquiv
g₁ : W₁ →ₗ[k] W₂ := ↑ULift.moduleEquiv.symm ∘ₗ f₁ ∘ₗ ↑ULift.moduleEquiv
⊢ ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0
Module: Mathlib.Algebra.Ring.MinimalAxioms

Goal state before:
pp: R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
mul_comm : ∀ (a b : R), a * b = b * a
one_mul : ∀ (a : R), 1 * a = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
a : R
⊢ a * 1 = a

Tactic:
rw [mul_comm, one_mul]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ toFreeSemigroup.comp (map f) = (FreeSemigroup.map f).comp toFreeSemigroup

Tactic:
ext1

Goal state after:
α : Type u
β : Type v
f : α → β
⊢ ⇑(toFreeSemigroup.comp (map f)) ∘ of = ⇑((FreeSemigroup.map f).comp toFreeSemigroup) ∘ of
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
⊢ (Magma.AssocQuotient.lift FreeMagma.toFreeSemigroup).comp
      (FreeSemigroup.lift (⇑Magma.AssocQuotient.of ∘ FreeMagma.of)) =
    MulHom.id (FreeSemigroup α)

Tactic:
ext1

Goal state after:
α : Type u
⊢ ⇑((Magma.AssocQuotient.lift FreeMagma.toFreeSemigroup).comp
          (FreeSemigroup.lift (⇑Magma.AssocQuotient.of ∘ FreeMagma.of))) ∘
      FreeSemigroup.of =
    ⇑(MulHom.id (FreeSemigroup α)) ∘ FreeSemigroup.of
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case refine_1
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
⊢ Function.Injective (⇑f ∘ ⇑(algebraMap R A))

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✝

pp: case refine_3
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
⊢ (∃ y, (algebraMap R A) y = x✝) → IsIntegral R x✝

Tactic:
· convert! inj
    aesop

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, (algebraMap R A) y = x✝

case refine_3
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
⊢ (∃ y, (algebraMap R A) y = x✝) → IsIntegral R x✝
Module: Mathlib.Algebra.GCDMonoid.IntegrallyClosed

Goal state before:
pp: case intro
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
a✝ : GCDMonoid R
x y : R
hg : IsUnit (gcd x y)
he : X * (algebraMap R (FractionRing R)) y = (algebraMap R (FractionRing R)) x
⊢ ∃ y, (algebraMap R (FractionRing R)) y = X

Tactic:
have :=
      Polynomial.dvd_pow_natDegree_of_eval₂_eq_zero (IsFractionRing.injective R <| FractionRing R)
        hp₁ y x _ hp₂ (by rw [mul_comm, he])

Goal state after:
case intro
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
a✝ : GCDMonoid R
x y : R
hg : IsUnit (gcd x y)
he : X * (algebraMap R (FractionRing R)) y = (algebraMap R (FractionRing R)) x
this : y ∣ x ^ p.natDegree
⊢ ∃ y, (algebraMap R (FractionRing R)) y = X
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
f : M → G
n : ℕ
y : M
this : fwdDiffₗ M G h = shiftₗ M G h - 1
⊢ (⇑(shiftₗ M G h - 1))^[n] f y = ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h)

Tactic:
← Module.End.pow_apply

Goal state after:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this : fwdDiffₗ M G h = shiftₗ M G h - 1
⊢ ((shiftₗ M G h - 1) ^ n) f y = ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h)
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ (h.inv (h.hom { down := a })).down = a

Tactic:
change ((h.hom ≫ h.inv) _).down = _

Goal state after:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ ((h.hom ≫ h.inv) { down := a }).down = a
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:
by
  rw [Equiv.eq_symm_apply, ← uSwitchEquiv_naturality f, Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 1)
x✝ : i ∈ Finset.univ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫
      f.app (op ⦋n✝ + 1⦌) ≫ Y.map (SimplexCategory.δ i.succ).op =
    0

Tactic:
← f.naturality,

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 1)
x✝ : i ∈ Finset.univ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.map (SimplexCategory.δ i.succ).op ≫ f.app (op ⦋n✝⦌) =
    0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.δ i.succ ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Tactic:
by
  dsimp [δ, σ]
  simp only [← X.map_comp, SimplexCategory.δ_comp_σ_succ, X.map_id]

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

Goal state before:
pp: i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (δ₀Iter (i + 1) h)) k) = ↑((ConcreteCategory.hom (δ 0 ≫ δ₀Iter i ⋯)) k)

Tactic:
dsimp% ConcreteCategory.comp_apply (δ 0) (δ₀Iter i),

Goal state after:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (δ₀Iter (i + 1) h)) k) =
    ↑((ConcreteCategory.hom (δ₀Iter i ⋯)) ((ConcreteCategory.hom (δ 0)) k))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (B✝.len + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
⊢ (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁ ≤
    (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂

Tactic:
by_contra h''
                  apply not_le.mpr h'
                  convert! f.toOrderHom.monotone (le_of_not_ge h'')
                  all_goals
                    exact (ConcreteCategory.congr_hom (Iso.inv_hom_id
                      (asIso ((forget SimplexCategory).map f))) _).symm

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : j ≤ ↑k
hk' : i ≤ k.castSucc
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) (i.succAbove k)) = ↑k - j

Tactic:
rw [Fin.succAbove_of_le_castSucc _ _ hk', σ₀Iter_coe_eq_of_ge ..]
      simp

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

Goal state before:
pp: X : SSet
inst✝ : X.Finite
n : ℕ
x y : ↑(X.nonDegenerate n)
h : (fun x ↦ N.mk ↑x ⋯) x = (fun x ↦ N.mk ↑x ⋯) y
⊢ x = y

Tactic:
rw [N.ext_iff, S.ext_iff'] at h

Goal state after:
X : SSet
inst✝ : X.Finite
n : ℕ
x y : ↑(X.nonDegenerate n)
h :
  ∃ (h : ((fun x ↦ N.mk ↑x ⋯) x).dim = ((fun x ↦ N.mk ↑x ⋯) y).dim),
    (((fun x ↦ N.mk ↑x ⋯) x).cast h).simplex = ((fun x ↦ N.mk ↑x ⋯) y).simplex
⊢ x = y
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
x✝¹ : SimplexCategoryᵒᵖ
x : Δ[n].obj x✝¹
x✝ : x ∈ ⊤.obj x✝¹
⊢ x ∈ (Subcomplex.ofSimplex (objEquiv.symm (𝟙 ⦋n⦌))).obj x✝¹

Tactic:
obtain ⟨f, rfl⟩ := objEquiv.symm.surjective x

Goal state after:
n : ℕ
x✝¹ : SimplexCategoryᵒᵖ
f : unop x✝¹ ⟶ ⦋n⦌
x✝ : objEquiv.symm f ∈ ⊤.obj x✝¹
⊢ objEquiv.symm f ∈ (Subcomplex.ofSimplex (objEquiv.symm (𝟙 ⦋n⦌))).obj x✝¹
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case refine_1
n : ℕ
x : Δ[n] _⦋n⦌
h : x ∈ Δ[n].nonDegenerate n
⊢ x = objEquiv.symm (𝟙 ⦋n⦌)

Tactic:
obtain ⟨f, rfl⟩ := objEquiv.symm.surjective x

Goal state after:
case refine_1
n : ℕ
f : unop (op ⦋n⦌) ⟶ ⦋n⦌
h : objEquiv.symm f ∈ Δ[n].nonDegenerate n
⊢ objEquiv.symm f = objEquiv.symm (𝟙 ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case refine_1
n : ℕ
x : Δ[n] _⦋n⦌
h : x ∈ Δ[n].nonDegenerate n
⊢ x = objEquiv.symm (𝟙 ⦋n⦌)

pp: case refine_2
n : ℕ
x : Δ[n] _⦋n⦌
⊢ x = objEquiv.symm (𝟙 ⦋n⦌) → x ∈ Δ[n].nonDegenerate n

Tactic:
· obtain ⟨f, rfl⟩ := objEquiv.symm.surjective x
    have : Mono f := by simpa using (mem_nonDegenerate_iff_mono _).mp h
    simpa only [EmbeddingLike.apply_eq_iff_eq] using SimplexCategory.eq_id_of_mono f

Goal state after:
case refine_2
n : ℕ
x : Δ[n] _⦋n⦌
⊢ x = objEquiv.symm (𝟙 ⦋n⦌) → x ∈ Δ[n].nonDegenerate n
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₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ : I₁
i✝ j✝ k✝ : I₂
a✝¹ : c₂.Rel i✝ j✝
a✝ : c₂.Rel j✝ k✝
⊢ d₂ i₁ i✝ j✝ ≫ d₂ i₁ j✝ k✝ = 0

Tactic:
apply d₂_comp_d₂

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₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ i₁' i₁'' : I₁
x✝¹ : c₁.Rel i₁ i₁'
x✝ : c₁.Rel i₁' i₁''
⊢ { f := fun i₂ ↦ d₁ i₁ i₁' i₂, comm' := ⋯ } ≫ { f := fun i₂ ↦ d₁ i₁' i₁'' i₂, comm' := ⋯ } = 0

Tactic:
ext i₂; apply d₁_comp_d₁

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1 + 1)
⊢ (ExtraDegeneracy.s f S (n + 1) ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.succAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) j =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S n) ≫
      WidePullback.π (fun x ↦ f.hom) j

Tactic:
induction j using Fin.cases

Goal state after:
case a.zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
⊢ (ExtraDegeneracy.s f S (n + 1) ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.succAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) 0 =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S n) ≫
      WidePullback.π (fun x ↦ f.hom) 0

case a.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
i✝ : Fin (n + 1)
⊢ (ExtraDegeneracy.s f S (n + 1) ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.succAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) i✝.succ =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S n) ≫
      WidePullback.π (fun x ↦ f.hom) i✝.succ