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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x✝ y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
b : Basis (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
span_b : N = span R (Set.range (⇑N.subtype ∘ ⇑b))
c : R
x : M
hx : x ∈ span R (Set.range (⇑N.subtype ∘ ⇑b))
hc : c • y + x = 0
⊢ c = 0

Tactic:
← span_b

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x✝ y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
b : Basis (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
span_b : N = span R (Set.range (⇑N.subtype ∘ ⇑b))
c : R
x : M
hx : x ∈ N
hc : c • y + x = 0
⊢ c = 0
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
j : l ⊕ m
val✝ : n
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val✝) j = M (Sum.inl val✝) j

Tactic:
rcases j with ⟨⟩

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : n
val✝ : l
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val✝¹) (Sum.inl val✝) =
    M (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : n
val✝ : m
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val✝¹) (Sum.inr val✝) =
    M (Sum.inl val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
j : l ⊕ m
val✝ : o
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val✝) j = M (Sum.inr val✝) j

Tactic:
rcases j with ⟨⟩

Goal state after:
case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : o
val✝ : l
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val✝¹) (Sum.inl val✝) =
    M (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : o
val✝ : m
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val✝¹) (Sum.inr val✝) =
    M (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
j : l ⊕ m
val✝ : n
⊢ (fromBlocks A B C D).map f (Sum.inl val✝) j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inl val✝) j

Tactic:
rcases j with ⟨⟩

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : n
val✝ : l
⊢ (fromBlocks A B C D).map f (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : n
val✝ : m
⊢ (fromBlocks A B C D).map f (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inl val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
j : l ⊕ m
val✝ : o
⊢ (fromBlocks A B C D).map f (Sum.inr val✝) j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inr val✝) j

Tactic:
rcases j with ⟨⟩

Goal state after:
case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : o
val✝ : l
⊢ (fromBlocks A B C D).map f (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : o
val✝ : m
⊢ (fromBlocks A B C D).map f (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : n ⊕ o
val✝ : l
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val✝) j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inl val✝) j

Tactic:
rcases j with ⟨⟩

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : l
val✝ : n
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val✝¹) (Sum.inl val✝) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : l
val✝ : o
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val✝¹) (Sum.inr val✝) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inl val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : n ⊕ o
val✝ : m
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val✝) j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inr val✝) j

Tactic:
rcases j with ⟨⟩

Goal state after:
case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : m
val✝ : n
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val✝¹) (Sum.inl val✝) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : m
val✝ : o
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val✝¹) (Sum.inr val✝) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inr val✝¹) (Sum.inr val✝)
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 <;> dsimp

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 (Sum.inr val✝) (f j) = fromBlocks C D A B (Sum.inl val✝) (f 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 (Sum.inl val✝) (f j) = fromBlocks C D A B (Sum.inr val✝) (f j)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : l ⊕ m
val✝ : n
⊢ (x • fromBlocks A B C D) (Sum.inl val✝) j = fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val✝) j

Tactic:
rcases j with ⟨⟩

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : n
val✝ : l
⊢ (x • fromBlocks A B C D) (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : n
val✝ : m
⊢ (x • fromBlocks A B C D) (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : l ⊕ m
val✝ : o
⊢ (x • fromBlocks A B C D) (Sum.inr val✝) j = fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val✝) j

Tactic:
rcases j with ⟨⟩

Goal state after:
case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : o
val✝ : l
⊢ (x • fromBlocks A B C D) (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : o
val✝ : m
⊢ (x • fromBlocks A B C D) (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
j : l ⊕ m
val✝ : n
⊢ fromBlocks 0 0 0 0 (Sum.inl val✝) j = 0 (Sum.inl val✝) j

Tactic:
rcases j with ⟨⟩

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
val✝¹ : n
val✝ : l
⊢ fromBlocks 0 0 0 0 (Sum.inl val✝¹) (Sum.inl val✝) = 0 (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
val✝¹ : n
val✝ : m
⊢ fromBlocks 0 0 0 0 (Sum.inl val✝¹) (Sum.inr val✝) = 0 (Sum.inl val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
j : l ⊕ m
val✝ : o
⊢ fromBlocks 0 0 0 0 (Sum.inr val✝) j = 0 (Sum.inr val✝) j

Tactic:
rcases j with ⟨⟩

Goal state after:
case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
val✝¹ : o
val✝ : l
⊢ fromBlocks 0 0 0 0 (Sum.inr val✝¹) (Sum.inl val✝) = 0 (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
val✝¹ : o
val✝ : m
⊢ fromBlocks 0 0 0 0 (Sum.inr val✝¹) (Sum.inr val✝) = 0 (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
j : l ⊕ m
val✝ : n
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inl val✝) j =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inl val✝) j

Tactic:
rcases j with ⟨⟩

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
val✝¹ : n
val✝ : l
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
val✝¹ : n
val✝ : m
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inl val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
j : l ⊕ m
val✝ : o
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inr val✝) j =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inr val✝) j

Tactic:
rcases j with ⟨⟩

Goal state after:
case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
val✝¹ : o
val✝ : l
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
val✝¹ : o
val✝ : m
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
j : p ⊕ q
val✝ : n
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inl val✝) j =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inl val✝) j

Tactic:
rcases j with ⟨⟩

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
val✝¹ : n
val✝ : p
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
val✝¹ : n
val✝ : q
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inl val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
j : p ⊕ q
val✝ : o
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inr val✝) j =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inr val✝) j

Tactic:
rcases j with ⟨⟩

Goal state after:
case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
val✝¹ : o
val✝ : p
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
val✝¹ : o
val✝ : q
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
j : l ⊕ m
val✝ : l
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val✝) j = diagonal (Sum.elim d₁ d₂) (Sum.inl val✝) j

Tactic:
rcases j with ⟨⟩

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ val✝ : l
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val✝¹) (Sum.inl val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ : l
val✝ : m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val✝¹) (Sum.inr val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inl val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
j : l ⊕ m
val✝ : m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val✝) j = diagonal (Sum.elim d₁ d₂) (Sum.inr val✝) j

Tactic:
rcases j with ⟨⟩

Goal state after:
case inr.inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ : m
val✝ : l
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val✝¹) (Sum.inl val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ val✝ : m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val✝¹) (Sum.inr val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
j : l ⊕ m
val✝ : l
⊢ fromBlocks 1 0 0 1 (Sum.inl val✝) j = 1 (Sum.inl val✝) j

Tactic:
rcases j with ⟨⟩

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ val✝ : l
⊢ fromBlocks 1 0 0 1 (Sum.inl val✝¹) (Sum.inl val✝) = 1 (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ : l
val✝ : m
⊢ fromBlocks 1 0 0 1 (Sum.inl val✝¹) (Sum.inr val✝) = 1 (Sum.inl val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
j : l ⊕ m
val✝ : m
⊢ fromBlocks 1 0 0 1 (Sum.inr val✝) j = 1 (Sum.inr val✝) j

Tactic:
rcases j with ⟨⟩

Goal state after:
case inr.inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ : m
val✝ : l
⊢ fromBlocks 1 0 0 1 (Sum.inr val✝¹) (Sum.inl val✝) = 1 (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
val✝¹ val✝ : m
⊢ fromBlocks 1 0 0 1 (Sum.inr val✝¹) (Sum.inr val✝) = 1 (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Sort u_1
S : ι → Subfield K
x : K
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
by
  simp only [iInf, mem_sInf, Set.forall_mem_range]

Goal state after:
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
⊢ p 0 ⋯

Tactic:
simp_rw [← @add_neg_cancel K _ 1]

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
⊢ p (1 + -1) ⋯
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i✝ x✝ : n
⊢ (mulVecLin 1 ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1 x✝ = (LinearMap.id ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1 x✝

Tactic:
simp [Matrix.one_apply, Pi.single_apply, eq_comm]

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

Goal state before:
pp: F : Type u_4
E : Type u_5
L : Type u_6
L' : Type u_7
inst✝¹⁰ : CommSemiring F
inst✝⁹ : CommSemiring L
inst✝⁸ : CommSemiring L'
inst✝⁷ : Semiring E
inst✝⁶ : Algebra F L
inst✝⁵ : Algebra L E
inst✝⁴ : Algebra F L'
inst✝³ : Algebra L' E
inst✝² : Algebra F E
inst✝¹ : IsScalarTower F L E
inst✝ : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i
S : Set E
⊢ Subalgebra.restrictScalars F (adjoin L S) = Subalgebra.restrictScalars F (adjoin L' S)

Tactic:
apply_fun Subalgebra.toSubsemiring using fun K K' h ↦ by rwa [SetLike.ext'_iff] at h ⊢
  change Subsemiring.closure _ = Subsemiring.closure _
  rw [hi, Set.range_comp, EquivLike.range_eq_univ, Set.image_univ]

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

Goal state before:
pp: R : Type u_8
A : Type u_9
K : Type u_10
B : Type u_11
L : Type u_12
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : CommRing K
inst✝¹⁰ : CommRing L
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R K
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : IsScalarTower R A K
inst✝⁴ : Algebra R B
inst✝³ : Algebra R L
inst✝² : Algebra B L
inst✝¹ : IsFractionRing B L
inst✝ : IsScalarTower R B L
h : A ≃ₐ[R] B
a : A
⊢ (algEquivOfAlgEquiv h) ((algebraMap A K) a) = (algebraMap B L) (h a)

Tactic:
by
  simp [algEquivOfAlgEquiv]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
x : R
y : ↥M
⊢ (monoidOf M).mk' x y = mk' (Localization M) x y

Tactic:
mk',

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
x : R
y : ↥M
⊢ (monoidOf M).mk' x y = (toLocalizationMap M (Localization M)).mk' x y