mathlib-initiative/mathlib-tactics huggingface dataset:
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₃
f : M →+ N →+ P
hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
s : R
m : M
n : N
⊢ (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) (FreeAddMonoid.of (s • m, n)) =
    (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) (FreeAddMonoid.of (m, s • n))

Tactic:
FreeAddMonoid.lift_eval_of,

Goal state after:
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₃
f : M →+ N →+ P
hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
s : R
m : M
n : N
⊢ (f (s • m, n).1) (s • m, n).2 = (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) (FreeAddMonoid.of (m, s • n))
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₃
f : M →+ N →+ P
hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
s : R
m : M
n : N
⊢ (f (s • m, n).1) (s • m, n).2 = (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) (FreeAddMonoid.of (m, s • n))

Tactic:
FreeAddMonoid.lift_eval_of,

Goal state after:
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₃
f : M →+ N →+ P
hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
s : R
m : M
n : N
⊢ (f (s • m, n).1) (s • m, n).2 = (f (m, s • n).1) (m, s • n).2
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 : ℕ
⊢ ∀ ⦃a₂ : ℕ⦄, (fun n ↦ r ^ n) n = (fun n ↦ r ^ n) a₂ → n = a₂

Tactic:
m

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n m : ℕ
⊢ (fun n ↦ r ^ n) n = (fun n ↦ r ^ n) m → n = m
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 : β
⊢ (f a)∗ * f a ≤ (f a)∗

Tactic:
exact kstar_mul_le_kstar

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + z * x)

Tactic:
exact h.add_mul_right_right z

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

Goal state before:
pp: case mp
m n a b : ℤ
h : a * m + b * n = 1
⊢ ↑1 = a * m + n * b

Tactic:
mul_comm n,

Goal state after:
case mp
m n a b : ℤ
h : a * m + b * n = 1
⊢ ↑1 = a * m + b * n
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case mpr
m n : ℤ
⊢ m.gcdA n * m + n * m.gcdB n = ↑1 → ∃ a b, a * m + b * n = 1

Tactic:
mul_comm n,

Goal state after:
case mpr
m n : ℤ
⊢ m.gcdA n * m + m.gcdB n * n = ↑1 → ∃ a b, a * m + b * n = 1
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case cons.mpr
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
⊢ ∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1

Tactic:
obtain ⟨u, v, huv⟩ := IsCoprime.prod_left fun b hb ↦ (Hb b hb).right

Goal state after:
case cons.mpr
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
⊢ ∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))
t : ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊥

Tactic:
obtain ⟨n, w⟩ := t

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊥
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
⊢ a % b = 0

Tactic:
by
    rw [e, ← add_left_cancel_iff, div_add_mod, add_zero]
    have := Classical.dec
    by_cases b0 : b = 0
    · simp only [b0, zero_mul]
    · rw [mul_div_cancel_left₀ _ b0]

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b c : R
hb : b ≠ 0
h : a * b = c
⊢ a = c / b

Tactic:
by
  rw [← h, mul_div_cancel_right₀ _ hb]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ map (↑f.symm) (map (↑f) I) = I

Tactic:
← RingEquiv.toRingHom_eq_coe,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ map f.symm.toRingHom (map (↑f) I) = I
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ map f.symm.toRingHom (map (↑f) I) = I

Tactic:
← RingEquiv.toRingHom_eq_coe,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ map f.symm.toRingHom (map f.toRingHom I) = I
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ comap (↑f) (comap (↑f.symm) I) = I

Tactic:
← RingEquiv.toRingHom_eq_coe,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ comap f.toRingHom (comap (↑f.symm) I) = I
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ comap f.toRingHom (comap (↑f.symm) I) = I

Tactic:
← RingEquiv.toRingHom_eq_coe,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ comap f.toRingHom (comap f.symm.toRingHom I) = I
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rcf : RingHomClass F R S
f : F
r : R
⊢ f r ∈ ⊥ ↔ f r = 0

Tactic:
Submodule.mem_bot

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rcf : RingHomClass F R S
f : F
r : R
⊢ f r = 0 ↔ f r = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (m : Π₀ (i : ι), M i), r • m = 0
i : ι
⊢ ∀ (m : M i), r • m = 0

Tactic:
m

Goal state after:
case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (m : Π₀ (i : ι), M i), r • m = 0
i : ι
m : M i
⊢ r • m = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (m : (i : ι) → M i), r • m = 0
i : ι
⊢ ∀ (m : M i), r • m = 0

Tactic:
m

Goal state after:
case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (m : (i : ι) → M i), r • m = 0
i : ι
m : M i
⊢ r • m = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
x : R
hx : x ∈ sInf A ∧ f x = y
J : Ideal R
hJ : J ∈ A ∧ map f J = j
⊢ y ∈ j

Tactic:
rw [← hJ.right, ← hx.right]

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
x : R
hx : x ∈ sInf A ∧ f x = y
J : Ideal R
hJ : J ∈ A ∧ map f J = j
⊢ f x ∈ map f J
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ Associated 0 0

Tactic:
Associated.of_eq

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : a ∉ s
ih : (s ∪ s₂).lcm f = GCDMonoid.lcm (s.lcm f) (s₂.lcm f)
⊢ GCDMonoid.lcm (f a) (GCDMonoid.lcm (s.lcm f) (s₂.lcm f)) = GCDMonoid.lcm (GCDMonoid.lcm (f a) (s.lcm f)) (s₂.lcm f)

Tactic:
lcm_assoc

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : a ∉ s
ih : (s ∪ s₂).lcm f = GCDMonoid.lcm (s.lcm f) (s₂.lcm f)
⊢ GCDMonoid.lcm (f a) (GCDMonoid.lcm (s.lcm f) (s₂.lcm f)) = GCDMonoid.lcm (f a) (GCDMonoid.lcm (s.lcm f) (s₂.lcm f))
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
⊢ ⊥.IsRadical

Tactic:
by rwa [isRadical_bot_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a b c : α
⊢ lcm (b * a) (c * a) = lcm b c * normalize a

Tactic:
simp only [mul_comm, lcm_mul_left]

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

Goal state before:
pp: case neg
α : 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 : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
⊢ Classical.choose ⋯ ∣ a

Tactic:
rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd a b), mul_comm,
        mul_dvd_mul_iff_right h]

Goal state after:
case neg
α : 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 : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
⊢ b ∣ lcm a b
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
r : R
⊢ Associated (generator (Ideal.span {r})) r

Tactic:
rw [← Ideal.span_singleton_eq_span_singleton]

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
r : R
⊢ Ideal.span {generator (Ideal.span {r})} = Ideal.span {r}
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
S : Ideal R
inst✝ : IsPrincipal S
x a : R
⊢ x = a • generator S ↔ x = generator S * a

Tactic:
by simp only [mul_comm, smul_eq_mul]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝ : EuclideanDomain R
S : Ideal R
h : ¬{x | x ∈ S ∧ x ≠ 0}.Nonempty
a : R
⊢ a ∈ S ↔ a ∈ ⊥

Tactic:
Submodule.mem_bot

Goal state after:
R : Type u
M : Type v
inst✝ : EuclideanDomain R
S : Ideal R
h : ¬{x | x ∈ S ∧ x ≠ 0}.Nonempty
a : R
⊢ a ∈ S ↔ a = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
by_cases Hb : f b ≤ f i

Goal state after:
case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : f b ≤ f i
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

case neg
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : ¬f b ≤ f i
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
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
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : κ → Finset ι := fun k ↦ (b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
⊢ False

Tactic:
let v' := fun k : Φ ⁻¹' {s} => v k

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : κ → Finset ι := fun k ↦ (b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
v' : ↑(Φ ⁻¹' {s}) → M := fun k ↦ v ↑k
⊢ False
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case a
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
s : Set M
li : LinearIndepOn R id s
⊢ #↑↑⟨s, li⟩ ≤ #ι

Tactic:
apply linearIndependent_le_basis v _ li

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
ι : Type u_2
b : Basis ι R R
⊢ Unique ι

Tactic:
by
  have : Cardinal.mk ι = ↑(Module.finrank R R) := (Module.mk_finrank_eq_card_basis b).symm
  have : Subsingleton ι ∧ Nonempty ι := by simpa [Cardinal.eq_one_iff_unique]
  exact Nonempty.some ((unique_iff_subsingleton_and_nonempty _).2 this)

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

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a t), ↑(f i)
has : a ∈ insert a t
hbt : b ∉ t
j : ι
hj : j ∈ t
⊢ (f j).IsPrime

Tactic:
refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl

Goal state after:
case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
j : ι
hj : j ∈ t
hat : j ∉ t
hp : ∀ i ∈ insert j t, i ≠ j → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert j t), ↑(f i)
has : j ∈ insert j t
⊢ False

case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
h : ↑I ⊆ ⋃ i ∈ ↑(insert a t), ↑(f i)
has : a ∈ insert a t
j : ι
hj : j ∈ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ j → (f i).IsPrime
hbt : j ∉ t
⊢ False
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert b t), ↑(f i)
has : a ∉ insert b t
hbs : b ∈ insert b t
j : ι
hj : j ∈ t
⊢ (f j).IsPrime

Tactic:
refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl

Goal state after:
case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
h : ↑I ⊆ ⋃ i ∈ ↑(insert b t), ↑(f i)
hbs : b ∈ insert b t
j : ι
hj : j ∈ t
hp : ∀ i ∈ insert b t, i ≠ j → i ≠ b → (f i).IsPrime
has : j ∉ insert b t
⊢ False

case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a : ι
I : Ideal R
t : Finset ι
j : ι
hj : j ∈ t
hbt : j ∉ t
hp : ∀ i ∈ insert j t, i ≠ a → i ≠ j → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert j t), ↑(f i)
has : a ∉ insert j t
hbs : j ∈ insert j t
⊢ False
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : CommRing α
inst✝¹ : Nontrivial m
inst✝ : Nontrivial α
a : m → α
h : Function.Injective (dotProduct a)
⊢ False

Tactic:
obtain ⟨b, hb, hba⟩ := exists_ne_zero_dotProduct_eq_zero a

Goal state after:
m : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : CommRing α
inst✝¹ : Nontrivial m
inst✝ : Nontrivial α
a : m → α
h : Function.Injective (dotProduct a)
b : m → α
hb : b ≠ 0
hba : b ⬝ᵥ a = 0
⊢ False
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : CommRing α
inst✝¹ : Nontrivial m
inst✝ : Nontrivial α
a : m → α
h : Function.Injective fun x ↦ x ⬝ᵥ a
⊢ False

Tactic:
obtain ⟨b, hb, hba⟩ := exists_ne_zero_dotProduct_eq_zero a

Goal state after:
m : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : CommRing α
inst✝¹ : Nontrivial m
inst✝ : Nontrivial α
a : m → α
h : Function.Injective fun x ↦ x ⬝ᵥ a
b : m → α
hb : b ≠ 0
hba : b ⬝ᵥ a = 0
⊢ False