mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : SMulCommClass R' R'₂ M
r' : R'
r'₂ : R'₂
x : M ⊗[R] N
⊢ r' • r'₂ • 0 = r'₂ • r' • 0

Tactic:
simp_rw [TensorProduct.smul_zero]

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: case refine_2
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
⊢ m • 0 ∈ M • N ⊔ M • P

Tactic:
apply (smul_zero (A := A) m).symm ▸ (M • N ⊔ M • P).zero_mem

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
⊢ 1 * a = a

Tactic:
ext x
    simp only [mem_mul, mem_one, smul_mul_assoc, exists_exists_eq_and, one_mul]
    refine ⟨?_, fun hx => ⟨1, x, hx, one_smul _ _⟩⟩
    rintro ⟨r, y, hy, rfl⟩
    exact smul_mem _ _ hy

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹² : KleeneAlgebra α
inst✝¹¹ : LE β
inst✝¹⁰ : LT β
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Max β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a : β
⊢ f a * (f a)∗ ≤ (f a)∗

Tactic:
exact mul_kstar_le_kstar

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

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Group G
inst✝² : MulAction G R
inst✝¹ : SMulCommClass G R R
inst✝ : IsScalarTower G R R
x : G
y z : R
x✝ : IsCoprime y z
a b : R
h : a * y + b * z = 1
⊢ x⁻¹ • a * x • y + b * z = 1

Tactic:
smul_mul_smul_comm,

Goal state after:
R : Type u_1
G : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Group G
inst✝² : MulAction G R
inst✝¹ : SMulCommClass G R R
inst✝ : IsScalarTower G R R
x : G
y z : R
x✝ : IsCoprime y z
a b : R
h : a * y + b * z = 1
⊢ (x⁻¹ * x) • (a * y) + b * z = 1
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case mpr
m n : ℤ
⊢ ↑(m.gcd n) = ↑1 → ∃ a b, a * m + b * n = 1

Tactic:
Int.gcd_eq_gcd_ab,

Goal state after:
case mpr
m n : ℤ
⊢ m * m.gcdA n + n * m.gcdB n = ↑1 → ∃ a b, a * m + b * n = 1
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
⊢ ∀ r ∈ ⊥, ∀ n ∈ N, r • n ∈ ⊥

Tactic:
rintro _ rfl _ _

Goal state after:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
n✝ : M
a✝ : n✝ ∈ N
⊢ 0 • 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
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
⊢ ⨆ i, map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N) = map f.toLinearMap M * map f.toLinearMap N

Tactic:
by
      rw [mul_eq_map₂]
      apply congr_arg sSup
      ext S
      constructor <;> rintro ⟨y, hy⟩
      · use ⟨f y, mem_map.mpr ⟨y.1, y.2, rfl⟩⟩
        refine Eq.trans ?_ hy
        ext
        simp
      · obtain ⟨y', hy', fy_eq⟩ := mem_map.mp y.2
        use ⟨y', hy'⟩
        refine Eq.trans ?_ hy
        rw [f.toLinearMap_apply] at fy_eq
        ext
        simp [fy_eq]

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' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
this : (LinearMap.toSpanSingleton R M x).range ≤ M'
⊢ x ∈ M'

Tactic:
← LinearMap.toSpanSingleton_apply_one R M x

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
this : (LinearMap.toSpanSingleton R M x).range ≤ M'
⊢ (LinearMap.toSpanSingleton R M x) 1 ∈ M'
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b : R
hb : b ≠ 0
hab : b ∣ a
⊢ b * (a / b) = a

Tactic:
← mul_div_assoc _ hab,

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
a b : R
hb : b ≠ 0
hab : b ∣ a
⊢ b * a / b = a
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: S : Type v
F : Type u_1
inst✝³ : CommSemiring S
R : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I J : Ideal R
⊢ ⇑f '' ↑I * ⇑f '' ↑J ⊆ ↑(map f (I * J))

Tactic:
rintro _ ⟨_, ⟨r, hri, rfl⟩, _, ⟨s, hsj, rfl⟩, rfl⟩

Goal state after:
S : Type v
F : Type u_1
inst✝³ : CommSemiring S
R : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I J : Ideal R
r : R
hri : r ∈ ↑I
s : R
hsj : s ∈ ↑J
⊢ (fun x1 x2 ↦ x1 * x2) (f r) (f s) ∈ ↑(map f (I * J))
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
r s : R
inst✝ : (span {r}).IsTwoSided
⊢ span {r} * span {s} = span {r * s}

Tactic:
rw [span_mul_span', Set.singleton_mul_singleton]

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
r : R
⊢ (∀ (a : M) (b : a ∈ N), r • ⟨a, b⟩ = 0) ↔ ∀ n ∈ N, r • n = 0

Tactic:
Subtype.ext_iff

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
r : R
⊢ (∀ (a : M) (b : a ∈ N), ↑(r • ⟨a, b⟩) = ↑0) ↔ ∀ n ∈ N, r • n = 0
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: a b : ℤ
⊢ Associated a b ↔ a = b ∨ a = -b

Tactic:
Int.associated_iff_natAbs

Goal state after:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a = b ∨ a = -b
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : Ring A
inst✝ : Ring B
f : A →+* B
surj : Function.Surjective ⇑f
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
x' : A
hx : f x' ∈ I
hx' : f x' = x
⊢ ∃ y ∈ J, f y = x

Tactic:
← Ideal.mem_comap,

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : Ring A
inst✝ : Ring B
f : A →+* B
surj : Function.Surjective ⇑f
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
x' : A
hx : x' ∈ comap f I
hx' : f x' = x
⊢ ∃ y ∈ J, f y = x
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
surj : Function.Surjective ⇑f
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
⊢ I = map f J

Tactic:
refine le_antisymm (fun x hx ↦ ?_)
    (Ideal.map_le_iff_le_comap.mpr (le_of_le_of_eq le_sup_right eq.symm))

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
surj : Function.Surjective ⇑f
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
hx : x ∈ I
⊢ x ∈ map f J
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s✝ : Multiset (Ideal R)
P : Ideal R
hp : P.IsPrime
I : Ideal R
s : Multiset (Ideal R)
ih : s.prod ≤ P ↔ ∃ I ∈ s, I ≤ P
⊢ (I ::ₘ s).prod ≤ P ↔ ∃ I_1 ∈ I ::ₘ s, I_1 ≤ P

Tactic:
by simp [hp.mul_le, ih]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
g₁ g₂ : GCDMonoid α
a b : α
⊢ gcd a b = gcd a b

Tactic:
refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_) <;>
      apply_rules +allowSynthFailures [dvd_gcd, gcd_dvd_left, gcd_dvd_right]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
a b : α
a0 : ¬a = 0
⊢ Associated (gcd a b * Classical.choose ⋯) (a * b)

Tactic:
rw [← Classical.choose_spec ((gcd_dvd_left a b).trans (Dvd.intro b rfl))]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
a b c : R
hab : IsCoprime a b
k : ℕ
h : Associated (c ^ k) (a * b)
⊢ ∃ d, Associated (d ^ k) a

Tactic:
obtain ⟨u, hu⟩ := h.symm
  exact exists_associated_pow_of_mul_eq_pow'
    ((isCoprime_mul_unit_right_right u.isUnit a b).mpr hab) <| mul_assoc a _ _ ▸ hu

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

Goal state before:
pp: α : Type u_1
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a b : G₀
⊢ Associated ((if a = 0 ∧ b = 0 then 0 else 1) * if a = 0 ∨ b = 0 then 0 else 1) (a * b)

Tactic:
by
    split_ifs <;> simp_all [Associated.comm]

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
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
Hi : ¬I ≤ f i
this : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i
r : R
hri : r ∉ ↑(f i)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ¬↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
exfalso

Goal state after:
case neg
ι : 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
Hi : ¬I ≤ f i
this : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i
r : R
hri : r ∉ ↑(f i)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ¬↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
⊢ False
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 : Finset ι
h : Basis (↥b) R M
⊢ finrank R M = b.card

Tactic:
by rw [finrank_eq_card_basis h, Fintype.card_coe]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
⊢ (v ⬝ᵥ fun j ↦ diagonal w j i) = v i * w i

Tactic:
have : ∀ j ≠ i, v j * diagonal w j i = 0 := fun j hij => by
    simp [diagonal_apply_ne _ hij]

Goal state after:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w j i = 0
⊢ (v ⬝ᵥ fun j ↦ diagonal w j i) = v i * w 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✝² : AddCommMonoid α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : m → n → α
i : m
j : n
⊢ (∑ i, ∑ j, single i j (x i j)) i j = of x i j

Tactic:
rw [← Fintype.sum_prod_type']

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : m → n → α
i : m
j : n
⊢ (∑ x_1, single x_1.1 x_1.2 (x x_1.1 x_1.2)) i j = of x i j
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ v ⬝ᵥ A *ᵥ w = v ᵥ* A ⬝ᵥ w

Tactic:
simp only [dotProduct, vecMul, mulVec, Finset.mul_sum, Finset.sum_mul, mul_assoc]

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ ∑ x, ∑ i, v x * (A x i * w i) = ∑ x, ∑ x_1, v x_1 * (A x_1 x * w x)
Module: Mathlib.Data.Matrix.Mul

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

Tactic:
by
  rw [vecMul_neg, neg_vecMul, neg_neg]

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : (toMultiset f).toFinset = f.support
⊢ (toMultiset (single a n) + toMultiset f).toFinset = (single a n + f).support

Tactic:
Multiset.toFinset_add,

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : (toMultiset f).toFinset = f.support
⊢ (toMultiset (single a n)).toFinset ∪ (toMultiset f).toFinset = (single a n + f).support
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ { ringCon := I.ringCon ⊓ J.ringCon } ≤ I

Tactic:
rw [ringCon_le_iff]; exact inf_le_left

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 : κ
⊢ ((lequivCongrLeft R e) ((lof R ι M (e.symm k)) x)) j = ((lof R κ (fun i ↦ M (e.symm i)) k) (cast ⋯ x)) j

Tactic:
simp [lof_eq_of, of_apply]

Goal state after:
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
Module: Mathlib.LinearAlgebra.TensorProduct.Associator

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
A : Type u_11
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
h : Function.Surjective ⇑(algebraMap R A)
a : A
m : M
n : N
⊢ (a • m) ⊗ₜ[R] n = m ⊗ₜ[R] (a • n)

Tactic:
obtain ⟨r, rfl⟩ := h a
    simp [smul_tmul]

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
S : Subalgebra R A
s : Set A
hS : S = adjoin R s
φ₁ φ₂ : ↥S →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
⊢ φ₁ = φ₂

Tactic:
subst hS; exact adjoin_ext h

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
m : M
n : N
⊢ (equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ[R] n) = Finsupp.mapRange (fun x ↦ x • m) ⋯ (𝒞.repr n)

Tactic:
ext; simp [equivFinsuppOfBasisRight]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
⊢ ↑(equivFinsuppOfBasisRight 𝒞).symm = (Finsupp.lsum R) fun i ↦ (mk R M N).flip (𝒞 i)

Tactic:
ext; simp [equivFinsuppOfBasisRight]

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := ⋯
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ⇑(linearCombination R id) ⇑s
⊢ f ∘ₗ φ ∘ₗ s = g

Tactic:
ext p

Goal state after:
case h
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun p ↦ Function.surjInv hf (g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ⇑(linearCombination R id) ⇑s
p : P
⊢ (f ∘ₗ φ ∘ₗ s) p = g p
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
⊢ ↑((selfAdjointPart R) x) + ↑((skewAdjointPart R) x) = x

Tactic:
simp only [smul_sub, selfAdjointPart_apply_coe, smul_add, skewAdjointPart_apply_coe,
    add_add_sub_cancel, invOf_two_smul_add_invOf_two_smul]

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

Goal state before:
pp: α : Type u
m : ℕ
n' : Type uₙ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
⊢ vecMulVec (vecCons x v) w = vecCons (x • w) (vecMulVec v w)

Tactic:
by
  ext i
  refine Fin.cases ?_ ?_ i <;> simp [vecMulVec]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f₁ f₂ : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (f₁ x✝¹ + f₂ x✝¹) ⊗ₜ[R] g x✝ = f₁ x✝¹ ⊗ₜ[R] g x✝ + f₂ x✝¹ ⊗ₜ[R] g x✝

Tactic:
add_tmul

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case neg.intro.refine_1.refine_1
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c✝ : ι → R
hc✝ : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c✝ i
val✝ : Fintype ι
y' : O := ∑ i, c✝ i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c✝ i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
c : R
z : O
zN' : z ∈ N'
hc : c • y + z = 0
⊢ c • a • y' + z = 0

Tactic:
rwa [← a_smul_y'] at hc

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

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂
sd : ↥S
hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)
⊢ ∃ u v, u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧ ↑u * ↑⟨sb * ↑s₁, h⟩ = v * ↑(sa * s₁)

Tactic:
use sd * sc

Goal state after:
case h
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂
sd : ↥S
hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)
⊢ ∃ v, (sd * sc) • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧ ↑(sd * sc) * ↑⟨sb * ↑s₁, h⟩ = v * ↑(sa * s₁)
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • (r₂, s₂).fst = rb • (r₁, s₁).fst
hb' : ↑sb * ↑(r₂, s₂).snd = rb * ↑(r₁, s₁).snd
r₃ : X
s₃ : ↥S
⊢ add' (r₁, s₁).fst (r₁, s₁).snd (r₃ /ₒ s₃) = add' (r₂, s₂).fst (r₂, s₂).snd (r₃ /ₒ s₃)

Tactic:
| _ r₃ s₃
       => 

Goal state after:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • (r₂, s₂).fst = rb • (r₁, s₁).fst
hb' : ↑sb * ↑(r₂, s₂).snd = rb * ↑(r₁, s₁).snd
r₃ : X
s₃ : ↥S
⊢ add' (r₁, s₁).fst (r₁, s₁).snd (r₃ /ₒ s₃) = add' (r₂, s₂).fst (r₂, s₂).snd (r₃ /ₒ s₃)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
⊢ (toMatrix v₁ v₁) id = 1

Tactic:
ext i j
  simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm]

Goal state after: