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

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (p : LTSeries α), RelSeries.last p = x → ↑p.length ≤ height ↑x

Tactic:
intro p

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
⊢ RelSeries.last p = x → ↑p.length ≤ height ↑x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x ≤ height ↑x

Tactic:
apply height_le
    intro p hlast
    let p' := p.map _ WithTop.coe_strictMono
    apply le_iSup₂_of_le p' (by simp [p', hlast]) (by simp [p'])

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
h'' : f (p.toFun i) < f x
⊢ False

Tactic:
obtain ⟨n', hn'⟩ : ∃ (n' : ℕ), n' = height (f (p i)) := ENat.ne_top_iff_exists.mp
        ((height_mono h''.le).trans_lt (h' ▸ ENat.natCast_lt_top _)).ne

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
h'' : f (p.toFun i) < f x
n' : ℕ
hn' : ↑n' = height (f (p.toFun i))
⊢ False
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ (Neg.aux R) (x + y) + (x + y) = (Neg.aux R) x + x + ((Neg.aux R) y + y)

Tactic:
map_add

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ (Neg.aux R) x + (Neg.aux R) y + (x + y) = (Neg.aux R) x + x + ((Neg.aux R) y + y)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
⊢ krullDim α ≤ (↑m + 1) * krullDim β + ↑m

Tactic:
by
  rw [Order.krullDim_eq_iSup_height, Order.krullDim_eq_iSup_height, iSup_le_iff]
  refine fun x ↦ (WithBot.coe_mono (height_le_of_krullDim_preimage_le f h x)).trans ?_
  push_cast
  gcongr
  exacts [right_eq_inf.mp rfl, le_iSup_iff.mpr fun b a ↦ a (f x)]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
this : 1 + a * (1 + a * a∗) ≤ 1 + a * a∗
⊢ a∗ ≤ 1 + a * a∗

Tactic:
rw [add_le_iff] at this

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
this : 1 ≤ 1 + a * a∗ ∧ a * (1 + a * a∗) ≤ 1 + a * a∗
⊢ a∗ ≤ 1 + a * a∗
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
this : 1 + (1 + a∗ * a) * a ≤ 1 + a∗ * a
⊢ a∗ ≤ 1 + a∗ * a

Tactic:
rw [add_le_iff] at this

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
this : 1 ≤ 1 + a∗ * a ∧ (1 + a∗ * a) * a ≤ 1 + a∗ * a
⊢ a∗ ≤ 1 + a∗ * a
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommGroup P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : N →ₗ[R] P
⊢ rTensor Q (-f) = -rTensor Q f

Tactic:
simp only [← coe_rTensorHom]
  exact (rTensorHom (R := R) (N := N) (P := P) Q).map_neg f

Goal state after:
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
b : I
t : Finset I
hbt : b ∉ t
ih : IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x
⊢ (IsCoprime (s b) x ∧ ∀ i ∈ t, IsCoprime (s i) x) ↔ ∀ i ∈ insert b t, IsCoprime (s i) x

Tactic:
Finset.forall_mem_insert

Goal state after:
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x
⊢ (IsCoprime (s b) x ∧ ∀ i ∈ t, IsCoprime (s i) x) ↔ IsCoprime (s b) x ∧ ∀ x_1 ∈ t, IsCoprime (s x_1) x
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: case neg
α : 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
⊢ sli[↑hi.choose] ≤ sli[↑hj.choose] ↔ ↑hi.choose ≤ ↑hj.choose

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case neg.refine_1
α : 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 : sli[↑hi.choose] ≤ sli[↑hj.choose]
⊢ ↑hi.choose ≤ ↑hj.choose

case neg.refine_2
α : 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
⊢ sli[↑hi.choose] ≤ sli[↑hj.choose]
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
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective ⇑↑(opLinearEquiv R)
⊢ map LinearMap.id (M * N) = map LinearMap.id M * map LinearMap.id N

Tactic:
map_id,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective ⇑↑(opLinearEquiv R)
⊢ M * N = map LinearMap.id M * map LinearMap.id N
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
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective ⇑↑(opLinearEquiv R)
⊢ M * N = map LinearMap.id M * map LinearMap.id N

Tactic:
map_id,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective ⇑↑(opLinearEquiv R)
⊢ M * N = M * map LinearMap.id N
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
H : ∀ i ∈ insert b t, IsRelPrime (s i) x
⊢ IsRelPrime (s b * ∏ x ∈ t, s x) x

Tactic:
Finset.forall_mem_insert

Goal state after:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
H : IsRelPrime (s b) x ∧ ∀ x_1 ∈ t, IsRelPrime (s x_1) x
⊢ IsRelPrime (s b * ∏ x ∈ t, s x) x
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: α : Type u_1
I : Type u_2
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x
⊢ (IsRelPrime (s b) x ∧ ∀ i ∈ t, IsRelPrime (s i) x) ↔ ∀ i ∈ insert b t, IsRelPrime (s i) x

Tactic:
Finset.forall_mem_insert

Goal state after:
α : Type u_1
I : Type u_2
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x
⊢ (IsRelPrime (s b) x ∧ ∀ i ∈ t, IsRelPrime (s i) x) ↔ IsRelPrime (s b) x ∧ ∀ x_1 ∈ t, IsRelPrime (s x_1) x
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
aux1 : a ∈ ↑(insert a r)
hir : a ∈ r
⊢ False

Tactic:
exact har hir

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
⊢ IsRelPrime (x ^ m) y ↔ IsRelPrime x y

Tactic:
refine ⟨fun h ↦ ?_, IsRelPrime.pow_left⟩
  rw [← Finset.card_range m, ← Finset.prod_const] at h
  exact h.of_prod_left 0 (Finset.mem_range.mpr hm)

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
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
⊢ I • comap f S ≤ comap f (I • S)

Tactic:
by
  refine Submodule.smul_le.mpr fun r hr x hx => ?_
  rw [Submodule.mem_comap] at hx ⊢
  rw [f.map_smul]
  exact Submodule.smul_mem_smul hr hx

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

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

Tactic:
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

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

Goal state before:
pp: case zero
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
⊢ 1 ≤ comap f 1

Tactic:
Ideal.one_eq_top,

Goal state after:
case zero
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
⊢ ⊤ ≤ comap f 1
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : R
h : ∀ (m : M'), x • m = 0
m : M
⊢ f (x • m) = f 0

Tactic:
rw [map_smul, h, f.map_zero]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
I : Ideal R
⊢ I ≤ N.annihilator ↔ I • N ≤ ⊥

Tactic:
smul_le,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
I : Ideal R
⊢ I ≤ N.annihilator ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ ⊥
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: ⊢ Associates ℤ ≃ ℕ

Tactic:
refine ⟨(·.out.natAbs), (Associates.mk ·), ?_, fun n ↦ ?_⟩

Goal state after:
case refine_1
⊢ Function.LeftInverse (fun x ↦ Associates.mk ↑x) fun x ↦ x.out.natAbs

case refine_2
n : ℕ
⊢ (fun x ↦ x.out.natAbs) ((fun x ↦ Associates.mk ↑x) n) = n
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
⊢ normalize (s.gcd f) = s.gcd f

Tactic:
by simp [gcd_def]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun x ↦ x ∈ {K | r ∉ K.radical}) m
hrm : r ∉ m.radical
this : ∀ x ∉ m, r ∈ (m ⊔ span {x}).radical
x y : R
hxym : x * y ∈ m
hxm : x ∉ m
hym : y ∉ m
n : ℕ
hrn : r ^ n ∈ m ⊔ span {x}
p : R
hpm : p ∈ m
q : R
hq : q ∈ span {x}
hpqrn : p + q = r ^ n
c : R
hcxq : c * x = q
k : ℕ
hrk : r ^ k ∈ m ⊔ span {y}
f : R
hfm : f ∈ m
g : R
hg : g ∈ span {y}
hfgrk : f + g = r ^ k
d : R
hdyg : d * y = g
⊢ r ^ (n + k) ∈ m

Tactic:
by
                  rw [pow_add, ← hpqrn, ← hcxq, ← hfgrk, ← hdyg, add_mul, mul_add (c * x),
                      mul_assoc c x (d * y), mul_left_comm x, ← mul_assoc]
                  refine
                    m.add_mem (m.mul_mem_right _ hpm)
                    (m.add_mem (m.mul_mem_left _ hfm) (m.mul_mem_left _ hxym))

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b : α
h : normalize b = b
⊢ lcm a b = b ↔ a ∣ b

Tactic:
by simpa only [lcm_comm b a] using lcm_eq_left_iff b a h

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

Goal state before:
pp: case hab
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a b ∣ c

Tactic:
rcases h with ⟨d, hd⟩

Goal state after:
case hab
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
⊢ gcd a b ∣ c
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case hba
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a c ∣ b

Tactic:
rcases h with ⟨d, hd⟩

Goal state after:
case hba
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
⊢ gcd a c ∣ b
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 j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i (insert j u)), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
⊢ ∀ k ∈ insert i u, (f k).IsPrime

Tactic:
Finset.forall_mem_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 j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i (insert j u)), ↑(f i_1)
hp : (f i).IsPrime ∧ (f j).IsPrime ∧ ∀ x ∈ u, (f x).IsPrime
hjt : j ∈ insert j u
⊢ (f i).IsPrime ∧ ∀ x ∈ u, (f x).IsPrime
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
x : M
⊢ x ∈ S ↔ x ∈ R ∙ generator S

Tactic:
span_singleton_generator

Goal state after:
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 = ⊥ ↔ R ∙ generator S = ⊥

Tactic:
span_singleton_generator

Goal state after:
R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
⊢ S = ⊥ ↔ S = ⊥
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ (∃ n f, Injective ⇑f) ↔ ∃ n f, Injective ⇑f

Tactic:
constructor <;> refine fun ⟨n, f, inj⟩ ↦ ⟨n, ?_⟩

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
x✝ : ∃ n f, Injective ⇑f
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
inj : Injective ⇑f
⊢ ∃ f, Injective ⇑f

case mpr
R : Type u
inst✝ : Semiring R
x✝ : ∃ n f, Injective ⇑f
n : ℕ
f : (ℕ →₀ R) →ₗ[R] Fin n → R
inj : Injective ⇑f
⊢ ∃ f, Injective ⇑f
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
x✝ : ∃ n f, Injective ⇑f
n : ℕ
f : (ℕ →₀ R) →ₗ[R] Fin n → R
inj : Injective ⇑f
⊢ ∃ f, Injective ⇑f

Tactic:
exact ⟨f ∘ₗ Finsupp.lmapDomain R R (↑) ∘ₗ (Finsupp.linearEquivFunOnFinite ..).symm.toLinearMap,
      inj.comp <| by simpa using! Finsupp.mapDomain_injective Fin.val_injective⟩

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
N : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] N
S : Submodule R M
hI : S.IsPrincipal
⊢ Submodule.map f S = Submodule.map f (R ∙ generator S)

Tactic:
span_singleton_generator

Goal state after:
R : Type u
M : Type v
N : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] N
S : Submodule R M
hI : S.IsPrincipal
⊢ Submodule.map f S = Submodule.map f S
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
d₁ d₂ : n → α
h : diagonal d₁ = diagonal d₂
i : n
⊢ d₁ i = d₂ i

Tactic:
by simpa using congr_arg (fun m : Matrix n n α => m i i) h

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_4
m : Type u_5
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
this : LinearIndependent R fun i ↦ b i • a
⊢ Fintype.card m = Fintype.card n

Tactic:
exact le_antisymm
    (b.card_le_card_of_linearIndependent (c.linearIndependent.map' (Submodule.subtype I)
      ((LinearMap.ker_eq_bot (f := (Submodule.subtype I : I →ₗ[R] S))).mpr Subtype.coe_injective)))
    (c.card_le_card_of_linearIndependent this)

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

Goal state before:
pp: R : Type u_2
ι : Type u_3
inst✝ : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
⊢ ↑I ⊆ ⋃ i ∈ s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i

Tactic:
rcases Set.Finite.exists_finset hs with ⟨t, ht⟩
  have heq : ⋃ i ∈ s, f i = ⋃ i ∈ t, (f i : Set R) := by
    ext
    simpa using exists_congr (fun i ↦ (and_congr_left fun a ↦ ht i).symm)
  have hmem_union : ((I : Set R) ⊆ ⋃ i ∈ s, f i) ↔ ((I : Set R) ⊆ ⋃ i ∈ (t : Set ι), f i) :=
    (congrArg _ heq).to_iff
  rw [hmem_union, Ideal.subset_union_prime a b (fun i hin ↦ hp i ((ht i).mp hin))]
  exact exists_congr (fun i ↦ and_congr_left fun _ ↦ ht i)

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 m
A : Matrix m n α
⊢ 0 ᵥ* A = 0

Tactic:
ext
  simp [vecMul]

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 m
v : m → α
⊢ v ᵥ* 0 = 0

Tactic:
ext
  simp [vecMul]

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

Goal state before:
pp: case inr.inl.inr
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j : n
hij : i ≠ j
⊢ M i i = M j j

Tactic:
exact diag_eq_of_commute_single (hM hij)

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✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
⊢ M * submatrix 1 (⇑e₁) e₂ = M.submatrix id (⇑e₁.symm ∘ e₂)

Tactic:
cases nonempty_fintype o

Goal state after:
case intro
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val✝ : Fintype o
⊢ M * submatrix 1 (⇑e₁) e₂ = M.submatrix id (⇑e₁.symm ∘ e₂)
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 m
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
⊢ submatrix 1 e₁ ⇑e₂ * M = M.submatrix (⇑e₂.symm ∘ e₁) id

Tactic:
cases nonempty_fintype o

Goal state after:
case intro
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype m
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
val✝ : Fintype o
⊢ submatrix 1 e₁ ⇑e₂ * M = M.submatrix (⇑e₂.symm ∘ e₁) id
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case intro
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype m
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
val✝ : Fintype o
⊢ submatrix 1 e₁ ⇑e₂ * M = M.submatrix (⇑e₂.symm ∘ e₁) id

Tactic:
let A := M.submatrix e₂.symm id

Goal state after:
case intro
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype m
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
val✝ : Fintype o
A : Matrix o n α := M.submatrix (⇑e₂.symm) id
⊢ submatrix 1 e₁ ⇑e₂ * M = M.submatrix (⇑e₂.symm ∘ e₁) id
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
R : Type u_7
S : Type u_8
inst✝² : Fintype n
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
v w : n → R
⊢ f (v ⬝ᵥ w) = ⇑f ∘ v ⬝ᵥ ⇑f ∘ w

Tactic:
by
  simp only [dotProduct, map_sum f, f.map_mul, Function.comp]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
N' : Type v'
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
cnd : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} #ι
⊢ ∃ f, Injective ⇑f

Tactic:
by
  nontriviality M
  have := Module.nontrivial R M
  rcases Module.Free.exists_set R M with ⟨_, ⟨B⟩⟩
  replace cnd := (Cardinal.lift_le.2 B.linearIndependent.cardinal_le_rank).trans cnd
  rw [Cardinal.lift_mk_le'] at cnd
  rcases cnd with ⟨i, hi⟩
  refine ⟨B.constr ℕ (v ∘ i), B.injective_constr_of_linearIndependent (hv.comp _ hi)⟩

Goal state after: