mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

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

pp: case some.inr
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

Tactic:
· simp [*, squashSeq]

Goal state after:
case some.inr
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case some.inr.some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
val✝ : Pair K
s_succ_mth_eq : s.get? (m + 1) = some val✝
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

Tactic:
· simp [*, squashSeq]

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
this : ¬n + 2 ≤ 1
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
have not_terminatedAt_n : ¬g.TerminatedAt n := Or.resolve_left hyp this

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
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case succ
K : Type u_1
v : K
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
conts : Pair K := g.contsAux (n' + 1 + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
this : IntFractPair.stream v (n' + 1) ≠ none
⊢ n' + 1 = 0 ∨ ¬g.TerminatedAt (n' + 1 - 1)

Tactic:
have : ¬g.TerminatedAt n' :=
          (not_congr of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none).2 this

Goal state after:
case succ
K : Type u_1
v : K
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
conts : Pair K := g.contsAux (n' + 1 + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
this✝ : IntFractPair.stream v (n' + 1) ≠ none
this : ¬g.TerminatedAt n'
⊢ n' + 1 = 0 ∨ ¬g.TerminatedAt (n' + 1 - 1)
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
I : Type u_3
e : I → R
inst✝¹ : Fintype I
J : Type u_4
inst✝ : Fintype J
i : J ≃ I
⊢ CompleteOrthogonalIdempotents (e ∘ ⇑i) ↔ CompleteOrthogonalIdempotents e

Tactic:
simp only [completeOrthogonalIdempotents_iff, OrthogonalIdempotents.equiv, Function.comp_apply,
    Fintype.sum_equiv i _ e (fun _ ↦ rfl)]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Type u_3
e : I → R
inst✝ : Fintype I
he : OrthogonalIdempotents e
⊢ none.elim (1 - ∑ i, e i) e + ∑ i, (some i).elim (1 - ∑ i, e i) e = 1

Tactic:
exact sub_add_cancel _ _

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

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this✝ : Nonempty { l // ↑l ≤ k }
this : Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ ((f - μ • 1) ^ ↑i).ker
⊢ x ∈ ⨆ l, ⨆ (_ : ↑l ≤ k), ((f - μ • 1) ^ l).ker ↔ ∃ l, ↑l ≤ k ∧ x ∈ ((f - μ • 1) ^ l).ker

Tactic:
LinearMap.mem_ker,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this✝ : Nonempty { l // ↑l ≤ k }
this : Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ ((f - μ • 1) ^ ↑i).ker
⊢ x ∈ ⨆ l, ⨆ (_ : ↑l ≤ k), ((f - μ • 1) ^ l).ker ↔ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) x = 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
this✝ : Nonempty { l // ↑l ≤ k }
this : Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ ((f - μ • 1) ^ ↑i).ker
⊢ (∃ i, x ∈ ((f - μ • 1) ^ ↑i).ker) ↔ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) x = 0

Tactic:
LinearMap.mem_ker,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this✝ : Nonempty { l // ↑l ≤ k }
this : Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ ((f - μ • 1) ^ ↑i).ker
⊢ (∃ i, ((f - μ • 1) ^ ↑i) x = 0) ↔ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) x = 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
x : M
⊢ x ∈ (f - μ • 1).ker ↔ f x = μ • x

Tactic:
LinearMap.mem_ker,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
⊢ (f - μ • 1) x = 0 ↔ f x = μ • x
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
x : M
⊢ x ∈ LinearMap.ker 1 ↔ x = 0

Tactic:
LinearMap.mem_ker,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
⊢ 1 x = 0 ↔ x = 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
⊢ f.eigenspace μ = (f - μ • 1).ker

Tactic:
eigenspace,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ (f.genEigenspace μ) 1 = (f - μ • 1).ker
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ r ∈ corner e ↔ e * r = r

Tactic:
mem_corner_iff idem,

Goal state after:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ e * r = r ∧ r * e = r ↔ e * r = r
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 : (i : I) → ⋯.Corner
i : I
⊢ ↑((fun r i ↦ ⟨(fun x ↦ e i * x * e i) r, ⋯⟩) ((fun r ↦ ∑ i, ↑(r i)) r) i) = ↑(r i)

Tactic:
simp_rw [Finset.mul_sum, Finset.sum_mul]
    rw [Finset.sum_eq_single i _ (by simp at ·)]
    · have ⟨r', eq⟩ := (r i).2
      rw [← eq]; simp_rw [← mul_assoc, (he.idem i).eq, mul_assoc, (he.idem i).eq]
    · intro j _ ne; have ⟨r', eq⟩ := (r j).2
      rw [← eq]; simp_rw [← mul_assoc, he.ortho ne.symm, zero_mul]

Goal state after:
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: case refine_3
R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : TrivSqZeroExt A A
⊢ ε ∈ (inlAlgHom R A A).range ⊔ R[ ε]

Tactic:
refine le_sup_right (α := Subalgebra R _) <| subset_adjoin <| Set.mem_singleton ε

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : DecidableEq α
x : α × Bool
n : ℕ
ih : reduce (List.replicate n x) = List.replicate n x
⊢ (List.casesOn (reduce (List.replicate n x)) [x] fun hd tl ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate n x

Tactic:
ih

Goal state after:
case succ
α : Type u_1
inst✝ : DecidableEq α
x : α × Bool
n : ℕ
ih : reduce (List.replicate n x) = List.replicate n x
⊢ (List.casesOn (List.replicate n x) [x] fun hd tl ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate n x
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
L3 : List (α × Bool)
x✝¹ : α
x✝ : Bool
h : reduce [] = [] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: L3
⊢ p

Tactic:
injections

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
L3 : List (α × Bool)
x✝¹ : α
x✝ : Bool
head✝ : α × Bool
tail✝ : List (α × Bool)
h : reduce [] = head✝ :: tail✝ ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: L3
⊢ p

Tactic:
injections

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

Tactic:
injections

Goal state after:
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)
fst_eq✝¹ : x = x'
snd_eq✝¹ : b = b'
tail_eq✝ : tail = L3
fst_eq✝ : y = x'
snd_eq✝ : c = !b'
⊢ p
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝¹ : Applicative m
F : α → m β
inst✝ : LawfulApplicative m
x✝¹ y✝ : FreeSemigroup α
x✝ : α
L1 : List α
y : α
L2 : List α
hd : α
tl : List α
ih :
  ∀ (x : α),
    traverse F ({ head := x, tail := tl } * { head := y, tail := L2 }) =
      (fun x1 x2 ↦ x1 * x2) <$> traverse F { head := x, tail := tl } <*> traverse F { head := y, tail := L2 }
x : α
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure <$> F x <*> traverse F ({ head := hd, tail := tl } * { head := y, tail := L2 }) =
    (fun x1 x2 ↦ x1 * x2) <$> ((fun x1 x2 ↦ x1 * x2) <$> pure <$> F x <*> traverse F { head := hd, tail := tl }) <*>
      traverse F { head := y, tail := L2 }

Tactic:
ih

Goal state after:
α β : Type u
m : Type u → Type u
inst✝¹ : Applicative m
F : α → m β
inst✝ : LawfulApplicative m
x✝¹ y✝ : FreeSemigroup α
x✝ : α
L1 : List α
y : α
L2 : List α
hd : α
tl : List α
ih :
  ∀ (x : α),
    traverse F ({ head := x, tail := tl } * { head := y, tail := L2 }) =
      (fun x1 x2 ↦ x1 * x2) <$> traverse F { head := x, tail := tl } <*> traverse F { head := y, tail := L2 }
x : α
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure <$> F x <*>
      ((fun x1 x2 ↦ x1 * x2) <$> traverse F { head := hd, tail := tl } <*> traverse F { head := y, tail := L2 }) =
    (fun x1 x2 ↦ x1 * x2) <$> ((fun x1 x2 ↦ x1 * x2) <$> pure <$> F x <*> traverse F { head := hd, tail := tl }) <*>
      traverse F { head := y, tail := L2 }
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ (of a ^ n).norm = n

Tactic:
norm,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ (of a ^ n).toWord.length = n
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
h : R[X]
hf_lC : (algebraMap R K) (g * h).leadingCoeff ≠ 0
hf_prim : (g * h).IsPrimitive
hfmodP : map (algebraMap R K) (g * h) = C ((algebraMap R K) (g * h).leadingCoeff) * map (algebraMap R K) q ^ p
⊢ ¬(algebraMap R K) g.leadingCoeff = 0

Tactic:
simp only [leadingCoeff_mul, map_mul, ne_eq, mul_eq_zero, not_or] at hf_lC

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
h : R[X]
hf_prim : (g * h).IsPrimitive
hfmodP : map (algebraMap R K) (g * h) = C ((algebraMap R K) (g * h).leadingCoeff) * map (algebraMap R K) q ^ p
hf_lC : ¬(algebraMap R K) g.leadingCoeff = 0 ∧ ¬(algebraMap R K) h.leadingCoeff = 0
⊢ ¬(algebraMap R K) g.leadingCoeff = 0
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
⊢ y ^ (p.scaleRoots x).natDegree ∈ span {x}

Tactic:
refine
    (scaleRoots.isWeaklyEisensteinAt _
          (Ideal.mem_span_singleton.mpr <| dvd_refl x)).pow_natDegree_le_of_root_of_monic_mem
      ?_ ((monic_scaleRoots_iff x).mpr hp) _ le_rfl

Goal state after:
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
⊢ (p.scaleRoots x).IsRoot y
Module: Mathlib.Algebra.GCDMonoid.IntegrallyClosed

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : IsGCDMonoid R
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
⊢ ∃ y, (algebraMap R (FractionRing R)) y = X

Tactic:
cases h
    obtain ⟨x, y, hg, he⟩ := IsLocalization.surj_of_gcd_domain (nonZeroDivisors R) X
    have :=
      Polynomial.dvd_pow_natDegree_of_eval₂_eq_zero (IsFractionRing.injective R <| FractionRing R)
        hp₁ y x _ hp₂ (by rw [mul_comm, he])
    have : IsUnit y := by
      rw [isUnit_iff_dvd_one, ← one_pow]
      exact
        (dvd_gcd this <| dvd_refl y).trans
          (gcd_pow_left_dvd_pow_gcd.trans <| pow_dvd_pow_of_dvd (isUnit_iff_dvd_one.1 hg) _)
    use x * (this.unit⁻¹ :)
    rw [map_mul]
    have coe_map_inv :=
      Units.coe_map_inv ((algebraMap R (FractionRing R) : R →* FractionRing R)) this.unit
    simp only [MonoidHom.coe_coe] at coe_map_inv
    rw [← coe_map_inv, eq_comm, Units.eq_mul_inv_iff_mul_eq]
    exact he

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a + star a).re = (↑(2 * a.re + c₂ * a.imI)).re

Tactic:
simp [two_mul]

Goal state after:
case re
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ a.re + (a.re + c₂ * a.imI) = a.re + a.re + c₂ * a.imI
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a + star a).imI = (↑(2 * a.re + c₂ * a.imI)).imI

Tactic:
simp [two_mul]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imJ
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a + star a).imJ = (↑(2 * a.re + c₂ * a.imI)).imJ

Tactic:
simp [two_mul]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imK
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a + star a).imK = (↑(2 * a.re + c₂ * a.imI)).imK

Tactic:
simp [two_mul]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
c₁ c₂ c₃ : R
inst✝ : Infinite R
⊢ #ℍ[R,c₁,c₂,c₃] = #R

Tactic:
mk_quaternionAlgebra,

Goal state after:
R : Type u_1
c₁ c₂ c₃ : R
inst✝ : Infinite R
⊢ #R ^ 4 = #R
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
n : ℕ
x✝¹ : M → G
x✝ : M
⊢ (fwdDiffₗ M G h ^ n) x✝¹ x✝ = Δ_[h]^[n] x✝¹ x✝

Tactic:
rw [Module.End.pow_apply, coe_fwdDiffₗ]

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

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
⊢ Δ_[h]^[n] f y = ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h)

Tactic:
have : fwdDiffₗ M G h = shiftₗ M G h - 1 := by simp only [shiftₗ, add_sub_cancel_right]
  rw [← coe_fwdDiffₗ, this, ← Module.End.pow_apply]
  -- use binomial theorem `Commute.add_pow` to expand this
  have : Commute (shiftₗ M G h) (-1) := (Commute.one_right _).neg_right
  convert congr_fun (LinearMap.congr_fun (this.add_pow n) f) y
  · simp only [sub_eq_add_neg]
  · rw [LinearMap.sum_apply, sum_apply]
    congr 1 with k
    have : ((-1) ^ (n - k) * n.choose k : Module.End ℤ (M → G))
              = ↑((-1) ^ (n - k) * n.choose k : ℤ) := by norm_cast
    rw [mul_assoc, Module.End.mul_apply, this, Module.End.intCast_apply, map_smul,
      Pi.smul_apply, shiftₗ_pow_apply]

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

Goal state before:
pp: case one
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
⊢ ∃ a, 1 = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
use 0; simp

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

Goal state before:
pp: case one
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ ∃ a, 1 = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
use 0; simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M : Submonoid G
hMp : M.IsMulPointed
hMs : M.IsMulSpanning
N : Submonoid G
hN : N.IsMulPointed
h : M ≤ N
⊢ N ≤ M

Tactic:
rw [SetLike.le_def] at h ⊢; aesop

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

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := e.mul
⊢ SemigroupWithZero α

Tactic:
let zero := e.zero

Goal state after:
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := e.mul
zero : Zero α := e.zero
⊢ SemigroupWithZero α
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
⊢ MulZeroClass α

Tactic:
let zero := e.zero

Goal state after:
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := e.zero
⊢ MulZeroClass α
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
⊢ MulZeroOneClass α

Tactic:
let zero := e.zero

Goal state after:
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := e.zero
⊢ MulZeroOneClass α
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : f.ValueGroup₀
⊢ ∃ a, (restrict₀ f) a = 0

Tactic:
use 0; simp

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X Y : FintypeCat
f : X ⟶ Y
x : (uSwitch.obj X).obj
⊢ (ConcreteCategory.hom f) ((Fintype.equivFin X.obj).symm x.down) =
    (Fintype.equivFin Y.obj).symm
      ((ConcreteCategory.hom
            (homMk
              (ULift.up ∘
                ⇑(Fintype.equivFin Y.obj) ∘
                  ⇑(ConcreteCategory.hom f.hom) ∘ ⇑(Fintype.equivFin X.obj).symm ∘ ULift.down)))
          x).down

Tactic:
rw [homMk_apply]

Goal state after:
X Y : FintypeCat
f : X ⟶ Y
x : (uSwitch.obj X).obj
⊢ (ConcreteCategory.hom f) ((Fintype.equivFin X.obj).symm x.down) =
    (Fintype.equivFin Y.obj).symm
      ((ULift.up ∘
            ⇑(Fintype.equivFin Y.obj) ∘ ⇑(ConcreteCategory.hom f.hom) ∘ ⇑(Fintype.equivFin X.obj).symm ∘ ULift.down)
          x).down
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n m : SimplexCategory
i : Fin (m.len + 1)
⊢ n.const m i = n.const ⦋0⦌ 0 ≫ ⦋0⦌.const m i

Tactic:
rw [const_comp]

Goal state after:
n m : SimplexCategory
i : Fin (m.len + 1)
⊢ n.const m i = n.const m ((Hom.toOrderHom (⦋0⦌.const m i)) 0)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ ⦋0⦌.const ⦋l⦌ i ≫ subinterval j l hjl = ⦋0⦌.const ⦋n⦌ ⟨j + ↑i, ⋯⟩

Tactic:
rw [const_comp]

Goal state after:
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ ⦋0⦌.const ⦋n⦌ ((Hom.toOrderHom (subinterval j l hjl)) i) = ⦋0⦌.const ⦋n⦌ ⟨j + ↑i, ⋯⟩
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 Q : Karoubi (J ⥤ C)
f : (karoubiFunctorCategoryEmbedding J C).obj P ⟶ (karoubiFunctorCategoryEmbedding J C).obj Q
⊢ P.p ≫ { app := fun j ↦ (f.app j).f, naturality := ⋯ } ≫ Q.p = { app := fun j ↦ (f.app j).f, naturality := ⋯ }

Tactic:
by
        ext j
        exact (f.app j).comm

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

Goal state before:
pp: case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
X Y : J ⥤ C
⊢ ∀ (f : X ⟶ Y),
    (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).map f =
      eqToHom ⋯ ≫ ((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).map f ≫ eqToHom ⋯

Tactic:
f

Goal state after:
case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
X Y : J ⥤ C
f : X ⟶ Y
⊢ (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).map f =
    eqToHom ⋯ ≫ ((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
X : J ⥤ C
⊢ autoParam
    (∀ (X_1 Y : J) (f : X_1 ⟶ Y),
      ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map f =
        eqToHom ⋯ ≫ (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
intro j j' φ

Goal state after:
case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
X : J ⥤ C
j j' : J
φ : j ⟶ j'
⊢ ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map φ =
    eqToHom ⋯ ≫ (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map φ ≫ eqToHom ⋯
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h_map
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X Y : SimplicialObject C
⊢ ∀ (f : X ⟶ Y),
    (alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).map f =
      eqToHom ⋯ ≫ ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).map f ≫ eqToHom ⋯

Tactic:
f

Goal state after:
case h_map
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X Y : SimplicialObject C
f : X ⟶ Y
⊢ (alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).map f =
    eqToHom ⋯ ≫ ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).map f ≫ eqToHom ⋯