mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: case neg
n : Type u_3
R : Type u_7
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
d : n → α
i j : n
h : ¬i = j
⊢ diagonal (r • d) i j = (r • diagonal d) i j

Tactic:
simp [h]

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

Goal state before:
pp: case pos
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : NegZeroClass α
d : n → α
i j : n
h : i = j
⊢ (-diagonal d) i j = diagonal (fun i ↦ -d i) i j

Tactic:
simp [h]

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

Goal state before:
pp: case neg
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : NegZeroClass α
d : n → α
i j : n
h : ¬i = j
⊢ (-diagonal d) i j = diagonal (fun i ↦ -d i) i j

Tactic:
simp [h]

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

Goal state before:
pp: case pos
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : SubNegZeroMonoid α
d₁ d₂ : n → α
i j : n
h : i = j
⊢ (diagonal d₁ - diagonal d₂) i j = diagonal (fun i ↦ d₁ i - d₂ i) i j

Tactic:
simp [h]

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

Goal state before:
pp: case neg
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : SubNegZeroMonoid α
d₁ d₂ : n → α
i j : n
h : ¬i = j
⊢ (diagonal d₁ - diagonal d₂) i j = diagonal (fun i ↦ d₁ i - d₂ i) i j

Tactic:
simp [h]

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

Goal state before:
pp: case pos
n : Type u_3
α : Type v
β : Type w
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
i✝ j✝ : n
h✝ : i✝ = j✝
⊢ f (d i✝) = f (d i✝)

Tactic:
simp [h]

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

Goal state before:
pp: case neg
n : Type u_3
α : Type v
β : Type w
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
i✝ j✝ : n
h✝ : ¬i✝ = j✝
⊢ f 0 = 0

Tactic:
simp [h]

Goal state after:
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 v
v : Basis ι R M
this : Nontrivial R
⊢ #ι ≤ ?m.29

pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ ?m.29 ≤ ⨆ ι, #↑↑ι

pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ Cardinal.{v}

Tactic:
swap

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ ?m.29 ≤ ⨆ ι, #↑↑ι

R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ #ι ≤ ?m.29

R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ Cardinal.{v}
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case pos
m : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : CommRing α
inst✝¹ : Nontrivial m
inst✝ : Nontrivial α
a : m → α
i j : m
hij : i ≠ j
h : a i = 0
⊢ Pi.single i 1 ≠ 0 ∧ Pi.single i 1 ⬝ᵥ a = 0

Tactic:
simp [h]

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

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
i : m
j : n
a b : α
i✝ : m
j✝ : n
h : i = i✝ ∧ j = j✝
⊢ a + b = ((of fun i' j' ↦ if i = i' ∧ j = j' then a else 0) + of fun i' j' ↦ if i = i' ∧ j = j' then b else 0) i✝ j✝

Tactic:
simp [h]

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

Goal state before:
pp: case neg
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
i : m
j : n
a b : α
i✝ : m
j✝ : n
h : ¬(i = i✝ ∧ j = j✝)
⊢ 0 = ((of fun i' j' ↦ if i = i' ∧ j = j' then a else 0) + of fun i' j' ↦ if i = i' ∧ j = j' then b else 0) i✝ j✝

Tactic:
simp [h]

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

Goal state before:
pp: case pos
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
i j : n
h : i = j
⊢ (diagonal d₁ * diagonal d₂) i j = diagonal (fun i ↦ d₁ i * d₂ i) i j

Tactic:
simp [h]

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

Goal state before:
pp: case neg
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
i j : n
h : ¬i = j
⊢ (diagonal d₁ * diagonal d₂) i j = diagonal (fun i ↦ d₁ i * d₂ i) i j

Tactic:
simp [h]

Goal state after:
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
M : Matrix l m α
x : m → α
y : n → α
i✝ : l
j✝ : n
⊢ (M * vecMulVec x y) i✝ j✝ = vecMulVec (M *ᵥ x) y i✝ j✝

Tactic:
simp_rw [mul_apply, vecMulVec_apply, mulVec, dotProduct, Finset.sum_mul, mul_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic

Goal state before:
pp: case intro
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Finite ι₁
inst✝ : Finite ι₂
val✝ : Fintype ι₁
⊢ Module.Finite R (Matrix ι₁ ι₂ M)

Tactic:
cases nonempty_fintype ι₂

Goal state after:
case intro.intro
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Finite ι₁
inst✝ : Finite ι₂
val✝¹ : Fintype ι₁
val✝ : Fintype ι₂
⊢ Module.Finite R (Matrix ι₁ ι₂ M)
Module: Mathlib.Data.Matrix.Mul

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

Tactic:
have : M = A.submatrix id e₁ := by
    simp only [A, submatrix_submatrix, Function.comp_id, submatrix_id_id, Equiv.symm_comp_self]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
hs : s.Nonempty
f : ι → M
a : M
⊢ a + s.sup' hs f = s.sup' hs fun i ↦ a + f i

Tactic:
add_comm a,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
hs : s.Nonempty
f : ι → M
a : M
⊢ s.sup' hs f + a = s.sup' ⋯ fun x ↦ f x + a
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
⊢ ((n • {a}).prod * f.prod fun a n ↦ a ^ n) = (single a n + f).prod fun a n ↦ a ^ n

Tactic:
Multiset.prod_nsmul,

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}.prod ^ n * 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: α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ f a * Multiset.count a {a} = f a

Tactic:
rw [Multiset.count_singleton_self, mul_one]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
⊢ Module.rank R M < ℵ₀ ↔ Module.Finite R M

Tactic:
rw [Free.rank_eq_card_chooseBasisIndex, mk_lt_aleph0_iff]
  exact ⟨fun h ↦ Finite.of_basis (Free.chooseBasis R M),
    fun I ↦ Finite.of_fintype (Free.ChooseBasisIndex R M)⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ I < J ↔ ↑I ⊂ ↑J

Tactic:
lt_iff_le_and_ne,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ I ≤ J ∧ I ≠ J ↔ ↑I ⊂ ↑J
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Unique ι
h : finrank R M = 1
v : M
i : ι
hv : v = 0
⊢ 0 i = 0

Tactic:
Finsupp.zero_apply

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Unique ι
h : finrank R M = 1
v : M
i : ι
hv : v = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: case mp.refine_1
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x✝ : R
s : TwoSidedIdeal R := mk' {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : x - y ∈ I
⊢ x - y ∈ s

Tactic:
rw [mem_mk']

Goal state after:
case mp.refine_1
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x✝ : R
s : TwoSidedIdeal R := mk' {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : x - y ∈ I
⊢ x - y ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: case mp.refine_2
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x✝ : R
s : TwoSidedIdeal R := mk' {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : x - y ∈ J
⊢ x - y ∈ s

Tactic:
rw [mem_mk']

Goal state after:
case mp.refine_2
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x✝ : R
s : TwoSidedIdeal R := mk' {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : x - y ∈ J
⊢ x - y ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : R
s : Set A
⊢ adjoin R (insert ((algebraMap R A) x) s) = adjoin R s

Tactic:
by
  rw [Set.insert_eq, adjoin_union]
  simp

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

Goal state before:
pp: R : Type u
inst✝ : InvolutiveStar R
r s : R
h : r = star s
⊢ s = star r

Tactic:
simp [h]

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:
simp [h]

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

Goal state before:
pp: case pos
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
h : j = i
⊢ ↑(w j)⁻¹ • 1 = ↑(w i)⁻¹ • 1

Tactic:
simp [h]

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

Goal state before:
pp: case neg
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
h : ¬j = i
⊢ ↑(w j)⁻¹ • 0 = ↑(w i)⁻¹ • 0

Tactic:
simp [h]

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

Goal state before:
pp: case pos
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : i = j
⊢ (diagonal d).toBlock p p i j = diagonal (fun i ↦ d ↑i) i j

Tactic:
simp [h]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
f : α → β
i✝ : m
j✝ : n
⊢ f (if i✝ = i then b j✝ else M i✝ j✝) = if i✝ = i then (f ∘ b) j✝ else f (M i✝ j✝)

Tactic:
exact apply_ite f _ _ _

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
f : α → β
i✝ : m
j✝ : n
⊢ f (if j✝ = j then c i✝ else M i✝ j✝) = if j✝ = j then (f ∘ c) i✝ else f (M i✝ j✝)

Tactic:
exact apply_ite f _ _ _

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

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
h : k = k'
⊢ ∑ j_1, M k i j_1 * N k j_1 j = ∑ x, ∑ x_1, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0

Tactic:
simp [h]

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

Goal state before:
pp: case neg
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
h : ¬k = k'
⊢ 0 = ∑ x, ∑ x_1, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0

Tactic:
simp [h]

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
inst✝ : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr x) i = 0 i

Tactic:
Finsupp.zero_apply

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 = 0
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
inst✝ : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr ⟨x, ⋯⟩) i = 0 i

Tactic:
Finsupp.zero_apply

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 = 0
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr✝ : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 1
hr' : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
h : m r = 0
⊢ a = 1

Tactic:
by simpa [h, Finset.prod_eq_one hr'.1] using hm

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

Goal state before:
pp: ι : 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
c : R
x : O
xM : x ∈ M
hx' : ϕ ⟨x, xM⟩ = 0
xM' : M.subtype ⟨x, xM⟩ ∈ M'
hc : c • y' + M.subtype ⟨x, xM⟩ = 0
⊢ c • ⟨y', y'M⟩ + ⟨x, xM⟩ = 0

Tactic:
exact @Subtype.coe_injective O (· ∈ M) _ _ hc

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ span R (⋃ i, {(LinearMap.single R (fun i ↦ R) i) 1 ᵥ* M}) = span R (⋃ i, {M.row i})

Tactic:
iUnion_singleton_eq_range,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ span R (Set.range fun x ↦ (LinearMap.single R (fun i ↦ R) x) 1 ᵥ* M) = span R (Set.range M.row)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: m : Type u_3
n : Type u_4
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
R : Type u_7
M₁ : Type u_8
M₂ : Type u_9
inst✝⁵ : Finite m
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
A : Matrix m n R
x : M₁
this : Fintype m
h : ∀ (j : m), (A *ᵥ ⇑(v₁.repr x)) j = 0
⊢ ∑ j, (A *ᵥ ⇑(v₁.repr x)) j • v₂ j = 0

Tactic:
simp [h]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝⁴ : MonoidWithZero R
S : Submonoid R
inst✝³ : OreSet S
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r t : R
s : ↥R⁰
hst : t * ↑s ∈ R⁰
hr : ¬r = 0
ht : t = 0
⊢ ↑⟨t * ↑s, hst⟩ = 0

Tactic:
simp [ht]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring S
inst✝⁶ : Algebra R S
m : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
b : Basis m R S
G : Type u_4
inst✝³ : Group G
inst✝² : DistribMulAction G S
inst✝¹ : SMulCommClass G R S
inst✝ : SMulCommClass G S S
g : G
x : S
i✝ j✝ : m
⊢ ((g • b).repr (x * (g • b) j✝)) i✝ = (b.repr (x * b j✝)) i✝

Tactic:
Basis.repr_smul,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring S
inst✝⁶ : Algebra R S
m : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
b : Basis m R S
G : Type u_4
inst✝³ : Group G
inst✝² : DistribMulAction G S
inst✝¹ : SMulCommClass G R S
inst✝ : SMulCommClass G S S
g : G
x : S
i✝ j✝ : m
⊢ (((DistribMulAction.toLinearEquiv R S g).symm ≪≫ₗ b.repr) (x * (g • b) j✝)) i✝ = (b.repr (x * b j✝)) i✝
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case refine_2
A : Type u_3
inst✝ : Semiring A
h : ∀ (n : ℕ) (f : End A (Fin n → A)), Surjective ⇑f → Injective ⇑f
n : ℕ
f g : End A (Fin n → A)
eq : f * g = 1
surj : Surjective ⇑f
⊢ g * f = 1

Tactic:
have := (LinearEquiv.ofBijective f ⟨h _ _ surj, surj⟩).symm_comp

Goal state after:
case refine_2
A : Type u_3
inst✝ : Semiring A
h : ∀ (n : ℕ) (f : End A (Fin n → A)), Surjective ⇑f → Injective ⇑f
n : ℕ
f g : End A (Fin n → A)
eq : f * g = 1
surj : Surjective ⇑f
this : ↑(LinearEquiv.ofBijective f ⋯).symm ∘ₗ ↑(LinearEquiv.ofBijective f ⋯) = LinearMap.id
⊢ g * f = 1
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
N : Submodule R M
inst✝ : Finite ι
b : Basis ι R M
h : finrank R ↥N = finrank R M
⊢ ∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i

Tactic:
cases nonempty_fintype ι
  let ⟨bM, bN, f, a, snf⟩ := N.smithNormalFormOfRankEq b h
  let e : Fin (Fintype.card ι) ≃ ι :=
    Equiv.ofBijective f
      ((Fintype.bijective_iff_injective_and_card f).mpr ⟨f.injective, Fintype.card_fin _⟩)
  have fe : ∀ i, f (e.symm i) = i := e.apply_symm_apply
  exact
    ⟨bM, a ∘ e.symm, bN.reindex e, fun i ↦ by
      simp only [snf, fe,
          Basis.coe_reindex, (· ∘ ·)]⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
hx : x ≠ 0
h : (sec M x).1 = 0
⊢ x = 0

Tactic:
by rw [← mk'_sec (M := M) S x, h, mk'_zero]

Goal state after:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: case exists_of_eq
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
x y : P
⊢ (algebraMap P S) x = (algebraMap P S) y → ∃ c, ↑c * x = ↑c * y

Tactic:
RingHom.algebraMap_toAlgebra,

Goal state after:
case exists_of_eq
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
x y : P
⊢ ((algebraMap R S).comp h.symm.toRingHom) x = ((algebraMap R S).comp h.symm.toRingHom) y → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: case e'_6
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map (↑h) M) S
⊢ inst✝¹ = ((algebraMap P S).comp h.symm.symm.toRingHom).toAlgebra

Tactic:
RingHom.algebraMap_toAlgebra,

Goal state after:
case e'_6
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map (↑h) M) S
⊢ inst✝¹ = (((algebraMap R S).comp h.symm.toRingHom).comp h.symm.symm.toRingHom).toAlgebra
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module.Finite R M
⊢ Module.Finite A (TensorProduct R A M)

Tactic:
classical
    obtain ⟨s, hs⟩ := h.fg_top
    refine ⟨⟨s.image (TensorProduct.mk R A M 1), eq_top_iff.mpr ?_⟩⟩
    rintro x -
    induction x with
    | zero => exact zero_mem _
    | tmul x y =>
      rw [Finset.coe_image, ← Submodule.span_span_of_tower R, Submodule.span_image, hs,
        Submodule.map_top, LinearMap.coe_range, ← mul_one x, ← smul_eq_mul,
        ← TensorProduct.smul_tmul']
      exact Submodule.smul_mem _ x (Submodule.subset_span <| Set.mem_range_self y)
    | add x y hx hy => exact Submodule.add_mem _ hx hy

Goal state after: