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

Goal state before:
pp: α : Type u
C : Seq α → Prop
a : α
s : Seq α
M : a ∈ s
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
⊢ C s

Tactic:
by
  obtain ⟨k, e⟩ := M; unfold Stream'.get at e
  induction k generalizing s with
  | zero =>
    have TH : s = cons a (tail s) := by
      apply destruct_eq_cons
      unfold destruct get? Functor.map
      rw [← e]
      rfl
    rw [TH]
    apply h1 _ _ (Or.inl rfl)
  | succ k IH =>
    cases s with
    | nil => injection e
    | cons b s' =>
      have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl
      rw [h_eq] at e
      apply h1 _ _ (Or.inr (IH e))

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
h : n < x.length
⊢ (x ++ₛ a).get n = x[n]

Tactic:
induction x generalizing n with
  | nil => simp at h
  | cons b x ih =>
    rcases n with (_ | n)
    · simp
    · simp [ih n (by simpa using h), cons_append_stream]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
l : List α
s : Stream' α
⊢ initsCore l s = l :: initsCore (l ++ [s.head]) s.tail

Tactic:
unfold initsCore corecOn
    rw [corec_eq]

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

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
h : s.tail.Terminates
⊢ n ≤ s.tail.length h

Tactic:
simp only [length, tail, Nat.le_find_iff, TerminatedAt, get?_mk, Stream'.tail]

Goal state after:
case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
h : s.tail.Terminates
⊢ ∀ m < n, ¬(↑s).get (m + 1) = none
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
n : ℕ
IH : ∀ (s : Seq α), (s.drop n).head = s.get? n
s : Seq α
⊢ (s.tail.drop n).head = s.tail.get? n

Tactic:
apply IH

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

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

Tactic:
by
  convert! zip_map _ _ _ _
  simp

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

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

Tactic:
by
  convert! zip_map _ _ _ _
  simp

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

Goal state before:
pp: case succ.inr
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
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ g.convs (n + 1) = g'.convs' n

Tactic:
· suffices g.convs (n + 1) = g'.convs n by
        -- invoke the IH for the squashed gcf
        rwa [← IH]
        intro gp' m m_lt_n s_mth_eq'
        -- case distinction on m + 1 = n or m + 1 < n
        rcases m_lt_n with n | succ_m_lt_n
        · -- the difficult case at the squashed position: we first obtain the values from
          -- the sequence
          obtain ⟨gp_succ_m, s_succ_mth_eq⟩ : ∃ gp_succ_m, g.s.get? (m + 1) = some gp_succ_m :=
            Option.ne_none_iff_exists'.mp not_terminatedAt_n
          obtain ⟨gp_m, mth_s_eq⟩ : ∃ gp_m, g.s.get? m = some gp_m :=
            g.s.ge_stable m.le_succ s_succ_mth_eq
          -- we then plug them into the recurrence
          suffices 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b by
            have ot : g'.s.get? m = some ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ :=
              squashSeq_nth_of_not_terminated mth_s_eq s_succ_mth_eq
            grind
          have m_lt_n : m < m.succ := Nat.lt_succ_self m
          refine ⟨(s_pos (Nat.lt_succ_of_lt m_lt_n) mth_s_eq).left, ?_⟩
          refine add_pos (s_pos (Nat.lt_succ_of_lt m_lt_n) mth_s_eq).right ?_
          have : 0 < gp_succ_m.a ∧ 0 < gp_succ_m.b := s_pos (lt_add_one <| m + 1) s_succ_mth_eq
          exact div_pos this.left this.right
        · -- the easy case: before the squashed position, nothing changes
          refine s_pos (Nat.lt_succ_of_lt <| Nat.lt_succ_of_lt succ_m_lt_n) ?_
          exact Eq.trans (squashGCF_nth_of_lt succ_m_lt_n).symm s_mth_eq'
      -- now the result follows from the fact that the convergents coincide at the squashed position
      -- as established in `succ_nth_conv_eq_squashGCF_nth_conv`.
      have : ∀ ⦃b⦄, g.partDens.get? n = some b → b ≠ 0 := by
        intro _ nth_partDen_eq
        grind [exists_s_b_of_partDen nth_partDen_eq]
      exact succ_nth_conv_eq_squashGCF_nth_conv @this

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

Goal state before:
pp: case inl
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_eq_zero : ifp.fr = 0
⊢ v - g.convs n = 0

Tactic:
replace g_finite_correctness : v = g.convs n := by
      simpa [GenContFract.compExactValue, ifp_fr_eq_zero] using! g_finite_correctness

Goal state after:
case inl
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_eq_zero : ifp.fr = 0
g_finite_correctness : v = g.convs n
⊢ v - g.convs n = 0
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
k : ℕ∞
x : M
h : f.HasUnifEigenvector μ k x
⊢ ∃ x ∈ (f.genEigenspace μ) k, x ≠ 0

Tactic:
use x

Goal state after:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
h : f.HasUnifEigenvector μ k x
⊢ x ∈ (f.genEigenspace μ) k ∧ x ≠ 0
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
inst✝⁹ : DecidableEq ι
R : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
N₁ : ι → Submodule R M₁
h₁ : IsInternal N₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
N₂ : ι → Submodule R M₂
h₂ : IsInternal N₂
κ₁ : ι → Type u_7
κ₂ : ι → Type u_8
inst✝³ : (i : ι) → Fintype (κ₁ i)
inst✝² : ∀ (i : ι), Finite (κ₂ i)
inst✝¹ : (i : ι) → DecidableEq (κ₁ i)
inst✝ : Fintype ι
b₁ : (i : ι) → Basis (κ₁ i) R ↥(N₁ i)
b₂ : (i : ι) → Basis (κ₂ i) R ↥(N₂ i)
f : M₁ →ₗ[R] M₂
hf : ∀ (i : ι), MapsTo ⇑f ↑(N₁ i) ↑(N₂ i)
i : ι
snd✝¹ : κ₂ i
j : ι
snd✝ : κ₁ j
⊢ ((h₂.collectedBasis b₂).repr (f ((h₁.collectedBasis b₁) ⟨j, snd✝⟩))) ⟨i, snd✝¹⟩ =
    if h : i = j then ((b₂ i).repr ((f.restrict ⋯) ((b₁ i) (cast ⋯ snd✝)))) snd✝¹ else 0

Tactic:
rcases eq_or_ne i j with rfl | hij

Goal state after:
case inl
ι : Type u_1
inst✝⁹ : DecidableEq ι
R : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
N₁ : ι → Submodule R M₁
h₁ : IsInternal N₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
N₂ : ι → Submodule R M₂
h₂ : IsInternal N₂
κ₁ : ι → Type u_7
κ₂ : ι → Type u_8
inst✝³ : (i : ι) → Fintype (κ₁ i)
inst✝² : ∀ (i : ι), Finite (κ₂ i)
inst✝¹ : (i : ι) → DecidableEq (κ₁ i)
inst✝ : Fintype ι
b₁ : (i : ι) → Basis (κ₁ i) R ↥(N₁ i)
b₂ : (i : ι) → Basis (κ₂ i) R ↥(N₂ i)
f : M₁ →ₗ[R] M₂
hf : ∀ (i : ι), MapsTo ⇑f ↑(N₁ i) ↑(N₂ i)
i : ι
snd✝¹ : κ₂ i
snd✝ : κ₁ i
⊢ ((h₂.collectedBasis b₂).repr (f ((h₁.collectedBasis b₁) ⟨i, snd✝⟩))) ⟨i, snd✝¹⟩ =
    if h : i = i then ((b₂ i).repr ((f.restrict ⋯) ((b₁ i) (cast ⋯ snd✝)))) snd✝¹ else 0

case inr
ι : Type u_1
inst✝⁹ : DecidableEq ι
R : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
N₁ : ι → Submodule R M₁
h₁ : IsInternal N₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
N₂ : ι → Submodule R M₂
h₂ : IsInternal N₂
κ₁ : ι → Type u_7
κ₂ : ι → Type u_8
inst✝³ : (i : ι) → Fintype (κ₁ i)
inst✝² : ∀ (i : ι), Finite (κ₂ i)
inst✝¹ : (i : ι) → DecidableEq (κ₁ i)
inst✝ : Fintype ι
b₁ : (i : ι) → Basis (κ₁ i) R ↥(N₁ i)
b₂ : (i : ι) → Basis (κ₂ i) R ↥(N₂ i)
f : M₁ →ₗ[R] M₂
hf : ∀ (i : ι), MapsTo ⇑f ↑(N₁ i) ↑(N₂ i)
i : ι
snd✝¹ : κ₂ i
j : ι
snd✝ : κ₁ j
hij : i ≠ j
⊢ ((h₂.collectedBasis b₂).repr (f ((h₁.collectedBasis b₁) ⟨j, snd✝⟩))) ⟨i, snd✝¹⟩ =
    if h : i = j then ((b₂ i).repr ((f.restrict ⋯) ((b₁ i) (cast ⋯ snd✝)))) snd✝¹ else 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k✝ : I → R
hk✝ : ∀ (i : I), e' i * e' i - e' i = e₀ * k✝ i
k : R
hk : ∑ i, e' i - 1 = e₀ * k
⊢ ∑ i, Option.rec e₀ ((1 - e₀) • e') i = 1

Tactic:
simp only [Fintype.sum_option, Pi.smul_apply, smul_eq_mul, ← Finset.mul_sum,
      sub_eq_iff_eq_add.mp hk]

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k✝ : I → R
hk✝ : ∀ (i : I), e' i * e' i - e' i = e₀ * k✝ i
k : R
hk : ∑ i, e' i - 1 = e₀ * k
⊢ e₀ + (1 - e₀) * (e₀ * k + 1) = 1
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ V₁ V₂ V₃ V₄ V₅ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
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₄
Vs : Fin (Nat.succ 0).succ.succ.succ.succ.succ → Type u₀ := ![V₀, V₁, V₂, V₃, V₄, V₅]
this✝¹ : (i : Fin 6) → AddCommGroup (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁷
    | 1 => inst✝¹⁴
    | 2 => inst✝¹¹
    | 3 => inst✝⁸
    | 4 => inst✝⁵
    | 5 => inst✝²
this✝ : (i : Fin 6) → Module k (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁶
    | 1 => inst✝¹³
    | 2 => inst✝¹⁰
    | 3 => inst✝⁷
    | 4 => inst✝⁴
    | 5 => inst✝¹
this : ∀ (i : Fin 6), FiniteDimensional k (Vs i)
fs : (i : Fin 5) → Vs i.castSucc →ₗ[k] Vs i.succ :=
  fun i ↦
    match i with
    | 0 => f₀
    | 1 => f₁
    | 2 => f₂
    | 3 => f₃
    | 4 => f₄
⊢ ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0

Tactic:
simpa [Fin.sum_univ_six] using! Module.sum_neg_one_pow_finrank_eq_zero_of_exact Vs fs inj
    (fun i ↦ by fin_cases i; exacts [exact₁, exact₂, exact₃, exact₄]) surj

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

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n✝ : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ x * (x ^ n.succ)⁻¹ = (x ^ n.succ)⁻¹ * x

Tactic:
pow_succ',

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n✝ : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ x * (x * x ^ n)⁻¹ = (x * x ^ n)⁻¹ * x
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ Red w (invRev (reduce (invRev w)))

Tactic:
have : Red (invRev (invRev w)) (invRev (reduce (invRev w))) := reduce.red.invRev

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
this : Red (invRev (invRev w)) (invRev (reduce (invRev w)))
⊢ Red w (invRev (reduce (invRev w)))
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff + r
hr : map (algebraMap R K) r = 0
hm : m = 0
hg' : ¬g.natDegree = 0
⊢ False

Tactic:
apply hgP

Goal state after:
case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ⋯
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := ⋯
hg : g = C g.leadingCoeff + r
hr : map (algebraMap R K) r = 0
hm : m = 0
hg' : ¬g.natDegree = 0
⊢ g.leadingCoeff ∈ P
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case refine_1
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : CommRing U
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : Algebra R U
inst✝⁵ : Algebra S U
inst✝⁴ : Algebra T U
inst✝³ : IsScalarTower S T U
inst✝² : IsScalarTower R T U
inst✝¹ : IsIntegralClosure S R T
inst✝ : IsIntegrallyClosedIn T U
⊢ Function.Injective ⇑((algebraMap T U).comp (algebraMap S T))

Tactic:
exact (IsIntegralClosure.algebraMap_injective T T U).comp
      (IsIntegralClosure.algebraMap_injective S R T)

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sum

Goal state before:
pp: case inl
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✝¹ : SMulCommClass M N α
inst✝ : SMulCommClass M N β
a : M
b : N
val✝ : α
⊢ a • b • inl val✝ = b • a • inl val✝

pp: case inr
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✝¹ : SMulCommClass M N α
inst✝ : SMulCommClass M N β
a : M
b : N
val✝ : β
⊢ a • b • inr val✝ = b • a • inr val✝

Tactic:
exacts [congr_arg inl (smul_comm _ _ _), congr_arg inr (smul_comm _ _ _)]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ normSq (a + b) = normSq a + (a * star b).re + ((b * star a).re + normSq b)

Tactic:
by
      simp_rw [normSq_def, star_add, add_mul, mul_add, re_add]

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

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
s : Set M
x : M
⊢ x ∈ closure s ↔ x ∈ s ∨ ∃ y, ∃ z ∈ s, y * z = x

Tactic:
← SetLike.mem_coe,

Goal state after:
M : Type u_1
inst✝ : Semigroup M
s : Set M
x : M
⊢ x ∈ ↑(closure s) ↔ x ∈ s ∨ ∃ y, ∃ z ∈ s, y * z = x
Module: Mathlib.Algebra.Group.Ideal

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
x : M
⊢ x ∈ closure s ↔ ∃ y, ∃ z ∈ s, y * z = x

Tactic:
← SetLike.mem_coe,

Goal state after:
M : Type u_1
inst✝ : Monoid M
s : Set M
x : M
⊢ x ∈ ↑(closure s) ↔ ∃ y, ∃ z ∈ s, y * z = x
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: case mul
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x✝ x y : M
hx : x ∈ closure (Set.range f)
hy : y ∈ closure (Set.range f)
hx' : ∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2
hy' : ∃ a, y = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∃ a, x * y = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'
    use v + w
    rw [Finsupp.prod_add_index]
    · simp
    · simp [zpow_add]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommGroup M
x : M
s : Set M
inst✝ : Fintype ↑s
⊢ x ∈ closure s ↔ ∃ a, x = ∏ i, ↑i ^ a i

Tactic:
conv_lhs => rw [← Subtype.range_coe (s := s)]
  exact mem_closure_range_iff_of_fintype

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: a b : ℤ
⊢ closure {a} ⊔ closure {b} = closure {a, b}

Tactic:
← closure_union,

Goal state after:
a b : ℤ
⊢ closure ({a} ∪ {b}) = closure {a, b}
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
x : M
s : Set M
inst✝ : Fintype ↑s
⊢ x ∈ closure s ↔ ∃ a, x = ∏ i, ↑i ^ a i

Tactic:
conv_lhs => rw [← Subtype.range_coe (s := s)]
  exact mem_closure_range_iff_of_fintype

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

Goal state before:
pp: case inl
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ ((snd G₀ H₀).comp (inl G₀ H₀)) 0 = 1 0

Tactic:
simp_all [WithZero.withZeroUnitsEquiv, snd, inl]

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

Goal state before:
pp: case inr
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
w✝ : G₀ˣ
⊢ ((snd G₀ H₀).comp (inl G₀ H₀)) ↑w✝ = 1 ↑w✝

Tactic:
simp_all [WithZero.withZeroUnitsEquiv, snd, inl]

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

Goal state before:
pp: case a
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
x✝ : ∃ a, ¬f a = 0 ∧ ∃ x, f a * ↑y = f x
a : A
ha : f a ≠ 0
x : A
hv : f x ≠ 0
v : Bˣ := ⋯
hv₀ : f x = ↑v
u : Bˣ := ⋯
ha₀ : f a = ↑u
hy : u⁻¹ * v = y
⊢ ↑v ∈ range ⇑f

Tactic:
use x

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f : P.Hom Q
⊢ P.p ≫ f.f = f.f ≫ Q.p

Tactic:
rw [p_comp, comp_p]

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete C
⊢ IsIdempotentComplete Cᵒᵖᵒᵖ

Tactic:
isIdempotentComplete_iff_of_equivalence (opOpEquivalence C)

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete C
⊢ IsIdempotentComplete C
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ δ i ≫ δ j.succ = δ j ≫ δ i.castSucc

Tactic:
ext k
  dsimp [δ, Fin.succAbove]
  rcases i with ⟨i, _⟩
  rcases j with ⟨j, _⟩
  rcases k with ⟨k, _⟩
  split_ifs <;> · simp at * <;> lia

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
P✝ Q : Karoubi (J ⥤ C)
f : P✝ ⟶ Q
X : J
P : Karoubi (J ⥤ C)
j j' : J
φ : j ⟶ j'
⊢ P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ

Tactic:
have h := congr_app P.idem j

Goal state after:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
P✝ Q : Karoubi (J ⥤ C)
f : P✝ ⟶ Q
X : J
P : Karoubi (J ⥤ C)
j j' : J
φ : j ⟶ j'
h : (P.p ≫ P.p).app j = P.p.app j
⊢ P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 2
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a

Tactic:
refine .inl ⟨1, ?_⟩

Goal state after:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 2
⊢ f = δ 1
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
Y' : SimplicialObject C
p : Y ⟶ Y'
n : ℕ
⊢ (H.h (Fin.last n) ≫ p.app (op ⦋n + 1⦌)) ≫ Y'.δ (Fin.last (n + 1)) = (f ≫ p).app (op ⦋n⦌)

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

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
⊢ ofSection x = range (yonedaEquiv.symm x)

Tactic:
ext U y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U ↔ y ∈ (range (yonedaEquiv.symm x)).obj U
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
⊢ ofSection x = range (uliftYonedaEquiv.symm x)

Tactic:
ext U y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U ↔ y ∈ (range (uliftYonedaEquiv.symm x)).obj U
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case h₁
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
F : Arrow C
A : X ⟶ F.augmentedCechNerve
x : SimplexCategoryᵒᵖ
⊢ (equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).left.app x = A.left.app x

Tactic:
refine WidePullback.hom_ext _ _ _ (fun j => ?_) ?_

Goal state after:
case h₁.refine_1
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
F : Arrow C
A : X ⟶ F.augmentedCechNerve
x : SimplexCategoryᵒᵖ
j : Fin ((Opposite.unop x).len + 1)
⊢ (equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).left.app x ≫ WidePullback.π (fun x ↦ F.hom) j =
    A.left.app x ≫ WidePullback.π (fun x ↦ F.hom) j

case h₁.refine_2
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
F : Arrow C
A : X ⟶ F.augmentedCechNerve
x : SimplexCategoryᵒᵖ
⊢ ((equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).left.app x ≫ WidePullback.base fun x ↦ F.hom) =
    A.left.app x ≫ WidePullback.base fun x ↦ F.hom
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
⊢ X.S

Tactic:
exact S.mk x

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

Goal state before:
pp: X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f
x : X _⦋m⦌
⊢ ofSimplex ((ConcreteCategory.hom (X.map f.op)) x) = ofSimplex x

Tactic:
refine le_antisymm (ofSimplex_map_le f x) ?_

Goal state after:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f
x : X _⦋m⦌
⊢ ofSimplex x ≤ ofSimplex ((ConcreteCategory.hom (X.map f.op)) x)