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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t : M ⊗[R] N
m : M
⊢ ∀ (y : N), m ⊗ₜ[R] y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

Tactic:
n

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t : M ⊗[R] N
m : M
n : N
⊢ m ⊗ₜ[R] n ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: case a
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure S * closure T ≤ closure (S * T)

Tactic:
refine mul_le.2 fun a ha b hb => ?_

Goal state after:
case a
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
⊢ a * b ∈ closure (S * T)
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + z * y) y
⊢ IsCoprime x y

Tactic:
exact h.of_add_mul_right_left

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
⊢ comap (↑(opLinearEquiv R)) 1 = 1

Tactic:
comap_op_one

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ 1 = 1
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
y : A
x✝ : y ∈ J
⊢ 0 ∈ I

Tactic:
apply Submodule.zero_mem

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
| span (s ×ˢ t)

Tactic:
Ideal.ideal_prod_eq (Ideal.span (s ×ˢ t))

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
| (map (RingHom.fst R S) (span (s ×ˢ t))).prod (map (RingHom.snd R S) (span (s ×ˢ t)))
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
m : A
hm : m ∈ I
⊢ ∀ n ∈ 1 / I, m * n ∈ 1

Tactic:
n

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
m : A
hm : m ∈ I
n : A
⊢ n ∈ 1 / I → m * n ∈ 1
Module: Mathlib.Algebra.EuclideanDomain.Field

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

Tactic:
simp [h, mul_div_cancel₀]

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

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

Tactic:
simp [h, mul_div_cancel₀]

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b : R
hb : b ≠ 0
h : ¬a - a * b / b = 0
this : ¬(a - a * b / b) * b ≺ b
⊢ False

Tactic:
rw [sub_mul, mul_comm (_ / _), sub_eq_iff_eq_add'.2 (div_add_mod (a * b) b).symm] at this

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
a b : R
hb : b ≠ 0
h : ¬a - a * b / b = 0
this : ¬a * b % b ≺ b
⊢ False
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : a ∣ b
⊢ gcd a b = a

Tactic:
gcd_val,

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : a ∣ b
⊢ gcd (b % a) a = a
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
this : P a b (gcd a b, xgcd a b)
⊢ gcd a b = a * gcdA a b + b * gcdB a b

Tactic:
xgcd_val

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
this : P a b (gcd a b, gcdA a b, gcdB a b)
⊢ gcd a b = a * gcdA a b + b * gcdB a b
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ (x - z * y) / y = x / y - z

Tactic:
by
  rw [mul_comm z y]
  exact sub_mul_div_left _ _ _ h1 h2

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ n ∈ span R s, r • n = 0
⊢ ∀ (n : ↑s), r • ↑n = 0

Tactic:
n

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ n ∈ span R s, r • n = 0
n : ↑s
⊢ r • ↑n = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ (∀ n ∈ span R s, r • n = 0) → ∀ (n : ↑s), r • ↑n = 0

pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ (∀ (n : ↑s), r • ↑n = 0) → ∀ n ∈ span R s, r • n = 0

Tactic:
· intro h n
    exact h _ (Submodule.subset_span n.prop)

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ (∀ (n : ↑s), r • ↑n = 0) → ∀ n ∈ span R s, r • n = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
⊢ ∀ n ∈ span R s, r • n = 0

Tactic:
n

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
⊢ n ∈ span R s → r • n = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ x ∈ s, r • x = 0

pp: case mpr.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ r • 0 = 0

pp: case mpr.refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (x y : M), x ∈ span R s → y ∈ span R s → r • x = 0 → r • y = 0 → r • (x + y) = 0

pp: case mpr.refine_4
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (a : R), ∀ x ∈ span R s, r • x = 0 → r • a • x = 0

Tactic:
· intro x hx
      exact h ⟨x, hx⟩

Goal state after:
case mpr.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ r • 0 = 0

case mpr.refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (x y : M), x ∈ span R s → y ∈ span R s → r • x = 0 → r • y = 0 → r • (x + y) = 0

case mpr.refine_4
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (a : R), ∀ x ∈ span R s, r • x = 0 → r • a • x = 0
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: a b : ℕ
⊢ Associated (a.gcd b * a.lcm b) (a * b)

Tactic:
rw [Nat.gcd_mul_lcm]; rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
⊢ map f (sInf {J | I ≤ J ∧ J.IsPrime}) = sInf {J | map f I ≤ J ∧ J.IsPrime}

Tactic:
convert! map_sInf hf this

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
⊢ {J | map f I ≤ J ∧ J.IsPrime} = map f '' {J | I ≤ J ∧ J.IsPrime}
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
i : ι
x : (i : ι) → R i
hx : x i = 0
⊢ x ∈ Ideal.span {1 - Pi.single i 1}

Tactic:
rw [Ideal.mem_span_singleton]

Goal state after:
ι : Type u_1
inst✝¹ : DecidableEq ι
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
i : ι
x : (i : ι) → R i
hx : x i = 0
⊢ 1 - Pi.single i 1 ∣ x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
h : f = 0
⊢ IsUnit (f.prod * ↑u)

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : z ∈ S
⊢ 1 ∈ T

Tactic:
obtain ⟨y, hy⟩ := (mem_iff_generator_dvd _).1 h

Goal state after:
case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : z ∈ S
y : R
hy : z = generator S * y
⊢ 1 ∈ T
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
p n : R
hp : Irreducible p
⊢ IsRelPrime p n ↔ ¬p ∣ n

Tactic:
hp.isRelPrime_iff_not_dvd

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
p n : R
hp : Irreducible p
⊢ ¬p ∣ n ↔ ¬p ∣ n
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
x y : R
⊢ Ideal.span {gcd x y} = Ideal.span {x, y}

Tactic:
by
  rw [← IsBezout.span_gcd, IsBezout.span_gcd_eq_span_gcd]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M N : Matrix m n α
h : M = N
⊢ ∀ (i : m) (j : n), M i j = N i j

Tactic:
by simp [h]

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

Goal state before:
pp: case inr
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✝ : Infinite ↑J
⊢ #↑(range ⇑v) ≤ #↑J

Tactic:
· let S : J → Set ι := fun j => ↑(v.repr j).support
    let S' : J → Set M := fun j => v '' S j
    have hs : range v ⊆ ⋃ j, S' j := by
      intro b hb
      rcases mem_range.1 hb with ⟨i, hi⟩
      have : span R J ≤ comap v.repr.toLinearMap (Finsupp.supported R R (⋃ j, S j)) :=
        span_le.2 fun j hj x hx => ⟨_, ⟨⟨j, hj⟩, rfl⟩, hx⟩
      rw [hJ] at this
      replace : v.repr (v i) ∈ Finsupp.supported R R (⋃ j, S j) := this trivial
      rw [v.repr_self, Finsupp.mem_supported, Finsupp.support_single _ one_ne_zero] at this
      · subst b
        rcases mem_iUnion.1 (this (Finset.mem_singleton_self _)) with ⟨j, hj⟩
        exact mem_iUnion.2 ⟨j, (mem_image _ _ _).2 ⟨i, hj, rfl⟩⟩
    refine le_of_not_gt fun IJ => ?_
    suffices #(⋃ j, S' j) < #(range v) by exact not_le_of_gt this ⟨Set.embeddingOfSubset _ _ hs⟩
    refine lt_of_le_of_lt (le_trans Cardinal.mk_iUnion_le_sum_mk
      (Cardinal.sum_le_sum _ (fun _ => ℵ₀) ?_)) ?_
    · exact fun j => (Cardinal.lt_aleph0_of_finite _).le
    · simpa

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

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

Tactic:
by
  simp [diagonal, h]

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

Goal state before:
pp: case intro
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
ι : Type w
h : Basis ι R M
val✝ : Fintype ι
⊢ ↑(finrank R M) = ↑(Fintype.card ι)

Tactic:
finrank_eq_card_basis h

Goal state after:
case intro
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
ι : Type w
h : Basis ι R M
val✝ : Fintype ι
⊢ ↑(Fintype.card ι) = ↑(Fintype.card ι)
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
⊢ u ⬝ᵥ (v + w) = u ⬝ᵥ v + u ⬝ᵥ w

Tactic:
simp [dotProduct, mul_add, Finset.sum_add_distrib]

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : Mul α
inst✝¹ : Zero α
inst✝ : NoZeroDivisors α
a b : n → α
ha✝ : a ≠ 0
hb : b ≠ 0
h : vecMulVec a b = 0
i : n
ha : a i ≠ 0 i
⊢ False

Tactic:
obtain ⟨j, hb⟩ := Function.ne_iff.mp hb

Goal state after:
n : Type u_3
α : Type v
inst✝² : Mul α
inst✝¹ : Zero α
inst✝ : NoZeroDivisors α
a b : n → α
ha✝ : a ≠ 0
hb✝ : b ≠ 0
h : vecMulVec a b = 0
i : n
ha : a i ≠ 0 i
j : n
hb : b j ≠ 0 j
⊢ False
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
x : l → α
y : m → α
M : Matrix m n α
i✝ : l
j✝ : n
⊢ ∑ j, x i✝ * y j * M j j✝ = x i✝ * ∑ x, y x * M x j✝

Tactic:
Finset.mul_sum,

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
x : l → α
y : m → α
M : Matrix m n α
i✝ : l
j✝ : n
⊢ ∑ j, x i✝ * y j * M j j✝ = ∑ i, x i✝ * (y i * M i j✝)
Module: Mathlib.Data.Matrix.Mul

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

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

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

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

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

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

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

Tactic:
n

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : CommMonoid α
f : α →₀ ℕ
a : α
⊢ ∀ (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 →
        ((toMultiset f).prod = f.prod fun a n ↦ a ^ n) →
          (toMultiset (single a b + f)).prod = (single a b + f).prod fun a n ↦ a ^ n

Tactic:
n

Goal state after:
case refine_2
α : Type u_1
inst✝ : CommMonoid α
f : α →₀ ℕ
a : α
n : ℕ
⊢ ∀ (f : α →₀ ℕ),
    a ∉ f.support →
      n ≠ 0 →
        ((toMultiset f).prod = f.prod fun a n ↦ a ^ n) →
          (toMultiset (single a n + f)).prod = (single a n + f).prod fun a n ↦ a ^ n
Module: Mathlib.Data.Finsupp.Multiset

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

Tactic:
n

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
n : ℕ
⊢ ∀ (f : α →₀ ℕ),
    a ∉ f.support →
      n ≠ 0 → (toMultiset f).toFinset = f.support → (toMultiset (single a n + f)).toFinset = (single a n + f).support
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
P : α → ℕ
hP : ∑ i, P i = n
⊢ Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P) = (Multiset.map (fun a ↦ ↑⟨P, hP⟩ a • {a}) univ.val).sum

Tactic:
ext a

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
P : α → ℕ
hP : ∑ i, P i = n
a : α
⊢ Multiset.count a (Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P)) =
    Multiset.count a (Multiset.map (fun a ↦ ↑⟨P, hP⟩ a • {a}) univ.val).sum
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case a.cons.cons.inr
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : A
tl : List A
ih : (∀ y ∈ tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = tl.prod
HL : hd ∈ Set.range ⇑(algebraMap R A) ∪ s ∧ ∀ x ∈ tl, x ∈ Set.range ⇑(algebraMap R A) ∪ s
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = tl.prod
hs : hd ∈ s
⊢ ∃ z_1 r_1, ∃ (_ : r_1 ∈ Submonoid.closure s), z_1 • r_1 = hd * z • r

Tactic:
· exact
        ⟨z, hd * r, Submonoid.mul_mem _ (Submonoid.subset_closure hs) hr,
          (mul_smul_comm _ _ _).symm⟩

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

Goal state before:
pp: case inr.inl
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ j₂ : J
hj : j₁ ≠ j₂
⊢ diagonal (fun j ↦ d i₁ j) j₁ j₂ = diagonal (fun ij ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₂)

Tactic:
diagonal_apply_ne _ hj,

Goal state after:
case inr.inl
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ j₂ : J
hj : j₁ ≠ j₂
⊢ 0 = diagonal (fun ij ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₂)
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
⊢ (comp I I J J R) (diagonal fun i ↦ diagonal fun j ↦ d i j) = diagonal fun ij ↦ d ij.1 ij.2

Tactic:
by
  ext ⟨i₁, j₁⟩ ⟨i₂, j₂⟩
  dsimp [comp_apply]
  obtain hi | rfl := ne_or_eq i₁ i₂
  · rw [diagonal_apply_ne _ hi, diagonal_apply_ne _ (ne_of_apply_ne Prod.fst hi),
      Matrix.zero_apply]
  rw [diagonal_apply_eq]
  obtain hj | rfl := ne_or_eq j₁ j₂
  · rw [diagonal_apply_ne _ hj, diagonal_apply_ne _ (ne_of_apply_ne Prod.snd hj)]
  rw [diagonal_apply_eq, diagonal_apply_eq]

Goal state after:
Module: Mathlib.Algebra.Field.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
q : ℚ
⊢ unop ↑q = unop (↑q.num / ↑q.den)

Tactic:
rw [unop_ratCast, Rat.cast_def, unop_div, unop_natCast,
    unop_intCast, div_eq_mul_inv]

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

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y z : R
⊢ SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z

Tactic:
SemiconjBy,

Goal state after:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y z : R
⊢ star x * star z = star y * star x ↔ x * y = z * x
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: case refine_1
R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
h : Commute x y
⊢ star y * x = x * y

Tactic:
hy.star_eq,

Goal state after:
case refine_1
R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
h : Commute x y
⊢ y * x = x * y
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ Commute x y ↔ IsSelfAdjoint (x * y)

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [isSelfAdjoint_iff, star_mul, hx.star_eq, hy.star_eq, h.eq]
  · simpa only [star_mul, hx.star_eq, hy.star_eq] using! h.symm

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : Star R
inst✝² : Star α
inst✝¹ : SMul R α
inst✝ : SMul Rᵐᵒᵖ α
c : R
M : Matrix m n α
h : ∀ (r : R) (a : α), star (r • a) = MulOpposite.op (star r) • star a
⊢ ∀ (i : n) (j : m), (c • M)ᴴ i j = (MulOpposite.op (star c) • Mᴴ) i j

Tactic:
by simp [h]

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

Goal state before:
pp: case inl.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
hji : j ≠ i
⊢ (diagonal v).updateCol i (Pi.single i x) j j = Function.update v i x j

Tactic:
· rw [updateCol_ne hji, diagonal_apply_eq, Function.update_of_ne hji]

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

Goal state before:
pp: R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ ∑ j, A (↑i) j * B j ↑k = ∑ j, A ↑i ↑j * B ↑j ↑k

Tactic:
Finset.sum_subtype

Goal state after:
R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ ∑ a, A ↑i ↑a * B ↑a ↑k = ∑ j, A ↑i ↑j * B ↑j ↑k

case h
R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ ∀ (x : n), x ∈ Finset.univ ↔ ?m.38 x

R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ n → Prop

R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ Fintype (Subtype ?m.38)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_14
inst✝¹ : Zero R
inst✝ : DecidableEq m
d : m → Matrix n n R
⊢ (comp m m n n R) (diagonal d) = (reindex (Equiv.prodComm n m) (Equiv.prodComm n m)) (blockDiagonal d)

Tactic:
ext
  simp [diagonal, blockDiagonal, Matrix.ite_apply]

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

Goal state before:
pp: α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i : m'
row : Fin m → m'
col : o' → n'
⊢ A.submatrix (vecCons i row) col = vecCons (fun j ↦ A i (col j)) (A.submatrix row col)

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

Goal state after: