mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case inl
α : Type u
a : α
s : Seq α
⊢ a ∈ cons a s

Tactic:
apply mem_cons

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

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
⊢ take n (x ++ₛ a) = List.take n x

Tactic:
by
  apply List.ext_getElem (by simp [h])
  intro _ _ _; rw [List.getElem_take, take_get, get_append_left]

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 s.get s.length

Tactic:
apply results_of_terminates

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

Goal state before:
pp: α : Type u
s : Stream' (Option α)
al : s.IsSeq
⊢ Stream'.map (Option.map id) s = s

Tactic:
Option.map_id,

Goal state after:
α : Type u
s : Stream' (Option α)
al : s.IsSeq
⊢ Stream'.map id s = s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
cb : Computation β
Hc : C (pure a) cb
h : LiftRelAux R C (pure a).destruct cb.destruct
⊢ LiftRel R (pure a) cb

Tactic:
simp only [destruct_pure, LiftRelAux.ret_left] at h

Goal state after:
case refine_1
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
cb : Computation β
Hc : C (pure a) cb
h : ∃ b, b ∈ cb ∧ R a b
⊢ LiftRel R (pure a) cb
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case zero
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
a : ℤ
⊢ (IntFractPair.stream (↑a) 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b }) = none

Tactic:
stream_succ_of_int,

Goal state after:
case zero
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
a : ℤ
⊢ none.bind (some ∘ fun p ↦ { a := 1, b := ↑p.b }) = none
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_succ_n_fr_ne_zero : ifp_succ_n.fr ≠ 0
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr

Tactic:
obtain ⟨ifp_n', nth_stream_eq', ifp_n_fract_ne_zero, ⟨rfl⟩⟩ :
        ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧
          ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n :=
        IntFractPair.succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq

Goal state after:
case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n'.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n'.fr⁻¹).fr ≠ 0
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n'.fr⁻¹).fr
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil.cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
s_2 : Seq (Seq1 γ)
x : γ
t : Seq γ
⊢ (join (((a, nil), Seq.cons (x, t) s_2), SS)).join = join (join ((a, nil), Seq.cons (x, t) s_2), Seq.map join SS)

Tactic:
cases t <;> simp

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

Goal state before:
pp: case zero
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q 0) = IntFractPair.stream v 0

Tactic:
simp only [IntFractPair.stream, Option.map_some, coe_of_rat_eq v_eq_q]

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 : ι × ι'
⊢ baseChange A ((b'.linearMap b) ij) = ((basis A b').linearMap (basis A b)) ij

Tactic:
apply (basis A b').ext

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 : ι × ι'
⊢ ∀ (i : ι'),
    (baseChange A ((b'.linearMap b) ij)) ((basis A b') i) = (((basis A b').linearMap (basis A b)) ij) ((basis A b') i)
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : Fintype I
⊢ CompleteOrthogonalIdempotents e ↔ (Pairwise fun x1 x2 ↦ e x1 * e x2 = 0) ∧ ∑ i, e i = 1

Tactic:
completeOrthogonalIdempotents_iff,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : Fintype I
⊢ OrthogonalIdempotents e ∧ ∑ i, e i = 1 ↔ (Pairwise fun x1 x2 ↦ e x1 * e x2 = 0) ∧ ∑ i, e i = 1
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
I : Type u_3
e : I → R
inst✝¹ : Fintype I
inst✝ : Unique I
⊢ CompleteOrthogonalIdempotents e ↔ e default = 1

Tactic:
completeOrthogonalIdempotents_iff,

Goal state after:
R : Type u_1
inst✝² : Semiring R
I : Type u_3
e : I → R
inst✝¹ : Fintype I
inst✝ : Unique I
⊢ OrthogonalIdempotents e ∧ ∑ i, e i = 1 ↔ e default = 1
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case succ
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 : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : f e₀ = e 0
h₅ : e₀ * ∑ i, e' i = 0
h₆ : (∑ i, e' i) * e₀ = 0
i : Fin (n + 1)
⊢ (⇑f ∘ (fun x ↦ x.elim e₀ e') ∘ ⇑(finSuccEquiv n).toEmbedding) i = e i

Tactic:
obtain ⟨_ | i, rfl⟩ := (finSuccEquiv n).symm.surjective i <;> simp [*]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Type u_3
e : I → R
inst✝ : Fintype I
he : OrthogonalIdempotents e
⊢ ∑ i, i.elim (1 - ∑ i, e i) e = 1

Tactic:
rw [Fintype.sum_option]
    exact sub_add_cancel _ _

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr.inr.succ.zero
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
h✝¹ : Nontrivial R
h✝ : Nontrivial S
n : ℕ
e : Fin (n + 1) → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin (n + 1) → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e
this : ∀ (i : Fin (n + 1)), f (e' i) = e i
⊢ (⇑f ∘ (fun x ↦ x.elim (1 - ∑ i, (e' ∘ ⇑(Fin.succEmb n)) i) (e' ∘ ⇑(Fin.succEmb n))) ∘ ⇑(finSuccEquiv n)) 0 = e 0

Tactic:
simp [this, Fin.sum_univ_succ, ← he.complete]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s : Finset I
⊢ ∀ (a : I) (s : Finset I), a ∉ s → (∏ i ∈ s, (1 - e i)) * x = x → (∏ i ∈ insert a s, (1 - e i)) * x = x

Tactic:
intro a s has e'

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s✝ : Finset I
a : I
s : Finset I
has : a ∉ s
e' : (∏ i ∈ s, (1 - e i)) * x = x
⊢ (∏ i ∈ insert a s, (1 - e i)) * x = x
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)
x y : Matrix n n R
⊢ c x y → (matrix n c.ofMatrix) x y

Tactic:
· 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.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k : I → R
hk : ∀ (i : I), e' i * e' i - e' i = e₀ * k i
⊢ f e₀ = 0

Tactic:
simpa using hfe₀.ge (Ideal.mem_span_singleton_self _)

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ r ∈ corner e ↔ r * e = r

Tactic:
mem_corner_iff_mul_left idem hc,

Goal state after:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ e * r = r ↔ r * e = r
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e r : R
he : IsIdempotentElem e
I : Ideal R
⊢ (Quotient.mk (span {e})) r ∈ map (Quotient.mk (span {e})) I ↔ (1 - e) * r ∈ I

Tactic:
simp only [Ideal.mem_map_iff_of_surjective _ Ideal.Quotient.mk_surjective,
    Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.mem_span_singleton]

Goal state after:
R : Type u_1
inst✝ : CommRing R
e r : R
he : IsIdempotentElem e
I : Ideal R
⊢ (∃ x ∈ I, e ∣ x - r) ↔ (1 - e) * r ∈ I
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g h : M →ₗ[R] M
⊢ (trace R M) (f * (g * h)) - (trace R M) (g * (f * h)) = (trace R M) (f * (g * h)) - (trace R M) (f * (h * g))

Tactic:
trace_mul_comm R g (f * h),

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g h : M →ₗ[R] M
⊢ (trace R M) (f * (g * h)) - (trace R M) (f * h * g) = (trace R M) (f * (g * h)) - (trace R M) (f * (h * g))
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
μ t : R
k : ℕ∞
m : M
hm : m ∈ (f.genEigenspace μ) k
⊢ m ∈ ((t • f).genEigenspace (t * μ)) k

Tactic:
simp_rw [mem_genEigenspace, ← exists_prop, LinearMap.mem_ker] at hm ⊢

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ l, ∃ (_ : ↑l ≤ k), ((f - μ • 1) ^ l) m = 0
⊢ ∃ l, ∃ (_ : ↑l ≤ k), ((t • f - (t * μ) • 1) ^ l) m = 0
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
hg : IsNilpotent (g - (algebraMap R (End R M)) μ)
⊢ (trace R M) (f ∘ₗ g) = μ * (trace R M) f

Tactic:
set n := g - algebraMap R _ μ
  replace hg : trace R M (f ∘ₗ n) = 0 := by
    rw [← isNilpotent_iff_eq_zero, ← Module.End.mul_eq_comp]
    refine isNilpotent_trace_of_isNilpotent (Commute.isNilpotent_mul_left ?_ hg)
    exact h_comm.sub_right (Algebra.commute_algebraMap_right μ f)
  have hμ : g = algebraMap R _ μ + n := eq_add_of_sub_eq' rfl
  have : f ∘ₗ algebraMap R _ μ = μ • f := by ext; simp -- TODO Surely exists?
  rw [hμ, comp_add, map_add, hg, add_zero, this, map_smul, smul_eq_mul]

Goal state after:
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
inst✝⁴ : IsDomain R
inst✝³ : IsTorsionFree R M
L : Type u_1
F : Type u_2
inst✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
g : L → Submodule R M := fun x ↦ ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g (t • x)
⊢ Disjoint (((t • f x).genEigenspace (t * μ x)) k) (((t • f x).genEigenspace (μ (t • x))) k)

Tactic:
exact disjoint_genEigenspace (t • f x) (Ne.symm contra) k k

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
⊢ ∀ (a b₁ b₂ : α), AssocRel α b₁ b₂ → Quot.mk (AssocRel α) (a * b₁) = Quot.mk (AssocRel α) (a * b₂)

Tactic:
rintro a b₁ b₂ (⟨c, d, e⟩ | ⟨c, d, e, f⟩)
      · exact quot_mk_assoc_left _ _ _ _
      · rw [← quot_mk_assoc, quot_mk_assoc_left, quot_mk_assoc]

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

Goal state before:
pp: α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : reduce L = L
x₁ : α
x₂ y₂ : Bool
l₁ l₂ : List (α × Bool)
hl : L = l₁ ++ (x₁, x₂) :: ((x₁, x₂).1, y₂) :: l₂
⊢ (x₁, x₂).2 = ((x₁, x₂).1, y₂).2

Tactic:
rw [eq_comm, ← Bool.ne_not]

Goal state after:
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : reduce L = L
x₁ : α
x₂ y₂ : Bool
l₁ l₂ : List (α × Bool)
hl : L = l₁ ++ (x₁, x₂) :: ((x₁, x₂).1, y₂) :: l₂
⊢ ((x₁, x₂).1, y₂).2 ≠ !(x₁, x₂).2
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: 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 := ker (algebraMap R K)
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
⊢ IsUnit g ∨ IsUnit h

Tactic:
by_cases hm : m = 0

Goal state after:
case pos
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 := ker (algebraMap R K)
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
⊢ IsUnit g ∨ IsUnit h

case neg
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 := ker (algebraMap R K)
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
⊢ IsUnit g ∨ IsUnit h
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_4
K : Type u_5
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : FaithfulSMul R K
inst✝ : IsIntegrallyClosedIn R K
this : IsDomain R
f : FractionRing R →ₐ[R] K := ⋯
x : FractionRing R
hx : IsIntegral R x
x✝ : R
⊢ (algebraMap R (FractionRing R)) x✝ = x ↔ (algebraMap R K) x✝ = f x

Tactic:
simp [← f.toRingHom.injective.eq_iff]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : CommRing U
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : Algebra R U
inst✝⁵ : Algebra S U
inst✝⁴ : Algebra T U
inst✝³ : IsScalarTower S T U
inst✝² : IsScalarTower R T U
inst✝¹ : IsIntegralClosure S R T
inst✝ : IsIntegrallyClosedIn T U
⊢ IsIntegralClosure S R U

Tactic:
refine ⟨?_, ?_⟩
  · rw [IsScalarTower.algebraMap_eq S T U]
    exact (IsIntegralClosure.algebraMap_injective T T U).comp
      (IsIntegralClosure.algebraMap_injective S R T)
  · intro x
    refine ⟨fun h ↦ ?_, ?_⟩
    · obtain ⟨x, rfl⟩ := (IsIntegralClosure.isIntegral_iff (R := T) (A := T)).mp h.tower_top
      rw [isIntegral_algebraMap_iff (IsIntegralClosure.algebraMap_injective T T U)] at h
      obtain ⟨x, rfl⟩ := (IsIntegralClosure.isIntegral_iff (R := R) (A := S)).mp h
      exact ⟨x, IsScalarTower.algebraMap_apply ..⟩
    · rintro ⟨x, rfl⟩
      rw [IsScalarTower.algebraMap_apply S T U]
      exact ((IsIntegralClosure.isIntegral_iff (A := S) (R := R) (B := T)).mpr ⟨x, rfl⟩).map
        (IsScalarTower.toAlgHom R T U)

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.IntegrallyClosed

Goal state before:
pp: case h
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
a✝ : GCDMonoid R
x y : R
hg : IsUnit (gcd x y)
he : X * (algebraMap R (FractionRing R)) y = (algebraMap R (FractionRing R)) x
this✝ : y ∣ x ^ p.natDegree
this : IsUnit y
coe_map_inv : ↑((Units.map ↑(algebraMap R (FractionRing R))) this.unit)⁻¹ = (algebraMap R (FractionRing R)) ↑this.unit⁻¹
⊢ X * ↑((Units.map ↑(algebraMap R (FractionRing R))) this.unit) = (algebraMap R (FractionRing R)) x

Tactic:
exact he

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
a : A
⊢ embedding ((restrict₀ f) a) = f a

Tactic:
by
  simp only [restrict₀_apply, embedding_apply]
  aesop

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsReduced M
ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y
⊢ IsMulTorsionFree M

Tactic:
refine ⟨fun n hn x y hxy ↦ ?_⟩
  by_cases h : x ≠ 0 ∧ y ≠ 0
  · exact ih x h.1 y h.2 n hn hxy
  grind [eq_zero_of_pow_eq_zero, zero_pow]

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

Goal state before:
pp: case mpr
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' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p') → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
apply split_imp_of_iso φ.symm p' p
    rw [← comp_id p, ← φ.hom_inv_id]
    slice_rhs 2 3 => rw [hpp']
    simp

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

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
⊢ j.castSucc.predAbove k.succ = i.succAbove (j.predAbove k)

Tactic:
have hjk := H.trans hik

Goal state after:
case inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
hjk : j.castSucc < k
⊢ j.castSucc.predAbove k.succ = i.succAbove (j.predAbove k)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ X.δ i ≫ X.δ j.succ = X.δ j ≫ X.δ i.castSucc

Tactic:
by
  dsimp [δ]
  simp only [← X.map_comp, SimplexCategory.δ_comp_δ H]

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 : X ⟶ Y
H : Homotopy f g
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
n : ℕ
⊢ F.map (H.h 0) ≫ (((whiskering C D).obj F).obj Y).δ 0 = (((whiskering C D).obj F).map g).app (op ⦋n⦌)

Tactic:
by
    simpa [SimplicialObject.δ] using!
      congrArg (fun k => F.map k) (H.h_zero_comp_δ_zero n)

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

Goal state before:
pp: n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
⊢ ∃ θ', θ = σ i ≫ θ'

Tactic:
by
  use δ i.succ ≫ θ
  ext x : 3
  simp only [len_mk, σ, mkHom, comp_toOrderHom, Hom.toOrderHom_mk, OrderHom.comp_coe,
    Function.comp_apply, Fin.predAboveOrderHom_coe]
  by_cases h' : x ≤ Fin.castSucc i
  · rw [Fin.predAbove_of_le_castSucc i x h']
    dsimp [δ]
    rw [Fin.succAbove_of_castSucc_lt]
    · rw [Fin.castSucc_castPred]
    · exact (Fin.castSucc_lt_succ_iff.mpr h')
  · simp only [not_le] at h'
    let y := x.pred <| by rintro (rfl : x = 0); simp at h'
    have hy : x = y.succ := (Fin.succ_pred x _).symm
    rw [hy] at h' ⊢
    rw [Fin.predAbove_of_castSucc_lt i y.succ h', Fin.pred_succ]
    by_cases h'' : y = i
    · rw [h'']
      refine hi.symm.trans ?_
      congr 1
      dsimp [δ]
      rw [Fin.succAbove_of_castSucc_lt i.succ]
      exact Fin.castSucc_lt_succ
    · dsimp [δ]
      rw [Fin.succAbove_of_le_castSucc i.succ _]
      simp only [Fin.lt_def, Fin.le_iff_val_le_val, Fin.val_succ, Fin.val_castSucc,
        Nat.lt_succ_iff, Fin.ext_iff] at h' h'' ⊢
      lia

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

Goal state before:
pp: X Y : SSet
y : Y _⦋0⦌
x✝³ x✝² : SimplexCategoryᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : X.obj x✝³
⊢ (ConcreteCategory.hom (Y.map ((Opposite.unop x✝²).const ⦋0⦌ 0).op)) y =
    (ConcreteCategory.hom (Y.map ((Opposite.unop x✝³).const ⦋0⦌ 0).op ≫ Y.map x✝¹)) y

Tactic:
← Functor.map_comp

Goal state after:
X Y : SSet
y : Y _⦋0⦌
x✝³ x✝² : SimplexCategoryᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : X.obj x✝³
⊢ (ConcreteCategory.hom (Y.map ((Opposite.unop x✝²).const ⦋0⦌ 0).op)) y =
    (ConcreteCategory.hom (Y.map (((Opposite.unop x✝³).const ⦋0⦌ 0).op ≫ x✝¹))) y
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ f, (ConcreteCategory.hom (F.map f)) x = y) → ∃ y_1, (ConcreteCategory.hom ((yonedaEquiv.symm x).app U)) y_1 = y

Tactic:
rintro ⟨f, rfl⟩
    exact ⟨f.unop, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U → ∃ x_1, (ConcreteCategory.hom (F.map x_1.op)) x = y

Tactic:
rintro ⟨f, rfl⟩
    exact ⟨f.unop, rfl⟩

Goal state after: