mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a ↦ ⟨v ↑a, ⋯⟩
⊢ LinearIndependent (ι := ↑s) K (Subtype.val ∘ f')

Tactic:
apply hli.comp

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := ⋯
⊢ Injective f'
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
⊢ ↑(image₂ f (s ∩ t) (s ∪ t)) ⊆ ↑(image₂ f s t)

Tactic:
by
    push_cast
    exact image2_inter_union_subset hf

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : AddMonoid M
motive : R[M] → Prop
x : R[M]
of : ∀ (m : M), motive ((AddMonoidAlgebra.of R M) (Multiplicative.ofAdd m))
add : ∀ (x y : R[M]), motive x → motive y → motive (x + y)
smul : ∀ (r : R) (x : R[M]), motive x → motive (r • x)
m : M
r : R
⊢ motive (ofCoeff (Finsupp.single m r))

Tactic:
by simpa using! smul r (.of R M m) (of m)

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
inst✝ : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : f aG = aH
hbe : f bG = bH
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : aH * bH = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ a = aG ∧ b = bG

Tactic:
refine huG ?_ ?_ he <;> rw [mem_filter]

Goal state after:
case refine_1
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
inst✝ : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : f aG = aH
hbe : f bG = bH
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : aH * bH = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ a ∈ A ∧ f a = aH

case refine_2
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
inst✝ : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : f aG = aH
hbe : f bG = bH
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : aH * bH = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ b ∈ B ∧ f b = bH
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
have hC : 1 ∈ C := mem_map.mpr ⟨a, ha, inv_mul_cancel a⟩

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
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 α β
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ∀ (f : F) (s : Finset α), image (⇑f) (s ^ (n + 2)) = image (⇑f) s ^ (n + 2)

Tactic:
by simp [image_mul, pow_succ _ n.succ, image_pow_of_ne_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
c : R
h : c ≠ 0
⊢ ((monomial 1) c).support = {1}

Tactic:
support_monomial 1 h

Goal state after:
R : Type u
inst✝ : Semiring R
c : R
h : c ≠ 0
⊢ {1} = {1}
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
i : ℕ
⊢ Function.update p.coeff n a i = if i = n then a else p.coeff i

Tactic:
Function.update_apply

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
i : ℕ
⊢ (if i = n then a else p.coeff i) = if i = n then a else p.coeff i
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
⊢ ∃ s, φ (Pi.single s 1) ≠ 0

Tactic:
by_contra
    simp_all

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case inl
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #A * #B
hc' : 1 < #(image (⇑f) A) * #(image (⇑f) B)
a1 b1 a2 b2 : G
hne : (a1, b1) ≠ (a2, b2)
hu1 : UniqueMul (image (⇑f) A) (image (⇑f) B) (a1, b1).1 (a1, b1).2
hu2 : UniqueMul (image (⇑f) A) (image (⇑f) B) (a2, b2).1 (a2, b2).2
h1 : a1 ∈ image (⇑f) A ∧ b1 ∈ image (⇑f) B
h2 : a2 ∈ image (⇑f) A ∧ b2 ∈ image (⇑f) B
⊢ ∃ p1,
    (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ ∃ p2, (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
mem_image

Goal state after:
case inl
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #A * #B
hc' : 1 < #(image (⇑f) A) * #(image (⇑f) B)
a1 b1 a2 b2 : G
hne : (a1, b1) ≠ (a2, b2)
hu1 : UniqueMul (image (⇑f) A) (image (⇑f) B) (a1, b1).1 (a1, b1).2
hu2 : UniqueMul (image (⇑f) A) (image (⇑f) B) (a2, b2).1 (a2, b2).2
h1 : (∃ a ∈ A, f a = a1) ∧ ∃ a ∈ B, f a = b1
h2 : (∃ a ∈ A, f a = a2) ∧ ∃ a ∈ B, f a = b2
⊢ ∃ p1,
    (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ ∃ p2, (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
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 : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ IsCompl p f.ker

Tactic:
by
  rw [← codRestrict_ker h]
  exact isCompl_of_proj h.codRestrict_apply_cod

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hf : IsProj m 0
⊢ range 0 = ⊥

Tactic:
range_zero

Goal state after:
case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hf : IsProj m 0
⊢ ⊥ = ⊥
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_4
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
⊢ LeftInverse (fun e ↦ ⟨↑(↑e).symm ∘ₗ inr R M P, ⋯⟩) fun l ↦
    ⟨(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm, ⋯⟩

pp: case refine_5
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
⊢ RightInverse (fun e ↦ ⟨↑(↑e).symm ∘ₗ inr R M P, ⋯⟩) fun l ↦
    ⟨(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm, ⋯⟩

Tactic:
· intro; ext; simp

Goal state after:
case refine_5
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
⊢ RightInverse (fun e ↦ ⟨↑(↑e).symm ∘ₗ inr R M P, ⋯⟩) fun l ↦
    ⟨(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm, ⋯⟩
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ (p.append q connect).last = q.last

Tactic:
by
  delta last
  convert! append_apply_right p q connect (Fin.last _)
  ext1
  dsimp
  lia

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

Goal state before:
pp: case refine_4
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
⊢ LeftInverse (fun e ↦ ⟨fst R M P ∘ₗ ↑↑e, ⋯⟩) fun l ↦ ⟨LinearEquiv.ofBijective ((↑l).prod g) ⋯, ⋯⟩

pp: case refine_5
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
⊢ RightInverse (fun e ↦ ⟨fst R M P ∘ₗ ↑↑e, ⋯⟩) fun l ↦ ⟨LinearEquiv.ofBijective ((↑l).prod g) ⋯, ⋯⟩

Tactic:
· intro; ext; simp

Goal state after:
case refine_5
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
⊢ RightInverse (fun e ↦ ⟨fst R M P ∘ₗ ↑↑e, ⋯⟩) fun l ↦ ⟨LinearEquiv.ofBijective ((↑l).prod g) ⋯, ⋯⟩
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
x : α
⊢ krullDim α < ↑⊤

Tactic:
simpa using krullDim_ne_top_of_finiteDimensionalOrder.lt_top

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
⊢ (if ⟨i, hi⟩.castSucc = 0 then a else ↑(f ↑⟨i, hi⟩.castSucc), if ⟨i, hi⟩.succ = 0 then a else ↑(f ↑⟨i, hi⟩.succ)) ∈
    {(a, b) | a < b}

Tactic:
· suffices f i < f (i + 1) by simp [Fin.ext_iff, hzero, this]
      apply hstrictmono
      lia

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

Goal state before:
pp: case closed_under_smul
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
r : R
n : M
hr : r ∈ sR
hn : n ∈ N
⊢ r • n ∈ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)

Tactic:
exact ⟨Finsupp.single r ⟨n, hn⟩, Finsupp.single_mem_supported _ _ hr, by simp⟩

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
S : Type u_11
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : AddCommMonoid S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R S
inst✝¹ : Module R P
inst✝ : Module R Q
g' : Q →ₗ[R] S
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ lTensor P g' ∘ₗ map f g = map f (g' ∘ₗ g)

Tactic:
by
  simp only [lTensor, ← map_comp, id_comp]

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
⊢ x * -y = -(x * y)

Tactic:
by
    refine le_antisymm (mul_le.2 fun m hm n hn => ?_)
      ((AddSubmonoid.neg_le _ _).2 <| mul_le.2 fun m hm n hn => ?_) <;>
        simp only [AddSubmonoid.mem_neg, ← mul_neg] at *
    · exact mul_mem_mul hm hn
    · exact mul_mem_mul hm (neg_mem_neg.2 hn)

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case insert.refine_2
R : Type u
I : Type v
inst✝ : CommSemiring R
z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsCoprime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ s a ∣ z

pp: case insert.refine_3
R : Type u
I : Type v
inst✝ : CommSemiring R
z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsCoprime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ ∏ x ∈ r, s x ∣ z

Tactic:
· exact Hs1 a (Finset.mem_insert_self a r)

Goal state after:
case insert.refine_3
R : Type u
I : Type v
inst✝ : CommSemiring R
z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsCoprime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ ∏ x ∈ r, s x ∣ z
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)
i : Fin n
⊢ ∃ j, sli[j] = val i

Tactic:
apply List.get_of_mem

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := ⋯
sli : List α := ⋯
i : Fin n
⊢ val i ∈ sli
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: case neg
α : 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
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
⊢ val i ≤ val j ↔ ↑hi.choose ≤ ↑hj.choose

Tactic:
conv_lhs => rw [← hi.choose_spec, ← hj.choose_spec]

Goal state after:
case neg
α : 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
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
⊢ sli[↑hi.choose] ≤ sli[↑hj.choose] ↔ ↑hi.choose ≤ ↑hj.choose
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
x y : R
hxy : x * y ∈ I
⊢ (x * y, 1) ∈ I.prod ⊤

Tactic:
mem_prod

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
x y : R
hxy : x * y ∈ I
⊢ (x * y, 1).1 ∈ I ∧ (x * y, 1).2 ∈ ⊤
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_1.refine_1
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
⊢ ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ ⇑(algebraMap S R) '' s → n ∈ N → r • n ∈ s • restrictScalars S N

Tactic:
rintro _ x ⟨r, r_in, rfl⟩ x_in

Goal state after:
case refine_1.refine_1
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x✝ : M
x_in✝ : x✝ ∈ ⇑(algebraMap S R) '' s • N
x : M
r : S
r_in : r ∈ s
x_in : x ∈ N
⊢ (algebraMap S R) r • x ∈ s • restrictScalars S N
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
m x : M
hx : x ∈ I • (R ∙ m)
m1 m2 : M
x✝¹ : ∃ y ∈ I, y • m = m1
x✝ : ∃ y ∈ I, y • m = m2
y1 : R
hyi1 : y1 ∈ I
hy1 : y1 • m = m1
y2 : R
hyi2 : y2 ∈ I
hy2 : y2 • m = m2
⊢ y1 • m + y2 • m = m1 + m2

Tactic:
hy1,

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
m x : M
hx : x ∈ I • (R ∙ m)
m1 m2 : M
x✝¹ : ∃ y ∈ I, y • m = m1
x✝ : ∃ y ∈ I, y • m = m2
y1 : R
hyi1 : y1 ∈ I
hy1 : y1 • m = m1
y2 : R
hyi2 : y2 ∈ I
hy2 : y2 • m = m2
⊢ m1 + y2 • m = m1 + m2
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ c a b : R
x✝ : a ≠ 0
IH : c ∣ b % a → c ∣ a → c ∣ gcd (b % a) a
ca : c ∣ a
cb : c ∣ b
⊢ c ∣ gcd a b

Tactic:
by
    rw [gcd_val]
    exact IH ((dvd_mod_iff ca).2 cb) ca

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m✝ : M
hm✝ : m✝ ∈ span R T
r' : R
m : M
hm : m ∈ span R T
mem : ∀ r ∈ Ideal.span S, r • m ∈ span R (S • T)
r : R
hr : r ∈ Ideal.span S
⊢ r • r' • m ∈ span R (S • T)

Tactic:
by rw [← mul_smul]; exact mem _ (Ideal.mul_mem_right _ _ hr)

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : y * z ∣ x
⊢ x / (y * z) = x / y / z

Tactic:
rcases eq_or_ne z 0 with rfl | hz

Goal state after:
case inl
R : Type u
inst✝ : EuclideanDomain R
x y : R
h1 : y ∣ x
h2 : y * 0 ∣ x
⊢ x / (y * 0) = x / y / 0

case inr
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : y * z ∣ x
hz : z ≠ 0
⊢ x / (y * z) = x / y / z
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case cons
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : Nontrivial α
a : α
s : Multiset α
ihs : s.lcm = 0 ↔ 0 ∈ s
⊢ (a ::ₘ s).lcm = 0 ↔ 0 ∈ a ::ₘ s

Tactic:
simp only [mem_cons, lcm_cons, lcm_eq_zero_iff, ihs, @eq_comm _ a]

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

Goal state before:
pp: case neg.refine_1.e_f
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
x : α
hx : x ∈ s
⊢ id x = s.gcd * f hx

Tactic:
id,

Goal state after:
case neg.refine_1.e_f
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
x : α
hx : x ∈ s
⊢ x = s.gcd * f hx
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case neg.refine_2.e_f
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
x : α
hx : x ∈ s
⊢ id x = s.gcd * f hx

Tactic:
id,

Goal state after:
case neg.refine_2.e_f
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
x : α
hx : x ∈ s
⊢ x = s.gcd * f hx
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∀ x ∈ s, f x = 0
⊢ normalize (id 1) = 1

Tactic:
id,

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∀ x ∈ s, f x = 0
⊢ normalize 1 = 1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a : α
u : αˣ
ha : a ≠ 0
⊢ a * (↑u * ↑(Exists.choose ⋯)) = a * ↑(Exists.choose ⋯)

Tactic:
(assoc a).choose_spec,

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a : α
u : αˣ
ha : a ≠ 0
⊢ a * (↑u * ↑(Exists.choose ⋯)) = out (Associates.mk a)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : gcd (a * b) (a * c) = a * d
⊢ d ∣ gcd b c

Tactic:
exact
      dvd_gcd ((mul_dvd_mul_iff_left ha).1 <| eq ▸ gcd_dvd_left _ _)
        ((mul_dvd_mul_iff_left ha).1 <| eq ▸ gcd_dvd_right _ _)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : d₁ ^ k ∣ a
⊢ d₁ ^ k ≠ 0

Tactic:
intro hdk

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : d₁ ^ k ∣ a
hdk : d₁ ^ k = 0
⊢ False
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}
hri : r ∉ I.radical
hIm : I ≤ ⊤
hm : Maximal (fun x ↦ x ∈ {K | r ∉ K.radical}) ⊤
hrm : r ∉ ⊤
this : ∀ x ∉ ⊤, r ∈ (⊤ ⊔ span {x}).radical
⊢ False

Tactic:
exact hrm trivial

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf✝ : factors a ≠ 0
b : α
hb : b ∈ factors a
f : Multiset α
hf : factors a = b ::ₘ f
⊢ f.card + 1 = 1

Tactic:
add_eq_right,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf✝ : factors a ≠ 0
b : α
hb : b ∈ factors a
f : Multiset α
hf : factors a = b ::ₘ f
⊢ f.card = 0
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
⊢ a = 0 ∨ b = 0 → lcm a b = 0

Tactic:
by rintro (rfl | rfl) <;> [apply lcm_zero_left; apply lcm_zero_right]

Goal state after: