mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered J
F : J ⥤ Under X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i : J
s' : Cocone F :=
  { pt := Under.mk ((F.obj i).hom ≫ s.ι.app i), ι := { app := fun j ↦ Under.homMk (s.ι.app j) ⋯, naturality := ⋯ } }
f : ((Under.forget X).mapCocone c).pt ⟶ s.pt
hf : ∀ (j : J), Under.Hom.right (c.ι.app j) ≫ f = s.ι.app j
⊢ c.pt.hom ≫ f = s'.pt.hom

Tactic:
simp [s', ← hf]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Small

Goal state before:
pp: P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ R, Q R ∧ ∃ f, (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} P

Tactic:
let f (S : Σ R : Subtype Q', FGAlgCatSkeleton R) : CommRingCat := .of S.2.eval.obj

Goal state after:
P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ R, Q R ∧ ∃ f, (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (R : Subtype Q') × FGAlgCatSkeleton ↑↑R → CommRingCat := fun S ↦ of ↑(FGAlgCatSkeleton.eval (↑↑S.fst) S.snd).obj
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} P
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
hc' : IsColimit ((forget CommRingCat).mapCocone c)
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
n : ℕ
hn : ∃ f_1, Function.Surjective ⇑f_1 ∧ (ker f_1.toRingHom).FG
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
⊢ ∃ π, iP ≫ π = f ∧ Function.Surjective ⇑(ConcreteCategory.hom π) ∧ (ker (CommRingCat.Hom.hom π)).FG

Tactic:
by
    obtain ⟨π, h₁, h₂⟩ := hn
    exact ⟨CommRingCat.ofHom π, by ext1; exact π.comp_algebraMap, h₁, h₂⟩

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
⊢ Limits.HasFiniteProducts ((toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)

Tactic:
refine ⟨fun n ↦ ⟨fun D ↦ ?_⟩⟩
  have := hQp.createsFiniteProductsForget hQi R
  exact CategoryTheory.hasLimit_of_created D (Under.forget _ _ R)

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g)) ⟶ A := ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder
h' : (R.tensorProd S).obj (R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
⊢ PreservesLimit (parallelPair f g) (R.tensorProd S) ↔
    Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (toAlgHom f) (toAlgHom g))

Tactic:
rw [preservesLimit_iff_isLimit_mapCone hc, e.nonempty_congr,
    (Under.equalizerForkIsLimit _ _).nonempty_isLimit_iff_isIso_lift]

Goal state after:
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g)) ⟶ A := ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder
h' : (R.tensorProd S).obj (R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
⊢ IsIso ((Under.equalizerForkIsLimit ((R.tensorProd S).map f) ((R.tensorProd S).map g)).lift (Fork.ofι h' w')) ↔
    Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (toAlgHom f) (toAlgHom g))
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
T : Type u_3
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S T
inst✝⁵ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f g : A →ₐ[R] B
inst✝ : Module.Flat R T
h₁ : Function.Surjective ⇑(algebraMap S T)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T)
⊢ ↥(RingHom.ker (TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T))) ≃ₗ[A ⊗[R] S]
    A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))

Tactic:
let ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
    { __ := Algebra.TensorProduct.comm _ _ _, commutes' _ := rfl }

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
T : Type u_3
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S T
inst✝⁵ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f g : A →ₐ[R] B
inst✝ : Module.Flat R T
h₁ : Function.Surjective ⇑(algebraMap S T)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T)
ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
  let __spread.0 := TensorProduct.comm R A S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ ↥(RingHom.ker (TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T))) ≃ₗ[A ⊗[R] S]
    A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
⊢ (∃ k, k • p = z • r) ↔ ∃ k k_1, k_1 • p + ↑k • p * (↑z)⁻¹ = r

Tactic:
have hz' : (z : R) ≠ 0 := Int.cast_ne_zero.mpr hz

Goal state after:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
⊢ (∃ k, k • p = z • r) ↔ ∃ k k_1, k_1 • p + ↑k • p * (↑z)⁻¹ = r
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
⊢ z • ⟦a✝¹⟧ = z • ⟦a✝⟧ ↔ ∃ k, ⟦a✝¹⟧ = ⟦a✝⟧ + ↑(↑k • (p / ↑z))

Tactic:
simp_rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_add,
    QuotientAddGroup.eq_iff_sub_mem, ← smul_sub, ← sub_sub]

Goal state after:
case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
⊢ z • (a✝¹ - a✝) ∈ AddSubgroup.zmultiples p ↔ ∃ k, a✝¹ - a✝ - ↑k • (p / ↑z) ∈ AddSubgroup.zmultiples p
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
h : s.get? 0 = none
n : ℕ
⊢ s.get? n = nil.get? n

Tactic:
exact le_stable s (Nat.zero_le _) h

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

Goal state before:
pp: case none
α : Type u
s s' : Computation α
f0 : s.val 0 = none
h :
  (match none with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = s'.think

pp: case some
α : Type u
s s' : Computation α
a' : α
f0 : s.val 0 = some a'
h :
  (match some a' with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = s'.think

Tactic:
· injection h with h'
    rw [← h']
    obtain ⟨f, al⟩ := s
    apply Subtype.ext
    dsimp [think, tail]
    rw [← f0]
    exact (Stream'.eta f).symm

Goal state after:
case some
α : Type u
s s' : Computation α
a' : α
f0 : s.val 0 = some a'
h :
  (match some a' with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = s'.think
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case mpr
α : Type u
x : α
s : Seq α
n : ℕ
h : s.TerminatedAt n
⊢ (cons x s).Terminates

Tactic:
exact ⟨n + 1, cons_terminatedAt_succ_iff.mpr h⟩

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

Goal state before:
pp: α : Type u
s : Stream' α
n : ℕ
⊢ take (n + 1 + 1) s = take (n + 1) s ++ [s.get (n + 1)]

Tactic:
rw [take_succ, take_succ' n, ← List.cons_append, ← take_succ, get_tail]

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

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
h : m ≤ n
⊢ take m a <+: take n a

Tactic:
rw [(by simp [h] : a.take m = (a.take n).take m)]

Goal state after:
α : Type u
m n : ℕ
a : Stream' α
h : m ≤ n
⊢ List.take m (take n a) <+: take n a
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
m n : ℕ
h_mn : m < n
x : α
h_get : s.get? m = some x
⊢ x ∈ take n s

Tactic:
by
  induction m generalizing n s with
  | zero =>
    obtain ⟨l, hl⟩ := Nat.exists_add_one_eq.mpr h_mn
    rw [← hl, take, head_eq_some h_get]
    simp
  | succ k ih =>
    obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_lt h_mn
    have : ∃ y, s.get? 0 = some y := by
      apply ge_stable _ _ h_get
      simp
    obtain ⟨y, hy⟩ := this
    rw [take, head_eq_some hy]
    simp only [destruct_cons, List.mem_cons]
    right
    apply ih (by lia)
    rwa [get?_tail]

Goal state after:
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
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
⊢ pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0

Tactic:
have not_terminated_at_n : ¬TerminatedAt g n := Or.resolve_left hyp n.succ_ne_zero

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
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
⊢ pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
⊢ (match IntFractPair.stream v (Nat.succ 0) with
    | some x => some { a := 1, b := ↑x.b }
    | none => none) =
    (IntFractPair.stream v 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b })

Tactic:
split <;> simp_all only [Option.bind_some, Option.bind_none, Function.comp_apply]

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
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
⊢ 1 ≤ ifp_n.fr⁻¹

Tactic:
one_le_inv₀
    ((nth_stream_fr_nonneg nth_stream_eq).lt_of_ne' stream_nth_fr_ne_zero)

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
⊢ ifp_n.fr ≤ 1
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
this : ∀ ⦃b : K⦄, g.partDens.get? n = some b → b ≠ 0
⊢ g.convs (n + 1) = g'.convs n

Tactic:
exact succ_nth_conv_eq_squashGCF_nth_conv @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
inst✝ : DecidableEq K
ha : P.a ≠ 0
h3 : (Polynomial.map φ P.toPoly).Splits
hd : P.discr ≠ 0
⊢ (map φ P).roots.toFinset.card = 3

Tactic:
toFinset_card_of_nodup <| (discr_ne_zero_iff_roots_nodup ha h3).mp hd,

Goal state after:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝² : Field F
inst✝¹ : Field K
φ : F →+* K
inst✝ : DecidableEq K
ha : P.a ≠ 0
h3 : (Polynomial.map φ P.toPoly).Splits
hd : P.discr ≠ 0
⊢ (map φ P).roots.card = 3
Module: Mathlib.RingTheory.Finiteness.Prod

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
hM : Module.Finite R M
hN : Module.Finite R N
⊢ ⊤.FG

Tactic:
← Submodule.prod_top

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
hM : Module.Finite R M
hN : Module.Finite R N
⊢ (⊤.prod ⊤).FG
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ (x - x ^ 2) ^ n ∣
    (x - x * x) ^ n *
      ((∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) * (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1)) ^ n)

pp: case h
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute x (1 - x)

pp: case hbc
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) ((1 - x) ^ n)

pp: case h
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (1 - x) (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1))

Tactic:
← pow_two

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ (x - x ^ 2) ^ n ∣
    (x - x ^ 2) ^ n *
      ((∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) * (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1)) ^ n)

case h
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute x (1 - x)

case hbc
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) ((1 - x) ^ n)

case h
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (1 - x) (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1))
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
w✝ x✝² y✝ z✝ : R
h₁ : ∀ (i j : n), c (single i j w✝) (single i j x✝²)
h₂ : ∀ (i j : n), c (single i j y✝) (single i j z✝)
x✝¹ x✝ : n
⊢ c (single x✝¹ x✝ (w✝ + y✝)) (single x✝¹ x✝ (x✝² + z✝))

Tactic:
by simpa [single_add] using c.add (h₁ _ _) (h₂ _ _)

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_1.some.some
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
i j : I
h : some i ≠ some j
⊢ Option.rec e₀ ((1 - e₀) • e') (some i) * Option.rec e₀ ((1 - e₀) • e') (some j) = 0

Tactic:
obtain ⟨k, hk⟩ := Ideal.mem_span_singleton.mp
        (hfe₀.le (show f (e' i * e' j) = 0 by simp [he', he.1.2 (by simpa using h)]))

Goal state after:
case refine_1.some.some
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
i j : I
h : some i ≠ some j
k : R
hk : e' i * e' j = e₀ * k
⊢ Option.rec e₀ ((1 - e₀) • e') (some i) * Option.rec e₀ ((1 - e₀) • e') (some j) = 0
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:
rintro ⟨r, rfl⟩

Goal state after:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
r : R
⊢ e * (fun x ↦ e * x * e) r = (fun x ↦ e * x * e) r ∧ (fun x ↦ e * x * e) r * e = (fun x ↦ e * x * e) r
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
x : TrivSqZeroExt A A
hx : x ∈ ⊤
⊢ x ∈ (inlAlgHom R A A).range ⊔ R[ ε]

Tactic:
clear hx

Goal state after:
R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : TrivSqZeroExt A A
⊢ x ∈ (inlAlgHom R A A).range ⊔ R[ ε]
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 : ℕ
⊢ ¬1 / x = 1

Tactic:
div_eq_iff_mul_eq hx0,

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
⊢ ¬1 * x = 1
Module: Mathlib.Algebra.Free

Goal state before:
pp: case refine_1.left
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
a c d e f : α
⊢ Quot.mk (AssocRel α) (a * c * (d * (e * f))) = Quot.mk (AssocRel α) (a * (c * (d * (e * f))))

Tactic:
quot_mk_assoc

Goal state after:
case refine_1.left
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
a c d e f : α
⊢ Quot.mk (AssocRel α) (a * (c * (d * (e * f)))) = Quot.mk (AssocRel α) (a * (c * (d * (e * f))))
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ toFreeSemigroup.comp (map f) = (FreeSemigroup.map f).comp toFreeSemigroup

Tactic:
by ext1; rfl

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
⊢ (Magma.AssocQuotient.lift FreeMagma.toFreeSemigroup).comp
      (FreeSemigroup.lift (⇑Magma.AssocQuotient.of ∘ FreeMagma.of)) =
    MulHom.id (FreeSemigroup α)

Tactic:
by ext1; rfl

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case a
α : Type u
inst✝ : Nonempty α
⊢ #(FreeGroup α) ≤ max #α ℵ₀

Tactic:
apply (mk_le_of_injective (FreeGroup.toWord_injective (α := α))).trans_eq
    simp only [mk_list_eq_max_mk_aleph0, mk_prod, lift_uzero, mk_fintype, Fintype.card_bool,
      Nat.cast_ofNat, lift_ofNat]
    obtain hα | hα := lt_or_ge #α ℵ₀
    · simp only [hα.le, max_eq_right, max_eq_right_iff]
      exact (mul_lt_aleph0 hα natCast_lt_aleph0).le
    · rw [max_eq_left hα, max_eq_left (hα.trans <| Cardinal.le_mul_right two_ne_zero),
        Cardinal.mul_eq_left hα _ (by simp)]
      exact natCast_le_aleph0.trans hα

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: α : Type u_1
⊢ Set.range ⇑toFreeMonoid = {1}ᶜ

Tactic:
by
  ext x; grind [eq_one_or_toFreeMonoid x]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ s
a n : ℕ
⊢ (fun x ↦ x ∈ a +ᵥ s) n ↔ a ≤ n ∧ n - a ∈ s

Tactic:
by
    simp only [Set.mem_vadd_set, vadd_eq_add]; aesop

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

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
s : Set M
I : SemigroupIdeal M := { carrier := s ∪ univ * s, smul_mem' := ⋯ }
this : closure s = I
⊢ ↑(closure s) = s ∪ univ * s

Tactic:
by rw [this]; rfl

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

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

Tactic:
sum_apply,

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

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
this : ⇑invMonoidHom '' v '' baseOf v f ⊆ ⇑invMonoidHom '' ⇑invMonoidHom '' v '' baseOf v (invMonoidHom.comp f)
⊢ ⇑invMonoidHom ∘ v '' baseOf v f ⊆ v '' baseOf v (invMonoidHom.comp f)

Tactic:
← image_comp invMonoidHom invMonoidHom,

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
this : ⇑invMonoidHom '' v '' baseOf v f ⊆ ⇑invMonoidHom ∘ ⇑invMonoidHom '' v '' baseOf v (invMonoidHom.comp f)
⊢ ⇑invMonoidHom ∘ v '' baseOf v f ⊆ v '' baseOf v (invMonoidHom.comp f)
Module: Mathlib.Algebra.GroupWithZero.Conj

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
⊢ IsConj a b ↔ ∃ c, c ≠ 0 ∧ c * a * c⁻¹ = b

Tactic:
rw [IsConj, Units.exists_iff_ne_zero (p := (SemiconjBy · a b))]
  congr! 2 with c
  exact and_congr_right (mul_inv_eq_iff_eq_mul₀ · |>.symm)

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

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : IsLeftCancelMulZero α
hs : s.erase 0 = ∅
⊢ #s ≤ #(s * s)

pp: case inr
α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : IsLeftCancelMulZero α
hs : (s.erase 0).Nonempty
⊢ #s ≤ #(s * s)

Tactic:
· rw [erase_eq_empty_iff] at hs
    obtain rfl | rfl := hs <;> simp

Goal state after:
case inr
α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : IsLeftCancelMulZero α
hs : (s.erase 0).Nonempty
⊢ #s ≤ #(s * s)
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p

Tactic:
by
  constructor
  · intro _ X p hp
    rcases IsIdempotentComplete.idempotents_split X p hp with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
    exact
      ⟨Nonempty.intro
          { cone := Fork.ofι i (show i ≫ 𝟙 X = i ≫ p by rw [comp_id, ← h₂, ← assoc, h₁, id_comp])
            isLimit := by
              apply Fork.IsLimit.mk'
              intro s
              refine ⟨s.ι ≫ e, ?_⟩
              constructor
              · simp [h₂, ← Limits.Fork.condition s]
              · intro m hm
                rw [Fork.ι_ofι] at hm
                rw [← hm]
                simp only [assoc, h₁]
                exact (comp_id m).symm }⟩
  · intro h
    refine ⟨?_⟩
    intro X p hp
    have : HasEqualizer (𝟙 X) p := h X p hp
    refine ⟨equalizer (𝟙 X) p, equalizer.ι (𝟙 X) p,
      equalizer.lift p (show p ≫ 𝟙 X = p ≫ p by rw [hp, comp_id]), ?_, equalizer.lift_ι _ _⟩
    ext
    simp only [assoc, limit.lift_π,
      Fork.ofι_π_app, id_comp]
    rw [← equalizer.condition, comp_id]

Goal state after: