mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ #(s ^ 0) ≤ #s ^ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ Set.range f = ↑s

Tactic:
← Set.image_univ,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ f '' Set.univ = ↑s
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Monoid α
inst✝ : Monoid β
s : Finset α
t : Finset β
⊢ s ×ˢ t ^ 0 = (s ^ 0) ×ˢ (t ^ 0)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: n : ℕ
⊢ ∀ (a : Fin n), (a ∈ Finset.univ.sort fun a b ↦ a ≤ b) ↔ a ∈ List.finRange n

Tactic:
by simp

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
f : End R M
h : ∀ (g : End R M) (x : M), g (f x) = f (g x)
h✝ : Subsingleton M
⊢ ∀ (g : R), g * 0 = 0 * g

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
t : Finset α
a : α
⊢ ↑(image (fun b ↦ a * b) t) = ↑(t.preimage (fun b ↦ a⁻¹ * b) ⋯)

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
t : Finset α
b : α
⊢ ↑(image (fun x ↦ x * b) t) = ↑(t.preimage (fun x ↦ x * b⁻¹) ⋯)

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
t : Finset α
b : α
⊢ image (fun x ↦ x * b⁻¹) t = t.preimage (fun x ↦ x * b) ⋯

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq β
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
x✝ : 1 ≠ 0
⊢ ∀ (f : F) (s : Finset α), image (⇑f) (s ^ 1) = image (⇑f) s ^ 1

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
i : α
⊢ (lmapDomain R R u) (single i 1) = single (u i) 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R[X]
⊢ a.toFinsupp = toFinsupp 0 ↔ a = 0

Tactic:
toFinsupp_inj

Goal state after:
R : Type u
inst✝ : Semiring R
a : R[X]
⊢ a = 0 ↔ a = 0
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R[X]
⊢ a.toFinsupp = toFinsupp 1 ↔ a = 1

Tactic:
toFinsupp_inj

Goal state after:
R : Type u
inst✝ : Semiring R
a : R[X]
⊢ a = 1 ↔ a = 1
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ #p.support = 0 ↔ p = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
k : ℕ
ih : (monomial n) r ^ k = (monomial (n * k)) (r ^ k)
⊢ (monomial n) r ^ (k + 1) = (monomial (n * (k + 1))) (r ^ (k + 1))

Tactic:
| succ k ih =>

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ (monomial 0).toFun 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ C 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: κ : Type u_5
π : κ → Type u_6
inst✝¹ : (i : κ) → Lattice (π i)
inst✝ : Nonempty κ
⊢ (pi univ fun x ↦ ⊥) = ⊥

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
k : ℕ
ih : (monomial n) r * X ^ k = (monomial (n + k)) r
⊢ (monomial n) r * X ^ (k + 1) = (monomial (n + (k + 1))) r

Tactic:
| succ k ih =>

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ n ∉ p.support ↔ p.coeff n = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : End R M
x✝ : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ ⟨p, hp⟩ ≤ ⟨⊤, ⋯⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : End R M
x✝ : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ ⟨⊥, ⋯⟩ ≤ ⟨p, hp⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (erase n 0).toFinsupp = toFinsupp 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ (erase n ((monomial n) a)).toFinsupp = toFinsupp 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℤ
⊢ C ↑n = ↑n

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ¬X.coeff 1 = coeff 0 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : DivisionSemiring R
q : ℚ≥0
f : R[X]
⊢ q • f = C ↑q * f

Tactic:
← NNRat.smul_one_eq_cast,

Goal state after:
R : Type u
inst✝ : DivisionSemiring R
q : ℚ≥0
f : R[X]
⊢ q • f = C (q • 1) * f
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝ : CommRing R
⊢ (Multiset.map (fun a ↦ X - C a) 0).prod = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝ : CommRing R
⊢ ∀ (a b : Multiset R),
    (Multiset.map (fun a ↦ X - C a) (a + b)).prod =
      (Multiset.map (fun a ↦ X - C a) a).prod * (Multiset.map (fun a ↦ X - C a) b).prod

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
ji : (j : η) × ιs j
⊢ (Pi.basis s).repr (single ji.fst ((s ji.fst) ji.snd)) = Finsupp.single ji 1

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: ι : Type u_5
R : Type u_6
M : Type u_7
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
w : ι → R
⊢ ((piEquiv ι R M) v) w = ∑ i, w i • v i

Tactic:
simp only [piEquiv, Basis.constr_apply_fintype, Basis.equivFun_apply]
  congr

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case right
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ p ⊔ q = ⊤

Tactic:
h.sup_eq_top

Goal state after:
case right
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ ⊤ = ⊤
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : ↥p
⊢ ↑x = (p.prodEquivOfIsCompl q h) (x, 0)

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : ↥q
⊢ ↑x = (p.prodEquivOfIsCompl q h) (0, x)

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
⊢ ∀ (x : E), ↑(p.prodEquivOfIsCompl q hpq).symm x = ((p.projectionOnto q hpq).prod (q.projectionOnto p ⋯)) x

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ p ≤ (q.projectionOnto p ⋯).ker

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ₁ φ₂ : ↥p →ₗ[R] F
ψ₁ ψ₂ : ↥q →ₗ[R] F
⊢ ∀ (u : ↥p), (φ₁ + φ₂) u = (ofIsCompl h φ₁ ψ₁ + ofIsCompl h φ₂ ψ₂) ↑u

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ₁ φ₂ : ↥p →ₗ[R] F
ψ₁ ψ₂ : ↥q →ₗ[R] F
⊢ ∀ (u : ↥q), (ψ₁ + ψ₂) u = (ofIsCompl h φ₁ ψ₁ + ofIsCompl h φ₂ ψ₂) ↑u

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_7
inst✝⁴ : CommRing R
E : Type u_8
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_9
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
c : R
⊢ ∀ (u : ↥p), (c • φ) u = (c • ofIsCompl h φ ψ) ↑u

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_7
inst✝⁴ : CommRing R
E : Type u_8
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_9
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
c : R
⊢ ∀ (u : ↥q), (c • ψ) u = (c • ofIsCompl h φ ψ) ↑u

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
x : ↥p
⊢ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯) ↑x = φ x

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
x : ↥q
⊢ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯) ↑x = ψ x

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_1
⊢ ⨆ x, 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ ↑d
htop : ⨆ i, f i = ⊤
⊢ ↑d < ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case mp.mpr
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f ⇑g
x₂ : M₂
x₁ : M₁
hy₁ : f' (τ₁ x₁) = τ₂ x₂
⊢ g' (τ₂ x₂) = 1

Tactic:
rw [comm₂₃, (h x₂).2 _, map_one]

Goal state after:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f ⇑g
x₂ : M₂
x₁ : M₁
hy₁ : f' (τ₁ x₁) = τ₂ x₂
⊢ x₂ ∈ Set.range ⇑f
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case mp
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
hf : IsProj ⊤ f
x✝ : M
⊢ f x✝ = id x✝

Tactic:
simp [hf.map_id]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T : E →ₗ[R] E
hT : IsIdempotentElem T
⊢ ∀ (u : ↥T.ker), 0 u = T ↑u

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝⁴ : Semiring S
M : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst✝¹ : AddCommMonoid E
inst✝ : Module S E
p : E →ₗ[S] M
⊢ q ∘ₗ p = p ↔ p.range ≤ q.range

Tactic:
by
  simp_rw [LinearMap.ext_iff, comp_apply, ← hq.mem_range_iff,
    SetLike.le_def, mem_range, forall_exists_index, forall_apply_eq_imp_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ f.range ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = T ∘ₗ f

Tactic:
by
  rw [hf.comp_eq_right_iff, range_comp, Module.End.mem_invtSubmodule_iff_map_le]

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c x✝¹ x✝ : α
⊢ (x✝¹, x✝) ∈ ∅ → (x✝, x✝¹) ∈ ∅

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c x✝¹ x✝ : α
⊢ (x✝¹, x✝) ∈ Set.univ → (x✝, x✝¹) ∈ Set.univ

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
e : { e // f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e }
⊢ g ∘ₗ ↑(↑e).symm ∘ₗ inr R M P = LinearMap.id

Tactic:
rw [← LinearMap.comp_assoc, (LinearEquiv.eq_comp_toLinearMap_symm _ _).mp e.2.2]; rfl

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c x✝² x✝¹ x✝ : α
⊢ (x✝², x✝¹) ∈ ∅ → (x✝¹, x✝) ∈ ∅ → (x✝², x✝) ∈ ∅

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c x✝² x✝¹ x✝ : α
⊢ (x✝², x✝¹) ∈ Set.univ → (x✝¹, x✝) ∈ Set.univ → (x✝², x✝) ∈ Set.univ

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalHom

Goal state before:
pp: R : Type u
S : Type u₁
T : Type u_1
inst✝⁸ : Monoid R
inst✝⁷ : Monoid S
inst✝⁶ : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction S B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction T C
⊢ ∀ (x y : A),
    (DistribMulActionHom.toMulActionHom 0).toFun (x * y) =
      (DistribMulActionHom.toMulActionHom 0).toFun x * (DistribMulActionHom.toMulActionHom 0).toFun y

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s✝ : SetRel β β
s : RelSeries r
a : α
h : (a, s.head) ∈ r
i : Fin (s.length + 1)
⊢ s.length + 1 + 1 = (s.cons a h).length + 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
l : List α
l_ne_nil : l ≠ []
hl : List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) l
x : α
hx : (x, l.head l_ne_nil) ∈ r
⊢ x :: l ≠ []

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s✝ : SetRel β β
s : RelSeries r
a : α
h : (s.last, a) ∈ r
i : Fin (s.length + 1)
⊢ s.length + 1 + 1 = (s.snoc a h).length + 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case mpr.inr
α : Type u_1
r : SetRel α α
p : RelSeries r
x : α
rel : (p.last, x) ∈ r
⊢ ∃ y, (Fin.append p.toFun (singleton r x).toFun ∘ Fin.cast ⋯) y = x

Tactic:
· exact ⟨Fin.last _, Fin.append_right _ _ 0⟩

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
x : α
hx : (x, p.head) ∈ r
⊢ (p.cons x hx).length ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
h : p.last = q.head
i : Fin (p.length + 1)
⊢ p.length + 1 ≤ (p.smash q h).length + 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
⊢ ∀ (i : Fin 0), (![inst✝.some] i.castSucc, ![inst✝.some] i.succ) ∈ r

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
⊢ height x < height y

Tactic:
rw [← ENat.add_one_le_iff hfin.ne, height_add_const, iSup₂_le_iff]

Goal state after:
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
⊢ ∀ (i : LTSeries α), RelSeries.last i = x → ↑i.length + 1 ≤ height y
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
⊢ { length := 0, toFun := ![inst✝.some], step := ⋯ }.length = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case mpr
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
H : ∀ (n : ℕ), ∃ x, x.length = n
⊢ ∀ (x : RelSeries r), ∃ y, x.length < y.length

Tactic:
l

Goal state after:
case mpr
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
H : ∀ (n : ℕ), ∃ x, x.length = n
l : RelSeries r
⊢ ∃ y, l.length < y.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
p : LTSeries α
hlast : RelSeries.last p = x
⊢ ↑p.length ≤ ↑(p.map f hf).length

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n m : ℕ
p : LTSeries α
hne : Nonempty { p_1 // RelSeries.last p_1 = RelSeries.last p }
ha : ∀ (p_1 : LTSeries α), RelSeries.last p_1 = RelSeries.last p → p_1.length ≠ n
hp : p.length = m
hnm : n < m
⊢ (RelSeries.drop p ⟨m - n, ⋯⟩).last = RelSeries.last p

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
n : ℕ
IH :
  ∀ (s : Fin (n + 1) → α) (h : ∀ (i : Fin n), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}),
    ∃ t i,
      t.toFun ∘ ⇑i = { length := n, toFun := s, step := h }.toFun ∧
        i 0 = 0 ∧ i (Fin.last { length := n, toFun := s, step := h }.length) = Fin.last t.length
s : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
t₁ : RelSeries {(a, b) | a ⋖ b}
i : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1) ↪ Fin (t₁.length + 1)
ht : t₁.toFun ∘ ⇑i = { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length) = Fin.last t₁.length
t₂ : ℕ → α
h₁ : t₂ 0 = s (Fin.last n).castSucc
m : ℕ
h₂ : t₂ m = s (Fin.last n).succ
ht₂ : ∀ i < m, t₂ i ⋖ t₂ (i + 1)
t₃ : RelSeries {(a, b) | a ⋖ b} := { length := m, toFun := fun x ↦ t₂ ↑x, step := ⋯ }
H : t₁.last = t₂ 0
⊢ t₁.length + 1 ≤ (t₁.smash t₃ H).length + 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
p : LTSeries α
hp : RelSeries.last p = y
⊢ (RelSeries.snoc p x ⋯).last ≤ x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
p : LTSeries α
hp : RelSeries.last p = y
⊢ ↑p.length + 1 ≤ ↑(RelSeries.snoc p x ⋯).length

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
⊢ height ⊥ = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ coheight ⊤ = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
H : ∀ (i : LTSeries α), False
x : α
⊢ ∀ (i : Fin 0), (x, x) ∈ {(a, b) | a < b}

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
this :
  ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [WellFoundedLT α] [WellFoundedGT α]
    (s : LTSeries α), RelSeries.head s = ⊥ → ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
h₁ : ¬RelSeries.head s = ⊥
t : RelSeries {(a, b) | a ⋖ b}
i : Fin ((RelSeries.cons s ⊥ ⋯).length + 1) ↪ Fin (t.length + 1)
hi : t.toFun ∘ ⇑i = (RelSeries.cons s ⊥ ⋯).toFun
ht : t.head = ⊥ ∧ t.last = ⊤
j : Fin (s.length + 1)
⊢ s.length + 1 + 1 = (RelSeries.cons s ⊥ ⋯).length + 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
H : ∀ (i : LTSeries α), ↑i.length ≤ 0
x y : α
h : x < y
⊢ 0 < ↑{ length := 1, toFun := ![x, y], step := ⋯ }.length

Tactic:
by simp

Goal state after: