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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Surjective ⇑f
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
Q : (α → R) ≃ₗ[R] α →₀ R := (Finsupp.linearEquivFunOnFinite R R α).symm
⊢ Fintype.card β ≤ Fintype.card α

Tactic:
exact card_le_of_surjective R (P.toLinearMap ∘ₗ f ∘ₗ Q) (P.surjective.comp (i.comp Q.surjective))

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
x y z : R
inst✝ : IsPrincipal (Ideal.span {x, y})
hx : z ∣ x
hy : z ∣ y
⊢ z ∣ gcd x y

Tactic:
by
  rw [← Ideal.span_singleton_le_span_singleton] at hx hy ⊢
  rw [span_gcd, Ideal.span_insert, sup_le_iff]
  exact ⟨hx, hy⟩

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommRing R
x y z : R
inst✝² : IsPrincipal (Ideal.span {x, y})
inst✝¹ : IsBezout R
inst✝ : IsCancelMulZero R
⊢ IsGCDMonoid R

Tactic:
exact ⟨toGCDDomain R⟩

Goal state after:
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:
simpa using congr_arg (fun m : Matrix n n α => m i i) h

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n
inst✝ : AddMonoidWithOne α
⊢ (diagonal fun x ↦ ↑0) = 0

Tactic:
rw [Nat.cast_zero, diagonal_zero]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
a b : Ideal R
hp : ∀ I ∈ S, I ≠ a → I ≠ b → I.IsPrime
ha : a ≠ ⊤
hb : b ≠ ⊤
x✝ : ∃ i ∈ S, M ≤ i
I : Ideal R
mem : I ∈ S
le : M ≤ I
⊢ I ≠ ⊤

Tactic:
simp_rw [← or_iff_not_imp_left] at hp

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
a b : Ideal R
ha : a ≠ ⊤
hb : b ≠ ⊤
x✝ : ∃ i ∈ S, M ≤ i
I : Ideal R
mem : I ∈ S
le : M ≤ I
hp : ∀ I ∈ S, I = a ∨ I = b ∨ I.IsPrime
⊢ I ≠ ⊤
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
I J : Ideal R
hs : ∀ (z : ↑s), ∃ m a b, ∃ (_ : a ∈ I) (_ : b ∈ J), a + b = ↑z ^ m
⊢ ∃ t, Set.range t ⊆ ↑I ∧ s ⊆ ↑(span (Set.range t) ⊔ J).radical

Tactic:
choose m a b ha hb heq using hs

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
I J : Ideal R
m : ↑s → ℕ
a b : ↑s → R
ha : ∀ (z : ↑s), a z ∈ I
hb : ∀ (z : ↑s), b z ∈ J
heq : ∀ (z : ↑s), a z + b z = ↑z ^ m z
⊢ ∃ t, Set.range t ⊆ ↑I ∧ s ⊆ ↑(span (Set.range t) ⊔ J).radical
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
⊢ IsRightRegular A ↔ Function.Injective fun v ↦ v ᵥ* A

Tactic:
by
  cases isEmpty_or_nonempty m
  · simp [IsRightRegular, Function.injective_of_subsingleton]
  exact mul_left_injective_iff_vecMul_injective

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

Goal state before:
pp: case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift.{u, v} #β
⊢ lift.{u, v} #β ^ Fintype.card α = lift.{u, v} #β

pp: α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift.{u, v} #β
⊢ lift.{v, u} #α ≤ ℵ₀

Tactic:
power_nat_eq this

Goal state after:
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift.{u, v} #β
⊢ lift.{u, v} #β = lift.{u, v} #β

case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift.{u, v} #β
⊢ 1 ≤ Fintype.card α

α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift.{u, v} #β
⊢ lift.{v, u} #α ≤ ℵ₀
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:
intro a n f _ _ ih

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 + f)) = toMultiset (mapDomain g (single a n + f))
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)) + Multiset.map g (toMultiset f) = toMultiset (mapDomain g (single a n + f))

Tactic:
ih,

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 + 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:
intro a n f _ _ ih

Goal state after:
case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : (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✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : (toMultiset f).prod = f.prod fun a n ↦ a ^ n
⊢ (toMultiset (single a n)).prod * (toMultiset f).prod = (single a n + f).prod fun a n ↦ a ^ n

Tactic:
ih,

Goal state after:
case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : (toMultiset f).prod = f.prod fun a n ↦ a ^ n
⊢ ((toMultiset (single a n)).prod * f.prod fun a n ↦ a ^ n) = (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✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : (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

Tactic:
rw [toMultiset_add, Multiset.prod_add, ih, toMultiset_single, Multiset.prod_nsmul,
      Finsupp.prod_add_index' pow_zero pow_add, Finsupp.prod_single_index, Multiset.prod_singleton]

Goal state after:
case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : (toMultiset f).prod = f.prod fun a n ↦ a ^ n
⊢ a ^ 0 = 1
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)).toFinset ∪ (toMultiset f).toFinset = (single a n + f).support

Tactic:
ih,

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 ∪ f.support = (single a n + f).support
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq ι
f g : ι →₀ ℕ
⊢ Multiset.toFinsupp.symm.toEquiv f ≤ Multiset.toFinsupp.symm.toEquiv g ↔ f ≤ g

Tactic:
simp [le_def, Multiset.le_iff_count]

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

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

Tactic:
rw [mem_iff]

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

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

Tactic:
rw [mem_iff]

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

Goal state before:
pp: ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
i : ι
f : γ →+ β i
x : γ
⊢ (⇑(of β i) ∘ ⇑f) x = (of β i) (f x)

Tactic:
Function.comp

Goal state after:
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
i : ι
f : γ →+ β i
x : γ
⊢ (of β i) (f x) = (of β i) (f x)
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: case inr
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
h : j ≠ i
⊢ ↑0 = ↑0

Tactic:
ZeroMemClass.coe_zero,

Goal state after:
case inr
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
h : j ≠ i
⊢ 0 = ↑0
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
⊢ ↑(iSup K) ⊆ ⋃ i, ↑(K i)

Tactic:
rw [coe_iSup_of_directed dir]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_11
inst✝¹ : Semiring S
inst✝ : Algebra R S
m : R ⊗[R] M
⊢ 1 ⊗ₜ[R] (TensorProduct.lid R M) m = (LinearMap.rTensor M (Algebra.algHom R R S).toLinearMap) m

Tactic:
suffices ∀ m, (LinearMap.rTensor M (Algebra.algHom R R S).toLinearMap).comp
    (TensorProduct.lid R M).symm.toLinearMap m = 1 ⊗ₜ[R] m by
    simp [← this]
  intros; simp

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

Goal state before:
pp: case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ ⇑f '' ⇑f ⁻¹' {0} ⊆ ↑(map f S)

Tactic:
exact (Set.image_preimage_subset f {0}).trans (Set.singleton_subset_iff.2 (S.map f).zero_mem)

Goal state after:
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
i : ι × κ
r : R
⊢ (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) = Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 1

Tactic:
nth_rw 1 [← mul_one r]
  exact finsuppTensorFinsupp'_symm_single_mul R ι κ i _ _

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

Goal state before:
pp: R : Type u
inst✝¹ : CommGroupWithZero R
inst✝ : StarMul R
x y : R
⊢ star (x / y) = star x / star y

Tactic:
by
  apply op_injective
  rw [division_def, op_div, mul_comm, star_mul, star_inv₀, op_mul, op_inv]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
a b : R
hab : Commute a (star b)
ha : IsStarNormal a
hb : IsStarNormal b
⊢ IsStarNormal (a + b)

Tactic:
isStarNormal_iff

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
⊢ Commute (star (a + b)) (a + b)
Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
v : n → α
⊢ (diagonal v)ᴴ = diagonal (star v)

Tactic:
conjTranspose,

Goal state after:
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
v : n → α
⊢ (diagonal v)ᵀ.map star = diagonal (star v)
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Star α
⊢ Mᴴ.updateRow j (star c) = (M.updateCol j c)ᴴ

Tactic:
conjTranspose,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Star α
⊢ (Mᵀ.map star).updateRow j (star c) = (M.updateCol j c)ᴴ
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Star α
⊢ (Mᵀ.map star).updateRow j (star c) = (M.updateCol j c)ᴴ

Tactic:
conjTranspose,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Star α
⊢ (Mᵀ.map star).updateRow j (star c) = (M.updateCol j c)ᵀ.map star
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝¹ : DecidableEq m
inst✝ : Star α
⊢ Mᴴ.updateCol i (star b) = (M.updateRow i b)ᴴ

Tactic:
conjTranspose,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝¹ : DecidableEq m
inst✝ : Star α
⊢ (Mᵀ.map star).updateCol i (star b) = (M.updateRow i b)ᴴ
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝¹ : DecidableEq m
inst✝ : Star α
⊢ (Mᵀ.map star).updateCol i (star b) = (M.updateRow i b)ᴴ

Tactic:
conjTranspose,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝¹ : DecidableEq m
inst✝ : Star α
⊢ (Mᵀ.map star).updateCol i (star b) = (M.updateRow i b)ᵀ.map star
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inl.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j : n
⊢ Pi.single j x j = Function.update v j x j

Tactic:
Pi.single_eq_same,

Goal state after:
case inl.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j : n
⊢ x = Function.update v j x j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

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

Tactic:
ext j k
  obtain rfl | hjk := eq_or_ne j k
  · rw [diagonal_apply_eq]
    obtain rfl | hji := eq_or_ne j i
    · rw [updateCol_self, Pi.single_eq_same, Function.update_self]
    · rw [updateCol_ne hji, diagonal_apply_eq, Function.update_of_ne hji]
  · rw [diagonal_apply_ne _ hjk]
    obtain rfl | hki := eq_or_ne k i
    · rw [updateCol_self, Pi.single_eq_of_ne hjk]
    · rw [updateCol_ne hki, diagonal_apply_ne _ hjk]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝³ : DecidableEq l
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
i : l
r : m → α
j : n
c : m → α
⊢ updateRow 0 i r * updateCol 0 j c = single i j (r ⬝ᵥ c)

Tactic:
by
  rw [updateRow_mul, vecMul_updateCol, mul_updateCol, single_eq_of_single_single, Matrix.zero_mul,
    vecMul_zero, zero_mulVec, updateCol_zero_zero, updateRow, ← Pi.single, ← Pi.single]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬Submodule.map ϕ N < Submodule.map ψ N
inst✝ : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr x) i = (b.repr 0) i

Tactic:
(eq_bot_iff_generator_eq_zero _).mpr hgen

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < Submodule.map ψ N
inst✝ : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr x) i = (b.repr 0) i
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis ι R ↥O
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr ⟨x, ⋯⟩) i = (b.repr 0) i

Tactic:
(eq_bot_iff_generator_eq_zero _).mpr hgen

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis ι R ↥O
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬⊥ < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr ⟨x, ⋯⟩) i = (b.repr 0) i
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
s : Set K
p : (x : K) → x ∈ closure s → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : x ∈ closure s), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : x ∈ closure s), p x hx → p x⁻¹ ⋯
mul : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯
x : K
h : x ∈ closure s
⊢ ∀ {a b : K},
    a ∈ {x | ∃ (hx : x ∈ closure s), p x hx} →
      b ∈ {x | ∃ (hx : x ∈ closure s), p x hx} → a * b ∈ {x | ∃ (hx : x ∈ closure s), p x hx}

Tactic:
rintro _ _ ⟨_, hx⟩ ⟨_, hy⟩

Goal state after:
K : Type u
inst✝ : DivisionRing K
s : Set K
p : (x : K) → x ∈ closure s → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : x ∈ closure s), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : x ∈ closure s), p x hx → p x⁻¹ ⋯
mul : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯
x : K
h : x ∈ closure s
a✝ b✝ : K
w✝¹ : a✝ ∈ closure s
hx : p a✝ w✝¹
w✝ : b✝ ∈ closure s
hy : p b✝ w✝
⊢ a✝ * b✝ ∈ {x | ∃ (hx : x ∈ closure s), p x hx}
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
s : Set K
p : (x : K) → x ∈ closure s → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : x ∈ closure s), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : x ∈ closure s), p x hx → p x⁻¹ ⋯
mul : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯
x : K
h : x ∈ closure s
⊢ ∀ {a b : K},
    a ∈ {x | ∃ (hx : x ∈ closure s), p x hx} →
      b ∈ {x | ∃ (hx : x ∈ closure s), p x hx} → a + b ∈ {x | ∃ (hx : x ∈ closure s), p x hx}

Tactic:
rintro _ _ ⟨_, hx⟩ ⟨_, hy⟩

Goal state after:
K : Type u
inst✝ : DivisionRing K
s : Set K
p : (x : K) → x ∈ closure s → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : x ∈ closure s), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : x ∈ closure s), p x hx → p x⁻¹ ⋯
mul : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯
x : K
h : x ∈ closure s
a✝ b✝ : K
w✝¹ : a✝ ∈ closure s
hx : p a✝ w✝¹
w✝ : b✝ ∈ closure s
hy : p b✝ w✝
⊢ a✝ + b✝ ∈ {x | ∃ (hx : x ∈ closure s), p x hx}
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case succ
R : Type u_1
inst✝² : CommSemiring R
n✝ : Type u_5
inst✝¹ : DecidableEq n✝
inst✝ : Fintype n✝
M : Matrix n✝ n✝ R
n : ℕ
ih : toLin' (M ^ n) = toLin' M ^ n
⊢ toLin' (M ^ n) ∘ₗ toLin' M = toLin' M ^ n * toLin' M

Tactic:
ih,

Goal state after:
case succ
R : Type u_1
inst✝² : CommSemiring R
n✝ : Type u_5
inst✝¹ : DecidableEq n✝
inst✝ : Fintype n✝
M : Matrix n✝ n✝ R
n : ℕ
ih : toLin' (M ^ n) = toLin' M ^ n
⊢ (toLin' M ^ n) ∘ₗ toLin' M = toLin' M ^ n * toLin' M
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case succ
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₁
f : M₁ →ₗ[R] M₁
k : ℕ
ih : (toMatrix v₁ v₁) f ^ k = (toMatrix v₁ v₁) (f ^ k)
⊢ (toMatrix v₁ v₁) f ^ k * (toMatrix v₁ v₁) f = (toMatrix v₁ v₁) (f ^ k * f)

Tactic:
ih,

Goal state after:
case succ
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₁
f : M₁ →ₗ[R] M₁
k : ℕ
ih : (toMatrix v₁ v₁) f ^ k = (toMatrix v₁ v₁) (f ^ k)
⊢ (toMatrix v₁ v₁) (f ^ k) * (toMatrix v₁ v₁) f = (toMatrix v₁ v₁) (f ^ k * f)
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationMap N
inst✝ : NoZeroDivisors M
n : N
hn : n ≠ 0
ms : M × ↥S
eq : n * f ↑ms.2 = f ms.1
⊢ n ∈ nonZeroDivisors N

Tactic:
have hs : ms.1 ≠ 0 := fun h ↦ hn (by rwa [h, f.map_zero, (f.map_units _).mul_left_eq_zero] at eq)

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationMap N
inst✝ : NoZeroDivisors M
n : N
hn : n ≠ 0
ms : M × ↥S
eq : n * f ↑ms.2 = f ms.1
hs : ms.1 ≠ 0
⊢ n ∈ nonZeroDivisors N
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case succ
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₁
A : Matrix n✝ n✝ R
n : ℕ
ih : (toLin v₁ v₁) (A ^ n) = (toLin v₁ v₁) A ^ n
⊢ (toLin v₁ v₁) (A ^ n) ∘ₗ (toLin v₁ v₁) A = (toLin v₁ v₁) A ^ n * (toLin v₁ v₁) A

Tactic:
ih,

Goal state after:
case succ
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₁
A : Matrix n✝ n✝ R
n : ℕ
ih : (toLin v₁ v₁) (A ^ n) = (toLin v₁ v₁) A ^ n
⊢ ((toLin v₁ v₁) A ^ n) ∘ₗ (toLin v₁ v₁) A = (toLin v₁ v₁) A ^ n * (toLin v₁ v₁) A