mathlib-initiative/mathlib-tactics huggingface dataset:
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
A' : Submodule R A
M' : Submodule R M
r : R
m✝ : M
hm✝ : m✝ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
a : A
ha : a ∈ A'.toAddSubmonoid
m : M
hm : m ∈ M'.toAddSubmonoid
⊢ r • a • m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier

Tactic:
rw [← smul_assoc]; exact AddSubmonoid.smul_mem_smul (A'.smul_mem r ha) hm

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I✝ : Ideal R
J✝ : Ideal S
I J : Ideal (R × S)
h : map (RingHom.fst R S) I ≤ map (RingHom.fst R S) J ∧ map (RingHom.snd R S) I ≤ map (RingHom.snd R S) J
⊢ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I) ≤ (map (RingHom.fst R S) J).prod (map (RingHom.snd R S) J)

Tactic:
exact inf_le_inf (comap_mono h.1) (comap_mono h.2)

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
P : Type u_7
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherian R M
inst✝ : IsNoetherian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : f.range = g.ker
⊢ ∀ (a : Submodule R N), Submodule.comap g.rangeRestrict (Submodule.map g.rangeRestrict a) = a ⊔ f.range

Tactic:
by simp [Submodule.comap_map_eq, h]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
l : M →ₛₗ[σ] P
hl : Bijective ⇑l
⊢ IsNoetherian R M ↔ IsNoetherian S P

Tactic:
isNoetherian_iff'

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
l : M →ₛₗ[σ] P
hl : Bijective ⇑l
⊢ WellFoundedGT (Submodule R M) ↔ WellFoundedGT (Submodule S P)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
h : comap f I = ⊥
x : S
⊢ x ∈ I ↔ x ∈ ⊥

Tactic:
obtain ⟨y, hy⟩ := hf x

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
h : comap f I = ⊥
x : S
y : R
hy : f y = x
⊢ x ∈ I ↔ x ∈ ⊥
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : IsNoetherian R R
inst✝ : IsNoetherian S S
⊢ IsNoetherian (R × S) (R × S)

Tactic:
isNoetherian_iff'

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : WellFoundedGT (Submodule R R)
inst✝ : WellFoundedGT (Submodule S S)
⊢ WellFoundedGT (Submodule (R × S) (R × S))
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
I : Ideal R
N : Submodule R M
x : ↥N
⊢ I • map N.subtype ⊤ = I • N

Tactic:
Submodule.map_top,

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
⊢ I • N.subtype.range = I • N
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
hf : Function.Bijective ⇑f
K : Ideal S
⊢ (comap f K).IsMaximal ↔ K.IsMaximal

Tactic:
by
  simpa only [isMaximal_def] using! (relIsoOfBijective _ hf).isCoatom_iff _

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
h : I ⊔ J = ⊤
i : R
hi : i ∈ I ⊔ K
⊢ i ∈ I ⊔ J * K

Tactic:
eq_top_iff_one

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
h : 1 ∈ I ⊔ J
i : R
hi : i ∈ I ⊔ K
⊢ i ∈ I ⊔ J * K
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ K = ⊤
i : R
hi : i ∈ I ⊔ J
⊢ i ∈ I ⊔ J * K

Tactic:
eq_top_iff_one

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
h : 1 ∈ I ⊔ K
i : R
hi : i ∈ I ⊔ J
⊢ i ∈ I ⊔ J * K
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ I ⊔ J = ⊤

Tactic:
eq_top_iff_one

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ 1 ∈ I ⊔ J
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ gcd 0 0 = 0

Tactic:
← zero_dvd_iff

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ 0 ∣ gcd 0 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y : R
⊢ IsCoprime (span {x}) (span {y}) ↔ IsCoprime x y

Tactic:
simp_rw [isCoprime_iff_codisjoint, codisjoint_iff, eq_top_iff_one, mem_span_singleton_sup,
    mem_span_singleton]
  constructor
  · rintro ⟨a, _, ⟨b, rfl⟩, e⟩; exact ⟨a, b, mul_comm b y ▸ e⟩
  · rintro ⟨a, b, e⟩; exact ⟨a, _, ⟨b, rfl⟩, mul_comm y b ▸ e⟩

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
S : Type u_1
F : Type u_3
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
I : Ideal S
hI : IsPrincipal (comap f I)
⊢ IsPrincipal I

Tactic:
by
  rw [← map_comap_of_surjective f hf I]
  exact hI.map_ringHom f

Goal state after:
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} = ⊤ ↔ 1 ∈ Ideal.span {gcd x y}

Tactic:
eq_top_iff_one

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
x y : R
⊢ 1 ∈ Ideal.span {gcd x y} ↔ 1 ∈ Ideal.span {gcd x y}
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
n m : R
⊢ Ideal.span {n} ⊓ Ideal.span {m} = Ideal.span {lcm n m}

Tactic:
rw [Ideal.ext_iff]

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
n m : R
⊢ ∀ (x : R), x ∈ Ideal.span {n} ⊓ Ideal.span {m} ↔ x ∈ Ideal.span {lcm n m}
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
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j ↦ ↑(v.repr ↑j).support
S' : ↑J → Set M := fun j ↦ ⇑v '' S j
b : M
hb : b ∈ range ⇑v
i : ι
hi : v i = b
this : ↑{i} ⊆ ⋃ j, S j
⊢ b ∈ ⋃ j, S' j

Tactic:
subst b

Goal state after:
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
S : ↑J → Set ι := fun j ↦ ↑(v.repr ↑j).support
S' : ↑J → Set M := fun j ↦ ⇑v '' S j
i : ι
this : ↑{i} ⊆ ⋃ j, S j
hb : v i ∈ range ⇑v
⊢ v i ∈ ⋃ j, S' j
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case i
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ⊆ ↑(span R w)
⊢ Injective ⇑(linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩)

Tactic:
intro f g h
    apply_fun linearCombination R ((↑) : w → M) at h
    simp only [linearCombination_linearCombination,
               Span.finsupp_linearCombination_repr] at h
    exact i 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 u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Finite ↑w
s : range v ⊆ ↑(span R w)
this : Fintype ↑w := Fintype.ofFinite ↑w
t : Finset ι
⊢ t.card ≤ Fintype.card ↑w

Tactic:
let v' := fun x : (t : Set ι) => v x

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Finite ↑w
s : range v ⊆ ↑(span R w)
this : Fintype ↑w := Fintype.ofFinite ↑w
t : Finset ι
v' : ↑↑t → M := fun x ↦ v ↑x
⊢ t.card ≤ Fintype.card ↑w
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
⊢ (diagonal v)ᵀ i j = diagonal v i j

Tactic:
by_cases h : i = j <;> simp [h, transpose, eqComm]

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

Goal state before:
pp: case i
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
⊢ Injective ⇑(linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩)

Tactic:
intro f g h
    apply_fun linearCombination R ((↑) : w → M) at h
    simp only [linearCombination_linearCombination,
               Span.finsupp_linearCombination_repr] at h
    exact i h

Goal state after:
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✝ : Zero α
i : m
j : n
c : α
i' : m
j' : n
h : ¬(i = i' ∧ j = j')
⊢ single i j c i' j' = 0

Tactic:
simp only [single, and_imp, ite_eq_right_iff, of_apply]

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
c : α
i' : m
j' : n
h : ¬(i = i' ∧ j = j')
⊢ i = i' → j = j' → c = 0
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✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
⊢ single i j c *ᵥ x = Function.update 0 i (c * x j)

Tactic:
ext i'

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_7
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
i' : n
⊢ (single i j c *ᵥ x) i' = Function.update 0 i (c * x j) i'
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
L M : Matrix l m α
N : Matrix m n α
⊢ (L + M) * N = L * N + M * N

Tactic:
ext
  apply add_dotProduct

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A B : Matrix m n α
x : n → α
⊢ (A + B) *ᵥ x = A *ᵥ x + B *ᵥ x

Tactic:
ext
  apply add_dotProduct

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
x y : m → α
⊢ (x + y) ᵥ* A = x ᵥ* A + y ᵥ* A

Tactic:
ext
  apply add_dotProduct

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

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
i j k : n
M : Matrix n n α
hM : Commute (single i j 1) M
hki : k ≠ i
⊢ M k i = 0

Tactic:
by
  have := ext_iff.mpr hM k j
  simp_all

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

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalCommSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype o
A : Matrix m n α
B : Matrix o n α
x : o → α
⊢ A *ᵥ x ᵥ* B = (A * Bᵀ) *ᵥ x

Tactic:
← mulVec_mulVec,

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalCommSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype o
A : Matrix m n α
B : Matrix o n α
x : o → α
⊢ A *ᵥ x ᵥ* B = A *ᵥ Bᵀ *ᵥ x
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : M ^ k *ᵥ Pi.single i 1 = 0
h' : l = l - k + k
⊢ (M ^ (l - k) * M ^ k) *ᵥ Pi.single i 1 = 0

Tactic:
← mulVec_mulVec,

Goal state after:
n : Type u_3
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : M ^ k *ᵥ Pi.single i 1 = 0
h' : l = l - k + k
⊢ M ^ (l - k) *ᵥ M ^ k *ᵥ Pi.single i 1 = 0
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_10
n : Type u_11
R : Type u_12
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : MulOne R
inst✝¹ : AddCommMonoid R
inst✝ : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
⊢ (B * A).submatrix ⇑(Equiv.refl n) ⇑(Equiv.refl n) = 1 ↔ B * A = 1

Tactic:
Equiv.coe_refl,

Goal state after:
m : Type u_10
n : Type u_11
R : Type u_12
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : MulOne R
inst✝¹ : AddCommMonoid R
inst✝ : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
⊢ (B * A).submatrix id id = 1 ↔ B * A = 1
Module: Mathlib.SetTheory.Cardinal.Finsupp

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

Tactic:
apply max_le

Goal state after:
case a.h₁
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{v, u} #α ≤ #(α →₀ β)

case h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{u, v} #β ≤ #(α →₀ β)
Module: Mathlib.SetTheory.Cardinal.Finsupp

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

Tactic:
· apply max_le <;> rw [← lift_id #(α →₀ β), ← lift_umax]
    · obtain ⟨b, hb⟩ := exists_ne (0 : β)
      exact lift_mk_le.{v}.2 ⟨⟨_, Finsupp.single_left_injective hb⟩⟩
    · inhabit α
      exact lift_mk_le.{u}.2 ⟨⟨_, Finsupp.single_injective default⟩⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
hx : x ∈ I
hy : y ∈ I
⊢ x + y ∈ I

Tactic:
simpa using! I.ringCon.add hx hy

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

Goal state before:
pp: case a
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ Subalgebra.toSubmodule (adjoin R s) ≤ span R ↑(Submonoid.closure s)

Tactic:
intro r hr

Goal state after:
case a
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
r : A
hr : r ∈ Subalgebra.toSubmodule (adjoin R s)
⊢ r ∈ span R ↑(Submonoid.closure s)
Module: Mathlib.LinearAlgebra.TensorProduct.Associator

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
x : M →ₗ[R] N
⊢ lTensor P (rTensor Q x) ∘ₗ ↑(assoc R P M Q) = ↑(assoc R P N Q) ∘ₗ rTensor Q (lTensor P x)

Tactic:
rTensor,

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
x : M →ₗ[R] N
⊢ lTensor P (map x id) ∘ₗ ↑(assoc R P M Q) = ↑(assoc R P N Q) ∘ₗ map (lTensor P x) id
Module: Mathlib.LinearAlgebra.TensorProduct.Associator

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
x : M →ₗ[R] N
⊢ rTensor Q (lTensor P x) ∘ₗ ↑(assoc R P M Q).symm = ↑(assoc R P N Q).symm ∘ₗ lTensor P (rTensor Q x)

Tactic:
rTensor,

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
x : M →ₗ[R] N
⊢ map (lTensor P x) id ∘ₗ ↑(assoc R P M Q).symm = ↑(assoc R P N Q).symm ∘ₗ lTensor P (map x id)
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: case single.single
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
⊢ ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] Finsupp.single k' n)) (i, k) =
    (Finsupp.single i' m) i ⊗ₜ[R] (Finsupp.single k' n) k

Tactic:
finsuppTensorFinsupp_single,

Goal state after:
case single.single
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
⊢ (Finsupp.single (i', k') (m ⊗ₜ[R] n)) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] (Finsupp.single k' n) k
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: case inr.inr.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
l' : L
hk : k ≠ k'
⊢ single k l r k' l' = single (i, k) (j, l) r (i, k') (j, l')

pp: case inr.inr.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
l' : L
⊢ single k l r k l' = single (i, k) (j, l) r (i, k) (j, l')

Tactic:
· rw [single_apply_of_row_ne hk,
      single_apply_of_row_ne (ne_of_apply_ne Prod.snd hk)]

Goal state after:
case inr.inr.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
l' : L
⊢ single k l r k l' = single (i, k) (j, l) r (i, k) (j, l')
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
inst✝¹ : StarRing R
S : Type u_1
inst✝ : NonAssocSemiring S
⊢ Function.Involutive fun f ↦ (starRingEnd R).comp f

Tactic:
by
    intro
    ext
    simp only [RingHom.coe_comp, Function.comp_apply, starRingEnd_self_apply]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semifield R
inst✝ : StarRing R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x / y)

Tactic:
simp only [isSelfAdjoint_iff, star_div₀, hx.star_eq, hy.star_eq]

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

Goal state before:
pp: case fst
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι ⊕ ι'
⊢ ((b.prod b') i).1 = (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i).1

Tactic:
cases i

Goal state after:
case fst.inl
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
val✝ : ι
⊢ ((b.prod b') (Sum.inl val✝)).1 =
    (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') (Sum.inl val✝)).1

case fst.inr
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
val✝ : ι'
⊢ ((b.prod b') (Sum.inr val✝)).1 =
    (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') (Sum.inr val✝)).1
Module: Mathlib.LinearAlgebra.Basis.Prod

Goal state before:
pp: case snd
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι ⊕ ι'
⊢ ((b.prod b') i).2 = (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i).2

Tactic:
cases i

Goal state after:
case snd.inl
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
val✝ : ι
⊢ ((b.prod b') (Sum.inl val✝)).2 =
    (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') (Sum.inl val✝)).2

case snd.inr
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
val✝ : ι'
⊢ ((b.prod b') (Sum.inr val✝)).2 =
    (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') (Sum.inr val✝)).2
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
i : o ⊕ n
j : p
⊢ (fromBlocks A B C D).submatrix Sum.swap f i j = (fromBlocks C D A B).submatrix id f i j

Tactic:
cases i

Goal state after:
case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝ : o
⊢ (fromBlocks A B C D).submatrix Sum.swap f (Sum.inl val✝) j = (fromBlocks C D A B).submatrix id f (Sum.inl val✝) j

case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝ : n
⊢ (fromBlocks A B C D).submatrix Sum.swap f (Sum.inr val✝) j = (fromBlocks C D A B).submatrix id f (Sum.inr val✝) j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
i : n ⊕ o
j : l ⊕ m
⊢ (-fromBlocks A B C D) i j = fromBlocks (-A) (-B) (-C) (-D) i j

Tactic:
cases i

Goal state after:
case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
j : l ⊕ m
val✝ : n
⊢ (-fromBlocks A B C D) (Sum.inl val✝) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val✝) j

case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
j : l ⊕ m
val✝ : o
⊢ (-fromBlocks A B C D) (Sum.inr val✝) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val✝) j