mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
p : ℕ
p_pos : p > 0
hp_mixedChar : MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
hI_p : CharP (R ⧸ I) p
⊢ False

Tactic:
replace hI_zero : CharP (R ⧸ I) 0 := @CharP.ofCharZero _ _ (h I hI_ne_top)

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
p : ℕ
p_pos : p > 0
hp_mixedChar : MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
hI_p : CharP (R ⧸ I) p
hI_zero : CharP (R ⧸ I) 0
⊢ False
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
n : ℕ
hn : n ≠ 0
⊢ n • r ∈ zmultiples p ↔ ∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p

Tactic:
← natCast_zsmul r,

Goal state after:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
n : ℕ
hn : n ≠ 0
⊢ ↑n • r ∈ zmultiples p ↔ ∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
x : α
h : s.head = some x
n : ℕ
⊢ s.get? n = (cons x s.tail).get? n

Tactic:
cases n <;> simp only [get?_cons_zero, get?_cons_succ, get?_tail]

Goal state after:
case zero
α : Type u
s : Seq α
x : α
h : s.head = some x
⊢ s.get? 0 = some x
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case refine_2
α : Type u
s : Seq α
n : ℕ
⊢ s.get? n = none → (∃ n, s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none

Tactic:
intro hn

Goal state after:
case refine_2
α : Type u
s : Seq α
n : ℕ
hn : s.get? n = none
⊢ (∃ n, s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case refine_2
α : Type u
s : Seq α
n : ℕ
⊢ ¬s.get? n = none → ∀ (x : ℕ), s.get? x = none → ∀ m ≤ n, ¬s.get? m = none

Tactic:
intro hn

Goal state after:
case refine_2
α : Type u
s : Seq α
n : ℕ
hn : ¬s.get? n = none
⊢ ∀ (x : ℕ), s.get? x = none → ∀ m ≤ n, ¬s.get? m = none
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s).TerminatedAt n
i : ℕ
hi : i < n + 1
⊢ -((↑s).partNums.get? i).getD 0 = -1

Tactic:
obtain ⟨gp, s_ith_eq⟩ : ∃ gp, (↑s : GenContFract K).s.get? i = some gp :=
      Option.ne_none_iff_exists'.1 <| mt (terminated_stable <| Nat.le_of_succ_le_succ hi) ‹_›

Goal state after:
K : Type u_1
inst✝ : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s).TerminatedAt n
i : ℕ
hi : i < n + 1
gp : Pair K
s_ith_eq : (↑s).s.get? i = some gp
⊢ -((↑s).partNums.get? i).getD 0 = -1
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRel R ca cb.think ↔ LiftRel R ca cb

Tactic:
← LiftRel.swap R,

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRel (swap R) cb.think ca ↔ LiftRel R ca cb
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case succ.inr
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Tactic:
· obtain ⟨p, hp⟩ := Option.ne_none_iff_exists'.mp hsome
      rw [hp] at ih
      rcases eq_or_ne p.fr 0 with hz | hnz
      · rw [stream_eq_none_of_fr_eq_zero hp hz, stream_eq_none_of_fr_eq_zero ih hz]
      · rw [stream_succ_of_some hp hnz, stream_succ_of_some ih hnz]

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
⊢ (map f₁ s₁).zip (map f₂ s₂) = map (Prod.map f₁ f₂) (s₁.zip s₂)

Tactic:
ext1 n
  simp
  cases s₁.get? n <;> cases s₂.get? n <;> simp

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case succ
n : ℕ
ih : ∀ (m : ℕ), fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
m : ℕ
⊢ fib (m + (n + 1) + 1) = fib m * fib (n + 1) + fib (m + 1) * fib (n + 1 + 1)

Tactic:
specialize ih (m + 1)

Goal state after:
case succ
n m : ℕ
ih : fib (m + 1 + n + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + (n + 1) + 1) = fib m * fib (n + 1) + fib (m + 1) * fib (n + 1 + 1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
R : α → α → Prop
inst✝ : IsTrans α R
hd tl_hd : α
tl_tl : Seq α
h_hd : R hd tl_hd
h_tl : Pairwise R (Seq.cons tl_hd tl_tl)
⊢ Pairwise R (Seq.cons hd (Seq.cons tl_hd tl_tl))

Tactic:
apply Pairwise.cons _ h_tl
  simp only [mem_cons_iff, forall_eq_or_imp]
  exact ⟨h_hd, fun x hx ↦ Trans.simple h_hd ((cons_elim h_tl).left x hx)⟩

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ fib n * (2 * fib (n + 1) - fib n) + fib (2 * n + 1) = fib (n + 1) * (2 * fib n + fib (n + 1))

Tactic:
fib_two_mul_add_one

Goal state after:
n : ℕ
⊢ fib n * (2 * fib (n + 1) - fib n) + (fib (n + 1) ^ 2 + fib n ^ 2) = fib (n + 1) * (2 * fib n + fib (n + 1))
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case inr
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib (n.pred + 1))

Tactic:
calc
    gcd (fib m) (fib (n.pred + 1 + m)) =
        gcd (fib m) (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1)) := by
        rw [← fib_add n.pred _]
        ring_nf
    _ = gcd (fib m) (fib (n.pred + 1) * fib (m + 1)) := by
        rw [add_comm, gcd_add_mul_right_right (fib m) _ (fib n.pred)]
    _ = gcd (fib m) (fib (n.pred + 1)) :=
      Coprime.gcd_mul_right_cancel_right (fib (n.pred + 1)) (Coprime.symm (fib_coprime_fib_succ m))

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

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

Tactic:
cases s_succ_nth_eq : s.get? (n + 1)

Goal state after:
case none.none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
s_succ_succ_nth_eq : s.get? (n + 2) = none
s_succ_nth_eq : s.get? (n + 1) = none
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n

case none.some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
s_succ_succ_nth_eq : s.get? (n + 2) = none
val✝ : Pair K
s_succ_nth_eq : s.get? (n + 1) = some val✝
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case inl
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
terminatedAt_n : g.TerminatedAt n
⊢ g.convs (n + 1) = (g.squashGCF n).convs n

Tactic:
have : squashGCF g n = g := squashGCF_eq_self_of_terminated terminatedAt_n
    simp only [this, convs_stable_of_terminated n.le_succ terminatedAt_n]

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

Goal state before:
pp: 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)
this : ↑(fib (n + 2)) ≤ nextConts.b
⊢ ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b

Tactic:
rwa [nextConts_b_eq] at this

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}
⊢ (x ≠ y ∧ x ≠ z) ∧ y ≠ z ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z

Tactic:
and_assoc

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
this : (x - x ^ 2) ^ n ∣ 1 - (1 - x ^ n) ^ n - (1 - (1 - x ^ n) ^ n) ^ 2
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)

Tactic:
hx,

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
this : 0 ∣ 1 - (1 - x ^ n) ^ n - (1 - (1 - x ^ n) ^ n) ^ 2
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)
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
⊢ g (((f - μ • 1) ^ l) x) = 0

Tactic:
hx,

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
⊢ g 0 = 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
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
⊢ (trace R M) (g ∘ₗ f) = 0

Tactic:
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]

Goal state after:
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
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
⊢ ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : R[ε] →ₐ[R] A
hε : f ε = g ε
⊢ f = g

Tactic:
ext
  dsimp
  simp only [one_smul, hε]

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case pos
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis (↥s) R M)
s : Finset M
b : Basis (↥s) R M
⊢ (trace R M) (f * g) = (trace R M) (g * f)

Tactic:
simp_rw [trace_eq_matrix_trace R b, LinearMap.toMatrix_mul]

Goal state after:
case pos
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis (↥s) R M)
s : Finset M
b : Basis (↥s) R M
⊢ ((toMatrix b b) f * (toMatrix b b) g).trace = ((toMatrix b b) g * (toMatrix b b) f).trace
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
p : Submodule R M
f g : End R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
μ₁ μ₂ : R
h : MapsTo ⇑f ↑(g.maxGenEigenspace μ₁) ↑(g.maxGenEigenspace μ₂)
x : ↥p
hx : x ∈ ↑(maxGenEigenspace (LinearMap.restrict g hg) μ₁)
⊢ (LinearMap.restrict f hf) x ∈ ↑(maxGenEigenspace (LinearMap.restrict g hg) μ₂)

Tactic:
simp_rw [SetLike.mem_coe, mem_maxGenEigenspace, ← LinearMap.restrict_smul_one _,
    LinearMap.restrict_sub _, Module.End.pow_restrict _, LinearMap.restrict_apply,
    Submodule.mk_eq_zero, ← mem_maxGenEigenspace] at hx ⊢

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f g : End R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
μ₁ μ₂ : R
h : MapsTo ⇑f ↑(g.maxGenEigenspace μ₁) ↑(g.maxGenEigenspace μ₂)
x : ↥p
hx : ↑x ∈ g.maxGenEigenspace μ₁
⊢ f ↑x ∈ g.maxGenEigenspace μ₂
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
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
⊢ (trace A (A ⊗[R] M)) (baseChange A f) = (algebraMap R A) ((trace R M) f)

Tactic:
let b' := Algebra.TensorProduct.basis A b

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
b' : Basis (Free.ChooseBasisIndex R M) A (A ⊗[R] M) := Algebra.TensorProduct.basis A b
⊢ (trace A (A ⊗[R] M)) (baseChange A f) = (algebraMap R A) ((trace R M) f)
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
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
b' : Basis (Free.ChooseBasisIndex R M) A (A ⊗[R] M) := Algebra.TensorProduct.basis A b
⊢ (trace A (A ⊗[R] M)) (baseChange A f) = (algebraMap R A) ((trace R M) f)

Tactic:
change _ = (algebraMap R A : R →+ A) _

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
b' : Basis (Free.ChooseBasisIndex R M) A (A ⊗[R] M) := Algebra.TensorProduct.basis A b
⊢ (trace A (A ⊗[R] M)) (baseChange A f) = ↑(algebraMap R A) ((trace R M) f)
Module: Mathlib.Algebra.Field.NegOnePow

Goal state before:
pp: K : Type u_1
n : ℤ
inst✝ : DivisionRing K
⊢ ↑↑n.negOnePow = (-1) ^ n

Tactic:
by
  rcases even_or_odd' n with ⟨k, rfl | rfl⟩
  · simp [zpow_mul, zpow_ofNat]
  · rw [zpow_add_one₀ (by simp), zpow_mul, zpow_ofNat]
    simp

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

Goal state before:
pp: case neg.nil
α : 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)
H : (x, b) :: (y, c) :: tail = [] ++ (x', b') :: (x', !b') :: L3
⊢ p

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:
· injections; subst_vars
        simp at h

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
⊢ p
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
x✝ x y : FreeMagma α
hx : (toFreeSemigroup x).length = x.length
hy : (toFreeSemigroup y).length = y.length
⊢ (toFreeSemigroup x).length + (toFreeSemigroup y).length = (x * y).length

Tactic:
hx,

Goal state after:
α : Type u
x✝ x y : FreeMagma α
hx : (toFreeSemigroup x).length = x.length
hy : (toFreeSemigroup y).length = y.length
⊢ x.length + (toFreeSemigroup y).length = (x * y).length
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
φ : ℕ → R
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree

Tactic:
hx,

Goal state after:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
φ : ℕ → R
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = -∑ i, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x✝ y✝ : R
a b x y : ℍ[R]
| ↑(x * y * star (x * y)).re

Tactic:
rw [← mul_star_eq_coe, star_mul, mul_assoc, ← mul_assoc y, y.mul_star_eq_coe,
      coe_commutes, ← mul_assoc, x.mul_star_eq_coe, ← coe_mul]

Goal state after:
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x✝ y✝ : R
a b x y : ℍ[R]
| ↑((x * star x).re * (y * star y).re)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

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

Tactic:
apply generalizedEisenstein (K := FractionRing (R ⧸ P)) (q := X) (p := f.natDegree)
    (by simp [map_X, irreducible_X]) monic_X hu
    (natDegree_pos_iff_degree_pos.mpr hfd0)

Goal state after:
case hfP
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
⊢ (algebraMap R (FractionRing (R ⧸ P))) f.leadingCoeff ≠ 0

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

case hfmodP2
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 (Ideal.Quotient.mk (ker (algebraMap R (FractionRing (R ⧸ P))) ^ 2)) (f %ₘ X) ≠ 0
Module: Mathlib.Algebra.Group.Ideal

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
s : Set M
⊢ ↑(closure s) = s ∪ univ * s

Tactic:
let I : SemigroupIdeal M :=
    { carrier := s ∪ univ * s
      smul_mem' x y := by
        rintro (hy | ⟨y, -, z, hz, rfl⟩)
        · exact .inr <| mul_mem_mul (mem_univ _) hy
        · simpa [← mul_assoc] using .inr <| mul_mem_mul (mem_univ _) hz }

Goal state after:
M : Type u_1
inst✝ : Semigroup M
s : Set M
I : SemigroupIdeal M := { carrier := s ∪ univ * s, smul_mem' := ⋯ }
⊢ ↑(closure s) = s ∪ univ * s
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
ih : ∀ {j : ℕ}, j < n → (Δ_[1]^[n] fun r ↦ r ^ j) = 0
j : ℕ
h : j < n + 1
this : (Δ_[1] fun r ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i
i : ℕ
hi : i ∈ range j
⊢ i < n

Tactic:
by have := mem_range.1 hi; lia

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

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

Tactic:
by have := mem_range.1 hi; lia

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

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

Tactic:
← smul_eq_mul,

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

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

Tactic:
← smul_eq_mul,

Goal state after:
R : Type u_3
inst✝ : CommRing R
n : ℕ
P : ℕ → R
⊢ (fun a ↦ ∑ x ∈ range n, Δ_[1]^[n] (fun x_1 ↦ P x • x_1 ^ x) a) = 0
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ ∃ e, { f := p.f, comm := ⋯ } ≫ e = 𝟙 { X := P.X, p := p.f, idem := hp } ∧ e ≫ { f := p.f, comm := ⋯ } = p

Tactic:
use ⟨p.f, by rw [hp, p_comp p]⟩

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ { f := p.f, comm := ⋯ } ≫ { f := p.f, comm := ⋯ } = 𝟙 { X := P.X, p := p.f, idem := hp } ∧
    { f := p.f, comm := ⋯ } ≫ { f := p.f, comm := ⋯ } = p
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 : ℕ
⊢ (p.app (op ⦋n⦌) ≫ H.h (Fin.last n)) ≫ Y.δ (Fin.last (n + 1)) = (p ≫ f).app (op ⦋n⦌)

Tactic:
by
    simpa [-h_last_comp_δ_last] using p.app _ ≫= H.h_last_comp_δ_last n

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

Goal state before:
pp: case succ
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ s ∉ (nerve X).nonDegenerate (n + 1) ↔ ¬StrictMono s.obj

Tactic:
← SSet.mem_degenerate_iff_notMem_nonDegenerate,

Goal state after:
case succ
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ s ∈ (nerve X).degenerate (n + 1) ↔ ¬StrictMono s.obj
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : ComposableArrows C 0
⊢ homEquiv (Edge.id x) = 𝟙 (nerveEquiv x)

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

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x : C
⊢ homEquiv (Edge.id (nerveEquiv.symm x)) = 𝟙 (nerveEquiv (nerveEquiv.symm x))
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
i : Fin (d'.1.len + 1)
⊢ (stdSimplex.opObjEquiv ((ConcreteCategory.hom ((stdSimplex.obj n).op.map f)) g)) i =
    ((ConcreteCategory.hom ((stdSimplex.obj n).map f)) (stdSimplex.opObjEquiv g)) i

Tactic:
stdSimplex.opObjEquiv_apply,

Goal state after:
n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
i : Fin (d'.1.len + 1)
⊢ ((opObjEquiv ((ConcreteCategory.hom ((stdSimplex.obj n).op.map f)) g)) i.rev).rev =
    ((ConcreteCategory.hom ((stdSimplex.obj n).map f)) (stdSimplex.opObjEquiv g)) i
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ C.d 0 (i + 2) = 0

Tactic:
by
  rw [C.shape]
  simp only [ComplexShape.up_Rel, zero_add]
  exact (Nat.one_lt_succ_succ _).ne

Goal state after: