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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
t : Set β
⊢ t ∩ R.cod ⊆ R.image (R.preimage t)

Tactic:
aesop (add simp [Set.subset_def])

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
t : Set β
⊢ R.image s ⊆ t ↔ s ⊆ R.core t

Tactic:
aesop (add simp [Set.subset_def])

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

Goal state before:
pp: G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
⊢ UniqueMul A B a0 b0

Tactic:
intro a b ha hb he

Goal state after:
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a0 * b0
⊢ a = a0 ∧ b = b0
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
⊢ UniqueMul A B (a1, b1).1 (a1, b1).2

Tactic:
intro a b ha hb he

Goal state after:
case refine_2
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = (a1, b1).1 * (a1, b1).2
⊢ a = (a1, b1).1 ∧ b = (a1, b1).2
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
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
⊢ [Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id, Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id,
      ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e].TFAE

Tactic:
tfae_have 1 → 3
  | ⟨hf, l, hl⟩ => ⟨_, (h.splitSurjectiveEquiv hf ⟨l, hl⟩).2⟩

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
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
tfae_1_to_3 : (Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
⊢ [Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id, Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id,
      ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e].TFAE
Module: Mathlib.Order.RelSeries

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

Tactic:
exact ⟨i.castSucc, Fin.append_left _ _ _⟩

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ height a ≤ n → ∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n

Tactic:
height_le_iff

Goal state after:
case mp
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ (∀ ⦃p : LTSeries α⦄, RelSeries.last p ≤ a → ↑p.length ≤ n) → ∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
H : ∀ (n : ℕ), ∃ x, x.length = n
l l' : RelSeries r
hl' : l'.length = l.length + 1
⊢ l.length < l'.length

Tactic:
by simp [hl']

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ ¬r.FiniteDimensional ↔ r.InfiniteDimensional

Tactic:
rw [finiteDimensional_iff, infiniteDimensional_iff]
  push Not
  constructor
  · intro H n
    induction n with
    | zero => refine ⟨⟨0, ![_root_.Nonempty.some ‹_›], by simp⟩, by simp⟩
    | succ n IH =>
      obtain ⟨l, hl⟩ := IH
      obtain ⟨l', hl'⟩ := H l
      exact ⟨l'.take ⟨n + 1, by simpa [hl] using hl'⟩, rfl⟩
  · intro H l
    obtain ⟨l', hl'⟩ := H (l.length + 1)
    exact ⟨l', by simp [hl']⟩

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : ↑n ≤ ↑m
ha : height a = ↑m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
Nat.cast_le

Goal state after:
case coe
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : height a = ↑m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ ↑n ≤ ↑(LTSeries.longestOf α).length ↔ ∃ l, l.length = n

Tactic:
Nat.cast_le

Goal state after:
case inr.inl
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ n ≤ (LTSeries.longestOf α).length ↔ ∃ l, l.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p ≤ x
q : LTSeries { x_1 // x_1 ∈ Set.Iic x } := LTSeries.mk p.length (fun i ↦ ⟨p.toFun i, ⋯⟩) ⋯
⊢ ↑p.length ≤ ⨆ p, ↑p.length

Tactic:
exact le_iSup (fun p ↦ (p.length : ℕ∞)) q

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
i✝ : RelSeries.last p ≤ ⊤
mono : StrictMono fun y ↦ ↑y
⊢ ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length

Tactic:
rw [← LTSeries.map_length p (fun x ↦ x.1) mono, ]

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
i✝ : RelSeries.last p ≤ ⊤
mono : StrictMono fun y ↦ ↑y
⊢ ↑(p.map (fun x_1 ↦ ↑x_1) mono).length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length
Module: Mathlib.Algebra.Ring.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n✝ m : ℕ
hnm : (fun n ↦ r ^ n) n✝ = (fun n ↦ r ^ n) m
n l : ℕ
h₁ : n ≤ n + l
h₂ : l = 0
⊢ n = n + l

Tactic:
rw [h₂, Nat.add_zero]

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
ι : Sort u_4
T : AddSubmonoid R
S : ι → AddSubmonoid A
t : R
ht : t ∈ T
s : A
hs : s ∈ ⨆ i, S i
⊢ 0 ∈ ⨆ i, T • S i

Tactic:
apply zero_mem

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹² : KleeneAlgebra α
inst✝¹¹ : LE β
inst✝¹⁰ : LT β
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Max β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a : β
⊢ 1 ≤ a∗

Tactic:
rw [← le, one, kstar]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹² : KleeneAlgebra α
inst✝¹¹ : LE β
inst✝¹⁰ : LT β
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Max β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a : β
⊢ 1 ≤ (f a)∗
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_4
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : s ∈ ⨆ i, S i
t : R
ht : t ∈ T
⊢ 0 ∈ ⨆ i, S i * T

Tactic:
apply zero_mem

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

Goal state before:
pp: case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : AddLeftMono R
x y : R
h : x < 0
⊢ IsCoprime |x| y ↔ IsCoprime x y

Tactic:
abs_of_neg h,

Goal state after:
case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : AddLeftMono R
x y : R
h : x < 0
⊢ IsCoprime (-x) y ↔ IsCoprime x y
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case insert
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 ∈ insert a r, s x ∣ z

Tactic:
Finset.prod_insert har

Goal state after:
case insert
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 * ∏ x ∈ r, s x ∣ z
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]
⊢ sli[↑hi.choose] ≤ sli[↑hj.choose] ↔ ↑hi.choose ≤ ↑hj.choose

Tactic:
have := li.pairwise_mergeSort (le := fun a b ↦ decide (a ≤ b))
      (fun a b c ↦ by simpa using le_trans) (by simpa using le_total)

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]
this : List.Pairwise (fun a b ↦ decide (a ≤ b) = true) (li.mergeSort fun a b ↦ decide (a ≤ b))
⊢ sli[↑hi.choose] ≤ sli[↑hj.choose] ↔ ↑hi.choose ≤ ↑hj.choose
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
ι : Sort u_2
t✝ : ι → Submodule R A
N : Submodule R M
t : A
ht : t ∈ ⨆ i, t✝ i
s : M
hs : s ∈ N
⊢ 0 ∈ ⨆ i, t✝ i • N

Tactic:
apply zero_mem

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

Goal state before:
pp: case zero
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
h : 0 ≠ 0
⊢ (M ^ 0).toAddSubmonoid = M.toAddSubmonoid ^ 0

Tactic:
exact (h rfl).elim

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid A
inst✝¹ : Mul A
inst✝ : Module R A
S S' : Set A
x : A
hx : x ∈ span R (S * S')
U : Finset A
h : ↑U ⊆ S * S'
hU : x ∈ span R ↑U
⊢ ∃ T T', ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ x ∈ span R (↑T * ↑T')

Tactic:
obtain ⟨T, T', hS, hS', h⟩ := Finset.subset_mul h

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid A
inst✝¹ : Mul A
inst✝ : Module R A
S S' : Set A
x : A
hx : x ∈ span R (S * S')
U : Finset A
h✝ : ↑U ⊆ S * S'
hU : x ∈ span R ↑U
T T' : Finset A
hS : ↑T ⊆ S
hS' : ↑T' ⊆ S'
h : U ⊆ T * T'
⊢ ∃ T T', ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ x ∈ span R (↑T * ↑T')
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case refine_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : (↑t).Pairwise (IsCoprime on s)
i : I
hi : i ∈ t
j : I
hj : j ∈ t ∧ j ∉ {i}
⊢ IsCoprime (s i) (s j)

Tactic:
Finset.mem_singleton

Goal state after:
case refine_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : (↑t).Pairwise (IsCoprime on s)
i : I
hi : i ∈ t
j : I
hj : j ∈ t ∧ ¬j = i
⊢ IsCoprime (s i) (s j)
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ ∏ x ∈ insert a r, s x ∣ z

Tactic:
Finset.prod_insert har

Goal state after:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ s a * ∏ x ∈ r, s x ∣ z
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case refine_1
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsRelPrime on fun i ↦ s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t ∧ j ∉ {i}
⊢ IsRelPrime (s i) (s j)

Tactic:
Finset.mem_singleton

Goal state after:
case refine_1
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsRelPrime on fun i ↦ s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t ∧ ¬j = i
⊢ IsRelPrime (s i) (s j)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ x / y = z / t ↔ t * x = y * z

Tactic:
by
  rw [div_eq_iff_eq_mul_of_dvd _ _ _ h1 h3, ← mul_div_assoc _ h4,
    eq_div_iff_mul_eq_of_dvd _ _ _ h2]
  obtain ⟨a, ha⟩ := h4
  use y * a
  rw [ha, mul_comm, mul_assoc, mul_comm y a]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
⊢ ∃ f_1, (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * ↑u ∧ f_1 ≠ ∅

Tactic:
refine ⟨(f.erase b).cons (b * u), fun a ha => ?_, ?_, Multiset.cons_ne_zero⟩

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
a : α
ha : a ∈ b * ↑u ::ₘ f.erase b
⊢ Irreducible a

case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
⊢ (b * ↑u ::ₘ f.erase b).prod = f.prod * ↑u
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
normUnit✝ : α → αˣ
normUnit_zero✝ : normUnit✝ 0 = 1
normUnit_one✝ : normUnit✝ 1 = 1
normUnit_mul_units✝ : ∀ {a : α} (u : αˣ), a ≠ 0 → normUnit✝ (a * ↑u) = u⁻¹ * normUnit✝ a
⊢ normUnit✝ = fun x ↦ 1

Tactic:
apply Subsingleton.elim

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
toNormalizationMonoid✝ : NormalizationMonoid α
normUnit_mul✝ : ∀ {a b : α}, a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b
normUnit_coe_units✝ : ∀ (u : αˣ), normUnit ↑u = u⁻¹
⊢ toNormalizationMonoid✝ = { normUnit := fun x ↦ 1, normUnit_zero := ⋯, normUnit_one := ⋯, normUnit_mul_units := ⋯ }

Tactic:
apply Subsingleton.elim

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝ : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
⊢ ∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I

Tactic:
by
  by_cases H : c.Nonempty
  · obtain ⟨K, hKmem⟩ := Set.nonempty_def.1 H
    refine ⟨sSup c, fun ⟨x, hx⟩ ↦ ?_, fun _ ↦ le_sSup⟩
    have hxmem : x ∈ sSup c := hx.symm ▸ Submodule.mem_span_singleton_self x
    obtain ⟨J, hJc, hxJ⟩ := (Submodule.mem_sSup_of_directed ⟨K, hKmem⟩ hchain.directedOn).1 hxmem
    have hsSupJ : sSup c = J := le_antisymm (by simp [hx, Ideal.span_le, hxJ]) (le_sSup hJc)
    exact hs hJc ⟨hsSupJ ▸ ⟨x, hx⟩⟩
  · simpa [Set.not_nonempty_iff_eq_empty.1 H, isPrincipalIdealRing_iff] using hR

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

Goal state before:
pp: case i.hf
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : RankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ Surjective ⇑(Finsupp.linearCombination R Subtype.val)

Tactic:
← LinearMap.range_eq_top,

Goal state after:
case i.hf
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : RankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ (Finsupp.linearCombination R Subtype.val).range = ⊤
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
n : ℕ
pos : n > 0
eq : (∃ f, Injective ⇑f) → ℵ₀ ≤ Module.rank R (Fin n.pred.succ → R)
⊢ ℵ₀ ≤ Module.rank R (Fin n.pred.succ → R)

Tactic:
exact eq ⟨.single R (fun _ ↦ _) 0, Pi.single_injective (M := fun _ ↦ _) _⟩

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
c : α
i' : m
j' : n
h : ¬(i = i' ∧ j = j')
⊢ single i j c i' j' = 0

Tactic:
simp only [single, and_imp, ite_eq_right_iff, of_apply]
  tauto

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : AddCommMonoid α
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : Nonempty m
inst✝ : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
⊢ P 0

Tactic:
by
      inhabit m
      inhabit n
      simpa using h_std_basis default default 0

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun i c ↦ c • v i) ∈ (finsuppTotal ι M I v).range

Tactic:
classical
    refine ⟨a.mapRange (fun r => if h : r ∈ I then ⟨r, h⟩ else 0)
      (by simp only [Submodule.zero_mem, ↓reduceDIte]; rfl), ?_⟩
    rw [finsuppTotal_apply, Finsupp.sum_mapRange_index]
    · apply Finsupp.sum_congr
      intro i _
      rw [dif_pos (ha i)]
    · exact fun _ => zero_smul _ _

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M✝ : Type u_2
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ I
a : A
ha : a ∈ M
⊢ r • a ∈ { toFun := map (Algebra.linearMap R A), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } I * M

Tactic:
rw [Algebra.smul_def]; exact Submodule.mul_mem_mul ⟨r, hr, rfl⟩ ha

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

Goal state before:
pp: case inr.inr.inr
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j k : n
hkl : j ≠ k
hij : i ≠ j
⊢ 0 = M j k

Tactic:
· rw [row_eq_zero_of_commute_single (hM hij) hkl.symm]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
y : α
hy : y ∈ {a}
⊢ a = y

Tactic:
Finset.mem_singleton

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
y : α
hy : y = a
⊢ a = y
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
h' : x ∈ {a}
⊢ x = a

Tactic:
Finset.mem_singleton

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
h' : x = a
⊢ x = a
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a a' : α
x✝ : f a' ≠ 0
H : a' ≠ a
⊢ f a' * Multiset.count a {a'} = 0

Tactic:
simp only [Multiset.count_singleton, if_false, H.symm, mul_zero]

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

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Free R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
inst✝¹ : Free R M'
inst✝ : StrongRankCondition R
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
β : Type v'
B' : Basis β R M'
⊢ lift.{v', v} (Module.rank R M) = lift.{v, v'} #β

Tactic:
cnd,

Goal state after:
R : Type u
M : Type v
M' : Type v'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Free R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
inst✝¹ : Free R M'
inst✝ : StrongRankCondition R
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
β : Type v'
B' : Basis β R M'
⊢ lift.{v, v'} (Module.rank R M') = lift.{v, v'} #β
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝ x y : A
hx✝ : x ∈ adjoin R s
hy✝ : y ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
hpy : y ∈ span R ↑(Subsemigroup.closure s)
⊢ ∀ (x y : A), x ∈ ↑(Subsemigroup.closure s) → y ∈ ↑(Subsemigroup.closure s) → x * y ∈ span R ↑(Subsemigroup.closure s)

Tactic:
exact fun x y hx hy ↦ subset_span <| mul_mem hx hy

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
h : ⇑f ⁻¹' {0} ⊆ ↑S
⊢ comap f (map f S) = S

Tactic:
convert! comap_map_eq f S

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
h : ⇑f ⁻¹' {0} ⊆ ↑S
⊢ S = S ⊔ adjoin R (⇑f ⁻¹' {0})