mathlib-initiative/mathlib-tactics huggingface dataset:
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
A' : Submodule R A
M' : Submodule R M
r : R
m : M
hm : m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
m₁ m₂ : M
h₁ : r • m₁ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
h₂ : r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
⊢ r • (m₁ + m₂) ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier

Tactic:
rw [smul_add]

Goal state after:
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
A' : Submodule R A
M' : Submodule R M
r : R
m : M
hm : m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
m₁ m₂ : M
h₁ : r • m₁ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
h₂ : r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
⊢ r • m₁ + r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
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 • s ∈ ⨆ i, t✝ i • N

Tactic:
by simp_rw [zero_smul]; apply zero_mem

Goal state after:
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
inst✝ : IsScalarTower R A A
N P : Submodule R A
h : N * P = 1
| N * P * ⊤

Tactic:
mul_assoc

Goal state after:
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
N P : Submodule R A
h : N * P = 1
| N * (P * ⊤)
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case cons.mp.refine_2.refine_1
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}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
x : I
hx : x ∈ t
⊢ (μ x * ∏ j ∈ t \ {x}, s j) * s a = μ x * ∏ j ∈ insert a t \ {x}, s j

Tactic:
mul_assoc

Goal state after:
case cons.mp.refine_2.refine_1
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}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
x : I
hx : x ∈ t
⊢ μ x * ((∏ j ∈ t \ {x}, s j) * s a) = μ x * ∏ j ∈ insert a t \ {x}, s j
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
s t : Submodule R A
⊢ s * t = span R (↑s * ↑t)

Tactic:
rw [mul_eq_map₂]; exact map₂_eq_span_image2 _ s t

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

Goal state before:
pp: case h
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
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ v * (μ x * ∏ j ∈ insert a t \ {x}, s j) = v * ((μ x * ∏ j ∈ t \ {x}, s j) * s a)

Tactic:
mul_assoc

Goal state after:
case h
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
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ v * (μ x * ∏ j ∈ insert a t \ {x}, s j) = v * (μ x * ((∏ j ∈ t \ {x}, s j) * s a))
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y : R
m : ℕ
hm : 0 < m
h : IsCoprime (∏ _x ∈ range m, x) y
⊢ IsCoprime x y

Tactic:
exact h.of_prod_left 0 (Finset.mem_range.mpr hm)

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

Goal state before:
pp: case succ
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
hx : x ∈ M ^ (n + 1)
⊢ C (n + 1) x hx

Tactic:
revert hx
    simp_rw [pow_succ]
    exact fun hx ↦ Submodule.mul_induction_on' (fun m hm x ih => mul_mem _ _ hm (n_ih _) _ ih)
      (fun x hx y hy Cx Cy => add _ _ _ _ _ Cx Cy) hx

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x y : α
m : ℕ
hm : 0 < m
h : IsRelPrime (∏ _x ∈ Finset.range m, x) y
⊢ IsRelPrime x y

Tactic:
exact h.of_prod_left 0 (Finset.mem_range.mpr hm)

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
x : ι → A
⊢ span R (∏ i ∈ s, {x i}) = R ∙ ∏ i ∈ s, x i

Tactic:
Set.finsetProd_singleton

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
x : ι → A
⊢ R ∙ ∏ i ∈ s, x i = R ∙ ∏ i ∈ s, x i
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
⊢ 1 ≤ 1 / I ↔ I ≤ 1

Tactic:
rw [le_div_iff_mul_le, one_mul]

Goal state after:
Module: Mathlib.RingTheory.OrzechProperty

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
⊢ Injective ⇑f

Tactic:
obtain ⟨n, g, hg⟩ := Module.Finite.exists_fin' R M
  have := small_of_surjective hg
  let := Equiv.addCommMonoid (equivShrink M).symm
  let := Equiv.module R (equivShrink M).symm
  let j : Shrink.{u} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
  have := Module.Finite.equiv j.symm
  let i' := j.symm.toLinearMap ∘ₗ i
  replace hi : Injective i' := by simpa [i'] using hi
  let f' := j.symm.toLinearMap ∘ₗ f ∘ₗ (LinearEquiv.ofInjective i' hi).symm.toLinearMap
  replace hf : Surjective f' := by simpa [f'] using hf
  simpa [f'] using injective_of_surjective_of_submodule' f' hf

Goal state after:
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
inst✝ : RingHomClass F R S
s : Set (Ideal S)
⊢ ⨅ I ∈ s, comap f I = ⨅ I ∈ comap f '' s, I

Tactic:
by rw [iInf_image]

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

Goal state before:
pp: case inr
R : Type u
inst✝ : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ a * b * d / a = b * d

Tactic:
rw [mul_assoc, mul_div_cancel_left₀ _ ha]

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

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

Tactic:
rw [smul_add]

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m : M
hm : m ∈ span R T
x✝³ x✝² : M
x✝¹ : x✝³ ∈ span R T
x✝ : x✝² ∈ span R T
h₁ : ∀ r ∈ Ideal.span S, r • x✝³ ∈ span R (S • T)
h₂ : ∀ r ∈ Ideal.span S, r • x✝² ∈ span R (S • T)
r : R
hr : r ∈ Ideal.span S
⊢ r • x✝³ + r • x✝² ∈ span R (S • T)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
⊢ x ∈ I • span R (Set.range f) ↔ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x

Tactic:
by
  constructor; swap
  · rintro ⟨a, ha, rfl⟩
    exact Submodule.sum_mem _ fun c _ => smul_mem_smul (ha c) <| subset_span <| Set.mem_range_self _
  refine fun hx => span_induction ?_ ?_ ?_ ?_ (mem_smul_span.mp hx)
  · rintro x ⟨y, hy, x, ⟨i, rfl⟩, rfl⟩
    refine ⟨Finsupp.single i y, fun j => ?_, ?_⟩
    · let := Classical.decEq ι
      rw [Finsupp.single_apply]
      split_ifs
      · assumption
      · exact I.zero_mem
    refine @Finsupp.sum_single_index ι R M _ _ i _ (fun i y => y • f i) ?_
    simp
  · exact ⟨0, fun _ => I.zero_mem, Finsupp.sum_zero_index⟩
  · rintro x y - - ⟨ax, hax, rfl⟩ ⟨ay, hay, rfl⟩
    refine ⟨ax + ay, fun i => I.add_mem (hax i) (hay i), Finsupp.sum_add_index' ?_ ?_⟩ <;>
      intros <;> simp only [zero_smul, add_smul]
  · rintro c x - ⟨a, ha, rfl⟩
    refine ⟨c • a, fun i => I.mul_mem_left c (ha i), ?_⟩
    rw [Finsupp.sum_smul_index, Finsupp.smul_sum] <;> intros <;> simp only [zero_smul, mul_smul]

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
⊢ lcm x y ∣ z

Tactic:
rw [lcm]
  by_cases hxy : gcd x y = 0
  · rw [hxy, div_zero]
    rw [EuclideanDomain.gcd_eq_zero_iff] at hxy
    rwa [hxy.1] at hxz
  rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩
  suffices x * y ∣ z * gcd x y by
    obtain ⟨p, hp⟩ := this
    use p
    generalize gcd x y = g at hxy hs hp ⊢
    subst hs
    rw [mul_left_comm, mul_div_cancel_left₀ _ hxy, ← mul_left_inj' hxy, hp]
    rw [← mul_assoc]
    simp only [mul_right_comm]
  rw [gcd_eq_gcd_ab, mul_add]
  apply dvd_add
  · rw [mul_left_comm]
    gcongr
    apply hyz.mul_right
  · rw [mul_left_comm, mul_comm]
    gcongr
    apply hxz.mul_right

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x : R
⊢ lcm 0 x = 0

Tactic:
rw [lcm, zero_mul, zero_div]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : J.IsTwoSided
a✝ b : R
ha : a✝ ∈ I * J
i : R
hi : i ∈ I
j : R
hj : j ∈ J
⊢ i * j * b ∈ I * J

Tactic:
mul_assoc

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : J.IsTwoSided
a✝ b : R
ha : a✝ ∈ I * J
i : R
hi : i ∈ I
j : R
hj : j ∈ J
⊢ i * (j * b) ∈ I * J
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case empty
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : Nontrivial α
⊢ lcm 0 = 0 ↔ 0 ∈ 0

Tactic:
| empty =>

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst✝ : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, I ⊔ J i = ⊤
i : ι
t : Finset ι
his : i ∈ s
hts : t ⊆ s
hit : i ∉ t
eq_top : I ⊔ ⨅ i ∈ t, J i = ⊤
⊢ ⊤ ≤ I ⊔ (⨅ x ∈ t, J x) ⊓ J i

Tactic:
refine le_trans ?_ (sup_le_sup_left mul_le_inf _)

Goal state after:
R : Type u
inst✝¹ : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst✝ : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, I ⊔ J i = ⊤
i : ι
t : Finset ι
his : i ∈ s
hts : t ⊆ s
hit : i ∉ t
eq_top : I ⊔ ⨅ i ∈ t, J i = ⊤
⊢ ⊤ ≤ I ⊔ (⨅ x ∈ t, J x) * J i
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ GCDMonoid.gcd a (fold GCDMonoid.gcd 0 (s.erase a)) =
    GCDMonoid.gcd a (GCDMonoid.gcd a (fold GCDMonoid.gcd 0 (s.erase a)))

Tactic:
← gcd_assoc,

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ GCDMonoid.gcd a (fold GCDMonoid.gcd 0 (s.erase a)) =
    GCDMonoid.gcd (GCDMonoid.gcd a a) (fold GCDMonoid.gcd 0 (s.erase a))
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case empty
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
⊢ ∅.gcd f = 0 ↔ ∀ x ∈ ∅, f x = 0

Tactic:
| empty =>

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
h : ∀ x ∈ s, a ∣ f x - g x
⊢ GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)

Tactic:
revert h

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
⊢ (∀ x ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
s✝ : Finset β
f g : β → α
a : α
b : β
s : Finset β
a✝ : b ∉ s
hi : (∀ x ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)
h : ∀ x ∈ insert b s, a ∣ f x - g x
⊢ GCDMonoid.gcd a (GCDMonoid.gcd (s.gcd f) (f b)) = GCDMonoid.gcd a (GCDMonoid.gcd (g b) (s.gcd g))

Tactic:
← gcd_assoc,

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
s✝ : Finset β
f g : β → α
a : α
b : β
s : Finset β
a✝ : b ∉ s
hi : (∀ x ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)
h : ∀ x ∈ insert b s, a ∣ f x - g x
⊢ GCDMonoid.gcd (GCDMonoid.gcd a (s.gcd f)) (f b) = GCDMonoid.gcd a (GCDMonoid.gcd (g b) (s.gcd g))
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case empty
ι : Type u_1
s : Finset ι
f : ι → ℤ
⊢ 0 ≤ ∅.gcd f

Tactic:
| empty =>

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

Goal state before:
pp: case empty
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
J : ι → Ideal R
hp : (↑∅).Pairwise (IsCoprime on J)
⊢ ∏ i ∈ ∅, J i = ⨅ i ∈ ∅, J i

Tactic:
| empty =>

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
u : αˣ
⊢ (if ↑u = 0 then 1 else Classical.choose ⋯) = u⁻¹

Tactic:
nontriviality α
    simp_rw [if_neg (Units.ne_zero u), Units.ext_iff]
    apply mul_left_cancel₀ (Units.ne_zero u)
    rw [Units.mul_inv, map_mk_unit_aux hinv u,
      Associates.mk_eq_mk_iff_associated.2 (associated_one_iff_isUnit.2 ⟨u, rfl⟩),
      Associates.mk_one, map_one]

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

Goal state before:
pp: case inr
α : 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
con : lcm a b = 0
h✝ : b = 0
⊢ False

Tactic:
exact absurd ‹b = 0› h_1

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

Goal state before:
pp: case inr
α : 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 c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
con : lcm c b = 0
h✝ : b = 0
⊢ False

Tactic:
exact absurd ‹b = 0› h_1

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case empty
R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
⊢ ∃ g, ∅.gcd f = ∑ a ∈ ∅, f a * g a

Tactic:
| empty =>

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : z ∈ S
y : R
hy : z = generator S * y
this : generator S ≠ 0
⊢ 1 ∈ T

Tactic:
← mul_one (generator S),

Goal state after:
case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S * 1 = generator T * z
h : z ∈ S
y : R
hy : z = generator S * y
this : generator S ≠ 0
⊢ 1 ∈ T
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos.inr.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
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
h' : ↑I ⊆ ↑(f i) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
k : ι
hkt : k ∈ t
ih : I ≤ f k
⊢ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
· exact Or.inr ⟨k, Finset.mem_insert_of_mem hkt, ih⟩

Goal state after:
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)
hr : r ∈ ↑(t.inf f)
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)
⊢ False

Tactic:
simp only [Finset.inf_eq_iInf, SetLike.mem_coe, Submodule.mem_iInf] at hr

Goal state after:
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
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
hb : (c * a + i) * b = b
⊢ c * a * b + i * b ∈ I ^ n

Tactic:
mul_assoc

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
hb : (c * a + i) * b = b
⊢ c * (a * b) + i * b ∈ I ^ n
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
hb : (c * a + i) * b = b
⊢ c * (a * b) + i * b ∈ I ^ n

Tactic:
exact add_mem (mul_mem_left _ _ h) (mul_mem_right _ _ hi)

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R
h✝ : Nontrivial R
⊢ ¬span {r} = ⊥ ↔ r ≠ 0

Tactic:
span_singleton_eq_bot

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R
h✝ : Nontrivial R
⊢ ¬r = 0 ↔ r ≠ 0
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
u : m → α
v w : n → α
⊢ vecMulVec u v *ᵥ w = MulOpposite.op (v ⬝ᵥ w) • u

Tactic:
ext i
  simp [mulVec, dotProduct, vecMulVec, Finset.mul_sum, mul_assoc]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
M : Matrix l m α
x : m → α
y : n → α
i✝ : l
j✝ : n
⊢ ∑ j, M i✝ j * (x j * y j✝) = ∑ i, M i✝ i * x i * y j✝

Tactic:
mul_assoc

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
x : l → α
y : m → α
M : Matrix m n α
i✝ : l
j✝ : n
⊢ ∑ j, x i✝ * y j * M j j✝ = ∑ i, x i✝ * (y i * M i j✝)

Tactic:
mul_assoc

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
I J : Ideal R
z : R
hzs : z ∈ s
hs : s ⊆ ↑{ carrier := {r | ∃ n, ∃ y ∈ I, ∃ z ∈ J, y + z = r ^ n}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ ∃ m a b, ∃ (_ : a ∈ I) (_ : b ∈ J), a + b = ↑⟨z, hzs⟩ ^ m

Tactic:
obtain ⟨m, y, hyq, b, hb, hy⟩ := hs hzs

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
I J : Ideal R
z : R
hzs : z ∈ s
hs : s ⊆ ↑{ carrier := {r | ∃ n, ∃ y ∈ I, ∃ z ∈ J, y + z = r ^ n}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
m : ℕ
y : R
hyq : y ∈ I
b : R
hb : b ∈ J
hy : y + b = z ^ m
⊢ ∃ m a b, ∃ (_ : a ∈ I) (_ : b ∈ J), a + b = ↑⟨z, hzs⟩ ^ m
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
⊢ 1 ᵥ* A = ∑ i, A i

Tactic:
ext; simp [vecMul, dotProduct]

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

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
x✝¹ : M ∈ Set.range ⇑(scalar n)
i j : n
x✝ : i ≠ j
r : α
hr : (scalar n) r = M
⊢ Commute ((scalar n) r) (single i j 1)

Tactic:
scalar_commute_iff

Goal state after:
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
x✝¹ : M ∈ Set.range ⇑(scalar n)
i j : n
x✝ : i ≠ j
r : α
hr : (scalar n) r = M
⊢ r • single i j 1 = MulOpposite.op r • single i j 1