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

Goal state before:
pp: α : Type u
R : α → α → Prop
inst✝ : IsTrans α R
hd tl_hd : α
tl_tl : Seq α
h_hd : R hd tl_hd
h_tl : Pairwise R (Seq.cons tl_hd tl_tl)
⊢ Pairwise R (Seq.cons hd (Seq.cons tl_hd tl_tl))

Tactic:
by
  apply Pairwise.cons _ h_tl
  simp only [mem_cons_iff, forall_eq_or_imp]
  exact ⟨h_hd, fun x hx ↦ Trans.simple h_hd ((cons_elim h_tl).left x hx)⟩

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

Goal state before:
pp: case inr
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
⊢ |v - (of v).convs n| < ε

Tactic:
suffices 1 / (B * nB) < ε from lt_of_le_of_lt abs_v_sub_conv_le this

Goal state after:
case inr
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
⊢ 1 / (B * nB) < ε
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ C (φ P.toPoly.leadingCoeff) * (Multiset.map (fun x ↦ X - C x) (Polynomial.map φ P.toPoly).roots).prod =
    C (φ P.a) * (X - C x) * (X - C y) * (X - C z)

Tactic:
leadingCoeff_of_a_ne_zero ha,

Goal state after:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ C (φ P.a) * (Multiset.map (fun x ↦ X - C x) (Polynomial.map φ P.toPoly).roots).prod =
    C (φ P.a) * (X - C x) * (X - C y) * (X - C z)
Module: Mathlib.GroupTheory.Congruence.BigOperators

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

Tactic:
induction l with
  | nil =>
    simpa only [List.map_nil, List.prod_nil] using c.refl 1
  | cons x xs ih =>
    rw [List.map_cons, List.map_cons, List.prod_cons, List.prod_cons]
    exact c.mul (h _ <| .head _) <| ih fun k hk ↦ h _ (.tail _ hk)

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),
    (∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I) →
      ∀ (i j : n) (y : Matrix n n R), ∃ z, z * y * single i j x + z - 1 ∈ matrix n I

Tactic:
intro x

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
⊢ (∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I) →
    ∀ (i j : n) (y : Matrix n n R), ∃ z, z * y * single i j x + z - 1 ∈ matrix n I
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun i j ↦ IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
⊢ Function.Surjective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i}))

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun i j ↦ IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : (i : I) → R ⧸ Ideal.span {1 - e i}
⊢ ∃ a, (RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) a = x
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
⊢ ∀ (a : R), (RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) a = 0 → a = 0

Tactic:
intro x

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
⊢ (RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) x = 0 → x = 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
f : End R M
μ : R
h : f.HasUnifEigenvalue μ 1
n : ℕ
m : M
hm : f.HasUnifEigenvector μ 1 m
⊢ m ∈ ((f ^ n).genEigenspace (μ ^ n)) 1

Tactic:
simpa [mem_genEigenspace_one] using hm.pow_apply n

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
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
⊢ (f.genEigenspace μ) k ≤ ⊥

Tactic:
intro x

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
⊢ x ∈ (f.genEigenspace μ) k → x ∈ ⊥
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 g : End R M
h : Commute f g
μ : R
k : ℕ∞
⊢ MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)

Tactic:
intro x

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
h : Commute f g
μ : R
k : ℕ∞
x : M
⊢ x ∈ ↑((f.genEigenspace μ) k) → g x ∈ ↑((f.genEigenspace μ) k)
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_1.some.some
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
i j : I
h : some i ≠ some j
k : R
hk : e' i * e' j = e₀ * k
⊢ (1 - e₀) * e' i * ((1 - e₀) * e' j) = 0

Tactic:
mul_mul_mul_comm,

Goal state after:
case refine_1.some.some
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
i j : I
h : some i ≠ some j
k : R
hk : e' i * e' j = e₀ * k
⊢ (1 - e₀) * (1 - e₀) * (e' i * e' j) = 0
Module: Mathlib.Algebra.DirectSum.LinearMap

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

Tactic:
let _ : Fintype {i // N i ≠ ⊥} := hN.fintype

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

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
n : ℕ∞
⊢ (f.genEigenspace μ) n ∈ f.invtSubmodule

Tactic:
intro x

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
n : ℕ∞
x : M
⊢ x ∈ (f.genEigenspace μ) n → x ∈ Submodule.comap f ((f.genEigenspace μ) n)
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r₁ r₂ : R
i : I
⊢ ↑⟨(fun x ↦ e i * x * e i) (r₁ + r₂), ⋯⟩ =
    ↑(((fun i ↦ ⟨(fun x ↦ e i * x * e i) r₁, ⋯⟩) + fun i ↦ ⟨(fun x ↦ e i * x * e i) r₂, ⋯⟩) i)

Tactic:
by simpa [mul_add] using! add_mul ..

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ((toMatrix c b) id * (toMatrix c c) f * (toMatrix b c) id).trace =
    ((toMatrix c c) f * (toMatrix b c) id * (toMatrix c b) id).trace

Tactic:
by
        rw [Matrix.mul_assoc, Matrix.trace_mul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case pos
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis (↥s) R M)
⊢ (trace R M) (f * g) = (trace R M) (g * f)

Tactic:
let ⟨s, ⟨b⟩⟩ := H

Goal state after:
case pos
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis (↥s) R M)
s : Finset M
b : Basis (↥s) R M
⊢ (trace R M) (f * g) = (trace R M) (g * f)
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 μ₂)
⊢ MapsTo ⇑(LinearMap.restrict f hf) ↑(maxGenEigenspace (LinearMap.restrict g hg) μ₁)
    ↑(maxGenEigenspace (LinearMap.restrict g hg) μ₂)

Tactic:
intro x

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
⊢ x ∈ ↑(maxGenEigenspace (LinearMap.restrict g hg) μ₁) →
    (LinearMap.restrict f hf) x ∈ ↑(maxGenEigenspace (LinearMap.restrict g hg) μ₂)
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
hμp : Disjoint (f.eigenspace μ) p
⊢ eigenspace (LinearMap.restrict f hfp) μ ≤ ⊥

Tactic:
intro x

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
hμp : Disjoint (f.eigenspace μ) p
x : ↥p
⊢ x ∈ eigenspace (LinearMap.restrict f hfp) μ → x ∈ ⊥
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
inv : Inv α := e.Inv
⊢ DivisionRing α

Tactic:
let div := e.div

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
inv : Inv α := e.Inv
div : Div α := e.div
⊢ DivisionRing α
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
⊢ Field α

Tactic:
let div := e.div

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
⊢ Field α
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₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hg₂ : Function.MulExact ⇑g₂ ⇑g₃
hi₁ : Function.Surjective ⇑i₁
hi₃ : Function.Surjective ⇑i₃
hi₄ : Function.Injective ⇑i₄
⊢ Function.Surjective ⇑i₂

Tactic:
intro x

Goal state after:
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₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hg₂ : Function.MulExact ⇑g₂ ⇑g₃
hi₁ : Function.Surjective ⇑i₁
hi₃ : Function.Surjective ⇑i₃
hi₄ : Function.Injective ⇑i₄
x : N₂
⊢ ∃ a, i₂ a = x
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 := IsFractionRing.liftAlgHom ⋯
⊢ ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, (algebraMap R (FractionRing R)) y = x

Tactic:
intro x

Goal state after:
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 := IsFractionRing.liftAlgHom ⋯
x : FractionRing R
⊢ IsIntegral R x → ∃ y, (algebraMap R (FractionRing R)) y = x
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝² : CommRing R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ ↑((algebraMap S R) 1) = 1

Tactic:
by simp only [map_one, coe_one]

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

Goal state before:
pp: case refine_2
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
⊢ ∀ {x : U}, IsIntegral R x ↔ ∃ y, (algebraMap S U) y = x

Tactic:
intro x

Goal state after:
case refine_2
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
x : U
⊢ IsIntegral R x ↔ ∃ y, (algebraMap S U) y = x
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : Monoid M
v : ι → M
s : Set ι
⊢ {i | IsMulIndecomposable v s i} ⊆ s

Tactic:
by
  aesop

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : GroupWithZero G
inst✝ : GroupWithZero H
f : G →*₀ H
a : H
ha : a ∈ MonoidHom.mrange f
h : ¬a = ↑0
⊢ ⟨a, ha⟩ * ⟨(↑⟨a, ha⟩)⁻¹, ⋯⟩ = 1

Tactic:
simpa using mul_inv_cancel₀ h

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : GroupWithZero G
inst✝ : GroupWithZero H
f : G →*₀ H
⊢ ∀ (a : ↥(MonoidHom.mrange f)), a ≠ 0 → a * ⟨(↑a)⁻¹, ⋯⟩ = 1

Tactic:
by
    rintro ⟨a, ha⟩ h
    simp only [ne_eq, Subtype.ext_iff] at h
    simpa using mul_inv_cancel₀ h

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
⊢ (restrict₀ f) a = 0 ↔ f a = 0

Tactic:
simp [restrict₀_apply]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ Function.Surjective ⇑(restrict₀ f)

Tactic:
intro x

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : f.ValueGroup₀
⊢ ∃ a, (restrict₀ f) a = x
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
r₁ s₁ r₂ s₂ : A
hr₁ : f r₁ ≠ 0
hs₁ : f s₁ ≠ 0
hr₂ : f r₂ ≠ 0
hs₂ : f s₂ ≠ 0
⊢ (Units.mk0 (f r₁) hr₁)⁻¹ * Units.mk0 (f s₁) hs₁ * ((Units.mk0 (f r₂) hr₂)⁻¹ * Units.mk0 (f s₂) hs₂) =
    (Units.mk0 (f r₁) ⋯ * Units.mk0 (f r₂) ⋯)⁻¹ * (Units.mk0 (f s₁) ⋯ * Units.mk0 (f s₂) ⋯)

Tactic:
mul_mul_mul_comm,

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
r₁ s₁ r₂ s₂ : A
hr₁ : f r₁ ≠ 0
hs₁ : f s₁ ≠ 0
hr₂ : f r₂ ≠ 0
hs₂ : f s₂ ≠ 0
⊢ (Units.mk0 (f r₁) hr₁)⁻¹ * (Units.mk0 (f r₂) hr₂)⁻¹ * (Units.mk0 (f s₁) hs₁ * Units.mk0 (f s₂) hs₂) =
    (Units.mk0 (f r₁) ⋯ * Units.mk0 (f r₂) ⋯)⁻¹ * (Units.mk0 (f s₁) ⋯ * Units.mk0 (f s₂) ⋯)
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Abelian D
⊢ IsIdempotentComplete D

Tactic:
isIdempotentComplete_iff_idempotents_have_kernels

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Abelian D
⊢ ∀ (X : D) (p : X ⟶ X), p ≫ p = p → HasKernel p
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: x y : SimplexCategory
h : x = y
⊢ Hom.toOrderHom (eqToHom h) = (Fin.castOrderIso ⋯).toOrderEmbedding.toOrderHom

Tactic:
by
  subst h
  rfl

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

Goal state before:
pp: n : ℕ
j : Fin (n + 2)
k : Fin (⦋n⦌.len + 1)
i : ℕ
isLt✝ : i < n + 2
H : ⟨i, isLt✝⟩ ≤ j
⊢ ↑(if (if k.castSucc < ⟨i, isLt✝⟩ then k.castSucc else k.succ).castSucc < j.succ then
        (if k.castSucc < ⟨i, isLt✝⟩ then k.castSucc else k.succ).castSucc
      else (if k.castSucc < ⟨i, isLt✝⟩ then k.castSucc else k.succ).succ) =
    ↑(if (if k.castSucc < j then k.castSucc else k.succ).castSucc < ⟨i, isLt✝⟩.castSucc then
        (if k.castSucc < j then k.castSucc else k.succ).castSucc
      else (if k.castSucc < j then k.castSucc else k.succ).succ)

Tactic:
rcases j with ⟨j, _⟩

Goal state after:
n : ℕ
k : Fin (⦋n⦌.len + 1)
i : ℕ
isLt✝¹ : i < n + 2
j : ℕ
isLt✝ : j < n + 2
H : ⟨i, isLt✝¹⟩ ≤ ⟨j, isLt✝⟩
⊢ ↑(if (if k.castSucc < ⟨i, isLt✝¹⟩ then k.castSucc else k.succ).castSucc < ⟨j, isLt✝⟩.succ then
        (if k.castSucc < ⟨i, isLt✝¹⟩ then k.castSucc else k.succ).castSucc
      else (if k.castSucc < ⟨i, isLt✝¹⟩ then k.castSucc else k.succ).succ) =
    ↑(if (if k.castSucc < ⟨j, isLt✝⟩ then k.castSucc else k.succ).castSucc < ⟨i, isLt✝¹⟩.castSucc then
        (if k.castSucc < ⟨j, isLt✝⟩ then k.castSucc else k.succ).castSucc
      else (if k.castSucc < ⟨j, isLt✝⟩ then k.castSucc else k.succ).succ)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.castSucc.castSucc

Tactic:
simp at * <;> lia

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

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.castSucc.succ

Tactic:
simp at * <;> lia

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

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.succ.castSucc

Tactic:
simp at * <;> lia

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

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.succ.succ

Tactic:
simp at * <;> lia

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

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.succ = ↑⟨k, isLt✝⟩.castSucc.castSucc

Tactic:
simp at * <;> lia

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

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.succ = ↑⟨k, isLt✝⟩.castSucc.succ

Tactic:
simp at * <;> lia

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

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.succ = ↑⟨k, isLt✝⟩.succ.castSucc

Tactic:
simp at * <;> lia

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

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.succ = ↑⟨k, isLt✝⟩.succ.succ

Tactic:
simp at * <;> lia

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

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ¬⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.succ.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.succ.castSucc = ↑⟨k, isLt✝⟩.castSucc.castSucc

Tactic:
simp at * <;> lia

Goal state after: