mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝⁴ : Fact κ.IsRegular
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
inst✝² : IsCardinalPresentable X κ
inst✝¹ : EssentiallySmall.{w, v_1, u_1} J
inst✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
i₁ i₂ : J
f₁ : X ⟶ F.obj i₁
f₂ : X ⟶ F.obj i₂
hf : f₁ ≫ c.ι.app i₁ = f₂ ≫ c.ι.app i₂
⊢ ∃ j u v, f₁ ≫ F.map u = f₂ ≫ F.map v

Tactic:
have := preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall X κ J
  have := isFiltered_of_isCardinalFiltered J κ
  exact exists_eq_of_preservesColimit_coyoneda hc f₁ f₂ hf

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝¹ : IsCardinalFiltered J κ
A : Type v'
inst✝ : Category.{u', v'} A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
this✝¹ : Small.{w, max u' v'} (Arrow A)
this✝ : Small.{w, v'} A
this : LocallySmall.{w, u', v'} A
e : A ≌ ShrinkHoms.{w} (Shrink.{w, v'} A) := (Shrink.equivalence A).trans (ShrinkHoms.equivalence (Shrink.{w, v'} A))
⊢ Cocone F

Tactic:
exact (Cocone.equivalenceOfReindexing e.symm (Iso.refl _)).inverse.obj
    (nonempty_cocone (κ := κ) (e.inverse ⋙ F) (by simpa)).some

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
hs : Cardinal.mk ι < κ
x✝ : { x // x ∈ Set.range f }
⊢ ∃ a, (fun i ↦ ⟨f i, ⋯⟩) a = x✝

Tactic:
by aesop

Goal state after:
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)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := ⋯
D : MulticospanIndex J' J := ⋯
c' : Cocone D.multicospan
⊢ CommRingCat.Hom.hom (a ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ())))) =
    CommRingCat.Hom.hom (b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))

Tactic:
apply hf.ext

Goal state after:
case h₁
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)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := ⋯
D : MulticospanIndex J' J := ⋯
c' : Cocone D.multicospan
⊢ (CommRingCat.Hom.hom (a ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ()))))).comp (CommRingCat.Hom.hom f) =
    (CommRingCat.Hom.hom (b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))).comp (CommRingCat.Hom.hom f)

case h₂
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)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := ⋯
D : MulticospanIndex J' J := ⋯
c' : Cocone D.multicospan
⊢ ∀ x ∈ hf.finset,
    (CommRingCat.Hom.hom (a ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ()))))) x =
      (CommRingCat.Hom.hom (b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))) x
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : J ⥤ Under R
inst✝ : PreservesColimit (F ⋙ Under.forget R) (forget CommRingCat)
c : Cocone F
hc : IsColimit c
⊢ ∀ (i j : J) (xi : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj i))
    (xj : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj j)),
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app i)) xi =
        (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map f)) xi =
          (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map g)) xj

Tactic:
intro i j f₁ f₂ e

Goal state after:
case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : J ⥤ Under R
inst✝ : PreservesColimit (F ⋙ Under.forget R) (forget CommRingCat)
c : Cocone F
hc : IsColimit c
i j : J
f₁ : (F ⋙ coyoneda.obj (Opposite.op S)).obj i
f₂ : (F ⋙ coyoneda.obj (Opposite.op S)).obj j
e :
  (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app i)) f₁ =
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app j)) f₂
⊢ ∃ k f g,
    (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map f)) f₁ =
      (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map g)) f₂
Module: Mathlib.Algebra.Category.Ring.Under.Limits

Goal state before:
pp: R : CommRingCat
A B : Under R
f g : A ⟶ B
⊢ ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder ≫ f = ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder ≫ g

Tactic:
by
  ext (a : AlgHom.equalizer (toAlgHom f) (toAlgHom g))
  exact a.property

Goal state after:
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: case inst
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ HasColimitsOfShape (Discrete PEmpty.{1}) (Comma (Functor.fromPUnit X) (𝟭 T))

Tactic:
exact inferInstanceAs (HasColimitsOfShape _ (Under X))

Goal state after:
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
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Module.Flat R M
⊢ tensorEqLocusInv S M f g ∘ₗ tensorEqLocus S M f g = id

Tactic:
by
      ext m x
      apply (Module.Flat.lTensor_preserves_injective_linearMap (eqLocus f g).subtype
        (eqLocus f g).injective_subtype)
      simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
x✝ : a ∈ s
n : ℕ
h : (fun b ↦ a = b) (s.get n)
⊢ (fun b ↦ f a = b) ((map f s).get n)

Tactic:
rw [get_map, h]

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

Goal state before:
pp: case succ
α : Type u
f : α → α
a : α
n : ℕ
ih : iterate f (f a) n = f ((iterate f a).get n)
⊢ f (iterate f (f a) n) = f (iterate f a (n + 1))

Tactic:
get

Goal state after:
case succ
α : Type u
f : α → α
a : α
n : ℕ
ih : iterate f (f a) n = f (iterate f a n)
⊢ f (iterate f (f a) n) = f (iterate f a (n + 1))
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : s.Results a n
⊢ s = (pure a).thinkN n

Tactic:
induction n generalizing s with | zero  =>  _ | succ n IH  =>  _ 

Goal state after:
case zero
α : Type u
a : α
s : Computation α
h : s.Results a 0
⊢ s = (pure a).thinkN 0

case succ
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
s : Computation α
h : s.Results a (n + 1)
⊢ s = (pure a).thinkN (n + 1)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: ⊢ nats = 0 :: map succ nats

Tactic:
apply Stream'.ext; intro n
  cases n
  · rfl
  rw [get_succ]; rfl

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

Goal state before:
pp: case cons.inr
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
obtain ⟨i1, i2⟩ := show c = b ∧ append t₁ s₂ = s' by simpa using e

Goal state after:
case cons.inr
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
i1 : c = b
i2 : t₁.append s₂ = s'
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

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

Tactic:
rw [hp] at ih

Goal state after:
case succ.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
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
x : α
s : Seq α
m n : ℕ
h : m < n
⊢ (s.set m x).drop n = s.drop n

Tactic:
by
  ext1 i
  simp [get?_set_of_ne _ _ (show n + i ≠ m by lia)]

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

Goal state before:
pp: case neg
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
this : ∀ (n : ℕ), b.drop n ≠ nil → motive (a.drop n) (b.drop n)
ha : ¬a.Terminates
⊢ b.length' ≤ a.length'

Tactic:
simp [length'_of_not_terminates ha]

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

Goal state before:
pp: K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminatedAt_succ_n : s.TerminatedAt (n + 1)
⊢ squashSeq s n = s

Tactic:
change s.get? (n + 1) = none at terminatedAt_succ_n
  cases s_nth_eq : s.get? n <;> simp only [*, squashSeq]

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
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
⊢ 1 ≤ b

Tactic:
by
  obtain ⟨gp_n, nth_s_eq, ⟨-⟩⟩ : ∃ gp_n, (of v).s.get? n = some gp_n ∧ gp_n.b = b :=
    exists_s_b_of_partDen nth_partDen_eq
  obtain ⟨ifp_n, succ_nth_stream_eq, ifp_n_b_eq_gp_n_b⟩ :
      ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ (ifp.b : K) = gp_n.b :=
    IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some nth_s_eq
  rw [← ifp_n_b_eq_gp_n_b]
  exact mod_cast IntFractPair.one_le_succ_nth_stream_b succ_nth_stream_eq

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b ≠ 0
⊢ P.toPoly.leadingCoeff = P.b

Tactic:
rw [of_a_eq_zero ha, leadingCoeff_quadratic hb]

Goal state after:
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
n : ℕ
hyp : n + 1 = 0 ∨ ¬(of v).TerminatedAt (n + 1 - 1)
⊢ n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 - 1)

Tactic:
exact Or.inr (Or.resolve_left hyp n.succ_ne_zero)

Goal state after:
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
c : Con M
s : Multiset ι
f g : ι → M
h : ∀ x ∈ s, c (f x) (g x)
⊢ c (Multiset.map f s).prod (Multiset.map g s).prod

Tactic:
rcases s

Goal state after:
case mk
ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
c : Con M
s : Multiset ι
f g : ι → M
a✝ : List ι
h : ∀ x ∈ Quot.mk (⇑(List.isSetoid ι)) a✝, c (f x) (g x)
⊢ c (Multiset.map f (Quot.mk (⇑(List.isSetoid ι)) a✝)).prod (Multiset.map g (Quot.mk (⇑(List.isSetoid ι)) a✝)).prod
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr.inl
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 : ℕ
e : Fin n → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), e i ∈ f.range
h✝¹ : Nontrivial R
h✝ : Subsingleton S
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

pp: case inr.inr
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 : ℕ
e : Fin n → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), e i ∈ f.range
h✝¹ : Nontrivial R
h✝ : Nontrivial S
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
· obtain ⟨n, hn⟩ := h 1 (Subsingleton.elim _ _)
    simp at hn

Goal state after:
case inr.inr
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 : ℕ
e : Fin n → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), e i ∈ f.range
h✝¹ : Nontrivial R
h✝ : Nontrivial S
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
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
⊢ f.HasUnifEigenvalue μ k

Tactic:
by
  rw [HasUnifEigenvalue, Submodule.ne_bot_iff]
  use x; exact h

Goal state after:
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
hN : {i | N i ≠ ⊥}.Finite
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
x✝¹ : Fintype { i // N i ≠ ⊥ } := hN.fintype
x✝ : Fintype ↑{i | N i ≠ ⊥} := hN.fintype
⊢ (trace R M) f = ∑ i, (trace R ↥(N ↑i)) (f.restrict ⋯)

Tactic:
trace_eq_sum_trace_restrict (isInternal_ne_bot_iff.mpr h) (hf ·)

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
hN : {i | N i ≠ ⊥}.Finite
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
x✝¹ : Fintype { i // N i ≠ ⊥ } := hN.fintype
x✝ : Fintype ↑{i | N i ≠ ⊥} := hN.fintype
⊢ ∑ i, (trace R ↥(N ↑i)) (f.restrict ⋯) = ∑ i, (trace R ↥(N ↑i)) (f.restrict ⋯)
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] M
⊢ (trace R M) (g ∘ₗ f) = (trace R N) (f ∘ₗ g)

Tactic:
have h := LinearMap.ext_iff.1 (LinearMap.ext_iff.1 (trace_comp_comm R M N) g) f
  simp only [llcomp_apply', compr₂_apply, flip_apply] at h
  exact h

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 ^ n)⁻¹ * (x * x⁻¹) = (x ^ n)⁻¹ * x⁻¹ * x

Tactic:
mul_inv_cancel₀ hx0,

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 ^ n)⁻¹ * 1 = (x ^ n)⁻¹ * x⁻¹ * x
Module: Mathlib.Algebra.Field.ZMod

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ p.Coprime k

Tactic:
rwa [Nat.Prime.coprime_iff_not_dvd Fact.out, ← CharP.cast_eq_zero_iff (ZMod p)]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ≥0
⊢ ↑x✝ = ↑x✝.num / ↑x✝.den

Tactic:
← coe_nnratCast,

Goal state after:
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ≥0
⊢ ↑↑x✝ = ↑x✝.num / ↑x✝.den
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ≥0
x✝ : ℍ[R]
⊢ x✝¹ • x✝ = ↑x✝¹ * x✝

Tactic:
← coe_nnratCast,

Goal state after:
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ≥0
x✝ : ℍ[R]
⊢ x✝¹ • x✝ = ↑↑x✝¹ * x✝
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case inl
m k : ℕ
hmn : m < m + k + 1
⊢ Δ_[1]^[m + k + 1] (fun x ↦ ↑(x.choose m)) 0 = 0

Tactic:
(by ring : m + k + 1 = k + 1 + m),

Goal state after:
case inl
m k : ℕ
hmn : m < m + k + 1
⊢ Δ_[1]^[k + 1 + m] (fun x ↦ ↑(x.choose m)) 0 = 0
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
⊢ (Δ_[1]^[n] fun r ↦ r ^ n) = ↑n !

Tactic:
induction n with
  | zero => aesop
  | succ n IH =>
    have : (Δ_[1] fun (r : R) ↦ r ^ (n + 1)) =
      ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i := by
      ext x
      simp [nsmul_eq_mul, fwdDiff, add_pow, sum_range_succ, mul_comm]
    simp_rw [iterate_succ_apply, this, fwdDiff_iter_finsetSum, fwdDiff_iter_const_smul,
       sum_range_succ]
    simpa [IH, factorial_succ] using sum_eq_zero fun i hi ↦ by
      rw [fwdDiff_iter_pow_eq_zero_of_lt (by have := mem_range.1 hi; lia), mul_zero]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M : Submonoid G
⊢ ∀ {x : G}, x ∈ (M ⊓ M⁻¹).carrier → x⁻¹ ∈ (M ⊓ M⁻¹).carrier

Tactic:
by aesop

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x✝³ : Subgroup G
x✝² : Submonoid G
x✝¹ : x✝³.toSubmonoid ≤ x✝²
x✝ : G
⊢ x✝ ∈ x✝³ → x✝ ∈ x✝².mulSupport

Tactic:
by aesop

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M : Submonoid G
⊢ M.IsMulPointed → M.mulSupport = ⊥

Tactic:
by aesop

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M : Submonoid G
hM : M.IsMulSpanning
a : G
⊢ a ∈ M ∨ a⁻¹ ∈ M

Tactic:
by aesop

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M N : Submonoid G
hM : M.IsMulSpanning
h : M ≤ N
⊢ N.IsMulSpanning

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₁ : v i ∉ closure (v '' t)
hi₂ : ∀ (k : ι), 1 < f (v k) → f (v k) < f (v i) → v k ∈ closure (v '' t)
hi₃ : i ∉ t
j k : ι
hj : 1 < f (v j)
hk : 1 < f (v k)
hjk : v i = v j * v k
⊢ f (v j) < f (v i)

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₁ : v i ∉ closure (v '' t)
hi₂ : ∀ (k : ι), 1 < f (v k) → f (v k) < f (v i) → v k ∈ closure (v '' t)
hi₃ : i ∉ t
j k : ι
hj : 1 < f (v j)
hk : 1 < f (v k)
hjk : v i = v j * v k
hj' : v j ∈ closure (v '' t)
⊢ f (v k) < f (v i)

Tactic:
by aesop

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ ∀ (x y : A),
    (if h : f (x * y) = 0 then 0 else ↑⟨Units.mk0 (f (x * y)) h, ⋯⟩) =
      (if h : f x = 0 then 0 else ↑⟨Units.mk0 (f x) h, ⋯⟩) * if h : f y = 0 then 0 else ↑⟨Units.mk0 (f y) h, ⋯⟩

Tactic:
by aesop

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
⊢ x = y

Tactic:
obtain ⟨u, hu⟩ : Associated x y := by
    have := (Associated.of_eq hxy).normalizedFactors_eq
    rwa [normalizedFactors_pow, normalizedFactors_pow, nsmul_right_inj hn,
      ← associated_iff_normalizedFactors_eq_normalizedFactors hx hy] at this

Goal state after:
M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
u : Mˣ
hu : x * ↑u = y
⊢ x = y
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ˣ
x✝ : ∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑y = f x
a : A
ha : f a ≠ 0
x : A
hax : f a * ↑y = f x
⊢ f x ≠ 0

Tactic:
by aesop

Goal state after:
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
x : Bˣ
hx : x ∈ f.valueGroup
r : A
hr : f r ≠ 0
s : A
hs : f s ≠ 0
hrs : f r * ↑x = f s
⊢ ⟨x, hx⟩ = valueGroup.mk f r s hr hs

Tactic:
simp only [valueGroup.mk, Subtype.mk.injEq]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
x : Bˣ
hx : x ∈ f.valueGroup
r : A
hr : f r ≠ 0
s : A
hs : f s ≠ 0
hrs : f r * ↑x = f s
⊢ x = (Units.mk0 (f r) hr)⁻¹ * Units.mk0 (f s) hs
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: a b : SimplexCategory
x✝² x✝¹ : a ⟶ b
x✝ : (fun f ↦ (Hom.toOrderHom f).toFun) x✝² = (fun f ↦ (Hom.toOrderHom f).toFun) x✝¹
⊢ x✝² = x✝¹

Tactic:
by aesop

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: ⊢ ⦋0⦌.const ⦋0⦌ 0 = 𝟙 ⦋0⦌

Tactic:
by aesop

Goal state after: