mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: case refine_1
C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
r : (R ⋙ forget RingCat).ColimitType
m : (M ⋙ forget Ab).ColimitType
U : C
a : (R ⋙ forget RingCat).obj U
V₁ : C
b₁ : (M ⋙ forget Ab).obj V₁
V₂ : C
f : V₁ ⟶ V₂
⊢ (M ⋙ forget Ab).ιColimitType (IsFiltered.max ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst)
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨U, a⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨V₁, b₁⟩.snd) =
    (M ⋙ forget Ab).ιColimitType (IsFiltered.max ⟨U, a⟩.fst ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.fst)
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.fst))) ⟨U, a⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.fst)))
          ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.snd)

Tactic:
obtain ⟨s, α, β, h₁, h₂⟩ :=
      bowtie (leftToMax U V₁) (leftToMax U V₂)
        (rightToMax U V₁) (f ≫ rightToMax U V₂)

Goal state after:
case refine_1
C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
r : (R ⋙ forget RingCat).ColimitType
m : (M ⋙ forget Ab).ColimitType
U : C
a : (R ⋙ forget RingCat).obj U
V₁ : C
b₁ : (M ⋙ forget Ab).obj V₁
V₂ : C
f : V₁ ⟶ V₂
s : C
α : IsFiltered.max U V₁ ⟶ s
β : IsFiltered.max U V₂ ⟶ s
h₁ : leftToMax U V₁ ≫ α = leftToMax U V₂ ≫ β
h₂ : rightToMax U V₁ ≫ α = (f ≫ rightToMax U V₂) ≫ β
⊢ (M ⋙ forget Ab).ιColimitType (IsFiltered.max ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst)
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨U, a⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨V₁, b₁⟩.snd) =
    (M ⋙ forget Ab).ιColimitType (IsFiltered.max ⟨U, a⟩.fst ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.fst)
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.fst))) ⟨U, a⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.fst)))
          ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.snd)
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
h : A →+ B' := ↑e
h' : B' →+ A := ↑e.symm
⊢ τB' = moduleTopology S B'

Tactic:
simp_rw [e.toHomeomorph.symm.isInducing.1, eq_moduleTopology R A, moduleTopology, induced_sInf]

Goal state after:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
h : A →+ B' := ↑e
h' : B' →+ A := ↑e.symm
⊢ sInf (TopologicalSpace.induced ⇑e.toHomeomorph.symm '' {t | ContinuousSMul R A ∧ ContinuousAdd A}) =
    sInf {t | ContinuousSMul S B' ∧ ContinuousAdd B'}
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
⊢ m = descMorphism F s

Tactic:
by
    ext x
    induction x using Quot.inductionOn with | h x => ?_
    induction x with
    | of j =>
      change _ = s.ι.app j _
      rw [← w j]
      rfl
    | one =>
      rw [quot_one, map_one]
      rfl
    | mul x y hx hy =>
      rw [quot_mul, map_mul, hx, hy]
      solve_by_elim

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X✝ Y✝ Z✝ : TopCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ freeMap R (f ≫ g) = freeMap R f ≫ freeMap R g

Tactic:
ext; exact DFunLike.congr_fun (Finsupp.lmapDomain_comp _ _ f.hom g.hom) _

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
⊢ ∀ {X_1 Y : C'} (f : X_1 ⟶ Y),
    (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}).map f ≫
        (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Y).trans Equiv.ulift.symm)).toIso.hom =
      (Equiv.ulift.trans ((e.toAdjunction.homEquiv X X_1).trans Equiv.ulift.symm)).toIso.hom ≫
        (e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃, v₁}).map f

Tactic:
intro _ _ f
        ext ⟨g⟩
        simp [Adjunction.homEquiv_unit]

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

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
j₀ : J
A : Type w
x✝ : SmallCategory A
F : A ⥤ Under j₀
hA : HasCardinalLT (Arrow A) κ
⊢ Cocone F

Tactic:
have := isFiltered_of_isCardinalFiltered J κ
    let c := cocone (F ⋙ Under.forget j₀) hA
    let x (a : A) : j₀ ⟶ IsFiltered.max j₀ c.pt := (F.obj a).hom ≫ c.ι.app a ≫
      IsFiltered.rightToMax j₀ c.pt
    have hκ' : HasCardinalLT A κ := hasCardinalLT_of_hasCardinalLT_arrow hA
    exact
      { pt := Under.mk (toCoeq x hκ')
        ι :=
          { app a := Under.homMk (c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ')
              (by simpa [x] using coeq_condition x hκ' a)
            naturality a b f := by
              ext
              have := c.w f
              dsimp at this ⊢
              simp only [reassoc_of% this, Category.comp_id] } }

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

Goal state before:
pp: case refine_1.hX
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := ⋯
iP : R ⟶ P := ⋯
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := ⋯
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
j : Fin n → J
x : (i : Fin n) → (fun X ↦ X) ((F ⋙ forget CommRingCat).obj (j i))
h :
  ∀ (i : Fin n),
    (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app (j i))) (x i) =
      (ConcreteCategory.hom (π ≫ g)) (MvPolynomial.X i)
i : J
hi : (a : Fin n) → j a ⟶ i
⊢ ∀ (i_1 : Fin n),
    (CommRingCat.Hom.hom (π ≫ g)) (MvPolynomial.X i_1) =
      (CommRingCat.Hom.hom
          (CommRingCat.ofHom
              (MvPolynomial.eval₂Hom (CommRingCat.Hom.hom (α.app i)) fun x_1 ↦
                (ConcreteCategory.hom (F.map (hi x_1))) (x x_1)) ≫
            c.ι.app i))
        (MvPolynomial.X i_1)

Tactic:
· intro i
        simp only [CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply,
          Functor.const_obj_obj, CommRingCat.hom_ofHom, MvPolynomial.coe_eval₂Hom,
          MvPolynomial.eval₂_X]
        exact (congr($(c.w (hi i)).hom (x i)).trans (h i)).symm

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

Goal state before:
pp: T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
g : X ⟶ Y
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
h : f = g
A : P.Under Q X
⊢ pushout.inl A.hom f ≫ ((pushoutCongr h).hom.app A).right = pushout.inl A.hom g

Tactic:
by
  subst h
  simp [pushoutCongr]

Goal state after:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ p > 0, MixedCharZero R p → P
⊢ ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P

Tactic:
q

Goal state after:
case mp
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ p > 0, MixedCharZero R p → P
q : ℕ
⊢ Nat.Prime q → MixedCharZero R q → P
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ ∀ p > 0, MixedCharZero R p → P

Tactic:
q

Goal state after:
case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
⊢ q > 0 → MixedCharZero R q → P
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S F✝ E✝ F : IntermediateField K L
E : IntermediateField (↥F) L
⊢ Algebra K ↥E

Tactic:
by infer_instance

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

Goal state before:
pp: case mpr
α : Type u
x x' : α
s s' : Seq α
⊢ x = x' ∧ s = s' → cons x s = cons x' s'

Tactic:
intro ⟨_, _⟩
    congr

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

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : s.Results a n
this : s.Terminates
⊢ s.length + 1 = n + 1

Tactic:
h.length

Goal state after:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.Results a n
this : s.Terminates
⊢ n + 1 = n + 1
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
⊢ (s.toList h).length = s.length h

Tactic:
toList,

Goal state after:
α : Type u
s : Seq α
h : s.Terminates
⊢ (take (s.length h) s).length = s.length h
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
⊢ (map f s).length h = s.length ⋯

Tactic:
rw [length]

Goal state after:
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
⊢ Nat.find h = s.length ⋯
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
x : α
s : Seq α
n : ℕ
⊢ (cons x s).drop (n + 1) = s.drop n

Tactic:
simp [← dropn_tail]

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : Nonempty ι
inst✝² : IsDirectedOrder ι
inst✝¹ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)
⊢ Nonempty ι

Tactic:
by infer_instance

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

Goal state before:
pp: case succ.cons
α : 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
m : ℕ
tb_hd : β
tb_tl : Seq β
hb : (cons tb_hd tb_tl).tail ≠ nil
ih : motive (a.drop m) (cons tb_hd tb_tl)
a_hd : α
a_tl : Seq α
ha : a.drop m = cons a_hd a_tl
h_tail : motive a_tl tb_tl
⊢ motive (a.drop m).tail (cons tb_hd tb_tl).tail

Tactic:
simpa [ha]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ q, (of v).nums n = ↑q

Tactic:
rcases exists_gcf_pair_rat_eq_nth_conts v n with ⟨⟨a, _⟩, nth_cont_eq⟩
  use a
  simp [num_eq_conts_a, nth_cont_eq]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
I : Type u_3
e : I → R
hf : Function.Injective ⇑f
⊢ OrthogonalIdempotents (⇑f ∘ e) ↔ OrthogonalIdempotents e

Tactic:
simp [iff_mul_eq, ← hf.eq_iff, apply_ite]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
I : Type u_3
e : I → R
hf : Function.Injective ⇑f
⊢ OrthogonalIdempotents (⇑f ∘ e) ↔ OrthogonalIdempotents e

Tactic:
by
  classical
  simp [iff_mul_eq, ← hf.eq_iff, apply_ite]

Goal state after:
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 : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p : n
⊢ ∀ (j : n) (y : Matrix n n R), ∃ z, z * y * single p j x + z - 1 ∈ matrix n I

Tactic:
q

Goal state after:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
⊢ ∀ (y : Matrix n n R), ∃ z, z * y * single p q x + z - 1 ∈ matrix n I
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
⊢ matrix n c.ofMatrix = c

Tactic:
ext x y
  constructor
  · intro h
    rw [matrix_eq_sum_single x, matrix_eq_sum_single y]
    refine c.finsetSum _ fun i _ ↦ c.finsetSum _ fun j _ ↦ h i j i j
  · intro h i' j' i j
    simpa using c.mul (c.mul (c.refl <| single i i' 1) h) (c.refl <| single j' j 1)

Goal state after:
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 : n
⊢ ∀ (j : n), I.jacobson.ringCon (M p j) (0 p j)

Tactic:
q

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
⊢ I.jacobson.ringCon (M p q) (0 p q)
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: case neg
ι : 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 ι
κ : ι → Type u_4
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal fun i ↦ N ↑i
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i)
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ ↑i
hi : σ ↑i ∉ s
⊢ ((h.collectedBasis b).repr (f ↑((b i) k))) ⟨i, k⟩ = 0

Tactic:
suffices f (b i k) = 0 by simp [this]

Goal state after:
case neg
ι : 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 ι
κ : ι → Type u_4
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal fun i ↦ N ↑i
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i)
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ ↑i
hi : σ ↑i ∉ s
⊢ f ↑((b i) k) = 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
p : Submodule R M
f g : End R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
μ₁ μ₂ : R
h : MapsTo ⇑f ↑(g.maxGenEigenspace μ₁) ↑(g.maxGenEigenspace μ₂)
x : ↥p
hx : ∃ k, ((g - μ₁ • 1) ^ k) ↑x = 0
⊢ ∃ k, ((g - μ₂ • 1) ^ k) (f ↑x) = 0

Tactic:
← mem_maxGenEigenspace

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f g : End R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
μ₁ μ₂ : R
h : MapsTo ⇑f ↑(g.maxGenEigenspace μ₁) ↑(g.maxGenEigenspace μ₂)
x : ↥p
hx : ↑x ∈ g.maxGenEigenspace μ₁
⊢ f ↑x ∈ g.maxGenEigenspace μ₂
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
⊢ ↑(l₁ + l₂) ≤ k₁ + k₂ ∧ ((f₁ + f₂ - (μ₁ + μ₂) • 1) ^ (l₁ + l₂)) m = 0

Tactic:
rw [this, h.add_pow', LinearMap.coe_sum, Finset.sum_apply]

Goal state after:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
⊢ ↑(l₁ + l₂) ≤ k₁ + k₂ ∧
    ∑ c ∈ Finset.antidiagonal (l₁ + l₂), ((l₁ + l₂).choose c.1 • ((f₁ - μ₁ • 1) ^ c.1 * (f₂ - μ₂ • 1) ^ c.2)) m = 0
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)
mul_comm : ∀ (a b : R), a * b = b * a
one_mul : ∀ (a : R), 1 * a = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
mul_one : ∀ (a : R), a * 1 = a
a b c : R
⊢ a * c + c * b = a * c + b * c

Tactic:
mul_comm b c

Goal state after:
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)
mul_comm : ∀ (a b : R), a * b = b * a
one_mul : ∀ (a : R), 1 * a = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
mul_one : ∀ (a : R), a * 1 = a
a b c : R
⊢ a * c + c * b = a * c + c * b
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : DivisionRing β
⊢ DivisionRing α

Tactic:
let add_group_with_one := e.addGroupWithOne
  let inv := e.Inv
  let div := e.div
  let mul := e.mul
  let npow := e.pow ℕ
  let zpow := e.pow ℤ
  let nnratCast := e.nnratCast
  let ratCast := e.ratCast
  let nnqsmul := e.smul ℚ≥0
  let qsmul := e.smul ℚ
  apply e.injective.divisionRing _ <;> intros <;> exact e.apply_symm_apply _

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
n : ℕ
⊢ (x ^ n).toWord = reduce (List.replicate n x.toWord).flatten

Tactic:
← mk_toWord (x := x)

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
n : ℕ
⊢ (mk x.toWord ^ n).toWord = reduce (List.replicate n (mk x.toWord).toWord).flatten
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

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

Tactic:
zero_add,

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
B : Type u_3
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
⊢ IsIntegrallyClosedIn R B → IsIntegrallyClosedIn R A

Tactic:
by
  rintro ⟨inj, cl⟩
  refine ⟨Function.Injective.of_comp (f := f) ?_, fun hx => ?_, ?_⟩
  · convert! inj
    aesop
  · obtain ⟨y, fx_eq⟩ := cl.mp ((isIntegral_algHom_iff f hf).mpr hx)
    aesop
  · rintro ⟨y, rfl⟩
    apply (isIntegral_algHom_iff f hf).mp
    simp_all

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
inst✝³ : DecidableEq γ
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : SMulCommClass α β γ
a : α
s : Finset β
t : Finset γ
⊢ ↑(a • s • t) = ↑(s • a • t)

Tactic:
simp only [coe_smul_finset, coe_smul, smul_comm]

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

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

pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
⊢ (P.coeff i • Δ_[1]^[P.natDegree] fun i_1 ↦ i_1 ^ i) x = 0

Tactic:
zero_add,

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

R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
⊢ (P.coeff i • Δ_[1]^[P.natDegree] fun i_1 ↦ i_1 ^ i) x = 0
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

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

Tactic:
classical
  induction hx using closure_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; exact ⟨Finsupp.single i 1, by simp⟩
  | one => use 0; simp
  | mul x y hx hy hx' hy' =>
    obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'
    use v + w
    rw [Finsupp.prod_add_index]
    · simp
    · simp [zpow_add]
  | inv x hx hx' =>
    obtain ⟨a, rfl⟩ := hx'
    use -a
    rw [Finsupp.prod_neg_index]
    · simp
    · simp

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

Goal state before:
pp: C : Type u_1
inst✝ : CommGroup C
x y z : Subgroup C
xz : x ≤ z
a : C
ha : a ∈ (x ⊔ y) ⊓ z
⊢ a ∈ x ⊔ y ⊓ z

Tactic:
rw [mem_inf, mem_sup] at ha

Goal state after:
C : Type u_1
inst✝ : CommGroup C
x y z : Subgroup C
xz : x ≤ z
a : C
ha : (∃ y_1 ∈ x, ∃ z ∈ y, y_1 * z = a) ∧ a ∈ z
⊢ a ∈ x ⊔ y ⊓ z
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case mpr
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : B
⊢ (∃ y, f y = x) ∧ ¬x = 0 → ∃ x_1, (∃ y, f y = ↑x_1) ∧ ↑x_1 = x

Tactic:
· rintro ⟨⟨y, hy⟩, hx₀⟩
    refine ⟨Units.mk0 x hx₀, ?_, rfl⟩
    simpa [Units.val_mk0, mem_range] using ⟨y, hy⟩

Goal state after: