mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case insert
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
a : α
⊢ (∃ x ∈ f i, ∃ y ∈ ∏ x ∈ is, f x, x * y = a) ↔
    ∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a

Tactic:
simp_rw [ih]

Goal state after:
case insert
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
a : α
⊢ (∃ x ∈ f i, ∃ y, (∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = a) ↔
    ∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: case le.refine_1
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
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
r : R
hr : r ∈ c.support
⊢ ↑((DistribSMul.toLinearMap R (↥N) r) (c r)) ∈ sR • N

Tactic:
mem_set_smul_def,

Goal state after:
case le.refine_1
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
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
r : R
hr : r ∈ c.support
⊢ ↑((DistribSMul.toLinearMap R (↥N) r) (c r)) ∈ sInf {p | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p}
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: case le.refine_2.mp
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
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
x : M
h : sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N
r : R
n : M
hr : r ∈ sR
hn : n ∈ N
⊢ r • n ∈ sR • N

Tactic:
mem_set_smul_def,

Goal state after:
case le.refine_2.mp
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
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
x : M
h : sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N
r : R
n : M
hr : r ∈ sR
hn : n ∈ N
⊢ r • n ∈ sInf {p | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p}
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: case mpr
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
x : M
inst✝ : SMulCommClass R R ↥N
⊢ (∃ c, ↑c.support ⊆ sR ∧ x = ↑(c.sum fun r m ↦ r • m)) → x ∈ sR • N

Tactic:
mem_set_smul_def,

Goal state after:
case mpr
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
x : M
inst✝ : SMulCommClass R R ↥N
⊢ (∃ c, ↑c.support ⊆ sR ∧ x = ↑(c.sum fun r m ↦ r • m)) → x ∈ sInf {p | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p}
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: case mpr
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
c : R →₀ ↥N
hc1 : ↑c.support ⊆ sR
p : Submodule R M
hp : p ∈ {p | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p}
⊢ ↑(c.sum fun r m ↦ r • m) ∈ p

Tactic:
Finsupp.sum,

Goal state after:
case mpr
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
c : R →₀ ↥N
hc1 : ↑c.support ⊆ sR
p : Submodule R M
hp : p ∈ {p | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p}
⊢ ↑(∑ a ∈ c.support, a • c a) ∈ p
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s t : Set R
x : Submodule R M
r : R
hr : r ∈ s
this : SMulCommClass R R ↥x
c : R →₀ ↥x
hc1 : ↑c.support ⊆ t
hm : ↑(c.sum fun r m ↦ r • m) ∈ t • x
⊢ r • ↑(c.sum fun r m ↦ r • m) ∈ (s * t) • x

Tactic:
Finsupp.sum,

Goal state after:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s t : Set R
x : Submodule R M
r : R
hr : r ∈ s
this : SMulCommClass R R ↥x
c : R →₀ ↥x
hc1 : ↑c.support ⊆ t
hm : ↑(c.sum fun r m ↦ r • m) ∈ t • x
⊢ r • ↑(∑ a ∈ c.support, a • c a) ∈ (s * t) • x
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
⊢ t • 0 ∈ ⨆ i, T • S i

Tactic:
simp_rw [smul_zero]; apply zero_mem

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:
induction s using Finset.cons_induction

Goal state after:
case empty
ι : Type u_1
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : ι → Finset α
a : α
⊢ a ∈ ∅.inf f ↔ ∀ i ∈ ∅, a ∈ f i

case cons
ι : Type u_1
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : ι → Finset α
a : α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : a ∈ s✝.inf f ↔ ∀ i ∈ s✝, a ∈ f i
⊢ a ∈ (cons a✝¹ s✝ h✝).inf f ↔ ∀ i ∈ cons a✝¹ s✝ h✝, a ∈ f i
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
a b : R
H : a * (x + y * z) + b * y = 1
⊢ a * x + (a * z + b) * y = 1

Tactic:
by
    simpa only [add_mul, mul_add, add_assoc, add_comm, add_left_comm, mul_assoc, mul_comm,
      mul_left_comm] using H

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

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
x y a b : R
h : a * x + b * y = 1
⊢ -a * -x + b * y = 1

Tactic:
rwa [neg_mul_neg]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y : R
h : y ∣ x
⊢ IsCoprime (x - 1) y

Tactic:
rw [← neg_sub, neg_left_iff, sub_eq_neg_add]

Goal state after:
R : Type u
inst✝ : CommRing R
x y : R
h : y ∣ x
⊢ IsCoprime (-x + 1) y
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
h : y ∣ x
⊢ IsRelPrime (x - 1) y

Tactic:
rw [← neg_sub, neg_left_iff, sub_eq_neg_add]

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
h : y ∣ x
⊢ IsRelPrime (-x + 1) y
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t : Finset I
h : ∀ i ∈ t, IsCoprime (s i) x
⊢ IsCoprime (∏ i ∈ t, s i) x

Tactic:
induction t using Finset.cons_induction with

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

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

Tactic:
by apply lt_of_le_of_ne h; contrapose h_eq; simp [h_eq]

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

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x✝ : A
⊢ x✝ ∈ MonoidHom.mker (spanSingleton R) ↔ ∃ x, IsUnit x ∧ (algebraMap R A) x = x✝

Tactic:
IsUnit,

Goal state after:
R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x✝ : A
⊢ x✝ ∈ MonoidHom.mker (spanSingleton R) ↔ ∃ x, (∃ u, ↑u = x) ∧ (algebraMap R A) x = x✝
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
hst : s.Nonempty ∧ t.Nonempty ∨ ¬s.Nonempty ∧ ¬t.Nonempty
⊢ span (s ×ˢ t) = (span s).prod (span t)

Tactic:
Set.not_nonempty_iff_eq_empty

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
hst : s.Nonempty ∧ t.Nonempty ∨ s = ∅ ∧ t = ∅
⊢ span (s ×ˢ t) = (span s).prod (span t)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case smul
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ : R'
c : R' →₀ R'
hc : ↑c.support ⊆ s
a✝ : (c.sum fun mi r ↦ r • mi) • n ∈ s • N
⊢ (a✝¹ • c.sum fun mi r ↦ r • mi) • n ∈ s • N

Tactic:
Finsupp.sum,

Goal state after:
case smul
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ : R'
c : R' →₀ R'
hc : ↑c.support ⊆ s
a✝ : (c.sum fun mi r ↦ r • mi) • n ∈ s • N
⊢ (a✝¹ • ∑ a ∈ c.support, c a • a) • n ∈ s • N
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set R
⊢ map f (span s) ≤ Submodule.span S (⇑f '' s)

Tactic:
· rw [map_le_iff_le_comap, span_le, coe_comap, ← Set.image_subset_iff]
    exact subset_span

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

Goal state before:
pp: case smul
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ : R'
c : R' →₀ R'
hc : ↑c.support ⊆ s
a✝ : (c.sum fun mi r ↦ r • mi) • n ∈ s • N
⊢ (a✝¹ • ∑ a ∈ c.support, c a • a) • n ∈ s • N

Tactic:
Finset.smul_sum,

Goal state after:
case smul
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ : R'
c : R' →₀ R'
hc : ↑c.support ⊆ s
a✝ : (c.sum fun mi r ↦ r • mi) • n ∈ s • N
⊢ (∑ x ∈ c.support, a✝¹ • c x • x) • n ∈ s • N
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
f : F
I✝ J : Ideal R✝
K L : Ideal S
G : Type u_2
inst✝³ : FunLike G S R✝
inst✝² : RingHomClass F R✝ S
ι✝ : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : Finite ι
I : Ideal ((i : ι) → R i)
r : (i : ι) → R i
x✝ : ∃ f, ∀ (x : ι), f x ∈ I ∧ (Pi.evalRingHom R x) (f x) = r x
r' : ι → (x : ι) → R x
hr' : ∀ (x : ι), r' x ∈ I ∧ (Pi.evalRingHom R x) (r' x) = r x
⊢ r ∈ I

Tactic:
have := Fintype.ofFinite ι

Goal state after:
R✝ : Type u
S : Type v
F : Type u_1
inst✝⁶ : Semiring R✝
inst✝⁵ : Semiring S
inst✝⁴ : FunLike F R✝ S
f : F
I✝ J : Ideal R✝
K L : Ideal S
G : Type u_2
inst✝³ : FunLike G S R✝
inst✝² : RingHomClass F R✝ S
ι✝ : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : Finite ι
I : Ideal ((i : ι) → R i)
r : (i : ι) → R i
x✝ : ∃ f, ∀ (x : ι), f x ∈ I ∧ (Pi.evalRingHom R x) (f x) = r x
r' : ι → (x : ι) → R x
hr' : ∀ (x : ι), r' x ∈ I ∧ (Pi.evalRingHom R x) (r' x) = r x
this : Fintype ι
⊢ r ∈ I
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case neg
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 * y ∣ z * gcd x y

Tactic:
gcd_eq_gcd_ab,

Goal state after:
case neg
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 * y ∣ z * (x * gcdA x y + y * gcdB x y)
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : (map (fun x ↦ a * x) s).gcd = normalize a * s.gcd
⊢ GCDMonoid.gcd (a * b) (map (fun x ↦ a * x) s).gcd = normalize a * GCDMonoid.gcd b s.gcd

Tactic:
← gcd_mul_left

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : (map (fun x ↦ a * x) s).gcd = normalize a * s.gcd
⊢ GCDMonoid.gcd (a * b) (map (fun x ↦ a * x) s).gcd = GCDMonoid.gcd (a * b) (a * s.gcd)
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: i j : ℤ
⊢ 0 ≤ GCDMonoid.gcd i j

Tactic:
simp [← coe_gcd]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Fintype ι
I : ι → ℕ
hI : Pairwise fun i j ↦ (I i).Coprime (I j)
⊢ ⨅ i, span {↑(I i)} = span {↑(∏ i, I i)}

Tactic:
rw [iInf_span_singleton, Nat.cast_prod]
  exact fun i j h ↦ (hI h).cast

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

Goal state before:
pp: case refine_2
β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : b ∉ t
h : (t.gcd fun x ↦ a * f x) = normalize a * t.gcd f
⊢ GCDMonoid.gcd (a * f b) (normalize a * t.gcd f) = normalize a * GCDMonoid.gcd (f b) (t.gcd f)

Tactic:
← gcd_mul_left

Goal state after:
case refine_2
β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : b ∉ t
h : (t.gcd fun x ↦ a * f x) = normalize a * t.gcd f
⊢ GCDMonoid.gcd (a * f b) (normalize a * t.gcd f) = GCDMonoid.gcd (a * f b) (a * t.gcd f)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a b : α
⊢ Associated a b → normalize a = normalize b

Tactic:
by
    rintro ⟨u, rfl⟩
    nontriviality α
    refine by_cases (by rintro rfl; simp only [zero_mul]) fun ha : a ≠ 0 ↦ ?_
    simp [normalize, normUnit_mul_units _ ha, mul_assoc]

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalize (x * y) = normalize x * normalize y

Tactic:
simp_rw [normalize, normUnit_mul hx hy]

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y * ↑(normUnit x * normUnit y) = x * ↑(normUnit x) * (y * ↑(normUnit y))
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
hI : I.IsRadical
hJ : J.IsRadical
⊢ I.radical ⊓ J.radical ≤ I ⊓ J

Tactic:
exact inf_le_inf hI hJ

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 b a)
k : ℕ
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ d₂ ^ k * (d₁ ^ k * b' * a') = d₂ ^ k * (b' * (d₁ ^ k * a'))

Tactic:
← mul_assoc b',

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ d₂ ^ k * (d₁ ^ k * b' * a') = d₂ ^ k * (b' * d₁ ^ k * a')
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

Tactic:
obtain ⟨h1, h2⟩ := not_or.1 h

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ n ≤ P
hn : ¬n = 0
⊢ I ≤ P

Tactic:
· exact (pow_le_iff hn).mp h

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

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, (f i).IsPrime
I : Ideal R
this : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
h✝ : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
h : I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
x✝ : ∃ i ∈ s, I ≤ f i
i : ι
his : i ∈ s
hi : I ≤ f i
⊢ ↑(f i) ⊆ ⋃ i ∈ ↑s, ↑(f i)

Tactic:
exact Set.subset_biUnion_of_mem (u := fun x ↦ (f x : Set R)) (Finset.mem_coe.2 his)

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ b ∈ factors a, Irreducible b) ∧ Associated (factors a).prod a

Tactic:
unfold factors; rw [dif_neg h]
  exact Classical.choose_spec (WfDvdMonoid.exists_factors a h)

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
x y : R
⊢ Ideal.span {gcd x y} = Ideal.span {x, y}

Tactic:
rw [← IsBezout.span_gcd, IsBezout.span_gcd_eq_span_gcd]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
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
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b : α
h : ¬a = 0
h_1 : b = 0
⊢ Associated (normalize a * lcm a 0) (a * 0)

Tactic:
eq_zero_of_zero_dvd (dvd_lcm_right _ _),

Goal state after:
case pos
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
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
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b : α
h : ¬a = 0
h_1 : b = 0
⊢ Associated (normalize a * 0) (a * 0)
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
x : M
h : Bijective ⇑(LinearMap.toSpanSingleton R M x)
⊢ Module.rank R M = 1

Tactic:
by
  rw [rank_eq_one_iff_finrank_eq_one, finrank_of_bijective_toSpanSingleton h]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
⊢ ↑(finrank R ↥N) = Module.rank R ↥N

Tactic:
finrank,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
⊢ ↑(toNat (Module.rank R ↥N)) = Module.rank R ↥N
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
inst✝⁷ : StrongRankCondition R
inst✝⁶ : Module.Finite R M
inst✝⁵ : Semiring S
inst✝⁴ : Module S M
inst✝³ : Module R S
inst✝² : IsScalarTower R S S
inst✝¹ : FaithfulSMul R S
inst✝ : IsScalarTower R S M
⊢ finrank S M ≤ finrank R M

Tactic:
finrank,

Goal state after:
R : Type u
S : Type u_1
M : Type v
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : Module.Finite R M
inst✝⁵ : Semiring S
inst✝⁴ : Module S M
inst✝³ : Module R S
inst✝² : IsScalarTower R S S
inst✝¹ : FaithfulSMul R S
inst✝ : IsScalarTower R S M
⊢ toNat (Module.rank S M) ≤ finrank R M
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
inst✝⁷ : StrongRankCondition R
inst✝⁶ : Module.Finite R M
inst✝⁵ : Semiring S
inst✝⁴ : Module S M
inst✝³ : Module R S
inst✝² : IsScalarTower R S S
inst✝¹ : FaithfulSMul R S
inst✝ : IsScalarTower R S M
⊢ toNat (Module.rank S M) ≤ finrank R M

Tactic:
finrank,

Goal state after:
R : Type u
S : Type u_1
M : Type v
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : Module.Finite R M
inst✝⁵ : Semiring S
inst✝⁴ : Module S M
inst✝³ : Module R S
inst✝² : IsScalarTower R S S
inst✝¹ : FaithfulSMul R S
inst✝ : IsScalarTower R S M
⊢ toNat (Module.rank S M) ≤ toNat (Module.rank R M)
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (∃ n, ℵ₀ ≤ Module.rank R (Fin n → R)) ↔ ∃ n > 0, finrank R (Fin n → R) ≤ 0

Tactic:
finrank,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (∃ n, ℵ₀ ≤ Module.rank R (Fin n → R)) ↔ ∃ n > 0, toNat (Module.rank R (Fin n → R)) ≤ 0
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i j : m
hij : j ≠ i
⊢ Pi.single i x j * v j = 0

Tactic:
by
    simp [Pi.single_eq_of_ne hij]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i j : m
hij : j ≠ i
⊢ v j * Pi.single i x j = 0

Tactic:
by
    simp [Pi.single_eq_of_ne hij]

Goal state after:
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 → α
⊢ ¬Function.Injective fun x ↦ x ⬝ᵥ a

Tactic:
by
  intro h
  obtain ⟨b, hb, hba⟩ := exists_ne_zero_dotProduct_eq_zero a
  simpa [hba, hb] using @h b 0

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

Goal state before:
pp: case intro.intro
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
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
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)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ P (∑ i, ∑ j, single i j (M i j))

Tactic:
← Finset.sum_product'

Goal state after:
case intro.intro
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
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
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)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ P (∑ x ∈ Finset.univ ×ˢ Finset.univ, single x.1 x.2 (M x.1 x.2))