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

Goal state before:
pp: case succ
K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
⊢ pred_conts.a * (g.contsAux (n + 1 + 1)).b - pred_conts.b * (g.contsAux (n + 1 + 1)).a =
    ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0

Tactic:
let pB := pred_conts.b

Goal state after:
case succ
K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
⊢ pred_conts.a * (g.contsAux (n + 1 + 1)).b - pred_conts.b * (g.contsAux (n + 1 + 1)).a =
    ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ t
⊢ a' ∈ s

Tactic:
by rw [mem_unique ma h2]; exact h1

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

Goal state before:
pp: α : Type u
β : Type v
s1 s2 : Computation α
f : α → β
h1 : s1 ~ s2
⊢ map f s1 ~ map f s2

Tactic:
rw [← lift_eq_iff_equiv]

Goal state after:
α : Type u
β : Type v
s1 s2 : Computation α
f : α → β
h1 : s1 ~ s2
⊢ LiftRel (fun x1 x2 ↦ x1 = x2) (map f s1) (map f s2)
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

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

Tactic:
stream_succ_of_some ih hnz

Goal state after:
case succ.inr.inr
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
hnz : p.fr ≠ 0
⊢ some (IntFractPair.of p.fr⁻¹) = some (IntFractPair.of p.fr⁻¹)
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
inst✝ : FloorRing K
terminates : (of v).Terminates
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → v = (of v).convs b

Tactic:
obtain ⟨n, terminatedAt_n⟩ : ∃ n, (of v).TerminatedAt n := terminates

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
inst✝ : FloorRing K
n : ℕ
terminatedAt_n : (of v).TerminatedAt n
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → v = (of v).convs b
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim.nil.cons
α : Type u
SS✝ SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x : α
s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s SS, s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join)
    (nil.append (Seq.cons ((x, s), S) SS).join.join).destruct
    (nil.append (Seq.map join (Seq.cons ((x, s), S) SS)).join).destruct

Tactic:
cases s with
        | nil => simpa using ⟨_, _, rfl, rfl⟩
        | cons x s => simpa using ⟨Seq.cons x (append s (Seq.join S)), SS, by simp, by simp⟩

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

Goal state before:
pp: case inr.succ
K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
pa pb : K
s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }
g' : GenContFract K := g.squashGCF (n' + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
succ_n'th_contsAux_eq : pred_conts = g.contsAux (n' + 1)
ppred_conts : Pair K := g.contsAux n'
n'th_contsAux_eq : ppred_conts = g.contsAux n'
pA : K := pred_conts.a
⊢ g.convs (n' + 1 + 1) = (g.squashGCF (n' + 1)).convs (n' + 1)

Tactic:
let pB := pred_conts.b

Goal state after:
case inr.succ
K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
pa pb : K
s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }
g' : GenContFract K := g.squashGCF (n' + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
succ_n'th_contsAux_eq : pred_conts = g.contsAux (n' + 1)
ppred_conts : Pair K := g.contsAux n'
n'th_contsAux_eq : ppred_conts = g.contsAux n'
pA : K := pred_conts.a
pB : K := pred_conts.b
⊢ g.convs (n' + 1 + 1) = (g.squashGCF (n' + 1)).convs (n' + 1)
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case zero
K : Type u_1
v : K
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v 0 = some ifp_n
⊢ 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1

Tactic:
obtain rfl : IntFractPair.of v = ifp_n := by injection nth_stream_eq

Goal state after:
case zero
K : Type u_1
v : K
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
nth_stream_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)
⊢ 0 ≤ (IntFractPair.of v).fr ∧ (IntFractPair.of v).fr < 1
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
g : GenContFract K := of v
not_terminated : ¬g.partDens.TerminatedAt n
b : K
nth_partDen_eq : g.partDens.get? n = some b
this : 1 ≤ b
⊢ g.dens n ≤ b * g.dens n

Tactic:
by
        simpa using mul_le_mul_of_nonneg_right this zero_le_of_den

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

Goal state before:
pp: case inr
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_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
⊢ let g := of v;
  let B := (g.contsAux (n + 1)).b;
  let pB := (g.contsAux n).b;
  v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
let pB := pred_conts.b

Goal state after:
case inr
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_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
⊢ let g := of v;
  let B := (g.contsAux (n + 1)).b;
  let pB := (g.contsAux n).b;
  v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
s : Finset I
⊢ IsIdempotentElem (∑ i ∈ s, e i)

Tactic:
classical
  simp [IsIdempotentElem, Finset.sum_mul, Finset.mul_sum, he.mul_eq]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Free

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
i : ι
⊢ (basis A b).repr.symm (Finsupp.single i a) = a ⊗ₜ[R] b.repr.symm (Finsupp.single i 1)

Tactic:
by
  simp [basis, Equiv.uniqueProd_symm_apply, basisAux]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case succ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : f e₀ = e 0
h₅ : e₀ * ∑ i, e' i = 0
h₆ : (∑ i, e' i) * e₀ = 0
i : Fin (n + 1)
⊢ (⇑f ∘ (fun x ↦ x.elim e₀ e') ∘ ⇑(finSuccEquiv n).toEmbedding) i = e i

Tactic:
obtain ⟨_ | i, rfl⟩ := (finSuccEquiv n).symm.surjective i

Goal state after:
case succ.none
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : f e₀ = e 0
h₅ : e₀ * ∑ i, e' i = 0
h₆ : (∑ i, e' i) * e₀ = 0
⊢ (⇑f ∘ (fun x ↦ x.elim e₀ e') ∘ ⇑(finSuccEquiv n).toEmbedding) ((finSuccEquiv n).symm none) =
    e ((finSuccEquiv n).symm none)

case succ.some
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : f e₀ = e 0
h₅ : e₀ * ∑ i, e' i = 0
h₆ : (∑ i, e' i) * e₀ = 0
i : Fin n
⊢ (⇑f ∘ (fun x ↦ x.elim e₀ e') ∘ ⇑(finSuccEquiv n).toEmbedding) ((finSuccEquiv n).symm (some i)) =
    e ((finSuccEquiv n).symm (some i))
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
hfn : IsNilpotent f
μ : R
hf : f.HasUnifEigenvalue μ 1
m : M
hm : f.HasUnifEigenvector μ 1 m
⊢ IsNilpotent μ

Tactic:
obtain ⟨n : ℕ, hn : f ^ n = 0⟩ := hfn

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ : R
hf : f.HasUnifEigenvalue μ 1
m : M
hm : f.HasUnifEigenvector μ 1 m
n : ℕ
hn : f ^ n = 0
⊢ IsNilpotent μ
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
⊢ matrix n I ≤ matrix n J → I ≤ J

pp: case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
⊢ I ≤ J → matrix n I ≤ matrix n J

Tactic:
· intro le x xI
      specialize @le (of fun _ _ => x) (by simp [xI])
      simpa using le

Goal state after:
case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
⊢ I ≤ J → matrix n I ≤ matrix n J
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
Mmem : M ∈ (matrix n I).jacobson
p q : n
⊢ M p q ∈ I.jacobson

Tactic:
rw [mem_jacobson_iff]

Goal state after:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
Mmem : M ∈ (matrix n I).jacobson
p q : n
⊢ ∀ (y : R), ∃ z, z * y * M p q + z - 1 ∈ I
Module: Mathlib.RingTheory.Idempotents

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

Tactic:
by rintro ⟨r, rfl⟩; simp_rw [← mul_assoc, idem.eq, mul_assoc, idem.eq, true_and]

Goal state after:
Module: Mathlib.Algebra.Ring.MinimalAxioms

Goal state before:
pp: R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
a : R
⊢ 0 * a = (0 + 0) * a

Tactic:
rw [zero_add]

Goal state after:
Module: Mathlib.Algebra.Ring.MinimalAxioms

Goal state before:
pp: R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
⊢ a * 0 = a * (0 + 0)

Tactic:
rw [zero_add]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
inst✝¹ : Mul α
β : Type v
inst✝ : Semigroup β
f✝ f : α →ₙ* β
x : AssocQuotient α
⊢ ∀ (a b : α), AssocRel α a b → f a = f b

Tactic:
rintro a b (⟨c, d, e⟩ | ⟨c, d, e, f⟩) <;> simp only [map_mul, mul_assoc]

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

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X : Type v
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀

Tactic:
by
  cases subsingleton_or_nontrivial R
  · exact (cardinalMk_eq_one R X).trans_le (le_max_of_le_right one_le_aleph0)
  cases isEmpty_or_nonempty X
  · exact (cardinalMk_eq_lift R X).trans_le (le_max_of_le_left <| le_max_left _ _)
  · exact (cardinalMk_eq_max_lift R X).le

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
H : lift.{u, v} #↑(Set.range ⇑((FreeAlgebra.lift R) Subtype.val)) ≤ lift.{v, max u v} #(FreeAlgebra R { x // x ∈ s })
⊢ lift.{u, v} #↥(adjoin R s) ≤ max (max (lift.{v, u} #R) (lift.{u, v} #↑s)) ℵ₀

Tactic:
lift_id'.{v, u}

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
H : lift.{u, v} #↑(Set.range ⇑((FreeAlgebra.lift R) Subtype.val)) ≤ #(FreeAlgebra R { x // x ∈ s })
⊢ lift.{u, v} #↥(adjoin R s) ≤ max (max (lift.{v, u} #R) (lift.{u, v} #↑s)) ℵ₀
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:
Module.End.pow_apply,

Goal state after:
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✝
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: M : Type u_2
inst✝¹ : Mul M
s t : Set M
inst✝ : IsCancelMul M
⊢ Nat.card ↑(s * t) ≤ Nat.card ↑s * Nat.card ↑t

Tactic:
obtain h | h := (s * t).infinite_or_finite

Goal state after:
case inl
M : Type u_2
inst✝¹ : Mul M
s t : Set M
inst✝ : IsCancelMul M
h : (s * t).Infinite
⊢ Nat.card ↑(s * t) ≤ Nat.card ↑s * Nat.card ↑t

case inr
M : Type u_2
inst✝¹ : Mul M
s t : Set M
inst✝ : IsCancelMul M
h : (s * t).Finite
⊢ Nat.card ↑(s * t) ≤ Nat.card ↑s * Nat.card ↑t
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

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

Tactic:
obtain ⟨i, rfl⟩ := h

Goal state after:
case mem
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
i : ι
⊢ ∃ a, f i = a.prod fun x1 x2 ↦ f x1 ^ x2
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

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

Tactic:
obtain ⟨i, rfl⟩ := h

Goal state after:
case mem
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
i : ι
⊢ ∃ a, f i = a.prod fun x1 x2 ↦ f x1 ^ x2
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
⊢ y ∈ f.valueGroup ↔ ∃ a, f a ≠ 0 ∧ ∃ x, f x ≠ 0 ∧ f a * ↑y = f x

Tactic:
rw [mem_valueGroup_iff_of_comm]
  exact ⟨fun ⟨a, ha, x, hax⟩ ↦ ⟨a, ha, x, by aesop, hax⟩, fun ⟨a, ha, x, hx, hax⟩ ↦ ⟨a, ha, x, hax⟩⟩

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 := 0 } = { down := 0 }

pp: case neg
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 := 0 } = { down := 1 }

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 }

pp: case neg
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 := 1 }

Tactic:
any_goals rfl

Goal state after:
case neg
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 := 0 } = { down := 1 }

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 }
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ HasEqualizer (𝟙 X) p

Tactic:
have : HasKernel (𝟙 _ - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp)

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasKernel (𝟙 X - p)
⊢ HasEqualizer (𝟙 X) p
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ ((toKaroubi C).obj Y).p ≫ i ≫ P.p = i

Tactic:
by simp [← Category.assoc, h₁, ← h₂]

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

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete C → IsIdempotentComplete D

pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete D → IsIdempotentComplete C

Tactic:
· exact Equivalence.isIdempotentComplete ε

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete D → IsIdempotentComplete C
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case h.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ e.unop ≫ i.unop = 𝟙 (unop Y)

Tactic:
simp only [← unop_comp, h₁]
    rfl

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

Goal state before:
pp: case h.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ e.unop ≫ i.unop = 𝟙 (unop Y)

pp: case h.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ i.unop ≫ e.unop = p

Tactic:
· simp only [← unop_comp, h₁]
    rfl

Goal state after:
case h.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ i.unop ≫ e.unop = p