mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
⊢ ((Pi.basis s).repr (single j ((s j) i))) ⟨j', i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩

Tactic:
by_cases hj : j = j'

Goal state after:
case pos
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : j = j'
⊢ ((Pi.basis s).repr (single j ((s j) i))) ⟨j', i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩

case neg
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ((Pi.basis s).repr (single j ((s j) i))) ⟨j', i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
hs2 : (s ⊓ f.ker).FG
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
⊢ s.FG

Tactic:
obtain ⟨t2, ht2⟩ := hs2

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
⊢ s.FG
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
x : E
⊢ (ofIsCompl hpq φ ψ) x = (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯) x

Tactic:
obtain ⟨a, b, rfl, _⟩ := existsUnique_add_of_isCompl hpq x

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
a : ↥p
b : ↥q
right✝ : ∀ (r : ↥p) (s : ↥q), ↑r + ↑s = ↑a + ↑b → r = a ∧ s = b
⊢ (ofIsCompl hpq φ ψ) (↑a + ↑b) = (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯) (↑a + ↑b)
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ι₂ → ℕ∞
inst✝¹ : Nonempty ι₁
inst✝ : Nonempty ι₂
h : ⨆ i, ⨆ j, f i j < ⊤
⊢ ∃ i j, f i j = ⨆ i, ⨆ j, f i j

Tactic:
rw [iSup_prod'] at h ⊢
  exact Prod.exists'.mp (exists_eq_iSup_of_lt_top h)

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inr
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

Tactic:
refine le_antisymm ?_ (iSup_le fun a => add_le_add (le_iSup _ _) (le_iSup _ _))

Goal state after:
case inr
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g ≤ ⨆ i, f i + g i
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
i : ι
⊢ a - (a - f i) ≤ a - ⨅ i, a - f i

Tactic:
exact tsub_le_tsub_left (iInf_le (a - f ·) i) _

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
R : SetRel α α
inst✝ : R.IsSymm
⊢ R.inv = R

Tactic:
by ext; exact R.comm

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: case mpr.mpr
α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b, (a, b) ∈ R
f : α → β
hf : ∀ (x : α), (x, f x) ∈ R
a : α
b : β
⊢ (a, b) ∈ R → (a, b) ∈ Function.graph f

Tactic:
exact (h _).unique (hf _)

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) (Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)).succ =
    q.head

Tactic:
convert! Fin.append_right p q _

Goal state after:
case e'_2
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) (Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)).succ =
    Fin.append p.toFun q.toFun (Fin.natAdd (p.length + 1) 0)
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inr
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
this :
  ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [WellFoundedLT α] [WellFoundedGT α]
    (s : LTSeries α),
    RelSeries.head s = ⊥ → RelSeries.last s = ⊤ → ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
h₂ : ¬RelSeries.last s = ⊤
⊢ ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤

pp: α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
⊢ ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤

Tactic:
· obtain ⟨t, i, hi, ht⟩ := this (s.snoc ⊤ (lt_top_iff_ne_top.mpr h₂)) (by simp [h₁]) (by simp)
    exact ⟨t, ⟨fun j ↦ i (.cast (by simp) j.castSucc), fun _ _ ↦ by simp⟩,
      funext fun j ↦ (congr_fun hi _).trans (RelSeries.snoc_cast_castSucc _ _ _ _), ht⟩

Goal state after:
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
⊢ ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case hbc
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ p.toFun (Fin.last p.length) < ⊤

Tactic:
rw [RelSeries.last] at hlast

Goal state after:
case hbc
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : p.toFun (Fin.last p.length) = ↑x
i : Fin (p.length + 1)
⊢ p.toFun (Fin.last p.length) < ⊤
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(height ⊤) = ↑(⨆ a, height a) + 1

Tactic:
height_eq_iSup_lt_height

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(⨆ y, ⨆ (_ : y < ⊤), height y + 1) = ↑(⨆ a, height a) + 1
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝⁴¹ : CommSemiring R
inst✝⁴⁰ : CommSemiring R₂
inst✝³⁹ : CommSemiring R₃
inst✝³⁸ : Monoid R'
inst✝³⁷ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³⁶ : AddCommMonoid M
inst✝³⁵ : AddCommMonoid N
inst✝³⁴ : AddCommMonoid P
inst✝³³ : AddCommMonoid Q
inst✝³² : AddCommMonoid S
inst✝³¹ : AddCommMonoid P'
inst✝³⁰ : AddCommMonoid Q'
inst✝²⁹ : AddCommMonoid M₂
inst✝²⁸ : AddCommMonoid N₂
inst✝²⁷ : AddCommMonoid P₂
inst✝²⁶ : AddCommMonoid Q₂
inst✝²⁵ : AddCommMonoid M₃
inst✝²⁴ : AddCommMonoid N₃
inst✝²³ : AddCommMonoid P₃
inst✝²² : AddCommMonoid Q₃
inst✝²¹ : DistribMulAction R' M
inst✝²⁰ : Module R'' M
inst✝¹⁹ : Module R M
inst✝¹⁸ : Module R N
inst✝¹⁷ : Module R S
inst✝¹⁶ : Module R P'
inst✝¹⁵ : Module R Q'
inst✝¹⁴ : Module R₂ M₂
inst✝¹³ : Module R₂ N₂
inst✝¹² : Module R₂ P₂
inst✝¹¹ : Module R₂ Q₂
inst✝¹⁰ : Module R₃ M₃
inst✝⁹ : Module R₃ N₃
inst✝⁸ : Module R₃ P₃
inst✝⁷ : Module R₃ Q₃
inst✝⁶ : SMulCommClass R R' M
inst✝⁵ : SMulCommClass R R'' M
R'₂ : Type u_22
inst✝⁴ : Monoid R'₂
inst✝³ : DistribMulAction R'₂ M
inst✝² : SMulCommClass R R'₂ M
inst✝¹ : SMul R'₂ R'
inst✝ : IsScalarTower R'₂ R' M
s : R'₂
r : R'
x : M ⊗[R] N
m : M
n : N
⊢ (s • r) • m ⊗ₜ[R] n = s • r • m ⊗ₜ[R] n

Tactic:
rw [smul_tmul', smul_tmul', smul_tmul', smul_assoc]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
e : α ↪o β
this : ∀ (b : β), Subsingleton ↑(⇑e ⁻¹' {b})
⊢ krullDim α ≤ krullDim β

Tactic:
simpa using Order.krullDim_le_of_krullDim_preimage_le' e e.monotone fun _ ↦
    Order.krullDim_nonpos_of_subsingleton

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

Goal state before:
pp: α : Type u_1
inst✝ : IdemSemiring α
n : ℕ
nezero : 1 ≤ n
⊢ ↑n = 1

Tactic:
induction n, nezero using Nat.le_induction with
  | base => exact Nat.cast_one
  | succ x _ hx => rw [Nat.cast_add, hx, Nat.cast_one, add_idem 1]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : IsCoprime y z
a b : R
h1 : a * x + b * z = 1
c d : R
h2 : c * y + d * z = 1
⊢ 1 * (c * y + d * z) = 1

Tactic:
h2,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : IsCoprime y z
a b : R
h1 : a * x + b * z = 1
c d : R
h2 : c * y + d * z = 1
⊢ 1 * 1 = 1
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: case h
α : 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
⊢ val i ≤ val j ↔ ↑⋯.choose ≤ ↑⋯.choose

Tactic:
by_cases h_eq : val i = val j

Goal state after:
case pos
α : 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
h_eq : val i = val j
⊢ val i ≤ val j ↔ ↑⋯.choose ≤ ↑⋯.choose

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
h_eq : ¬val i = val j
⊢ val i ≤ val j ↔ ↑⋯.choose ≤ ↑⋯.choose
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case e'_3.e'_6
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 * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ μ x * ∏ j ∈ insert a t \ {x}, s j = (μ * fun x ↦ s a) x * ∏ j ∈ t \ {x}, s j

Tactic:
convert! (mul_assoc _ _ _).symm
          rw [prod_eq_prod_sdiff_singleton_mul (mem x hx), mul_comm, sdiff_sdiff_comm,
            sdiff_singleton_eq_erase a, erase_insert hat]

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

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

Tactic:
Submonoid.mem_map,

Goal state after:
R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x✝ : A
⊢ x✝ ∈ MonoidHom.mker (spanSingleton R) ↔ ∃ x ∈ IsUnit.submonoid R, (algebraMap R A) x = x✝
Module: Mathlib.Algebra.EuclideanDomain.Field

Goal state before:
pp: K : Type u_1
inst✝ : Field K
a b : K
⊢ b * (a / b) + (a - a * b / b) = a

Tactic:
by_cases h : b = 0 <;> simp [h, mul_div_cancel₀]

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

Goal state before:
pp: case mpr
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ (∃ x ∈ I, e x = y) → y ∈ map e I

Tactic:
rintro ⟨x, hx, rfl⟩
    exact mem_map_of_mem e hx

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : gcd x y = 0
⊢ y = 0

pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : ¬gcd x y = 0
⊢ y = 0

Tactic:
· rw [EuclideanDomain.gcd_eq_zero_iff] at hgxy
      exact hgxy.2

Goal state after:
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : ¬gcd x y = 0
⊢ y = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
r : R
I : Ideal R
f : R →+* S
⊢ map f (span {r}) * map f I = f r • map f I

Tactic:
Ideal.map_span,

Goal state after:
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
r : R
I : Ideal R
f : R →+* S
⊢ span (⇑f '' {r}) * map f I = f r • map f I
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case neg.refine_1.e_f
α : 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
x : α
hx : x ∈ s
⊢ x = s.gcd * f hx

Tactic:
← hf hx

Goal state after:
case neg.refine_1.e_f
α : 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
x : α
hx : x ∈ s
⊢ x = x
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case neg.refine_2.e_f
α : 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
x : α
hx : x ∈ s
⊢ x = s.gcd * f hx

Tactic:
← hf hx

Goal state after:
case neg.refine_2.e_f
α : 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
x : α
hx : x ∈ s
⊢ x = x
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
w x y z : R
inst✝ : (span {w, x}).IsTwoSided
⊢ span {w, x} * span {y, z} = span {w * y, w * z, x * y, x * z}

Tactic:
rw [span_mul_span']

Goal state after:
R : Type u
inst✝¹ : Semiring R
w x y z : R
inst✝ : (span {w, x}).IsTwoSided
⊢ span ({w, x} * {y, z}) = span {w * y, w * z, x * y, x * z}
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
x : R
inst✝ : (R ∙ x).IsPrincipal
⊢ Ideal.map f (Ideal.span {x}) = Submodule.span S (⇑f '' {x})

Tactic:
Ideal.map_span,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
x : R
inst✝ : (R ∙ x).IsPrincipal
⊢ Ideal.span (⇑f '' {x}) = Submodule.span S (⇑f '' {x})
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
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
⊢ d₁ ^ k ∣ a

Tactic:
apply (dvd_gcd_mul_of_dvd_mul h2).trans

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
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
⊢ gcd (d₁ ^ k) b * a ∣ a
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : CommSemiring R
inst✝¹ : Module R M
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
inst✝ : (ϕ.submoduleImage N).IsPrincipal
x : M
hx : x ∈ N
⊢ generator (ϕ.submoduleImage N) ∣ ϕ ⟨x, ⋯⟩

Tactic:
rw [← mem_iff_generator_dvd, LinearMap.mem_submoduleImage_of_le hNO]
  exact ⟨x, hx, rfl⟩

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

Goal state before:
pp: α : 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 : α
⊢ Associated ((if a = 0 then b else if b = 0 then a else Classical.choose ⋯) * lcm a b) (a * b)

Tactic:
by
      split_ifs with h h_1
      · rw [h, eq_zero_of_zero_dvd (dvd_lcm_left _ _), mul_zero, zero_mul]
      · rw [h_1, eq_zero_of_zero_dvd (dvd_lcm_right _ _)]
      rw [mul_comm, ← Classical.choose_spec (exists_gcd a b)]

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

Goal state before:
pp: case neg
l : Type u_1
m : Type u_2
α : Type v
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : ¬i = j
⊢ diagonal d (e i) (e j) = 0

Tactic:
diagonal_apply_ne _ (he.ne h)

Goal state after:
case neg
l : Type u_1
m : Type u_2
α : Type v
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : ¬i = j
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : κ → Finset ι := fun k ↦ (b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
v' : ↑(Φ ⁻¹' {s}) → M := fun k ↦ v ↑k
i' : LinearIndependent (ι := ↑(Φ ⁻¹' {s})) R v'
⊢ False

Tactic:
have w' : Finite (Φ ⁻¹' {s}) := by
    apply i'.finite_of_le_span_finite v' (s.image b)
    rintro m ⟨⟨p, ⟨rfl⟩⟩, rfl⟩
    simp only [SetLike.mem_coe, Finset.coe_image]
    apply Basis.mem_span_repr_support

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : κ → Finset ι := fun k ↦ (b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
v' : ↑(Φ ⁻¹' {s}) → M := fun k ↦ v ↑k
i' : LinearIndependent (ι := ↑(Φ ⁻¹' {s})) R v'
w' : Finite ↑(Φ ⁻¹' {s})
⊢ False
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 ⊆ ↑(f a) ∪ ↑(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

Tactic:
subset_union_prime' hp',

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 ∨ I ≤ f a ∨ ∃ i ∈ t, I ≤ f i
has : a ∈ insert a t
hbt : b ∉ t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i ∈ insert a t, I ≤ f i
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
ι : Type u_10
u : m → α
s : Finset ι
v : ι → m → α
⊢ u ⬝ᵥ ∑ i ∈ s, v i = ∑ i ∈ s, u ⬝ᵥ v i

Tactic:
simp only [dotProduct, Finset.sum_apply, Finset.mul_sum]

Goal state after:
m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
ι : Type u_10
u : m → α
s : Finset ι
v : ι → m → α
⊢ ∑ x, ∑ i ∈ s, u x * v i x = ∑ i ∈ s, ∑ i_1, u i_1 * v i i_1
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 ⊆ ↑(f b) ∪ ↑(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

Tactic:
subset_union_prime' hp',

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 ∨ I ≤ f b ∨ ∃ i ∈ t, I ≤ 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
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) ∪ ↑(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:
subset_union_prime' hp',

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 ≤ 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.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
v : ι → M
inst✝ : Fintype ι
f : ι →₀ ↥I
⊢ (finsuppTotal ι M I v) f = ∑ i, ↑(f i) • v i

Tactic:
rw [finsuppTotal_apply, Finsupp.sum_fintype]
  exact fun _ => zero_smul _ _

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
v : m → α
⊢ 1 *ᵥ v = v

Tactic:
by
  ext
  rw [← diagonal_one, mulVec_diagonal, one_mul]

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:
by
  simp [Matrix.mul_apply, map_sum]

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

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

Tactic:
apply le_antisymm
  · calc
      #(α →₀ β) ≤ #(Finset (α × β)) := mk_le_of_injective (Finsupp.graph_injective α β)
      _ = #(α × β) := mk_finset_of_infinite _
      _ = max (lift.{v} #α) (lift.{u} #β) := by
        rw [mk_prod, mul_eq_max_of_aleph0_le_left] <;> simp
  · apply max_le <;> rw [← lift_id #(α →₀ β), ← lift_umax]
    · obtain ⟨b, hb⟩ := exists_ne (0 : β)
      exact lift_mk_le.{v}.2 ⟨⟨_, Finsupp.single_left_injective hb⟩⟩
    · inhabit α
      exact lift_mk_le.{u}.2 ⟨⟨_, Finsupp.single_injective default⟩⟩

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 + f))

Tactic:
mapDomain_add,

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 (mapDomain g (single a n) + mapDomain g f)