mathlib-initiative/mathlib-tactics huggingface dataset:
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))
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊥

Tactic:
by
  -- A little off-by-one cleanup first:
  suffices t : ∃ n : ℕ, ∀ m, n ≤ m → f (m + 1) = ⊥ by
    obtain ⟨n, w⟩ := t
    use n + 1
    rintro (_ | m) p
    · cases p
    · apply w
      exact Nat.succ_le_succ_iff.mp p
  obtain ⟨n, w⟩ := monotone_stabilizes_iff_noetherian.mpr inferInstance (partialSups f)
  refine ⟨n, fun m p ↦ (h m).eq_bot_of_ge <| sup_eq_left.mp ?_⟩
  simpa only [partialSups_add_one] using (w (m + 1) <| le_add_right p).symm.trans <| w m p

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
I : Ideal R
N : Submodule R M
x : ↥N
⊢ map N.subtype (I • ⊤) = I • N

Tactic:
Submodule.map_smul'',

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
⊢ I • map N.subtype ⊤ = I • 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
inst✝ : RingHomClass F R S
hf : Function.Bijective ⇑f
I : Ideal R
⊢ ⊤ ≤ I ↔ I = ⊤

Tactic:
top_le_iff

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
inst✝ : RingHomClass F R S
hf : Function.Bijective ⇑f
I : Ideal R
⊢ I = ⊤ ↔ I = ⊤
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : ¬gcd x y = 0
z : R
hz : x = gcd x y * z
⊢ gcd x y * (y * z) = x * y

Tactic:
rw [← mul_assoc, mul_right_comm, ← hz]

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : 0 ≤ n
⊢ I ^ n ≤ I ^ 0

Tactic:
Submodule.pow_zero,

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : 0 ≤ n
⊢ I ^ n ≤ 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
I J : Ideal R
e : I ≤ J
⊢ I ^ 0 ≤ J ^ 0

Tactic:
Submodule.pow_zero,

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
I J : Ideal R
e : I ≤ J
⊢ 1 ≤ J ^ 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
⊢ (I ^ Nat.zero).IsTwoSided

Tactic:
Submodule.pow_zero,

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
⊢ IsTwoSided 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
m : ℕ
⊢ I ^ m = I ^ m * I ^ 0

Tactic:
Submodule.pow_zero,

Goal state after:
case inl
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
m : ℕ
⊢ I ^ m = I ^ m * 1
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (span R s).annihilator = ⨅ g, (toSpanSingleton R M ↑g).ker

Tactic:
by
  ext; simp [mem_annihilator_span]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ gcd ?m.36 = GCDMonoid.gcd s₁.gcd s₂.gcd

pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

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

Tactic:
gcd_add

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

case s₁
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

case s₂
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ ?s₁ + ?s₂
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ gcd ?m.36 = GCDMonoid.gcd s₁.gcd s₂.gcd

pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

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

Tactic:
gcd_add

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

case s₁
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

case s₂
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ ?s₁ + ?s₂
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ ∃ t, s = map (fun x ↦ s.gcd * x) t ∧ t.gcd = 1

Tactic:
refine ⟨s.pmap @f fun _ ↦ id, ?_, extract_gcd' s _ h ?_⟩

Goal state after:
case neg.refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ s = map (fun x ↦ s.gcd * x) (pmap f s ⋯)

case neg.refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ s = map (fun x ↦ s.gcd * x) (pmap f s ⋯)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : n = 0
⊢ I ^ 0 = ⊤

Tactic:
Submodule.pow_zero,

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : n = 0
⊢ 1 = ⊤
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case refine_2.refine_2
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ ∀ (a : β) (s : Finset β), a ∉ s → {x ∈ s | f x = 0}.gcd f = 0 → {x ∈ insert a s | f x = 0}.gcd f = 0

Tactic:
intro a s _ h
        rw [filter_insert]
        split_ifs with h1 <;> simp [h, h1]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
h : IsGCDMonoid α
k m n : α
H : k ∣ m * n
⊢ ∃ a₁ a₂, a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂

Tactic:
cases h
    by_cases h0 : gcd k m = 0
    · rw [gcd_eq_zero_iff] at h0
      rcases h0 with ⟨rfl, rfl⟩
      exact ⟨0, n, dvd_refl 0, dvd_refl n, by simp⟩
    · obtain ⟨a, ha⟩ := gcd_dvd_left k m
      refine ⟨gcd k m, a, gcd_dvd_right _ _, ?_, ha⟩
      rw [← mul_dvd_mul_iff_left h0, ← ha]
      exact dvd_gcd_mul_of_dvd_mul H

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ IsUnit (gcd d₁ b ^ k)

Tactic:
apply IsUnit.pow

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ IsUnit (gcd d₁ b)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
f : Multiset α
hf : ∀ b ∈ f, Prime b
u : αˣ
ha : f.prod * ↑u ≠ 0
⊢ IsPrimal (f.prod * ↑u)

Tactic:
exact ((Submonoid.isPrimal α).multiset_prod_mem f (hf · · |>.isPrimal)).mul u.isUnit.isPrimal

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Classical.choose ⋯).prod ~ᵤ a

Tactic:
exact (Classical.choose_spec (exists_prime_factors a ane0)).2

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ factors 0 = 0

Tactic:
by simp [factors]

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

Goal state before:
pp: case zero
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
s : Finset ι
a b : ι
hn : s = ∅
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i

Tactic:
subst hn

Goal state after:
case zero
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
a b : ι
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑∅, ↑(f i)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ ∅, I ≤ f i
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
⊢ S = ⊥ ↔ generator S = 0

Tactic:
by rw [← @span_singleton_eq_bot R M, span_singleton_generator]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
x y z : R
inst✝ : IsPrincipal (Ideal.span {x, y})
hx : Ideal.span {x} ≤ Ideal.span {z}
hy : Ideal.span {y} ≤ Ideal.span {z}
⊢ Ideal.span {gcd x y} ≤ Ideal.span {z}

Tactic:
rw [span_gcd, Ideal.span_insert, sup_le_iff]

Goal state after:
R : Type u
inst✝¹ : CommRing R
x y z : R
inst✝ : IsPrincipal (Ideal.span {x, y})
hx : Ideal.span {x} ≤ Ideal.span {z}
hy : Ideal.span {y} ≤ Ideal.span {z}
⊢ Ideal.span {x} ≤ Ideal.span {z} ∧ Ideal.span {y} ≤ Ideal.span {z}
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case insert
R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * ↑u + s.gcd f * y * ↑u = GCDMonoid.gcd (f a) (s.gcd f)
g : α → R
hg : s.gcd f = ∑ a ∈ s, f a * g a
⊢ GCDMonoid.gcd (f a) (s.gcd f) = ∑ a_1 ∈ insert a s, f a_1 * update (fun x ↦ g x * (y * ↑u)) a (x * ↑u) a_1

Tactic:
sum_insert ha,

Goal state after:
case insert
R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * ↑u + s.gcd f * y * ↑u = GCDMonoid.gcd (f a) (s.gcd f)
g : α → R
hg : s.gcd f = ∑ a ∈ s, f a * g a
⊢ GCDMonoid.gcd (f a) (s.gcd f) =
    f a * update (fun x ↦ g x * (y * ↑u)) a (x * ↑u) a +
      ∑ x_1 ∈ s, f x_1 * update (fun x ↦ g x * (y * ↑u)) a (x * ↑u) x_1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : 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 i) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)

Tactic:
Set.biUnion_insert,

Goal state after:
ι : 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
⊢ ↑I ⊆ ↑(f i) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : 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) ∪ ↑(f i) ∪ ⋃ j ∈ ↑t, ↑(f j)

Tactic:
Set.biUnion_insert,

Goal state after:
ι : 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
⊢ ↑I ⊆ ↑(f a) ∪ ↑(f i) ∪ ⋃ j ∈ ↑t, ↑(f j)
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

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

Tactic:
· apply Surjective.comp (g := b.repr.toLinearMap)
    · apply LinearEquiv.surjective
    rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination]
    simpa using s

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✝
R : Type u_2
M : Type u_3
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
s t : Set M
inst✝ : Module.Finite R ↥(span R t)
hs : LinearIndepOn R id s
hst : s ⊆ t
⊢ Module.rank R ↥(span R t) < ℵ₀

Tactic:
exact Module.rank_lt_aleph0 ..

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

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

Tactic:
Set.biUnion_insert,

Goal state after:
case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ↑(f a) ∪ ⋃ x ∈ insert b ↑u, ↑(f x)
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
hp' : ∀ i ∈ u, (f i).IsPrime
⊢ ∃ i ∈ insert a (insert b u), I ≤ f i
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ↑(f a) ∪ ⋃ x ∈ insert b ↑u, ↑(f x)
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
hp' : ∀ i ∈ u, (f i).IsPrime
⊢ ∃ i ∈ insert a (insert b u), I ≤ f i

Tactic:
Set.biUnion_insert,

Goal state after:
case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ↑(f a) ∪ (↑(f b) ∪ ⋃ x ∈ ↑u, ↑(f x))
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
hp' : ∀ i ∈ u, (f i).IsPrime
⊢ ∃ i ∈ insert a (insert b u), I ≤ f i
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
⊢ Module.rank R ↥N < ℵ₀

Tactic:
exact lt_of_le_of_lt (Submodule.rank_le N) (rank_lt_aleph0 R M)

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

Goal state before:
pp: case neg
ι : 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
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i ∈ insert a t, I ≤ f i

Tactic:
Set.biUnion_insert,

Goal state after:
case neg
ι : 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 ⊆ ↑(f a) ∪ ⋃ x ∈ ↑t, ↑(f x)
has : a ∈ insert a t
hbt : b ∉ t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i ∈ insert a t, I ≤ f i
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
ι : 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
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i ∈ insert b t, I ≤ f i

Tactic:
Set.biUnion_insert,

Goal state after:
case pos
ι : 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 ⊆ ↑(f b) ∪ ⋃ x ∈ ↑t, ↑(f x)
has : a ∉ insert b t
hbs : b ∈ insert b t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i ∈ insert b t, I ≤ f i
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
a : α
⊢ single i j a = of (Pi.single i (Pi.single j a))

Tactic:
ext a b
  unfold single
  by_cases hi : i = a <;> by_cases hj : j = b <;> simp [*]

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

Goal state before:
pp: case neg.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
i : ι
t : Finset ι
left✝ : i ∉ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime
h : ↑I ⊆ ⋃ i_1 ∈ insert i ↑t, ↑(f i_1)
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
Set.biUnion_insert,

Goal state after:
case neg.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
i : ι
t : Finset ι
left✝ : i ∉ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime
h : ↑I ⊆ ↑(f i) ∪ ⋃ x ∈ ↑t, ↑(f x)
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i_1 ∈ insert i t, I ≤ f i_1
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case inl.hi
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq o
inst✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
i' : l
j' : m
hi : f.symm i ≠ i'
⊢ i ≠ f i'

Tactic:
exact f.symm_apply_eq.not.1 hi

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

Goal state before:
pp: n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ v i * Pi.single j x i = Pi.single j (v j * x) i

Tactic:
exact Pi.apply_single (fun i x => v i * x) (fun i => mul_zero _) j x i

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
I : Ideal R
f : M →ₗ[R] N
h : Function.Surjective ⇑f
⊢ comap f (I • ⊤) = comap f (map f (I • ⊤))

Tactic:
Submodule.map_smul'',

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
I : Ideal R
f : M →ₗ[R] N
h : Function.Surjective ⇑f
⊢ comap f (I • ⊤) = comap f (I • map f ⊤)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
I J : Ideal R
hs : s ⊆ ↑(I ⊔ J).radical
⊢ ∃ t, Set.range t ⊆ ↑I ∧ s ⊆ ↑(span (Set.range t) ⊔ J).radical

Tactic:
replace hs : ∀ z : s, ∃ (m : ℕ) (a b : R) (ha : a ∈ I) (hb : b ∈ J), a + b = z ^ m := by
    rintro ⟨z, hzs⟩
    simp only [Ideal.radical, Submodule.mem_sup] at hs
    obtain ⟨m, y, hyq, b, hb, hy⟩ := hs hzs
    exact ⟨m, y, b, hyq, hb, hy⟩
  choose m a b ha hb heq using hs
  refine ⟨a, by rwa [Set.range_subset_iff], fun z hz ↦ ⟨m ⟨z, hz⟩, heq ⟨z, hz⟩ ▸ ?_⟩⟩
  exact Ideal.add_mem _ (mem_sup_left (subset_span ⟨⟨z, hz⟩, rfl⟩)) (mem_sup_right <| hb _)

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → m
e₂ : n ≃ o
⊢ M.submatrix e₁ id * N.submatrix (⇑e₂) id = M.submatrix e₁ ⇑e₂.symm * N

Tactic:
ext; simp [mul_apply, ← e₂.bijective.sum_comp]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → p
e₂ : o ≃ n
⊢ M.submatrix id ⇑e₂ * N.submatrix id e₁ = M * N.submatrix (⇑e₂.symm) e₁

Tactic:
ext; simp [mul_apply, ← e₂.bijective.sum_comp]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
β : Type w
inst✝² : Fintype n
inst✝¹ : NonAssocSemiring α
inst✝ : NonAssocSemiring β
M : Matrix m n α
N : Matrix n o α
i : m
j : o
f : α →+* β
⊢ f ((M * N) i j) = (M.map ⇑f * N.map ⇑f) i j

Tactic:
simp [Matrix.mul_apply, map_sum]

Goal state after:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : Multiset.map g (toMultiset f) = toMultiset (mapDomain g f)
⊢ Multiset.map g (toMultiset (single a n)) + toMultiset (mapDomain g f) =
    toMultiset (mapDomain g (single a n) + mapDomain g f)

Tactic:
mapDomain_single,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : Multiset.map g (toMultiset f) = toMultiset (mapDomain g f)
⊢ Multiset.map g (toMultiset (single a n)) + toMultiset (mapDomain g f) = toMultiset (single (g a) n + mapDomain g f)
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : Multiset.map g (toMultiset f) = toMultiset (mapDomain g f)
⊢ (Multiset.mapAddMonoidHom g) (n • {a}) + toMultiset (mapDomain g f) = n • {g a} + toMultiset (mapDomain g f)

Tactic:
(Multiset.mapAddMonoidHom g).map_nsmul

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : Multiset.map g (toMultiset f) = toMultiset (mapDomain g f)
⊢ n • (Multiset.mapAddMonoidHom g) {a} + toMultiset (mapDomain g f) = n • {g a} + toMultiset (mapDomain g f)