mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv

Goal state before:
pp: K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →ₗ[K] W := applyₗ z ∘ₗ f.toLinearMap ∘ₗ smulRightₗ v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
this : ∀ (A : End K V) (x : V), T (A x) = (f A) (T x)
surj : Function.Surjective ⇑T
x y : V
hxy : T x = T y
h_smul : (smulRightₗ v) x = (smulRightₗ v) y
⊢ x = y

Tactic:
simpa [huv.isUnit.smul_left_cancel] using congr((fun f ↦ f u) $h_smul)

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✝ : IsNoetherian R M
f : End R M
μ : R
⊢ (f.genEigenspace μ) ⊤ = (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)

Tactic:
have := WellFoundedGT.iSup_eq_monotonicSequenceLimit <|
    (f.genEigenspace μ).comp <| WithTop.coeOrderHom.toOrderHom
  convert! this using 1
  simp only [genEigenspace, OrderHom.coe_mk, le_top, iSup_pos, OrderHom.comp_coe,
    Function.comp_def]
  rw [iSup_prod', iSup_subtype', ← sSup_range, ← sSup_range]
  congr 1
  aesop

Goal state after:
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Free R ↥(N i)
s : Finset ι
h : iSupIndep fun i ↦ N ↑i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo ⇑f ↑p ↑p
⊢ (trace R ↥p) (restrict f hp') = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)

Tactic:
let N' : s → Submodule R p := fun i ↦ (N i).comap p.subtype
  replace h : IsInternal N' := hp ▸ isInternal_biSup_submodule_of_iSupIndep (s : Set ι) h
  have hf' : ∀ i, MapsTo (restrict f hp') (N' i) (N' i) := fun i x hx' ↦ by simpa using! hf i hx'
  let e : (i : s) → N' i ≃ₗ[R] N i := fun ⟨i, hi⟩ ↦ (N i).comapSubtypeEquivOfLe (hp ▸ le_biSup N hi)
  have _i1 : ∀ i, Module.Finite R (N' i) := fun i ↦ Module.Finite.equiv (e i).symm
  have _i2 : ∀ i, Module.Free R (N' i) := fun i ↦ Module.Free.of_equiv (e i).symm
  rw [trace_eq_sum_trace_restrict h hf', ← s.sum_coe_sort]
  have : ∀ i : s, f.restrict (hf i) = (e i).conj ((f.restrict hp').restrict (hf' i)) := fun _ ↦ rfl
  simp [this]

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 1 * (↑fg).1 a = (↑fg).1 a * (↑fg).2 1

Tactic:
rw [← fg.prop.2.1, ← fg.prop.2.2, smul_eq_mul, op_smul_eq_mul, mul_one, one_mul]

Goal state after:
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
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) }
a : A
⊢ (lift fe) (inl a) = (↑fe).1 a

Tactic:
lift_apply_apply,

Goal state after:
R : Type u_1
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) }
a : A
⊢ (↑fe).1 (inl a).fst + (↑fe).1 (inl a).snd * (↑fe).2 = (↑fe).1 a
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α × Bool
⊢ reduce (List.replicate n x) = List.replicate n x

Tactic:
induction n with
  | zero => simp [reduce]
  | succ n ih =>
    rw [List.replicate_succ, reduce.cons, ih]
    cases n with
    | zero => simp
    | succ n => simp [List.replicate_succ]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ : Type u
x✝ x y : FreeMagma α✝
ih1 : traverse pure x = pure x
ih2 : traverse pure y = pure y
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure x <*> traverse pure y = pure (x * y)

Tactic:
ih2,

Goal state after:
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ : Type u
x✝ x y : FreeMagma α✝
ih1 : traverse pure x = pure x
ih2 : traverse pure y = pure y
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure x <*> pure y = pure (x * y)
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> Functor.Comp.mk (traverse f <$> traverse g x) <*>
      traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y =
    Functor.Comp.mk (traverse f <$> traverse g (x * y))

Tactic:
ih2,

Goal state after:
α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> Functor.Comp.mk (traverse f <$> traverse g x) <*>
      Functor.Comp.mk (traverse f <$> traverse g y) =
    Functor.Comp.mk (traverse f <$> traverse g (x * y))
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (pure ∘ f) x = pure (f <$> x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure (f <$> x) <*> traverse (pure ∘ f) y = pure (f <$> (x * y))

Tactic:
ih2,

Goal state after:
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (pure ∘ f) x = pure (f <$> x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure (f <$> x) <*> pure (f <$> y) = pure (f <$> (x * y))
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ : Type u
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse pure (of x) = pure (of x)
ih2 : traverse pure y = pure y
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure (of x) <*> traverse pure y = pure (of x * y)

Tactic:
ih2,

Goal state after:
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ : Type u
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse pure (of x) = pure (of x)
ih2 : traverse pure y = pure y
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure (of x) <*> pure y = pure (of x * y)
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x) = Functor.Comp.mk (traverse f <$> traverse g (pure x))
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> Functor.Comp.mk (traverse f <$> traverse g (pure x)) <*>
      traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y =
    Functor.Comp.mk (traverse f <$> traverse g (pure x * y))

Tactic:
ih2,

Goal state after:
α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x) = Functor.Comp.mk (traverse f <$> traverse g (pure x))
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> Functor.Comp.mk (traverse f <$> traverse g (pure x)) <*>
      Functor.Comp.mk (traverse f <$> traverse g y) =
    Functor.Comp.mk (traverse f <$> traverse g (pure x * y))
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (pure ∘ f) (of x) = pure (f <$> of x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure (f <$> of x) <*> traverse (pure ∘ f) y = pure (f <$> (of x * y))

Tactic:
ih2,

Goal state after:
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (pure ∘ f) (of x) = pure (f <$> of x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure (f <$> of x) <*> pure (f <$> y) = pure (f <$> (of x * y))
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝² : CommRing R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ { toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x =
    x * { toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s

Tactic:
by ext <;> simp [Algebra.commutes]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ (C g.leadingCoeff * q ^ m + r) * (C h.leadingCoeff * q ^ n + s) %ₘ q = r * s %ₘ q

Tactic:
simp only [add_mul, mul_add, map_add, ← modByMonicHom_apply]

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ q.modByMonicHom (C g.leadingCoeff * q ^ m * (C h.leadingCoeff * q ^ n)) +
        q.modByMonicHom (r * (C h.leadingCoeff * q ^ n)) +
      (q.modByMonicHom (C g.leadingCoeff * q ^ m * s) + q.modByMonicHom (r * s)) =
    q.modByMonicHom (r * s)
Module: Mathlib.Algebra.Group.Action.Sum

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a✝ : M
b✝ : α
c : β
x✝ : α ⊕ β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
a : M
b : N
x : α ⊕ β
⊢ (a • b) • x = a • b • x

Tactic:
by
    cases x
    exacts [congr_arg inl (smul_assoc _ _ _), congr_arg inr (smul_assoc _ _ _)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case hfmodP
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ map (algebraMap R (FractionRing (R ⧸ P))) f =
    C ((algebraMap R (FractionRing (R ⧸ P))) f.leadingCoeff) * map (algebraMap R (FractionRing (R ⧸ P))) X ^ f.natDegree

Tactic:
← map_C,

Goal state after:
case hfmodP
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ map (algebraMap R (FractionRing (R ⧸ P))) f =
    map (algebraMap R (FractionRing (R ⧸ P))) (C f.leadingCoeff) *
      map (algebraMap R (FractionRing (R ⧸ P))) X ^ f.natDegree
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
⊢ (Δ_[1]^[P.natDegree + 1] fun x ↦ eval x P) = 0

Tactic:
have hP : P.natDegree < P.natDegree + 1 := Nat.lt_succ_self P.natDegree

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
hP : P.natDegree < P.natDegree + 1
⊢ (Δ_[1]^[P.natDegree + 1] fun x ↦ eval x P) = 0
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: case h.h_add
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℤ
hx : (v.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
w : ι →₀ ℤ
hy : (w.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∀ a ∈ v.support ∪ w.support, ∀ (b₁ b₂ : ℤ), f a ^ (b₁ + b₂) = f a ^ b₁ * f a ^ b₂

Tactic:
simp [zpow_add]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
a : α
inst✝ : Fintype β
ha : a ≠ 0
⊢ ↑(a • univ) = ↑univ

Tactic:
by push_cast; exact Set.smul_set_univ₀ ha

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₀
inst✝ : DecidablePred fun x ↦ x = 0
x : G₀
hx : x ≠ 0
⊢ (snd G₀ H₀) ((inl G₀ H₀) x) = 1

Tactic:
by
  rw [← comp_apply, snd_comp_inl, one_apply_of_ne_zero hx]

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₀
inst✝ : DecidablePred fun x ↦ x = 0
x : H₀
hx : x ≠ 0
⊢ (fst G₀ H₀) ((inr G₀ H₀) x) = 1

Tactic:
by
  rw [← comp_apply, fst_comp_inr, one_apply_of_ne_zero hx]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : MulZeroOneClass G
inst✝¹ : MulZeroOneClass H
inst✝ : Nontrivial H
f : G →*₀ H
⊢ 1 ≠ 0

Tactic:
simp [Subtype.ext_iff]

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

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

Tactic:
obtain ⟨y', hy'⟩ := hb'

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : MonoidWithZero B
f : A →*₀ B
a✝ b✝ : Bˣ
y : A
hy : f y = ↑a✝
y' : A
hy' : f y' = ↑b✝
⊢ a✝ * b✝ ∈ Units.val ⁻¹' range ⇑f
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

Tactic:
intro _ ⟨y, hy⟩

Goal state after:
case h₁
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
a✝ : Bˣ
y : A
hy : f y = ↑a✝⁻¹
⊢ a✝ ∈ ↑f.valueMonoid
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : SimplexCategory
f : ⦋0⦌ ⟶ n
x : Fin (⦋0⦌.len + 1)
⊢ ↑((Hom.toOrderHom f) x) = ↑((Hom.toOrderHom (⦋0⦌.const n ((Hom.toOrderHom f) 0))) x)

Tactic:
match x with | 0 => rfl

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

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
⊢ diag l ≫ subinterval j l hjl = intervalEdge j l hjl

Tactic:
unfold subinterval intervalEdge diag mkOfLe
  ext (i : Fin 2)
  match i with | 0 | 1 => simp <;> lia

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

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
⊢ j.succ.predAbove k.succ = i.succAbove (j.predAbove k)

Tactic:
Fin.succ_predAbove_succ,

Goal state after:
case inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
⊢ (j.predAbove k).succ = i.succAbove (j.predAbove k)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (Truncated C n)

Tactic:
dsimp [Truncated]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (Truncated C n)

Tactic:
dsimp [Truncated]
  infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
⊢ X.δ j ≫ X.δ₀Iter i hi = X.δ₀Iter (i + 1) ⋯

Tactic:
by
  dsimp [δ, δ₀Iter]
  rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_δ ..]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
⊢ X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.δ₀Iter (i + 1) hi).op = X.map (SimplexCategory.δ₀Iter i ⋯).op

Tactic:
rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_σ ..]

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

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
hf : Mono f
h : n.len = m.len
⊢ IsIso f

Tactic:
obtain rfl : n = m := by aesop

Goal state after:
n : SimplexCategory
f : n ⟶ n
hf : Mono f
h : n.len = n.len
⊢ IsIso f
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
hf : Epi f
h : n.len = m.len
⊢ IsIso f

Tactic:
obtain rfl : n = m := by aesop

Goal state after:
n : SimplexCategory
f : n ⟶ n
hf : Epi f
h : n.len = n.len
⊢ IsIso f
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) (i.succ.succAbove (x.castPred ⋯))

Tactic:
Fin.succAbove_of_castSucc_lt

Goal state after:
case pos
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) (x.castPred ⋯).castSucc

case pos.h
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
⊢ (x.castPred ⋯).castSucc < i.succ
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n✝ : ℕ
i j : Fin (n✝ + 1)
hij : i ≤ j
⊢ (p.app (op ⦋n✝⦌) ≫ H.h j) ≫ Y.σ i.castSucc = X'.σ i ≫ p.app (op ⦋n✝ + 1⦌) ≫ H.h j.succ

Tactic:
simpa using p.app _ ≫= H.h_comp_σ_castSucc_of_le i j hij

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 : ↑k < j
hk' : i ≤ k.castSucc
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) (i.succAbove k)) = 0

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

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: 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} {Y Y' : Arrow C} (f : Augmented.toArrow.obj X ⟶ Y) (g : Y ⟶ Y'),
    (cechNerveEquiv X Y') (f ≫ g) = (cechNerveEquiv X Y) f ≫ augmentedCechNerve.map g

Tactic:
dsimp [cechNerveEquiv]
        -- The next three lines were not needed before https://github.com/leanprover/lean4/pull/2644
        intro X Y Y' f g
        change equivalenceLeftToRight X Y' (f ≫ g) =
          equivalenceLeftToRight X Y f ≫ augmentedCechNerve.map g
        cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
x y : SimplexCategory
g : x ⟶ y
⊢ (widePushout f.left (fun x ↦ f.right) fun x ↦ f.hom) ⟶ widePushout f.left (fun x ↦ f.right) fun x ↦ f.hom

Tactic:
by
    refine WidePushout.desc (WidePushout.head _)
      (fun i => (@WidePushout.ι _ _ _ _ _ (fun _ => f.hom) (_) (g.toOrderHom i))) (fun j => ?_)
    rw [← WidePushout.arrow_ι]

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

Goal state before:
pp: case mpr
X : SSet
n : ℕ
i : Fin (n + 1)
y : X _⦋n⦌
⊢ (ConcreteCategory.hom (SimplicialObject.σ X i)) y ∈ X.degenerate (n + 1)

Tactic:
apply σ_mem_degenerate

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

Goal state before:
pp: case a
X : SSet
x y : X.N
h : x.subcomplex = y.subcomplex
⊢ x ≤ y

pp: case a
X : SSet
x y : X.N
h : x.subcomplex = y.subcomplex
⊢ y ≤ x

Tactic:
all_goals
  · rw [le_iff, h]

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

Goal state before:
pp: case mpr
X : SSet
A : X.Subcomplex
n : ℕ
⊢ X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌) → A.toSSet.degenerate n = ⊤

Tactic:
intro h
    simp only [Set.inf_eq_inter, Set.inter_eq_right] at h
    ext x
    simpa [A.mem_degenerate_iff] using h x.prop

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Even j
⊢ (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₁).hom ≫
      { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven }.f =
    ((alternatingConst A hOdd hEven hc).sc' i j k).f ≫ (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₂).hom

Tactic:
by
      simp_all only [alternatingConst, dite_eq_ite, Iso.refl_hom, Category.id_comp,
        shortComplexFunctor'_obj_f, ↓reduceIte, Category.comp_id, right_eq_ite_iff]
      intro hi
      have := hc i j hij
      exact False.elim <| Nat.not_odd_iff_even.2 hi <| by simp_all [Nat.odd_add]

Goal state after: