mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_1
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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
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
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
⊢ Bijective ⇑((↑l).prod g)

Tactic:
have h₂ : ∀ x, g (f x) = 0 := congr_fun h.comp_eq_zero

Goal state after:
case refine_1
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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
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
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ Bijective ⇑((↑l).prod g)
Module: Mathlib.Order.RelSeries

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

Tactic:
dsimp; lia

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
connect : (p.last, q.head) ∈ r
i : Fin (q.length + 1)
⊢ p.length + 1 + (q.length + 1) = (p.append q connect).length + 1

Tactic:
dsimp; lia

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

Goal state before:
pp: case refine_2
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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
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
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
⊢ f = ↑(LinearEquiv.ofBijective ((↑l).prod g) ⋯).symm ∘ₗ inl R M P ∧
    g = snd R M P ∘ₗ ↑(LinearEquiv.ofBijective ((↑l).prod g) ⋯)

Tactic:
have h₂ : ∀ x, g (f x) = 0 := congr_fun h.comp_eq_zero

Goal state after:
case refine_2
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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
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
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ f = ↑(LinearEquiv.ofBijective ((↑l).prod g) ⋯).symm ∘ₗ inl R M P ∧
    g = snd R M P ∘ₗ ↑(LinearEquiv.ofBijective ((↑l).prod g) ⋯)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ ↑p.length ≤ height x

Tactic:
let p' := p.eraseLast.snoc x (by
      apply lt_of_lt_of_le
      · apply p.step ⟨p.length - 1, by lia⟩
      · convert! hlast
        simp only [Fin.succ_mk, RelSeries.last, Fin.last]
        congr; lia)
    suffices p'.length ≤ height x by
      simp only [RelSeries.snoc_length, RelSeries.eraseLast_length, Nat.cast_add, ENat.natCast_sub,
        Nat.cast_one, p'] at this
      convert! this
      norm_cast
      lia
    refine le_iSup₂_of_le p' ?_ le_rfl
    simp [p']

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
g : { f // StrictMono f.snd }
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono ⟨lf, f⟩.snd
e : (fun f ↦ mk (↑(↑f).fst) (↑f).snd ⋯) ⟨⟨lf, f⟩, mf⟩ = (fun f ↦ mk (↑(↑f).fst) (↑f).snd ⋯) g
⊢ ⟨⟨lf, f⟩, mf⟩ = g

Tactic:
obtain ⟨⟨lg, g⟩, mg⟩ := g

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono ⟨lf, f⟩.snd
lg : Fin n
g : Fin (↑lg + 1) → α
mg : StrictMono ⟨lg, g⟩.snd
e : (fun f ↦ mk (↑(↑f).fst) (↑f).snd ⋯) ⟨⟨lf, f⟩, mf⟩ = (fun f ↦ mk (↑(↑f).fst) (↑f).snd ⋯) ⟨⟨lg, g⟩, mg⟩
⊢ ⟨⟨lf, f⟩, mf⟩ = ⟨⟨lg, g⟩, mg⟩
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁸ : CommSemiring R
inst✝³⁷ : CommSemiring R₂
inst✝³⁶ : CommSemiring R₃
inst✝³⁵ : Monoid R'
inst✝³⁴ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³³ : AddCommMonoid M
inst✝³² : AddCommMonoid N
inst✝³¹ : AddCommMonoid P
inst✝³⁰ : AddCommMonoid Q
inst✝²⁹ : AddCommMonoid S
inst✝²⁸ : AddCommMonoid P'
inst✝²⁷ : AddCommMonoid Q'
inst✝²⁶ : AddCommMonoid M₂
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid P₂
inst✝²³ : AddCommMonoid Q₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid N₃
inst✝²⁰ : AddCommMonoid P₃
inst✝¹⁹ : AddCommMonoid Q₃
inst✝¹⁸ : DistribMulAction R' M
inst✝¹⁷ : Module R'' M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module R N
inst✝¹⁴ : Module R S
inst✝¹³ : Module R P'
inst✝¹² : Module R Q'
inst✝¹¹ : Module R₂ M₂
inst✝¹⁰ : Module R₂ N₂
inst✝⁹ : Module R₂ P₂
inst✝⁸ : Module R₂ Q₂
inst✝⁷ : Module R₃ M₃
inst✝⁶ : Module R₃ N₃
inst✝⁵ : Module R₃ P₃
inst✝⁴ : Module R₃ Q₃
inst✝³ : SMul R' R
inst✝² : IsScalarTower R' R M
inst✝¹ : DistribMulAction R' N
inst✝ : IsScalarTower R' R N
r : R'
m : M
n : N
⊢ (r • m) ⊗ₜ[R] n = m ⊗ₜ[R] (r • n)

Tactic:
conv_lhs => rw [← one_smul R m]
    conv_rhs => rw [← one_smul R n]
    rw [← smul_assoc, ← smul_assoc]
    exact Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_smul _ _ _

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
⊢ 0 < krullDim α ↔ Nontrivial α

Tactic:
← not_subsingleton_iff_nontrivial,

Goal state after:
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
⊢ 0 < krullDim α ↔ ¬Subsingleton α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
⊢ 0 < krullDim α ↔ Nontrivial α

Tactic:
← not_subsingleton_iff_nontrivial,

Goal state after:
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
⊢ 0 < krullDim α ↔ ¬Subsingleton α
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
R'' : Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring R''
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R'' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R'' M
r s : R''
x✝ : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : (r + s) • x = r • x + s • x
ihy : (r + s) • y = r • y + s • y
⊢ r • x + s • x + (r • y + s • y) = r • x + r • y + (s • x + s • y)

Tactic:
add_add_add_comm

Goal state after:
R : Type u_1
R'' : Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring R''
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R'' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R'' M
r s : R''
x✝ : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : (r + s) • x = r • x + s • x
ihy : (r + s) • y = r • y + s • y
⊢ r • x + r • y + (s • x + s • y) = r • x + r • y + (s • x + s • y)
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
n : N
hn : IsAddUnit n
m : M
⊢ IsAddUnit (m ⊗ₜ[R] n)

Tactic:
by
  rw [isAddUnit_iff_exists_neg] at hn ⊢
  have ⟨b, eq⟩ := hn
  exact ⟨m ⊗ₜ[R] b, by rw [← tmul_add, eq, tmul_zero]⟩

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝⁴⁹ : CommSemiring R
inst✝⁴⁸ : CommSemiring R₂
inst✝⁴⁷ : CommSemiring R₃
inst✝⁴⁶ : Monoid R'
inst✝⁴⁵ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A✝ : Type u_6
M✝ : Type u_7
N✝ : Type u_8
P : Type u_9
Q : Type u_10
S✝ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝⁴⁴ : AddCommMonoid M✝
inst✝⁴³ : AddCommMonoid N✝
inst✝⁴² : AddCommMonoid P
inst✝⁴¹ : AddCommMonoid Q
inst✝⁴⁰ : AddCommMonoid S✝
inst✝³⁹ : AddCommMonoid P'
inst✝³⁸ : AddCommMonoid Q'
inst✝³⁷ : AddCommMonoid M₂
inst✝³⁶ : AddCommMonoid N₂
inst✝³⁵ : AddCommMonoid P₂
inst✝³⁴ : AddCommMonoid Q₂
inst✝³³ : AddCommMonoid M₃
inst✝³² : AddCommMonoid N₃
inst✝³¹ : AddCommMonoid P₃
inst✝³⁰ : AddCommMonoid Q₃
inst✝²⁹ : DistribMulAction R' M✝
inst✝²⁸ : Module R'' M✝
inst✝²⁷ : Module R M✝
inst✝²⁶ : Module R N✝
inst✝²⁵ : Module R S✝
inst✝²⁴ : Module R P'
inst✝²³ : Module R Q'
inst✝²² : Module R₂ M₂
inst✝²¹ : Module R₂ N₂
inst✝²⁰ : Module R₂ P₂
inst✝¹⁹ : Module R₂ Q₂
inst✝¹⁸ : Module R₃ M₃
inst✝¹⁷ : Module R₃ N₃
inst✝¹⁶ : Module R₃ P₃
inst✝¹⁵ : Module R₃ Q₃
inst✝¹⁴ : Module R P
inst✝¹³ : Module R Q
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R M
inst✝⁹ : Module R N
inst✝⁸ : CommSemiring A
inst✝⁷ : Module A M
inst✝⁶ : Module A N
inst✝⁵ : SMulCommClass R A M
inst✝⁴ : CommSemiring S
inst✝³ : Module S M
inst✝² : SMulCommClass R S M
inst✝¹ : SMulCommClass A S M
inst✝ : CompatibleSMul R A M N
s : S
x : M ⊗[A] N
⊢ (lift
          {
            toFun := fun m ↦
              let __spread.0 := (mk R M N) m;
              { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ }).toFun
      (s • x) =
    (RingHom.id S) s •
      (lift
            {
              toFun := fun m ↦
                let __spread.0 := (mk R M N) m;
                { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ }).toFun
        x

Tactic:
induction x with
    | zero => simp
    | add x y _ _ => simp_all
    | tmul x y => simp [smul_tmul']

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} = ⊤

Tactic:
ext t

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t : M ⊗[R] N
⊢ t ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} ↔ t ∈ ⊤
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: case add
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ m n, m₁ ⊗ₜ[R] n₁ + m₂ ⊗ₜ[R] n₂ = m ⊗ₜ[R] n
x y : M ⊗[R] N
h₁ : ∃ m n, x = m ⊗ₜ[R] n
h₂ : ∃ m n, y = m ⊗ₜ[R] n
⊢ ∃ m n, x + y = m ⊗ₜ[R] n

Tactic:
| add x y h₁ h₂ =>

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ ⇑(map f g) '' {t | ∃ m n, m ⊗ₜ[R] n = t} = {t | ∃ m n, f m ⊗ₜ[R] g n = t}

Tactic:
ext t

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
t : P ⊗[R] Q
⊢ t ∈ ⇑(map f g) '' {t | ∃ m n, m ⊗ₜ[R] n = t} ↔ t ∈ {t | ∃ m n, f m ⊗ₜ[R] g n = t}
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z

Tactic:
rw [← mul_one z, ← h, mul_add]

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (a * x) + z * (b * y)
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x
⊢ IsCoprime (∏ i ∈ insert b t, s i) x ↔ ∀ i ∈ insert b t, IsCoprime (s i) x

Tactic:
rw [Finset.prod_insert hbt, IsCoprime.mul_left_iff, ih, Finset.forall_mem_insert]

Goal state after:
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this : ∀ (i : Fin n), ∃ j, sli[j] = val i
i j : Fin n
h_eq : val i = val j
⊢ val i ≤ val j ↔ ↑⋯.choose ≤ ↑⋯.choose

Tactic:
simp [h_eq]

Goal state after:
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this✝ : ∀ (i : Fin n), ∃ j, sli[j] = val i
i j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
this :
  ∀ (i j : Fin (li.mergeSort fun a b ↦ decide (a ≤ b)).length),
    i < j →
      decide ((li.mergeSort fun a b ↦ decide (a ≤ b)).get i ≤ (li.mergeSort fun a b ↦ decide (a ≤ b)).get j) = true
h : ↑hi.choose ≤ ↑hj.choose
h_eq : ↑hi.choose = ↑hj.choose
⊢ sli[↑hi.choose] = sli[↑hj.choose]

Tactic:
simp [h_eq]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
N P : Submodule R A
h : N * P = 1
| ⊤

Tactic:
← mul_one ⊤,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
N P : Submodule R A
h : N * P = 1
| ⊤ * 1
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
H : ∀ i ∈ insert b t, IsRelPrime (s i) x
⊢ IsRelPrime (∏ i ∈ insert b t, s i) x

Tactic:
Finset.prod_insert hbt

Goal state after:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
H : ∀ i ∈ insert b t, IsRelPrime (s i) x
⊢ IsRelPrime (s b * ∏ x ∈ t, s x) x
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
a✝ b✝ : A
ha : a✝ ∈ {x | ∀ y ∈ J, x * y ∈ I}
hb : b✝ ∈ {x | ∀ y ∈ J, x * y ∈ I}
y : A
hy : y ∈ J
⊢ (a✝ + b✝) * y ∈ I

Tactic:
by
        rw [add_mul]
        exact Submodule.add_mem _ (ha _ hy) (hb _ hy)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
h : comap f I = ⊥
x : S
y : R
hy : f y = x
⊢ x ∈ I ↔ x ∈ ⊥

Tactic:
aesop (add norm [Submodule.eq_bot_iff])

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: S : Type v
F : Type u_1
inst✝³ : CommSemiring S
R : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I J : Ideal R
⊢ ⇑f '' ↑I * ⇑f '' ↑J ⊆ ↑(map f (I * J))

Tactic:
by
      rintro _ ⟨_, ⟨r, hri, rfl⟩, _, ⟨s, hsj, rfl⟩, rfl⟩
      simp_rw [← map_mul]; exact mem_map_of_mem f (mul_mem_mul hri hsj)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
I J : Ideal R
⊢ I + J = 1 ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1

Tactic:
rw [one_eq_top, eq_top_iff_one, add_eq_sup, Submodule.mem_sup]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
b : Associates α
⊢ ∀ (a_1 : α), a ∣ Associates.out ⟦a_1⟧ ↔ Associates.mk a ≤ ⟦a_1⟧

Tactic:
simp [Associates.out_mk, Associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
b : Associates α
⊢ ∀ (a_1 : α), Associates.out ⟦a_1⟧ ∣ a ↔ ⟦a_1⟧ ≤ Associates.mk a

Tactic:
simp [Associates.out_mk, Associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₁ : a ∈ I
ha₂ : a ≠ 0
⊢ ∃ x ∈ I, Prime x

Tactic:
replace ha₁ : (factors a).prod ∈ I := by
    obtain ⟨u : Rˣ, hu : (factors a).prod * u = a⟩ := factors_prod ha₂
    rwa [← hu, mul_unit_mem_iff_mem _ u.isUnit] at ha₁

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₂ : a ≠ 0
ha₁ : (factors a).prod ∈ I
⊢ ∃ x ∈ I, Prime x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a : α
hn0 : a ≠ 0
hnu : ¬IsUnit a
⊢ ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod = a ∧ f ≠ ∅

Tactic:
obtain ⟨f, hi, u, rfl⟩ := exists_factors a hn0
    obtain ⟨b, h⟩ := Multiset.exists_mem_of_ne_zero fun h : f = 0 => hnu <| by simp [h]
    classical
      refine ⟨(f.erase b).cons (b * u), fun a ha => ?_, ?_, Multiset.cons_ne_zero⟩
      · obtain rfl | ha := Multiset.mem_cons.1 ha
        exacts [Associated.irreducible ⟨u, rfl⟩ (hi b h), hi a (Multiset.mem_of_mem_erase ha)]
      · rw [Multiset.prod_cons, mul_comm b, mul_assoc, Multiset.prod_erase h, mul_comm]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b : α
x✝ : a ∣ 1 ∧ b ∣ 1
c : α
hc : 1 = a * c
d : α
hd : 1 = b * d
⊢ lcm ↑(Units.mkOfMulEqOne a c ⋯) ↑(Units.mkOfMulEqOne b d ⋯) = 1

Tactic:
lcm_units_coe_left,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b : α
x✝ : a ∣ 1 ∧ b ∣ 1
c : α
hc : 1 = a * c
d : α
hd : 1 = b * d
⊢ normalize ↑(Units.mkOfMulEqOne b d ⋯) = 1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b : α
⊢ (if a = 0 then b else if b = 0 then a else Classical.choose ⋯) ∣ a

Tactic:
split_ifs with h h_1
      · rw [h]
        apply dvd_zero
      · exact dvd_rfl
      have h0 : lcm a b ≠ 0 := by
        intro con
        have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
        rw [con, zero_dvd_iff, mul_eq_zero] at h
        cases h
        · exact absurd ‹a = 0› h
        · exact absurd ‹b = 0› h_1
      rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd a b), mul_comm,
        mul_dvd_mul_iff_right h]
      apply dvd_lcm_right

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : generator T ∈ S
⊢ T ≤ S

Tactic:
← T.span_singleton_generator,

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : generator T ∈ S
⊢ Ideal.span {generator T} ≤ S
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case intro
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : RankCondition R
ι : Type u_2
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
this✝ : Nontrivial R
this : Finite ι
val✝ : Fintype ι
⊢ Fintype.card ι ≤ Fintype.card ↑w

Tactic:
exact Basis.le_span'' b s

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R✝ : Type u
S : Type u_1
M✝ : Type v
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
ι : Type w
ι' : Type w'
inst✝⁴ : StrongRankCondition R✝
R : Type u_2
M : Type u_3
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
s t : Set M
inst✝ : Module.Finite R ↥(span R t)
hs : LinearIndepOn R id s
hst : s ⊆ t
⊢ Fintype ↑(hs.extend hst)

Tactic:
refine Classical.choice (Cardinal.lt_aleph0_iff_fintype.1 ?_)
  rw [← rank_span_set (hs.linearIndepOn_extend hst), hs.span_extend_eq_span]
  exact Module.rank_lt_aleph0 ..

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ 0 < finrank R M ↔ Nontrivial M

Tactic:
← not_subsingleton_iff_nontrivial,

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ 0 < finrank R M ↔ ¬Subsingleton M
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
α : Type u_7
inst✝¹ : DecidableEq m
inst✝ : Zero α
i : m
r : α
⊢ diagonal (Pi.single i r) = single i i r

Tactic:
ext j k
  dsimp [diagonal, single]
  grind

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
⊢ IsLeftRegular A ↔ Function.Injective A.mulVec

Tactic:
cases isEmpty_or_nonempty m

Goal state after:
case inl
m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
h✝ : IsEmpty m
⊢ IsLeftRegular A ↔ Function.Injective A.mulVec

case inr
m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
h✝ : Nonempty m
⊢ IsLeftRegular A ↔ Function.Injective A.mulVec