mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case cons.cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
⊢ (join (((a, Seq.cons x s_1), Seq.cons x_1 s_2), SS)).join =
    join (join ((a, Seq.cons x s_1), Seq.cons x_1 s_2), Seq.map join SS)

Tactic:
obtain ⟨y, t⟩ := x_1

Goal state after:
case cons.cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
s_2 : Seq (Seq1 γ)
y : γ
t : Seq γ
⊢ (join (((a, Seq.cons x s_1), Seq.cons (y, t) s_2), SS)).join =
    join (join ((a, Seq.cons x s_1), Seq.cons (y, t) s_2), Seq.map join SS)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
s_succ_nth_eq : s.get? (n + 1) = none
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
rw [squashSeq_eq_self_of_terminated s_succ_nth_eq]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
terminatedAt_n : g.TerminatedAt n
g'_eq_g : g' = g
gp✝ : Pair K
m✝ : ℕ
m_lt_n : m✝ < n
s_mth_eq : g.s.get? m✝ = some gp✝
⊢ 0 < gp✝.a ∧ 0 < gp✝.b

Tactic:
exact s_pos (Nat.lt_succ_of_lt m_lt_n) s_mth_eq

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
have : ¬n + 2 ≤ 1 := by lia

Goal state after:
case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
⊢ P.toPoly.degree ≤ 2

Tactic:
simpa only [of_a_eq_zero ha] using degree_quadratic_le

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ ((((φ P.a ≠ 0 ∧ φ P.a ≠ 0) ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z) ∧ (((φ P.a ≠ 0 ∧ φ P.a ≠ 0) ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z

Tactic:
_root_.map_ne_zero,

Goal state after:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ ((((P.a ≠ 0 ∧ P.a ≠ 0) ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z) ∧ (((P.a ≠ 0 ∧ P.a ≠ 0) ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case right
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := ⋯
nextConts : Pair K := ⋯
conts : Pair K := ⋯
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := ⋯
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := ⋯
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := ⋯
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
⊢ den ≤ den'

Tactic:
suffices gp.b * conts.b ≤ ifp_n.fr⁻¹ * conts.b by
      simp only [den, den']; gcongr

Goal state after:
case right
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
⊢ gp.b * conts.b ≤ ifp_n.fr⁻¹ * conts.b
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
⊢ CompleteOrthogonalIdempotents fun x ↦ Pi.single x 1

Tactic:
refine ⟨⟨by simp [IsIdempotentElem, ← Pi.single_mul], ?_⟩, Finset.univ_sum_single 1⟩
  intro i j hij
  ext k
  by_cases hi : i = k
  · subst hi; simp [hij]
  · simp [hi]

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

Goal state before:
pp: case neg
ι : 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✝² : DecidableEq ι
κ : ι → Type u_4
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal fun i ↦ N ↑i
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i)
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ ↑i
hi : σ ↑i ∉ s
⊢ ((h.collectedBasis b).repr (f ↑((b i) k))) ⟨i, k⟩ = 0

Tactic:
suffices f (b i k) = 0 by simp [this]
    simpa [hN _ hi] using hf i <| Subtype.mem (b i k)

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

Goal state before:
pp: 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

Tactic:
rw [← LinearMap.comp_apply, ← Module.End.mul_eq_comp, h.eq, Module.End.mul_eq_comp,
    LinearMap.comp_apply, hx, map_zero]

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✝³ : DecidableEq ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
inst✝ : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
⊢ (trace R M) f = 0

Tactic:
have hN : {i | N i ≠ ⊥}.Finite := WellFoundedGT.finite_ne_bot_of_iSupIndep
    h.submodule_iSupIndep

Goal state after:
ι : 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✝³ : DecidableEq ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
inst✝ : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : {i | N i ≠ ⊥}.Finite
⊢ (trace R M) f = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
a b : R
⊢ (fun x ↦ e * x * e) (a * e * e * b) = (fun x ↦ e * x * e) a * (fun x ↦ e * x * e) b

Tactic:
simp_rw [mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

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

Tactic:
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
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r₁ r₂ : R
i : I
⊢ e i * (r₁ * (e i * e i) * r₂) * e i = e i * r₁ * e i * (e i * r₂ * e i)

Tactic:
simp_rw [mul_assoc]

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

Goal state before:
pp: case refine_1
k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
inj : finrank k ↥(f 0).range = finrank k (V (Fin.castSucc 0))
surj : (f (Fin.last n)).range = ⊤
⊢ ↑(finrank k (V 0)) = ↑(finrank k ↥(f 0).range)

pp: case refine_2
k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
inj : finrank k ↥(f 0).range = finrank k (V (Fin.castSucc 0))
surj : (f (Fin.last n)).range = ⊤
i : Fin n
⊢ ↑(finrank k (V i.succ.castSucc)) = ↑(finrank k ↥(f i.castSucc).range) + ↑(finrank k ↥(f i.succ).range)

pp: case refine_3
k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
inj : finrank k ↥(f 0).range = finrank k (V (Fin.castSucc 0))
surj : (f (Fin.last n)).range = ⊤
⊢ ↑(finrank k (V (Fin.last (n + 1)))) = ↑(finrank k ↥(f (Fin.last n)).range)

Tactic:
· aesop

Goal state after:
case refine_2
k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
inj : finrank k ↥(f 0).range = finrank k (V (Fin.castSucc 0))
surj : (f (Fin.last n)).range = ⊤
i : Fin n
⊢ ↑(finrank k (V i.succ.castSucc)) = ↑(finrank k ↥(f i.castSucc).range) + ↑(finrank k ↥(f i.succ).range)

case refine_3
k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
inj : finrank k ↥(f 0).range = finrank k (V (Fin.castSucc 0))
surj : (f (Fin.last n)).range = ⊤
⊢ ↑(finrank k (V (Fin.last (n + 1)))) = ↑(finrank k ↥(f (Fin.last n)).range)
Module: Mathlib.Algebra.Field.Periodic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddCommMonoid α
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Periodic f c
a : γ
x : α
ha : ¬a = 0
⊢ (fun x ↦ f (a • x)) (x + a⁻¹ • c) = (fun x ↦ f (a • x)) x

Tactic:
simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝³ : AddMonoid α
inst✝² : Neg β
inst✝¹ : GroupWithZero γ
inst✝ : DistribMulAction γ α
h : Antiperiodic f c
a : γ
ha : a ≠ 0
x : α
⊢ (fun x ↦ f (a • x)) (x + a⁻¹ • c) = -(fun x ↦ f (a • x)) x

Tactic:
simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β α✝ β✝ γ✝ : Type u
x✝ : FreeMagma α✝
f : α✝ → FreeMagma β✝
g : β✝ → FreeMagma γ✝
x y : FreeMagma α✝
ih1 : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ih2 : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ x * y >>= f >>= g = x * y >>= fun x ↦ f x >>= g

Tactic:
mul_bind,

Goal state after:
α β α✝ β✝ γ✝ : Type u
x✝ : FreeMagma α✝
f : α✝ → FreeMagma β✝
g : β✝ → FreeMagma γ✝
x y : FreeMagma α✝
ih1 : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ih2 : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f) * (y >>= f) >>= g = x * y >>= fun x ↦ f x >>= g
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β α✝ β✝ γ✝ : Type u
x✝ : FreeMagma α✝
f : α✝ → FreeMagma β✝
g : β✝ → FreeMagma γ✝
x y : FreeMagma α✝
ih1 : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ih2 : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f) * (y >>= f) >>= g = x * y >>= fun x ↦ f x >>= g

Tactic:
mul_bind,

Goal state after:
α β α✝ β✝ γ✝ : Type u
x✝ : FreeMagma α✝
f : α✝ → FreeMagma β✝
g : β✝ → FreeMagma γ✝
x y : FreeMagma α✝
ih1 : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ih2 : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f >>= g) * (y >>= f >>= g) = x * y >>= fun x ↦ f x >>= g
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β α✝ β✝ γ✝ : Type u
x✝ : FreeMagma α✝
f : α✝ → FreeMagma β✝
g : β✝ → FreeMagma γ✝
x y : FreeMagma α✝
ih1 : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ih2 : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f >>= g) * (y >>= f >>= g) = x * y >>= fun x ↦ f x >>= g

Tactic:
mul_bind,

Goal state after:
α β α✝ β✝ γ✝ : Type u
x✝ : FreeMagma α✝
f : α✝ → FreeMagma β✝
g : β✝ → FreeMagma γ✝
x y : FreeMagma α✝
ih1 : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ih2 : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f >>= g) * (y >>= f >>= g) = (x >>= fun x ↦ f x >>= g) * (y >>= fun x ↦ f x >>= g)
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case cons
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 TL : List (α × Bool)
htl : reduce tl1 = TL
ih : Red tl1 TL
⊢ Red (hd1 :: tl1)
    (List.rec [hd1] (fun head tail tail_ih ↦ if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail) TL)

Tactic:
cases TL with
    | nil => exact Red.cons_cons ih
    | cons hd2 tl2 =>
      dsimp only
      split_ifs with h
      · cases hd1
        cases hd2
        cases h
        dsimp at *
        subst_vars
        apply Red.trans (Red.cons_cons ih)
        exact Red.Step.cons_not_rev.to_red
      · exact Red.cons_cons ih

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

Goal state before:
pp: case neg.cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
H : (x, b) :: (y, c) :: tail = a :: L2 ++ (x', b') :: (x', !b') :: L3
⊢ p

Tactic:
refine @reduce.not _ L1 L2 L3 x' b' ?_

Goal state after:
case neg.cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
H : (x, b) :: (y, c) :: tail = a :: L2 ++ (x', b') :: (x', !b') :: L3
⊢ reduce L1 = L2 ++ (x', b') :: (x', !b') :: L3
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β α✝ β✝ γ✝ : Type u
x✝ : FreeSemigroup α✝
g : α✝ → FreeSemigroup β✝
f : β✝ → FreeSemigroup γ✝
x : α✝
y : FreeSemigroup α✝
ih1 : pure x >>= g >>= f = pure x >>= fun x ↦ g x >>= f
ih2 : y >>= g >>= f = y >>= fun x ↦ g x >>= f
⊢ pure x * y >>= g >>= f = pure x * y >>= fun x ↦ g x >>= f

Tactic:
mul_bind,

Goal state after:
α β α✝ β✝ γ✝ : Type u
x✝ : FreeSemigroup α✝
g : α✝ → FreeSemigroup β✝
f : β✝ → FreeSemigroup γ✝
x : α✝
y : FreeSemigroup α✝
ih1 : pure x >>= g >>= f = pure x >>= fun x ↦ g x >>= f
ih2 : y >>= g >>= f = y >>= fun x ↦ g x >>= f
⊢ (pure x >>= g) * (y >>= g) >>= f = pure x * y >>= fun x ↦ g x >>= f
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β α✝ β✝ γ✝ : Type u
x✝ : FreeSemigroup α✝
g : α✝ → FreeSemigroup β✝
f : β✝ → FreeSemigroup γ✝
x : α✝
y : FreeSemigroup α✝
ih1 : pure x >>= g >>= f = pure x >>= fun x ↦ g x >>= f
ih2 : y >>= g >>= f = y >>= fun x ↦ g x >>= f
⊢ (pure x >>= g) * (y >>= g) >>= f = pure x * y >>= fun x ↦ g x >>= f

Tactic:
mul_bind,

Goal state after:
α β α✝ β✝ γ✝ : Type u
x✝ : FreeSemigroup α✝
g : α✝ → FreeSemigroup β✝
f : β✝ → FreeSemigroup γ✝
x : α✝
y : FreeSemigroup α✝
ih1 : pure x >>= g >>= f = pure x >>= fun x ↦ g x >>= f
ih2 : y >>= g >>= f = y >>= fun x ↦ g x >>= f
⊢ (pure x >>= g >>= f) * (y >>= g >>= f) = pure x * y >>= fun x ↦ g x >>= f
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β α✝ β✝ γ✝ : Type u
x✝ : FreeSemigroup α✝
g : α✝ → FreeSemigroup β✝
f : β✝ → FreeSemigroup γ✝
x : α✝
y : FreeSemigroup α✝
ih1 : pure x >>= g >>= f = pure x >>= fun x ↦ g x >>= f
ih2 : y >>= g >>= f = y >>= fun x ↦ g x >>= f
⊢ (pure x >>= g >>= f) * (y >>= g >>= f) = pure x * y >>= fun x ↦ g x >>= f

Tactic:
mul_bind,

Goal state after:
α β α✝ β✝ γ✝ : Type u
x✝ : FreeSemigroup α✝
g : α✝ → FreeSemigroup β✝
f : β✝ → FreeSemigroup γ✝
x : α✝
y : FreeSemigroup α✝
ih1 : pure x >>= g >>= f = pure x >>= fun x ↦ g x >>= f
ih2 : y >>= g >>= f = y >>= fun x ↦ g x >>= f
⊢ (pure x >>= g >>= f) * (y >>= g >>= f) = (pure x >>= fun x ↦ g x >>= f) * (y >>= fun x ↦ g x >>= f)
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 : α✝
⊢ traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x) = Functor.Comp.mk (traverse f <$> traverse g (pure x))

Tactic:
by simp only [traverse_pure, functor_norm, Function.comp_def]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
⊢ ∃ y, (algebraMap S K) y = x

Tactic:
obtain ⟨z, hz⟩ := (isIntegrallyClosed_iff _).mp ‹_› hy

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ∃ y, (algebraMap S K) y = x
Module: Mathlib.Algebra.Group.Action.Option

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝² : SMul M α
inst✝¹ : SMul N α
a : M
b✝ : α
x : Option α
inst✝ : FaithfulSMul M α
m₁✝ m₂✝ : M
h : ∀ (a : Option α), m₁✝ • a = m₂✝ • a
b : α
⊢ m₁✝ • b = m₂✝ • b

Tactic:
injection h (some b)

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

Goal state before:
pp: C : Type u_1
inst✝ : CommGroup C
x y z : Subgroup C
xz : x ≤ z
b : C
hb : b ∈ x
c : C
hc : c ∈ y
haz : b * c ∈ z
⊢ ∃ y_1 ∈ x, ∃ z_1 ∈ y ⊓ z, y_1 * z_1 = b * c

Tactic:
exact ⟨b, hb, c, mem_inf.2 ⟨hc, (mul_mem_cancel_left (xz hb)).1 haz⟩, rfl⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
f : Set (Submonoid M)
hf : ∀ s ∈ f, s.MulSaturated
x✝¹ x✝ : M
hxy : x✝¹ * x✝ ∈ InfSet.sInf f
⊢ x✝¹ ∈ InfSet.sInf f ∧ x✝ ∈ InfSet.sInf f

Tactic:
simp_rw [mem_sInf] at hxy ⊢
  exact ⟨fun s hs ↦ (hf s hs <| hxy s hs).1, fun s hs ↦ (hf s hs <| hxy s hs).2⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹

Tactic:
obtain rfl | ha := eq_or_ne a 0
  · obtain rfl | hs := s.eq_empty_or_nonempty <;> simp [*]
  -- was `simp` and very slow (https://github.com/leanprover-community/mathlib4/issues/19751)
  · ext; simp only [mem_inv', ne_eq, MulOpposite.op_eq_zero_iff, not_false_eq_true, ←
      inv_smul_mem_iff₀, MulOpposite.smul_eq_mul_unop, MulOpposite.unop_inv, MulOpposite.unop_op,
      inv_eq_zero, inv_inv, smul_eq_mul, mul_inv_rev, ha]

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

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

Tactic:
· exfalso
        exact hm a (eq_of_le_of_not_lt h₂ h₁)

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

Goal state before:
pp: n : SimplexCategory
f g : ⦋0⦌ ⟶ n
h0 : (toOrderHom f) 0 = (toOrderHom g) 0
i : Fin (⦋0⦌.len + 1)
⊢ ↑((toOrderHom f) 0) = ↑((toOrderHom g) 0)

Tactic:
exact h0 ▸ rfl

Goal state after:
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
i : Fin (⦋1⦌.len + 1)
⊢ ↑((toOrderHom f) 0) = ↑((toOrderHom g) 0)

Tactic:
exact h0 ▸ rfl

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

Goal state after:
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₂
h'' :
  ¬(ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁ ≤
      (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: X✝ Y✝ : SimplexCategory
f : X✝ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
⊢ X✝.len = Y✝.len

Tactic:
exact le_antisymm (len_le_of_mono f) (len_le_of_epi f)

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

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

Tactic:
have h₁ := Y.δ_comp_σ_self (i := j.succ)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f✝ g f : X ⟶ Y
n✝ : ℕ
j : Fin (n✝ + 1)
h₁ : Y.σ j.succ ≫ Y.δ j.succ.castSucc = 𝟙 (Y _⦋n✝ + 1⦌)
⊢ (X.σ j.succ ≫ f.app (op ⦋n✝ + 1 + 1⦌)) ≫ Y.δ j.castSucc.succ =
    (X.σ j.castSucc ≫ f.app (op ⦋n✝ + 1 + 1⦌)) ≫ Y.δ j.castSucc.succ