mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : α → α
a : α
⊢ corec f g a = f a :: corec f g (g a)

Tactic:
corec_def,

Goal state after:
α : Type u
β : Type v
f : α → β
g : α → α
a : α
⊢ map f (iterate g a) = f a :: corec f g (g a)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
⊢ corec id id a = const a

Tactic:
corec_def,

Goal state after:
α : Type u
a : α
⊢ map id (iterate id a) = const a
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ s.TerminatedAt n ↔ (s.get? n).isNone = true

Tactic:
by unfold TerminatedAt; cases s.get? n <;> simp

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

Goal state before:
pp: case refl
α : Type u
a : α
m n : ℕ
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ ⟨f, al⟩.val m = some a → ⟨f, al⟩.val m = some a

Tactic:
exact id

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

Goal state before:
pp: α : Type u
s : Computation α
T : s.Terminates
a : α
h : a ∈ s
⊢ s.Results a s.length

Tactic:
rw [← get_eq_of_mem _ h]; apply results_of_terminates

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

Goal state before:
pp: case a
α : Type u
s : Computation α
h : s.Terminates
⊢ s.length + 1 ≤ s.think.length

Tactic:
· have : (Option.isSome ((think s).val (length (think s))) : Prop) :=
      Nat.find_spec ((terminates_def _).1 s.think_terminates)
    revert this; rcases length (think s) with - | n <;> intro this
    · simp [think, Stream'.cons] at this
    · apply Nat.succ_le_succ
      apply Nat.find_min'
      apply this

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ map f s
⊢ ∃ a, a ∈ s ∧ f a = b

Tactic:
by
  rw [← bind_pure] at h
  let ⟨a, as, fb⟩ := exists_of_mem_bind h
  exact ⟨a, as, mem_unique (ret_mem _) fb⟩

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
⊢ LiftRel S (map f1 s1) (map f2 s2)

Tactic:
← bind_pure,

Goal state after:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
⊢ LiftRel S (s1.bind (pure ∘ f1)) (map f2 s2)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
x : α
⊢ (cons x s).enum = cons (0, x) (map (Prod.map Nat.succ id) s.enum)

Tactic:
ext ⟨n⟩ : 1
  · simp
  · simp only [get?_enum, get?_cons_succ, map_get?, Option.map_map]
    congr

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

Goal state before:
pp: case succ.some.inl
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_zero : fr = 0
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

Tactic:
simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_zero]

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
inst✝ : IsStrictOrderedRing K
q : ℚ
h : K
s : Stream'.Seq (Pair K)
gcf_v_eq : of ↑q = { h := h, s := s }
⊢ ↑⌊↑q⌋ = h

Tactic:
injection gcf_v_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 = 1
⊢ P.toPoly.Monic

Tactic:
by
  nontriviality R
  rw [Monic, leadingCoeff_of_a_ne_zero (ha ▸ one_ne_zero), ha]

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
hc : P.c = 1
a✝ : Nontrivial R
⊢ P.c = 1

Tactic:
hc

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 1
a✝ : Nontrivial R
⊢ 1 = 1
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : n ≤ 3
⊢ (↑((fun P ↦ ⟨P.toPoly, ⋯⟩)
            ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f))).coeff
      n =
    (↑f).coeff n

Tactic:
interval_cases n

Goal state after:
case inl.«0»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 0 ≤ 3
⊢ (↑((fun P ↦ ⟨P.toPoly, ⋯⟩)
            ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f))).coeff
      0 =
    (↑f).coeff 0

case inl.«1»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 1 ≤ 3
⊢ (↑((fun P ↦ ⟨P.toPoly, ⋯⟩)
            ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f))).coeff
      1 =
    (↑f).coeff 1

case inl.«2»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 2 ≤ 3
⊢ (↑((fun P ↦ ⟨P.toPoly, ⋯⟩)
            ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f))).coeff
      2 =
    (↑f).coeff 2

case inl.«3»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 3 ≤ 3
⊢ (↑((fun P ↦ ⟨P.toPoly, ⋯⟩)
            ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f))).coeff
      3 =
    (↑f).coeff 3
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
⊢ b * ((of v).contsAux (n + 1)).b ≤ ((of v).contsAux (n + 2)).b

Tactic:
obtain ⟨gp_n, nth_s_eq, rfl⟩ : ∃ gp_n, (of v).s.get? n = some gp_n ∧ gp_n.b = b :=
    exists_s_b_of_partDen nth_partDen_eq
  simp [of_partNum_eq_one (partNum_eq_s_a nth_s_eq), zero_le_of_contsAux_b,
    GenContFract.contsAux_recurrence nth_s_eq rfl rfl]

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

Goal state before:
pp: R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
⊢ (1 ⊗ₜ[R] if ij.2 = k then b ij.1 else 0) = if ij.2 = k then (basis A b) ij.1 else 0

Tactic:
basis_apply

Goal state after:
R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
⊢ (1 ⊗ₜ[R] if ij.2 = k then b ij.1 else 0) = if ij.2 = k then 1 ⊗ₜ[R] b ij.1 else 0
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv

Goal state before:
pp: K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →ₗ[K] W := applyₗ z ∘ₗ f.toLinearMap ∘ₗ smulRightₗ v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
this : ∀ (A : End K V) (x : V), T (A x) = (f A) (T x)
surj : Function.Surjective ⇑T
x y : V
hxy : T x = T y
⊢ (smulRightₗ v) x = (smulRightₗ v) y

Tactic:
apply f.injective <| LinearMap.ext fun z ↦ ?_

Goal state after:
K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : v u ≠ 0
z✝ : W
hz : ¬(f (smulRight v u)) z✝ = 0 z✝
T : V →ₗ[K] W := applyₗ z✝ ∘ₗ f.toLinearMap ∘ₗ smulRightₗ v
hT : ∀ (x : V), T x = (f (smulRight v x)) z✝
this : ∀ (A : End K V) (x : V), T (A x) = (f A) (T x)
surj : Function.Surjective ⇑T
x y : V
hxy : T x = T y
z : W
⊢ (f ((smulRightₗ v) x)) z = (f ((smulRightₗ v) y)) z
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
e : I → R
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents (⇑f ∘ e)
⊢ CompleteOrthogonalIdempotents e

Tactic:
obtain ⟨e', h₁, h₂⟩ := lift_of_isNilpotent_ker f h he'' (fun _ ↦ ⟨_, rfl⟩)
  obtain rfl : e = e' := by
    ext i
    refine eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute
      (he _) (h₁.idem _) (h _ ?_) ((he' i).comm _)
    simpa [RingHom.mem_ker, sub_eq_zero] using congr_fun h₂.symm i
  exact h₁

Goal state after:
Module: Mathlib.Algebra.Divisibility.Prod

Goal state before:
pp: case mk.mk
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Semigroup G₁
inst✝ : Semigroup G₂
fst✝¹ : G₁
snd✝¹ : G₂
fst✝ : G₁
snd✝ : G₂
⊢ (fst✝¹, snd✝¹) ∣ (fst✝, snd✝) ↔ (fst✝¹, snd✝¹).1 ∣ (fst✝, snd✝).1 ∧ (fst✝¹, snd✝¹).2 ∣ (fst✝, snd✝).2

Tactic:
simp only [dvd_def, Prod.exists, Prod.mk_mul_mk, Prod.mk.injEq,
    exists_and_left, exists_and_right]

Goal state after:
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { _fe // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 (_fe.1 a) }
a : A
ad : A[ε]
⊢ (lift fe) (a • ad) = (↑fe).1 a * (lift fe) ad

Tactic:
by
  rw [← inl_mul_eq_smul, map_mul, lift_apply_inl]

Goal state after:
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
P : Type u_4
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
⊢ (trace R M) (h ∘ₗ g ∘ₗ f) = (trace R M) ((h ∘ₗ g) ∘ₗ f)

Tactic:
← comp_assoc

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
⊢ (trace R M) ((h ∘ₗ g) ∘ₗ f) = (trace R M) ((h ∘ₗ g) ∘ₗ f)
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
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
this : f ∘ₗ (algebraMap R (M →ₗ[R] M)) μ = μ • f
⊢ μ • (trace R M) f = μ * (trace R M) f

Tactic:
smul_eq_mul

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
this : f ∘ₗ (algebraMap R (M →ₗ[R] M)) μ = μ • f
⊢ μ * (trace R M) f = μ * (trace R M) f
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
⊢ reduce (reduce L₁ ++ reduce L₂) = reduce (L₁ ++ L₂)

Tactic:
rw [← toWord_mk (L₁ := L₁ ++ L₂), ← mul_mk, toWord_mul, toWord_mk, toWord_mk]

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

Goal state before:
pp: R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), f a = 0 ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
this : eval₂ f (f x * z) (p.scaleRoots x) = 0
⊢ (p.scaleRoots x).IsRoot y

Tactic:
hz,

Goal state after:
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), f a = 0 ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
this : eval₂ f (f y) (p.scaleRoots x) = 0
⊢ (p.scaleRoots x).IsRoot y
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case hr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ⋯
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n✝ : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n✝ + s
hs : map (algebraMap R K) s = 0
hn0 : n✝ = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n✝ = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
⊢ r.coeff x.1 ∈ P

pp: case hs
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ⋯
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n✝ : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n✝ + s
hs : map (algebraMap R K) s = 0
hn0 : n✝ = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n✝ = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
⊢ s.coeff x.2 ∈ P

Tactic:
· rw [mem_ker, ← coeff_map, hr, coeff_zero]

Goal state after:
case hs
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ⋯
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n✝ : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n✝ + s
hs : map (algebraMap R K) s = 0
hn0 : n✝ = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n✝ = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
⊢ s.coeff x.2 ∈ P
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
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ (algebraMap R K) z = (algebraMap R K) ↑⟨y, y_mem⟩ * x

Tactic:
hz,

Goal state after:
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
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ⟨y, y_mem⟩ • x = (algebraMap R K) ↑⟨y, y_mem⟩ * x
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
k m n : ℕ
x : M
⊢ x ^ k * x ^ m * x ^ n = x ^ k * (x ^ m * x ^ n)

Tactic:
simp only [← npow_add, add_assoc]

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
n : ℕ
y : M
⊢ f (y + n • h) = ∑ k ∈ range (n + 1), n.choose k • Δ_[h]^[k] f y

Tactic:
convert!
    congr_fun (LinearMap.congr_fun ((Commute.one_right (fwdDiffₗ M G h)).add_pow n) f) y using 1
  · rw [← shiftₗ_pow_apply h f, shiftₗ]
  · simp [Module.End.pow_apply, coe_fwdDiffₗ]

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 : ⇑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,

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.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✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
⊢ ⇑invMonoidHom ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f

Tactic:
image_comp,

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
⊢ ⇑invMonoidHom '' v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f
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✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
⊢ ⇑invMonoidHom '' ⇑invMonoidHom ∘ v '' IsMulIndecomposable.baseOf v f = v '' IsMulIndecomposable.baseOf v f

Tactic:
image_comp,

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
⊢ ⇑invMonoidHom '' ⇑invMonoidHom '' v '' IsMulIndecomposable.baseOf v f = v '' IsMulIndecomposable.baseOf v f
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: case refine_2
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
h₁ : ⇑invMonoidHom ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f
h₂ : v '' {i | f (v i) < 1} = v '' {i | 1 < f' (v i)}
⊢ v '' {i | 1 < f' (v i)} ⊆ ↑(closure (⇑invMonoidHom ∘ v '' IsMulIndecomposable.baseOf v f'))

Tactic:
image_comp,

Goal state after:
case refine_2
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
h₁ : ⇑invMonoidHom ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f
h₂ : v '' {i | f (v i) < 1} = v '' {i | 1 < f' (v i)}
⊢ v '' {i | 1 < f' (v i)} ⊆ ↑(closure (⇑invMonoidHom '' v '' IsMulIndecomposable.baseOf v f'))
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
Z✝ : Karoubi C
g h : Z✝ ⟶ (toKaroubi C).obj X✝
eq : g ≫ (toKaroubi C).map f = h ≫ (toKaroubi C).map f
⊢ g = h

Tactic:
ext
    rw [← cancel_mono f]
    simpa using eq

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
hi : n + i = m
⊢ X.σ₀Iter i hi ≫ X.δ₀Iter i hi = 𝟙 (X _⦋n⦌)

Tactic:
by
  simp [σ₀Iter, δ₀Iter, ← Functor.map_comp, ← op_comp]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f✝ g f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 2)
j : Fin (n✝ + 1)
hij : i ≤ j.castSucc
⊢ (X.σ j.succ ≫ f.app (op ⦋n✝ + 1 + 1⦌)) ≫ Y.δ i.castSucc = X.δ i ≫ X.σ j ≫ f.app (op ⦋n✝ + 1⦌)

Tactic:
simp [Y.δ_comp_σ_of_le hij]

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

Goal state before:
pp: n : ℕ
⊢ σ₀Iter 0 ⋯ = 𝟙 ⦋n⦌

Tactic:
ext
  simp [σ₀Iter]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Op

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v, u_1} C
X : SimplicialObject C
n : SimplexCategoryᵒᵖ
⊢ (opFunctorCompOpFunctorIso.hom.app X).app n = opObjIso.hom ≫ opObjIso.hom

Tactic:
by
  simp [opFunctorCompOpFunctorIso, opObjIso, opFunctor]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Op

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v, u_1} C
X : SimplicialObject C
n : SimplexCategoryᵒᵖ
⊢ (opFunctorCompOpFunctorIso.inv.app X).app n = opObjIso.inv ≫ opObjIso.inv

Tactic:
by
  simp [opFunctorCompOpFunctorIso, opObjIso, opFunctor]

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

Goal state before:
pp: S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 2)
x : S _⦋n + 1⦌
⊢ (ConcreteCategory.hom (SimplicialObject.δ S i ≫ f.app (op ⦋n⦌))) x =
    (ConcreteCategory.hom (f.app (op ⦋n + 1⦌) ≫ SimplicialObject.δ T i)) x

Tactic:
exact congr_hom (SimplicialObject.δ_naturality f i) x

Goal state after: