mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
i : Fin (p.length + 1)
⊢ (p.drop i).last = p.last

Tactic:
simp only [last, drop, Fin.last]
  congr
  lia

Goal state after:
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✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
r : R'
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
m : M
n₁ n₂ : N
⊢ (SMul.aux r) (FreeAddMonoid.of (m, n₁) + FreeAddMonoid.of (m, n₂)) = (SMul.aux r) (FreeAddMonoid.of (m, n₁ + n₂))

Tactic:
by simp_rw [map_add, SMul.aux_of, tmul_add]

Goal state after:
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✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
⊢ ∀ (x : M ⊗[R] N), 0 • x = 0

Tactic:
by simp [TensorProduct.zero_smul]

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
m : M
hm : ∃ b, m + b = 0
n : N
⊢ ∃ b, m ⊗ₜ[R] n + b = 0

Tactic:
have ⟨b, eq⟩ := hm

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
m : M
hm : ∃ b, m + b = 0
n : N
b : M
eq : m + b = 0
⊢ ∃ b, m ⊗ₜ[R] n + b = 0
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
x✝ : Fin (p.length - 1 + 1)
i : ℕ
hi : i < p.length - 1 + 1
⊢ p.toFun ⟨i + 1, ⋯⟩ ≠ ⊥

Tactic:
by
        apply ne_bot_of_gt (b := p.head)
        apply p.strictMono
        exact compare_gt_iff_gt.mp rfl

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S : Type u_6
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
r✝ : ℤ
m : M
p : P
r : ℕ
ih : (↑r • m) ⊗ₜ[R] p = m ⊗ₜ[R] (↑r • p)
⊢ ((↑r + 1) • m) ⊗ₜ[R] p = m ⊗ₜ[R] ((↑r + 1) • p)

Tactic:
simpa [add_smul, tmul_add, add_tmul] using ih

Goal state after:
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
⊢ Function.Injective fun n ↦ r ^ n

Tactic:
intro n m hnm

Goal state after:
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 = m
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: case succ
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
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
ih : congr f g ^ n = congr (f ^ n) (g ^ n)
⊢ congr (f ^ n) (g ^ n) * congr f g = congr (f ^ n * f) (g ^ n * g)

Tactic:
congr_mul

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
⊢ a ∈ s.inf f ↔ ∀ i ∈ s, a ∈ f i

Tactic:
by induction s using Finset.cons_induction <;> simp [*]

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

Goal state before:
pp: case right
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'
h' : ↑U ⊆ ↑T * ↑T'
h'' : x ∈ span R (↑T * ↑T')
⊢ x ∈ span R (↑T * ↑T')

Tactic:
assumption

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : IsNoetherianRing R
inst✝ : IsNoetherianRing S
⊢ IsNoetherianRing (R × S)

Tactic:
IsNoetherianRing,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : IsNoetherian R R
inst✝ : IsNoetherian S S
⊢ IsNoetherian (R × S) (R × S)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ ↑I
i j : ι
this : DecidableEq ι := Classical.decEq ι
h✝ : i = j
⊢ y ∈ I

Tactic:
assumption

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

Goal state before:
pp: case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x ∣ z * gcdB x y

Tactic:
apply hxz.mul_right

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

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

Tactic:
exact h _

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
I J : Ideal R
inst✝² : IsDomain R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R
hx : x ≠ 0
⊢ I * span {x} ≤ J * span {x} ↔ I ≤ J

Tactic:
simp [SetLike.le_def, mem_mul_span_singleton, hx]

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
I J : Ideal R
inst✝² : IsDomain R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R
hx : x ≠ 0
⊢ I * span {x} ≤ J * span {x} ↔ I ≤ J

Tactic:
by
  simp [SetLike.le_def, mem_mul_span_singleton, hx]

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

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

Tactic:
rw [eq_comm]

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ x / y + z = (x + y * z) / y
Module: Mathlib.Algebra.EuclideanDomain.Basic

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

Tactic:
rw [eq_comm]

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ x / y - z = (x - y * z) / y
Module: Mathlib.Algebra.EuclideanDomain.Basic

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

Tactic:
rw [eq_comm]

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ x + y / z = (z * x + y) / z
Module: Mathlib.Algebra.EuclideanDomain.Basic

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

Tactic:
rw [eq_comm]

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ x - y / z = (z * x - y) / z
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁.ndunion s₂).dedup.lcm = GCDMonoid.lcm s₁.lcm s₂.lcm

Tactic:
dedup_ext.2,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (dedup ?m.27).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ ?m.27

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).dedup.lcm = GCDMonoid.lcm s₁.lcm s₂.lcm

Tactic:
dedup_ext.2,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (dedup ?m.27).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ ?m.27

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (ndinsert a s).dedup.lcm = GCDMonoid.lcm a s.lcm

Tactic:
dedup_ext.2,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (dedup ?m.24).lcm = GCDMonoid.lcm a s.lcm

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ ?m.24

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ Multiset α
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ s.gcd = 0 → ∀ (x : α), x ∈ s → x = 0

pp: case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ s → x = 0) → s.gcd = 0

Tactic:
· intro h x hx
    apply eq_zero_of_zero_dvd
    rw [← h]
    apply gcd_dvd hx

Goal state after:
case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ s → x = 0) → s.gcd = 0
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁.ndunion s₂).dedup.gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

Tactic:
dedup_ext.2,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (dedup ?m.27).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ ?m.27

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).dedup.gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

Tactic:
dedup_ext.2,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (dedup ?m.27).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ ?m.27

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (ndinsert a s).dedup.gcd = GCDMonoid.gcd a s.gcd

Tactic:
dedup_ext.2,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (dedup ?m.24).gcd = GCDMonoid.gcd a s.gcd

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ ?m.24

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ Multiset α
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f = {x ∈ s | f x ≠ 0}.gcd f

Tactic:
gcd_union

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ GCDMonoid.gcd ({x ∈ s | f x = 0}.gcd f) ({x ∈ s | f x ≠ 0}.gcd f) = {x ∈ s | f x ≠ 0}.gcd f
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
⊢ IsCoprime I J

Tactic:
by
  rw [isCoprime_iff_sup_eq]
  by_contra hIJ
  obtain ⟨P, hP, hIJ⟩ := Ideal.exists_le_maximal _ hIJ
  exact h P (le_trans le_sup_left hIJ) (le_trans le_sup_right hIJ) hP.isPrime

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
this : (I * J).radical ≤ I.radical ⊓ J.radical
⊢ (I * J).radical ≤ I.radical ⊓ J.radical

Tactic:
assumption

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
⊢ c ∣ c ^ k

Tactic:
exact dvd_pow_self _ hk.ne'

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

Goal state before:
pp: α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
⊢ {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 ↦ x1 > x2

Tactic:
by
  have : {I : Ideal α | I.IsPrincipal} = ((fun a ↦ Ideal.span {a}) '' Set.univ) := by
    ext
    simp [Submodule.isPrincipal_iff, eq_comm]
  rw [this, Set.wellFoundedOn_image, Set.wellFoundedOn_univ]
  convert! wellFounded_dvdNotUnit (α := α)
  ext
  exact Ideal.span_singleton_lt_span_singleton

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
K : Type u
inst✝ : DivisionSemiring K
⊢ IsPrincipal ⊤

Tactic:
apply top_isPrincipal

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
K : Type u
inst✝ : DivisionSemiring K
S : Ideal K
⊢ IsPrincipal S

Tactic:
by
    rcases Ideal.eq_bot_or_top S with (rfl | rfl)
    · apply bot_isPrincipal
    · apply top_isPrincipal

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
a b : R
⊢ ∃ x y, gcd a b = a * x + b * y

Tactic:
← gcd_dvd_iff_exists

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
a b : R
⊢ gcd a b ∣ gcd a b
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ nonPrincipals R = ∅ ↔ IsPrincipalIdealRing R

Tactic:
by
  simp [Set.eq_empty_iff_forall_notMem, isPrincipalIdealRing_iff]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case pos
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
H : c.Nonempty
K : Ideal R
hKmem : K ∈ c
x✝ : IsPrincipal (sSup c)
x : R
hx : sSup c = R ∙ x
⊢ False

Tactic:
have hxmem : x ∈ sSup c := hx.symm ▸ Submodule.mem_span_singleton_self x

Goal state after:
case pos
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
H : c.Nonempty
K : Ideal R
hKmem : K ∈ c
x✝ : IsPrincipal (sSup c)
x : R
hx : sSup c = R ∙ x
hxmem : x ∈ sSup c
⊢ False
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg.inr.inr
ι : 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) ∪ (↑(f i) ∪ ⋃ x ∈ ↑t, ↑(f x))
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
Hi : ¬I ≤ f i
this : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i
r : R
hri : r ∉ ↑(f i)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ¬↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
s : R
hsI : s ∈ ↑I
hs : s ∉ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
hsi : s ∈ f i
j : ι
hjt : j ∈ ↑t
hj : r + s ∈ ↑(f j)
hr : ∀ i ∈ t, r ∈ f i
⊢ False

Tactic:
exact hs <| Or.inr <| Set.mem_biUnion hjt <|
        add_sub_cancel_left r s ▸ (f j).sub_mem hj <| hr j hjt

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
s : Set R
N : Submodule R M
⊢ Ideal.span s • N = s • N

Tactic:
rw [← coe_set_smul, coe_span_smul]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : n = 0
⊢ ((n + 1) • s).toFinset = s.toFinset

Tactic:
rw [h, zero_add, one_nsmul]

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon (x - y) 0 → I.ringCon x y

Tactic:
· intro h; convert! I.ringCon.add h (I.ringCon.refl y) <;> abel

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

Goal state before:
pp: ι✝ : Type v
β : ι✝ → Type w
inst✝² : (i : ι✝) → AddCommMonoid (β i)
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x : ⨁ (x : ι), M
⊢ (of (fun x ↦ M) default) ((toAddMonoid fun x ↦ AddMonoidHom.id M) 0) = 0

Tactic:
rw [map_zero, map_zero]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
F : Type u_4
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
φ ψ : F
S T : Subalgebra R A
hS : Set.EqOn ⇑φ ⇑ψ ↑S
hT : Set.EqOn ⇑φ ⇑ψ ↑T
⊢ Set.EqOn ⇑φ ⇑ψ ↑(S ⊔ T)

Tactic:
rw [← AlgHom.coe_coe φ, ← AlgHom.coe_coe ψ, ← le_equalizer] at hS hT ⊢

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
F : Type u_4
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
φ ψ : F
S T : Subalgebra R A
hS : S ≤ (↑φ).equalizer ↑ψ
hT : T ≤ (↑φ).equalizer ↑ψ
⊢ S ⊔ T ≤ (↑φ).equalizer ↑ψ
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ IsInternal A ↔ IsCompl (A i) (A j)

Tactic:
rw [isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, iSup, ← Set.image_univ, h,
    Set.image_insert_eq, Set.image_singleton, sSup_pair, iSupIndep_pair hij this]

Goal state after:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ Disjoint (A i) (A j) ∧ A i ⊔ A j = ⊤ ↔ IsCompl (A i) (A j)
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (↑S.val).range = S.toSubring

Tactic:
← toSubring_subtype,

Goal state after:
R : Type u_3
A : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ S.toSubring.subtype.range = S.toSubring
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
⊢ A ≃ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)

Tactic:
refine LinearEquiv.ofLinearMap ((selfAdjointPart R).prod (skewAdjointPart R))
    (LinearMap.coprod ((selfAdjoint.submodule R A).subtype) (skewAdjoint.submodule R A).subtype)
    ?_ (LinearMap.ext <| StarModule.selfAdjointPart_add_skewAdjointPart R)
  -- Note: with https://github.com/leanprover-community/mathlib4/pull/6965 `Submodule.coe_subtype` doesn't fire in `dsimp` or `simp`
  ext x <;> dsimp <;> erw [Submodule.coe_subtype, Submodule.coe_subtype] <;> simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_14
inst✝¹ : Zero R
inst✝ : DecidableEq m
d : m → Matrix n n R
i✝ j✝ : m × n
⊢ (comp m m n n R) (diagonal d) i✝ j✝ = (reindex (Equiv.prodComm n m) (Equiv.prodComm n m)) (blockDiagonal d) i✝ j✝

Tactic:
simp [diagonal, blockDiagonal, Matrix.ite_apply]

Goal state after: