mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_1.refine_2
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
⊢ ∀ (r : R) ⦃m : M⦄, m ∈ ⇑(algebraMap S R) '' s • N → m ∈ s • restrictScalars S N → r • m ∈ s • restrictScalars S N

Tactic:
intro r y h h'

Goal state after:
case refine_1.refine_2
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
r : R
y : M
h : y ∈ ⇑(algebraMap S R) '' s • N
h' : y ∈ s • restrictScalars S N
⊢ r • y ∈ s • restrictScalars S N
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {M : ι → Type u_7} [inst : (i : ι) → AddCommGroup (M i)] [inst_1 : (i : ι) → Module R (M i)]
    [∀ (i : ι), IsNoetherian R (M i)], IsNoetherian R ((i : ι) → M i)

Tactic:
apply Finite.induction_empty_option _ _ _ ι

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {α β : Type u_6} (a : α ≃ β),
    (∀ {M : α → Type u_7} [inst : (i : α) → AddCommGroup (M i)] [inst_1 : (i : α) → Module R (M i)]
        [∀ (i : α), IsNoetherian R (M i)], IsNoetherian R ((i : α) → M i)) →
      ∀ {M : β → Type u_7} [inst : (i : β) → AddCommGroup (M i)] [inst_1 : (i : β) → Module R (M i)]
        [∀ (i : β), IsNoetherian R (M i)], IsNoetherian R ((i : β) → M i)

R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {M : PEmpty.{u_6 + 1} → Type u_7} [inst : (i : PEmpty.{u_6 + 1}) → AddCommGroup (M i)]
    [inst_1 : (i : PEmpty.{u_6 + 1}) → Module R (M i)] [∀ (i : PEmpty.{u_6 + 1}), IsNoetherian R (M i)],
    IsNoetherian R ((i : PEmpty.{u_6 + 1}) → M i)

R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {α : Type u_6} [Fintype α],
    (∀ {M : α → Type u_7} [inst : (i : α) → AddCommGroup (M i)] [inst_1 : (i : α) → Module R (M i)]
        [∀ (i : α), IsNoetherian R (M i)], IsNoetherian R ((i : α) → M i)) →
      ∀ {M : Option α → Type u_7} [inst : (i : Option α) → AddCommGroup (M i)]
        [inst_1 : (i : Option α) → Module R (M i)] [∀ (i : Option α), IsNoetherian R (M i)],
        IsNoetherian R ((i : Option α) → M i)
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {M : ι → Submodule R N} [∀ (i : ι), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)

Tactic:
apply Finite.induction_empty_option _ _ _ ι

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {α β : Type u_6} (a : α ≃ β),
    (∀ {M : α → Submodule R N} [∀ (i : α), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)) →
      ∀ {M : β → Submodule R N} [∀ (i : β), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)

R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {M : PEmpty.{u_6 + 1} → Submodule R N} [∀ (i : PEmpty.{u_6 + 1}), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)

R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {α : Type u_6} [Fintype α],
    (∀ {M : α → Submodule R N} [∀ (i : α), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)) →
      ∀ {M : Option α → Submodule R N} [∀ (i : Option α), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {R : ι → Type u_1} [inst : (i : ι) → Semiring (R i)] [∀ (i : ι), IsNoetherianRing (R i)],
    IsNoetherianRing ((i : ι) → R i)

Tactic:
apply Finite.induction_empty_option _ _ _ ι

Goal state after:
ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {α β : Type u_2} (a : α ≃ β),
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : α) → R i)) →
      ∀ {R : β → Type u_1} [inst : (i : β) → Semiring (R i)] [∀ (i : β), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : β) → R i)

ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {R : PEmpty.{u_2 + 1} → Type u_1} [inst : (i : PEmpty.{u_2 + 1}) → Semiring (R i)]
    [∀ (i : PEmpty.{u_2 + 1}), IsNoetherianRing (R i)], IsNoetherianRing ((i : PEmpty.{u_2 + 1}) → R i)

ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {α : Type u_2} [Fintype α],
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : α) → R i)) →
      ∀ {R : Option α → Type u_1} [inst : (i : Option α) → Semiring (R i)] [∀ (i : Option α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : Option α) → R i)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: M : Type u_1
inst✝ : AddCommGroup M
a : M
⊢ (ℤ ∙ a).toAddSubgroup = AddSubgroup.zmultiples a

Tactic:
ext i
  simp [Submodule.mem_span_singleton, AddSubgroup.mem_zmultiples_iff]

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y x✝ s✝ t✝ s'✝ t'✝ : R
⊢ (xgcdAux 0 s✝ t✝ x✝ s'✝ t'✝).1 = gcd 0 x✝

Tactic:
xgcd_zero_left,

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y x✝ s✝ t✝ s'✝ t'✝ : R
⊢ (x✝, s'✝, t'✝).1 = gcd 0 x✝
Module: Mathlib.Algebra.EuclideanDomain.Basic

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

Tactic:
zero_mul,

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x : R
⊢ 0 / gcd 0 x = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
h : I ⊔ J = ⊤
i : R
hi : i ∈ I ⊔ K
⊢ i ∈ I ⊔ J * K

Tactic:
by
    rw [eq_top_iff_one] at h; rw [Submodule.mem_sup] at h hi ⊢
    obtain ⟨i1, hi1, j, hj, h⟩ := h; obtain ⟨i', hi', k, hk, rfl⟩ := hi
    refine ⟨_, add_mem hi' (mul_mem_right k _ hi1), _, mul_mem_mul hj hk, ?_⟩
    rw [add_assoc, ← add_mul, h, one_mul]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
I : Ideal R
f : F
⊢ map f I = ⊥ ↔ I ≤ RingHom.ker f

Tactic:
rw [RingHom.ker, eq_bot_iff, map_le_iff_le_comap]

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

Goal state before:
pp: case neg
z : ℤ
hz : -z = z
h : z < 0
⊢ 0 ≤ z

Tactic:
lia

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

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : ¬n ≤ i
⊢ m ≤ n + m - i

Tactic:
lia

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Semiring S
inst✝ : Algebra R S
I : Ideal R
x y : ↥I
⊢ (idealMap S I) (x * y) = (idealMap S I) x * (idealMap S I) y

Tactic:
ext
  simp

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

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
hs : ∃ x ∈ s, f x ≠ 0
hg : ∀ b ∈ s, f b = s.gcd f * g b
⊢ Associated (s.gcd f * 1) (s.gcd fun x ↦ s.gcd f * g x)

Tactic:
simp [← gcd_congr rfl hg]

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a✝ : Nontrivial α
⊢ (if 1 = 0 then 1 else Exists.choose ⋯) = 1

Tactic:
rw [← Units.val_inj]

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a✝ : Nontrivial α
⊢ ↑(if 1 = 0 then 1 else Exists.choose ⋯) = ↑1
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∃ x ∈ s, f x ≠ 0
⊢ ∃ g, (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1

Tactic:
choose g' hg using @gcd_dvd _ _ _ _ s f
      refine ⟨fun b ↦ if hb : b ∈ s then g' hb else 0, fun b hb ↦ ?_,
          extract_gcd' f _ h fun b hb ↦ ?_⟩
      · simp only [hb, hg, dite_true]
      rw [dif_pos hb, hg hb]

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

Goal state before:
pp: α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
H : Ideal.span {a} = ⊤
⊢ False

Tactic:
rw [Ideal.span_singleton_eq_top] at H

Goal state after:
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
H : IsUnit a
⊢ False
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a✝ : Nontrivial α
⊢ normUnit (0 * ↑1) = 1

Tactic:
zero_mul,

Goal state after:
case inl
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a✝ : Nontrivial α
⊢ normUnit 0 = 1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case hba
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : gcd (a * b) (a * c) = a * d
⊢ a * gcd b c ∣ gcd (a * b) (a * c)

Tactic:
exact dvd_gcd (mul_dvd_mul_left a <| gcd_dvd_left _ _) (mul_dvd_mul_left a <| gcd_dvd_right _ _)

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

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

Tactic:
simp [factors]

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
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ f (Associates.mk (a * b)) = f (Associates.mk a * Associates.mk b)

Tactic:
Associates.mk_mul_mk

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ f (Associates.mk (a * b)) = f (Associates.mk (a * b))
Module: Mathlib.LinearAlgebra.Dimension.Subsingleton

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Subsingleton M
⊢ Module.rank R M = 0

Tactic:
by
  rw [Module.rank, ← bot_eq_zero, eq_bot_iff]
  exact ciSup_le fun s ↦ by simp [(linearIndependent_subsingleton_iff _).mp s.2]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
S : Type u_1
F : Type u_3
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
I : Ideal S
hI : IsPrincipal (comap f I)
⊢ IsPrincipal I

Tactic:
rw [← map_comap_of_surjective f hf I]
  exact hI.map_ringHom f

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝ : Add α
M N : Matrix m n α
⊢ (M + N)ᵀ = Mᵀ + Nᵀ

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝ : Sub α
M N : Matrix m n α
⊢ (M - N)ᵀ = Mᵀ - Nᵀ

Tactic:
ext
  simp

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

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Fintype ↑J
⊢ #↑(range ⇑v) ≤ #↑J

Tactic:
rw [← Cardinal.lift_le, Cardinal.mk_range_eq_of_injective v.injective, Cardinal.mk_fintype J]

Goal state after:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Fintype ↑J
⊢ lift.{v, w} #ι ≤ lift.{w, v} ↑(Fintype.card ↑J)
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 ⊆ ↑(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

Tactic:
← Set.union_self (f i : Set R),

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) ∪ ↑(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.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:
rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f i : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h

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 ∨ ∃ i ∈ t, I ≤ f i
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.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
a : α
⊢ a • M = (diagonal fun x ↦ a) * M

Tactic:
ext
  simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
a : α
⊢ MulOpposite.op a • M = M * diagonal fun x ↦ a

Tactic:
ext
  simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
A : Matrix m n α
x y : m → α
x✝ : n
⊢ ((x - y) ᵥ* A) x✝ = (x ᵥ* A - y ᵥ* A) x✝

Tactic:
apply sub_dotProduct

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

Goal state before:
pp: n : Type u_3
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : (M ^ k).row i = 0
h' : k ≤ l
⊢ l = k + (l - k)

Tactic:
lia

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

Goal state before:
pp: n : Type u_3
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : (M ^ k).col i = 0
h' : k ≤ l
⊢ l = l - k + k

Tactic:
lia

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: case inr
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Infinite α
⊢ #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)

Tactic:
· apply mk_finsupp_lift_of_infinite

Goal state after:
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
x : ↑T
i : ι
hx : ↑x ∈ S i
⊢ iUnionLift S f hf T hT x = f i ⟨↑x, hx⟩

Tactic:
by obtain ⟨x, hx⟩ := x; exact hf _ _ _ _ _

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ (f.sum fun x n ↦ Multiset.count a (n • {x})) = f.sum fun x n ↦ n * Multiset.count a {x}

Tactic:
by simp only [Multiset.count_nsmul]

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

Goal state before:
pp: m : Type u_2
α : Type u_11
inst✝ : AddZeroClass α
i : m
⊢ (Pi.evalAddMonoidHom (fun i ↦ α) i).comp (diagAddMonoidHom m α) = entryAddMonoidHom α i i

Tactic:
by
  simp [AddMonoidHom.ext_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toFinsupp (s ∪ t) = toFinsupp s ⊔ toFinsupp t

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toFinsupp (s ∩ t) = toFinsupp s ⊓ toFinsupp t

Tactic:
ext
  simp

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon x y ↔ x - y ∈ I

Tactic:
mem_iff

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon x y ↔ I.ringCon (x - y) 0
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I✝ I J : TwoSidedIdeal R
h :
  { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } I ≤
    { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } J
x : R
hx : x ∈ I
⊢ x ∈ J

Tactic:
mem_iff

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I✝ I J : TwoSidedIdeal R
h :
  { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } I ≤
    { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } J
x : R
hx : I.ringCon x 0
⊢ J.ringCon x 0
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
a b c d : R
h1 : a - b ∈ carrier
h2 : c - d ∈ carrier
⊢ a * c - b * d = a * c - a * d + (a - b) * d

Tactic:
sub_mul

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
a b c d : R
h1 : a - b ∈ carrier
h2 : c - d ∈ carrier
⊢ a * c - b * d = a * c - a * d + (a * d - b * d)
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
x : R
⊢ x ∈ mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right ↔ x ∈ carrier

Tactic:
mem_iff

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
x : R
⊢ (mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right).ringCon x 0 ↔ x ∈ carrier
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: ι₁ ι₂ : Type v
inst✝² : DecidableEq ι₂
f : ι₁ → ι₂
β : ι₁ → Type w
inst✝¹ : (i : ι₁) → AddCommMonoid (β i)
inst✝ : DecidableEq ι₁
i : ι₁
x : β i
h : (y : ι₂) × { x // f x = y } ≃ ι₁ := Equiv.sigmaFiberEquiv f
k : (j : ι₂) × { i₁ // f i₁ = j } := ⟨f i, ⟨i, ⋯⟩⟩
⊢ sigmaCurry ((equivCongrLeft (Equiv.sigmaFiberEquiv f).symm) ((of β (h k)) x)) =
    sigmaCurry ((of (fun k ↦ β ↑k.snd) k) x)

Tactic:
exact congrArg sigmaCurry (equivCongrLeft_of (h := h.symm) _ _)

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
⊢ (sSup S).toSubsemiring = sSup (toSubsemiring '' S)

Tactic:
have h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S := by
    rw [Set.image_image]
    congr! with x
    exact x.toSubsemiring.closure_eq.symm
  rw [h, sSup_image, ← Subsemiring.closure_sUnion, sSup_def, adjoin_toSubsemiring]
  congr 1
  rw [Set.union_eq_right]
  rintro _ ⟨x, rfl⟩
  obtain ⟨y, hy⟩ := hS
  simp only [Set.mem_sUnion, Set.mem_image, exists_exists_and_eq_and, SetLike.mem_coe]
  exact ⟨y, hy, algebraMap_mem y x⟩

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
κ : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
e : ι ≃ κ
k : κ
x : M (e.symm k)
j : κ
⊢ (if h : k = j then ⋯ ▸ x else 0) = if h : k = j then ⋯ ▸ x else 0

Tactic:
lia

Goal state after:
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
s : Set ι
h : iSupIndep fun i ↦ A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
this : (⇑e ∘ fun i ↦ Submodule.comap p.subtype (A ↑i)) = fun i ↦ ⟨A ↑i, ⋯⟩
⊢ iSupIndep fun i ↦ Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)

Tactic:
← iSupIndep_map_orderIso_iff e,

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
s : Set ι
h : iSupIndep fun i ↦ A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
this : (⇑e ∘ fun i ↦ Submodule.comap p.subtype (A ↑i)) = fun i ↦ ⟨A ↑i, ⋯⟩
⊢ iSupIndep (⇑e ∘ fun i ↦ Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i))