mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsLocalRing R
h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ ∀ (p : ℕ), p ≠ 0 → CharP R p → P

Tactic:
intro p p_pos p_char

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsLocalRing R
h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
p_char : CharP R p
⊢ P
Module: Mathlib.Data.Seq.Defs

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

Tactic:
by
  constructor
  · apply cons_injective2
  · intro ⟨_, _⟩
    congr

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

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
H : s.destruct = none
⊢ motive Seq.nil

Tactic:
apply nil

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

Goal state before:
pp: α : Type u
i : ℕ
s : Stream' α
⊢ (drop i s).tail = drop (i + 1) s

Tactic:
ext; simp [Nat.add_comm, Nat.add_left_comm]

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

Goal state before:
pp: case succ.cons
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
s' : Seq α
e : some a = ↑s' k
h_eq : ↑(cons b s') k.succ = ↑s' k
⊢ C (cons b s')

Tactic:
apply h1 _ _ (Or.inr (IH e))

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

Goal state before:
pp: case zero.pure
α : Type u
a a' : α
h : (pure a').Results a 0
⊢ pure a' = (pure a).thinkN 0

Tactic:
rw [← eq_of_pure_mem h.mem]

Goal state after:
case zero.pure
α : Type u
a a' : α
h : (pure a').Results a 0
⊢ pure a = (pure a).thinkN 0
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
⊢ (initsCore [s.head] s.tail).tail = initsCore [s.head, s.tail.head] s.tail.tail

Tactic:
rw [inits_core_eq]

Goal state after:
α : Type u
s : Stream' α
⊢ ([s.head] :: initsCore ([s.head] ++ [s.tail.head]) s.tail.tail).tail = initsCore [s.head, s.tail.head] s.tail.tail
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
⊢ ∀
    a ∈
      Ideal.span
        {a |
          (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
            (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
              (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a},
    (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) a = 0

Tactic:
by
      suffices Ideal.span _ ≤
          Ideal.comap (FreeCommRing.lift fun x : Σ i : ι, G i ↦ g x.fst x.snd) ⊥ by
        intro x hx
        exact (mem_bot P).1 (this hx)
      rw [Ideal.span_le]
      intro x hx
      rw [SetLike.mem_coe, Ideal.mem_comap, mem_bot]
      rcases hx with (⟨i, j, hij, x, rfl⟩ | ⟨i, rfl⟩ | ⟨i, x, y, rfl⟩ | ⟨i, x, y, rfl⟩) <;>
        simp only [map_sub, lift_of, Hg, map_one, map_add, map_mul,
          (g i).map_one, (g i).map_add, (g i).map_mul, sub_self]

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

Goal state before:
pp: case inr
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
m : ℕ
hy : some y = s.get? m
h_nm : n ≠ m
⊢ p y

Tactic:
apply h_all _ (get?_mem hy.symm)

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)
i : ι
⊢ 0 ≠ (Ring.DirectLimit.of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ?m.64) 1

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)
i : ι
⊢ ι

Tactic:
· intro H; rcases Ring.DirectLimit.of.zero_exact H.symm with ⟨j, hij, hf⟩
          rw [(f' i j hij).map_one] at hf
          exact one_ne_zero hf

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

Goal state before:
pp: case pos
α : 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
hb : ¬b.TerminatedAt (a.length ha)
hb_cons : b.drop (a.length ha) ≠ nil
⊢ False

Tactic:
specialize this (a.length ha) hb_cons

Goal state after:
case pos
α : 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
ha : a.Terminates
this : motive (a.drop (a.length ha)) (b.drop (a.length ha))
hb : ¬b.TerminatedAt (a.length ha)
hb_cons : b.drop (a.length ha) ≠ nil
⊢ False
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Seq α
⊢ bind (a, s) (ret ∘ f) = map f (a, s)

Tactic:
simp [bind, map, map_comp, ret]

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
h1 : fib (n + 1) = ∑ p ∈ Finset.antidiagonal n, p.1.choose p.2
h2 : fib (n + 1 + 1) = ∑ p ∈ Finset.antidiagonal (n + 1), p.1.choose p.2
⊢ ∑ p ∈ Finset.antidiagonal n, p.1.choose p.2 + fib (n + 1 + 1) = ∑ p ∈ Finset.antidiagonal (n + 2), p.1.choose p.2

Tactic:
h2,

Goal state after:
n : ℕ
h1 : fib (n + 1) = ∑ p ∈ Finset.antidiagonal n, p.1.choose p.2
h2 : fib (n + 1 + 1) = ∑ p ∈ Finset.antidiagonal (n + 1), p.1.choose p.2
⊢ ∑ p ∈ Finset.antidiagonal n, p.1.choose p.2 + ∑ p ∈ Finset.antidiagonal (n + 1), p.1.choose p.2 =
    ∑ p ∈ Finset.antidiagonal (n + 2), p.1.choose p.2
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map (fun x ↦ (map g (f x)).join) s)

Tactic:
simp only [show (fun x => join (map g (f x))) = join ∘ (map g ∘ f) from rfl]

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map (join ∘ map g ∘ f) s)
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
⊢ gp.a = 1 ∧ ∃ z, gp.b = ↑z

Tactic:
have : gp = ⟨1, ifp.b⟩ := by
    have : (of v).s.get? n = some ⟨1, ifp.b⟩ :=
      get?_of_eq_some_of_succ_get?_intFractPair_stream stream_succ_nth_eq
    have : some gp = some ⟨1, ifp.b⟩ := by rwa [nth_s_eq] at this
    injection this

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
this : gp = { a := 1, b := ↑ifp.b }
⊢ gp.a = 1 ∧ ∃ z, gp.b = ↑z
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
i j : n
x y : R
⊢ Relation.Map (⇑c) (fun x ↦ x i j) (fun x ↦ x i j) x y → c.ofMatrix x y

Tactic:
rintro ⟨X, Y, h, rfl, rfl⟩ i' j'

Goal state after:
case mpr
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
i j : n
X Y : Matrix n n R
h : c X Y
i' j' : n
⊢ c (single i' j' ((fun x ↦ x i j) X)) (single i' j' ((fun x ↦ x i j) Y))
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
⊢ (f.genEigenspace μ) ⊤ ≤ (f.genEigenspace μ) ↑(finrank K V)

Tactic:
rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]
      exact (f.genEigenspace _).monotone <| by simpa using maxUnifEigenspaceIndex_le_finrank f μ

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f g : End R M
h_comm✝ : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
μ : R
hf' : MapsTo ⇑f ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
hg' : MapsTo ⇑g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
this : IsNilpotent (restrict (f - (algebraMap R (End R M)) μ) ⋯)
⊢ (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0

Tactic:
rw [restrict_comp hf' hg', trace_comp_eq_mul_of_commute_of_isNilpotent μ h_comm this,
    hg, mul_zero]

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

Goal state before:
pp: case refine_2
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
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ ((f - μ₂ • 1) ^ l).ker
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
⊢ ⨆ i, Submodule.map (g ^ l) (⨆ (_ : i ∈ s), (f.genEigenspace i) k) ≤ ⨆ a ∈ s, (f.genEigenspace a) k

Tactic:
Submodule.map_iSup (ι := _ ∈ s)

Goal state after:
case refine_2
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
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ ((f - μ₂ • 1) ^ l).ker
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
⊢ ⨆ i ∈ s, Submodule.map (g ^ l) ((f.genEigenspace i) k) ≤ ⨆ a ∈ s, (f.genEigenspace a) k
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
p : Submodule R M
hfp : ∀ x ∈ p, f x ∈ p
μ : R
⊢ Submodule.map p.subtype (eigenspace (LinearMap.restrict f hfp) μ) ≤ f.eigenspace μ

Tactic:
rintro a ⟨x, hx, rfl⟩

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hfp : ∀ x ∈ p, f x ∈ p
μ : R
x : ↥p
hx : x ∈ ↑(eigenspace (LinearMap.restrict f hfp) μ)
⊢ p.subtype x ∈ f.eigenspace μ
Module: Mathlib.Algebra.GroupWithZero.Action.ConjAct

Goal state before:
pp: α : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
⊢ ∀ (x y : ConjAct G₀) (b : G₀), (x * y) • b = x • y • b

Tactic:
simp [smul_def, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x y : K
h' : Commute x y
h : x ≠ y
n : ℕ
this : x - y ≠ 0
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) / (x - y)

Tactic:
mul_div_cancel_right₀ _ this

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
x y : K
h' : Commute x y
h : x ≠ y
n : ℕ
this : x - y ≠ 0
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x : K
h : x ≠ 1
n : ℕ
this : x - 1 ≠ 0
⊢ ∑ i ∈ range n, x ^ i = (∑ i ∈ range n, x ^ i) * (x - 1) / (x - 1)

Tactic:
mul_div_cancel_right₀ _ this

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
x : K
h : x ≠ 1
n : ℕ
this : x - 1 ≠ 0
⊢ ∑ i ∈ range n, x ^ i = ∑ i ∈ range n, x ^ i
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x y : K
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
this : x - y ≠ 0
⊢ ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = (∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) / (x - y)

Tactic:
mul_div_cancel_right₀ _ this

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
x y : K
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
this : x - y ≠ 0
⊢ ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i)
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Semigroup β
f✝ f : α → β
⊢ ∀ (x y : FreeSemigroup α),
    List.foldl (fun a b ↦ a * f b) (f (x * y).head) (x * y).tail =
      List.foldl (fun a b ↦ a * f b) (f x.head) x.tail * List.foldl (fun a b ↦ a * f b) (f y.head) y.tail

Tactic:
by simp [← List.foldl_map, List.foldl_assoc]

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
m : M₃
hm : i₃ m = 1
⊢ g₃ (i₃ m) = i₄ (f₃ m)

Tactic:
simpa using DFunLike.congr_fun hc₃ m

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : x ^ f.natDegree + ∑ i, f.coeff ↑i * x ^ ↑i = 0
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ x ^ f.natDegree ∈ 𝓟

Tactic:
rw [eq_neg_of_add_eq_zero_left hroot, neg_mem_iff]

Goal state after:
R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : x ^ f.natDegree + ∑ i, f.coeff ↑i * x ^ ↑i = 0
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ ∑ i, f.coeff ↑i * x ^ ↑i ∈ 𝓟
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
⊢ IsIntegrallyClosed S

Tactic:
let K := FractionRing R
  let g : S →+* K := IsLocalization.map _ (T := R⁰) (RingHom.id R) hM
  let := g.toAlgebra
  have : IsScalarTower R S K := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
  have := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M S K
  refine (isIntegrallyClosed_iff_isIntegralClosure (K := K)).mpr
    ⟨IsFractionRing.injective _ _, fun {x} ↦ ⟨?_, fun e ↦ e.choose_spec ▸ isIntegral_algebraMap⟩⟩
  intro hx
  obtain ⟨⟨y, y_mem⟩, hy⟩ := hx.exists_multiple_integral_of_isLocalization M _
  obtain ⟨z, hz⟩ := (isIntegrallyClosed_iff _).mp ‹_› hy
  refine ⟨IsLocalization.mk' S z ⟨y, y_mem⟩, (IsLocalization.lift_mk'_spec _ _ _ _).mpr ?_⟩
  rw [RingHom.comp_id, hz, ← Algebra.smul_def, Submonoid.mk_smul]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
hq0 : a ≠ 0
⊢ a ^ 2 = star a * -a ↔ star a = -a

Tactic:
← neg_sq,

Goal state after:
case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
hq0 : a ≠ 0
⊢ (-a) ^ 2 = star a * -a ↔ star a = -a
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : SMul α β
inst✝¹ : IsLeftCancelSMul α β
inst✝ : DecidableEq β
s : Set α
t : Finset β
⊢ (s.PairwiseDisjoint fun x ↦ x • t) ↔ Set.InjOn (fun p ↦ p.1 • p.2) (s ×ˢ ↑t)

Tactic:
by
  simp_rw [← pairwiseDisjoint_coe, coe_smul_finset, Set.pairwiseDisjoint_smul_iff]

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

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
y : M
⊢ (shiftₗ M G h) f y = f (y + h)

Tactic:
simp [shiftₗ, fwdDiff]

Goal state after:
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:
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.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 : ∀ (f : G →* S), v '' baseOf v (invMonoidHom.comp f) ⊆ ⇑invMonoidHom ∘ v '' baseOf v f
⊢ v '' baseOf v (invMonoidHom.comp f) = ⇑invMonoidHom ∘ v '' baseOf v f

Tactic:
apply subset_antisymm (this f)

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 : ∀ (f : G →* S), v '' baseOf v (invMonoidHom.comp f) ⊆ ⇑invMonoidHom ∘ v '' baseOf v f
⊢ ⇑invMonoidHom ∘ v '' baseOf v f ⊆ v '' baseOf v (invMonoidHom.comp f)
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
⊢ False

Tactic:
obtain ⟨i, hi⟩ := s.toFinite.exists_minimalFor (f ∘ v) s hne

Goal state after:
ι : 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
⊢ False
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
x : H₀ˣ
⊢ (inr G₀ H₀) ↑x = ↑(1, x)

Tactic:
by
  simp [inr]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹

Tactic:
by
  obtain rfl | ha := eq_or_ne a 0
  · obtain rfl | hs := s.eq_empty_or_nonempty <;> simp [*]
  -- was `simp` and very slow (https://github.com/leanprover-community/mathlib4/issues/19751)
  · ext; simp only [mem_inv', ne_eq, not_false_eq_true, ← inv_smul_mem_iff₀, smul_eq_mul,
      MulOpposite.op_inv, inv_eq_zero, MulOpposite.op_eq_zero_iff, inv_inv,
      MulOpposite.smul_eq_mul_unop, MulOpposite.unop_op, mul_inv_rev, ha]

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

Goal state before:
pp: G₀ : Type u_1
H₀ : Type u_2
inst✝¹ : GroupWithZero G₀
inst✝ : GroupWithZero H₀
⊢ Function.Surjective ⇑(snd G₀ H₀)

Tactic:
classical
  exact Function.HasRightInverse.surjective ⟨inr .., fun _ ↦ by simp⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
s : Finset α
t : Finset β
⊢ s • -t = -(s • t)

Tactic:
by
  simp_rw [← image_neg_eq_neg]; exact image_image₂_right_comm smul_neg

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : MonoidWithZero B
f : A →*₀ B
a✝ b✝ : Bˣ
hb : a✝ ∈ Units.val ⁻¹' range ⇑f
hb' : b✝ ∈ Units.val ⁻¹' range ⇑f
⊢ a✝ * b✝ ∈ Units.val ⁻¹' range ⇑f

Tactic:
obtain ⟨y, hy⟩ := hb

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : MonoidWithZero B
f : A →*₀ B
a✝ b✝ : Bˣ
hb' : b✝ ∈ Units.val ⁻¹' range ⇑f
y : A
hy : f y = ↑a✝
⊢ a✝ * b✝ ∈ Units.val ⁻¹' range ⇑f
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case h₂
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ f.valueMonoid ≤ Submonoid.closure (↑f.valueMonoid ∪ (↑f.valueMonoid)⁻¹)

Tactic:
· simp [Submonoid.closure_union]

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

Goal state before:
pp: case refine_2
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
hy : f a * ↑y = f x
hv : f x ≠ 0
⊢ y ∈ f.valueGroup

Tactic:
let v := (Ne.isUnit hv).unit

Goal state after:
case refine_2
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
hy : f a * ↑y = f x
hv : f x ≠ 0
v : Bˣ := ⋯.unit
⊢ y ∈ f.valueGroup
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ (h.hom (h.inv { down := a })).down = a

Tactic:
change ((h.inv ≫ h.hom) _).down = _

Goal state after:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ ((h.inv ≫ h.hom) { down := a }).down = a
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'

Tactic:
use Y, i ≫ φ.hom, φ.inv ≫ e

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ (i ≫ φ.hom) ≫ φ.inv ≫ e = 𝟙 Y ∧ (φ.inv ≫ e) ≫ i ≫ φ.hom = p'
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f = g → f.f = g.f

pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f.f = g.f → f = g

Tactic:
· intro h
    rw [h]

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f.f = g.f → f = g