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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
a b : M
y : CliffordAlgebra Q
⊢ x * (((algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) - (ι Q) b * (ι Q) a) * y) =
    (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (x * y) - x * (ι Q) b * ((ι Q) a * y)

Tactic:
sub_mul,

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
a b : M
y : CliffordAlgebra Q
⊢ x * ((algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * y - (ι Q) b * (ι Q) a * y) =
    (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (x * y) - x * (ι Q) b * ((ι Q) a * y)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ (ι Q) a * ((ι Q) b * x) = -((ι Q) b * ((ι Q) a * x))

Tactic:
rw [← mul_assoc, ι_mul_ι_comm_of_isOrtho h, neg_mul, mul_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : M
⊢ ((algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) - (ι Q) b * (ι Q) a) * (ι Q) a =
    (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)

Tactic:
sub_mul,

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : M
⊢ (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (ι Q) a - (ι Q) b * (ι Q) a * (ι Q) a =
    (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
b c : F
hc : c = b * (a ^ 2 - 1)
⊢ diag2 a ha * SpecialLinearGroup.transvection ⋯ b * (diag2 a ha)⁻¹ * (SpecialLinearGroup.transvection ⋯ b)⁻¹ =
    SpecialLinearGroup.transvection ⋯ c

Tactic:
diag2_inv a ha,

Goal state after:
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
b c : F
hc : c = b * (a ^ 2 - 1)
⊢ diag2 a ha * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹ ⋯ * (SpecialLinearGroup.transvection ⋯ b)⁻¹ =
    SpecialLinearGroup.transvection ⋯ c
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ diag2 a ha =
    SpecialLinearGroup.transvection ⋯ a * SpecialLinearGroup.transvection ⋯ (-a⁻¹) *
            SpecialLinearGroup.transvection ⋯ a *
          SpecialLinearGroup.transvection ⋯ (-1) *
        SpecialLinearGroup.transvection ⋯ 1 *
      SpecialLinearGroup.transvection ⋯ (-1)

Tactic:
ext i j

Goal state after:
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
i j : Fin 2
⊢ ↑(diag2 a ha) i j =
    ↑(SpecialLinearGroup.transvection ⋯ a * SpecialLinearGroup.transvection ⋯ (-a⁻¹) *
                SpecialLinearGroup.transvection ⋯ a *
              SpecialLinearGroup.transvection ⋯ (-1) *
            SpecialLinearGroup.transvection ⋯ 1 *
          SpecialLinearGroup.transvection ⋯ (-1))
      i j
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring S₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring S₂
inst✝¹⁰ : AddCommMonoid N₂
inst✝⁹ : Module R N₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m N₂
⊢ (toMatrix₂Aux R (fun i ↦ Pi.single i 1) fun j ↦ Pi.single j 1) (toLinearMap₂'Aux σ₁ σ₂ f) = f

Tactic:
ext i j

Goal state after:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring S₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring S₂
inst✝¹⁰ : AddCommMonoid N₂
inst✝⁹ : Module R N₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m N₂
i : n
j : m
⊢ (toMatrix₂Aux R (fun i ↦ Pi.single i 1) fun j ↦ Pi.single j 1) (toLinearMap₂'Aux σ₁ σ₂ f) i j = f i j
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ v x✝³ * (w x✝¹ * M x✝³ x✝¹) = v x✝³ * (M x✝³ x✝¹ * w x✝¹)

Tactic:
mul_comm (w _),

Goal state after:
n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ v x✝³ * (M x✝³ x✝¹ * w x✝¹) = v x✝³ * (M x✝³ x✝¹ * w x✝¹)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
⊢ (toMatrix₂' R) (B.compl₁₂ l r) = (toMatrix' l)ᵀ * (toMatrix₂' R) B * toMatrix' r

Tactic:
ext i j

Goal state after:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ (toMatrix₂' R) (B.compl₁₂ l r) i j = ((toMatrix' l)ᵀ * (toMatrix₂' R) B * toMatrix' r) i j
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: n : Type u_11
m : Type u_12
n' : Type u_13
R : Type u_16
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
M : Matrix n' n R
⊢ M * (toMatrix₂' R) B = (toMatrix₂' R) (B ∘ₗ toLin' Mᵀ)

Tactic:
simp only [B.toMatrix₂'_comp, transpose_transpose, toMatrix'_toLin']

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

Goal state before:
pp: ⊢ S • S • S • T • S • T • S = T⁻¹

Tactic:
ext i j

Goal state after:
i j : Fin 2
⊢ ↑(S • S • S • T • S • T • S) i j = ↑T⁻¹ i j
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
σ₁ σ₂ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : M₁
y : M₂
⊢ (B (∑ i, (b₁.repr x) i •> b₁ i)) (∑ i, (b₂.repr y) i •> b₂ i) =
    ⇑σ₁ ∘ ⇑(b₁.repr x) ⬝ᵥ (toMatrix₂ b₁ b₂) B *ᵥ ⇑σ₂ ∘ ⇑(b₂.repr y)

Tactic:
suffices ∑ j, ∑ i, σ₂ (b₂.repr y j) * σ₁ (b₁.repr x i) * B (b₁ i) (b₂ j) =
           ∑ i, ∑ j, σ₁ (b₁.repr x i) * σ₂ (b₂.repr y j) * B (b₁ i) (b₂ j) by
    simpa [dotProduct, Matrix.mulVec_eq_sum, Finset.mul_sum, -Basis.sum_repr, ← mul_assoc]

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
σ₁ σ₂ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : M₁
y : M₂
⊢ ∑ j, ∑ i, σ₂ ((b₂.repr y) j) * σ₁ ((b₁.repr x) i) * (B (b₁ i)) (b₂ j) =
    ∑ i, ∑ j, σ₁ ((b₁.repr x) i) * σ₂ ((b₂.repr y) j) * (B (b₁ i)) (b₂ j)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
⊢ (toMatrix₂ b₁' b₂') (B.compl₁₂ l r) = ((toMatrix b₁' b₁) l)ᵀ * (toMatrix₂ b₁ b₂) B * (toMatrix b₂' b₂) r

Tactic:
ext i j

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ (toMatrix₂ b₁' b₂') (B.compl₁₂ l r) i j = (((toMatrix b₁' b₁) l)ᵀ * (toMatrix₂ b₁ b₂) B * (toMatrix b₂' b₂) r) i j
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
Q : QuadraticMap R M N
inst✝ : Invertible 2
x y : M
⊢ ((associated Q) x) y = 0 ↔ Q.IsOrtho x y

Tactic:
by
  simp_rw [isOrtho_def, associated_apply, invOf_smul_eq_iff, smul_zero, sub_sub, sub_eq_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
Q : QuadraticForm R (n → R)
⊢ Q.toMatrix'.IsSymm

Tactic:
ext i j

Goal state after:
R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
Q : QuadraticForm R (n → R)
i j : n
⊢ Q.toMatrix'.transpose i j = Q.toMatrix' i j
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
N : Type u_5
n : Type w
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
b : Basis n R N
Q : QuadraticForm R N
⊢ (toMatrix b Q).IsSymm

Tactic:
ext i j

Goal state after:
R : Type u_3
N : Type u_5
n : Type w
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
b : Basis n R N
Q : QuadraticForm R N
i j : n
⊢ (toMatrix b Q).transpose i j = toMatrix b Q i j
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
⊢ s ∈ {s | #s = n} ↔ #s = n

Tactic:
Set.mem_ofPred_eq

Goal state after:
α : Type u_1
n : ℕ
s : Finset α
⊢ #s = n ↔ #s = n
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv : CliffordAlgebra Q
⊢ ∀ (hx : xv ∈ (ι Q).range ^ (2 * k) * (ι Q).range ^ n.val), motive xv ⋯

Tactic:
pow_mul

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv : CliffordAlgebra Q
⊢ ∀ (hx : xv ∈ ((ι Q).range ^ 2) ^ k * (ι Q).range ^ n.val), motive xv ⋯
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: case inl.inl
α : Type u_1
n : ℕ
h1 : 0 < n
val✝ : Fintype α
h2 : n < Nat.card α
h : (Nat.card α).choose n = 0
⊢ False

Tactic:
Nat.choose_eq_zero_iff

Goal state after:
case inl.inl
α : Type u_1
n : ℕ
h1 : 0 < n
val✝ : Fintype α
h2 : n < Nat.card α
h : Nat.card α < n
⊢ False
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Finite α
⊢ (Nat.card α).choose n = 0 ↔ Nat.card α < n

Tactic:
Nat.choose_eq_zero_iff

Goal state after:
α : Type u_1
n : ℕ
inst✝ : Finite α
⊢ Nat.card α < n ↔ Nat.card α < n
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ M.mk F
      ⟨⟨IsFiltered.max i j,
            (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd +
              (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩.fst,
        r •
          ⟨IsFiltered.max i j,
              (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd +
                (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩.snd⟩ =
    M.mk F ⟨⟨i, x⟩.fst, r • ⟨i, x⟩.snd⟩ + M.mk F ⟨⟨j, y⟩.fst, r • ⟨j, y⟩.snd⟩

Tactic:
smul_add,

Goal state after:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ M.mk F
      ⟨⟨IsFiltered.max i j,
            (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd +
              (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩.fst,
        r • (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd +
          r • (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩ =
    M.mk F ⟨⟨i, x⟩.fst, r • ⟨i, x⟩.snd⟩ + M.mk F ⟨⟨j, y⟩.fst, r • ⟨j, y⟩.snd⟩
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case a
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
f : Fin n → ↑(⇑(ExteriorAlgebra.ι R) '' s)
hx : (List.ofFn fun i ↦ ↑(f i)).prod ∈ (⇑(ExteriorAlgebra.ι R) '' s) ^ n
⊢ (List.ofFn fun i ↦ ↑(f i)).prod ∈ ↑(span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s}))

Tactic:
refine mem_span_of_mem ⟨ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f, ?_, ?_⟩

Goal state after:
case a.refine_1
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
f : Fin n → ↑(⇑(ExteriorAlgebra.ι R) '' s)
hx : (List.ofFn fun i ↦ ↑(f i)).prod ∈ (⇑(ExteriorAlgebra.ι R) '' s) ^ n
⊢ ⇑ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f ∈ {a | range a ⊆ s}

case a.refine_2
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
f : Fin n → ↑(⇑(ExteriorAlgebra.ι R) '' s)
hx : (List.ofFn fun i ↦ ↑(f i)).prod ∈ (⇑(ExteriorAlgebra.ι R) '' s) ^ n
⊢ (ExteriorAlgebra.ιMulti R n) (⇑ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f) = (List.ofFn fun i ↦ ↑(f i)).prod
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
this : ∃ σ, (ExteriorAlgebra.ιMulti R n) ((v ∘ α) ∘ ⇑σ) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))
⊢ (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))

Tactic:
obtain ⟨σ, hσ⟩ := this
    rw [AlternatingMap.map_perm] at hσ
    refine (Submodule.smul_mem_iff_of_isUnit _ (r := (σ.sign : R)) ?_).mp hσ
    rw [isUnit_iff_exists_inv]
    use (σ.sign : R)
    norm_cast
    simp only [Int.units_mul_self, Units.val_one, Int.cast_one]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
j : J
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (F.obj j).map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (colimit.ι (F ⋙ evaluation R Y) j) =
    colimit.ι (F ⋙ evaluation R X) j ≫ (((Functor.const J).obj (colimitPresheafOfModules F)).obj j).map f

Tactic:
by
            dsimp
            erw [colimit.ι_desc_assoc, assoc, ← ι_preservesColimitIso_inv]
            rfl

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ ∃ c, Nonempty (op d ⟶ F.op.obj c)

Tactic:
obtain ⟨c, ⟨t⟩⟩ := h₁

Goal state after:
case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
d : D
h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
c : C
t : F.obj c ⟶ d
⊢ ∃ c, Nonempty (op d ⟶ F.op.obj c)
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
⊢ F.Final → ∀ (d : D), IsFiltered (StructuredArrow d F)

Tactic:
rw [final_iff_of_isFiltered]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
⊢ ((∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) ∧
      ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t) →
    ∀ (d : D), IsFiltered (StructuredArrow d F)
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
d : I s
c : (i : α) → I i
f g : d ⟶ (Pi.eval I s).obj c
c't : (s : α) → (c' : I s) × (c s ⟶ c') := Function.update (fun t ↦ ⟨c t, 𝟙 (c t)⟩) s ⟨coeq f g, coeqHom f g⟩
⊢ f ≫ ⟨coeq f g, coeqHom f g⟩.snd = g ≫ ⟨coeq f g, coeqHom f g⟩.snd

Tactic:
simpa using coeq_condition _ _

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
inst✝ : Epi f
X : Cᵒᵖ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.app X))

Tactic:
by
  rw [← ModuleCat.epi_iff_surjective]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
Q : DiagramOfCocones (curry.obj G) := DiagramOfCocones.mkOfHasColimits (curry.obj G)
Q' : (j : J) → IsColimit (Q.obj j) := fun j ↦ colimit.isColimit ((curry.obj G).obj j)
c' : Cocone G
f : (coconeOfHasColimitCurryCompColim G).pt ⟶ c'.pt
h : ∀ (j : J × K), (coconeOfHasColimitCurryCompColim G).ι.app j ≫ f = c'.ι.app j
⊢ f = colimit.desc (curry.obj G ⋙ colim) (coconeOfCoconeCurry G Q' c')

Tactic:
dsimp [coconeOfHasColimitCurryCompColim] at f h ⊢

Goal state after:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
Q : DiagramOfCocones (curry.obj G) := DiagramOfCocones.mkOfHasColimits (curry.obj G)
Q' : (j : J) → IsColimit (Q.obj j) := fun j ↦ colimit.isColimit ((curry.obj G).obj j)
c' : Cocone G
f : colimit (curry.obj G ⋙ colim) ⟶ c'.pt
h : ∀ (j : J × K), (colimit.ι ((curry.obj G).obj j.1) j.2 ≫ colimit.ι (curry.obj G ⋙ colim) j.1) ≫ f = c'.ι.app j
⊢ f = colimit.desc (curry.obj G ⋙ colim) (coconeOfCoconeCurry G Q' c')
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j ≫ (colimitIsoColimitCurryCompColim G).inv =
    colimit.ι G (j, k)

Tactic:
by
  simp [colimitIsoColimitCurryCompColim, Trans.simple, colimitUncurryIsoColimitCompColim]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝³ : X₁✝ ⟶ Y₁✝
x✝² : X₂✝ ⟶ Y₂✝
x✝¹ : Y₁✝ ⟶ Z₁✝
x✝ : Y₂✝ ⟶ Z₂✝
⊢ (x✝³ ⊗ₘ x✝²) ≫ (x✝¹ ⊗ₘ x✝) = x✝³ ≫ x✝¹ ⊗ₘ x✝² ≫ x✝

Tactic:
ext1; apply tensorHom_comp_tensorHom

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
T : Set (GrothendieckTopology C)
⊢ (sInf T).toPretopology = sInf (GrothendieckTopology.toPretopology '' T)

Tactic:
ext X S
  simp [mem_sInf, GrothendieckTopology.mem_toPretopology, GrothendieckTopology.mem_sInf]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: case refine_3
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ ∀ {m : s.pt ⟶ (Fork.ofι f w).pt}, m ≫ (Fork.ofι f w).ι = s.ι → m = ↾fun i ↦ Classical.choose ⋯

Tactic:
intro m hm
      ext i
      exact (Classical.choose_spec (t (s.ι i) (congr_hom s.condition i))).2 _ (congr_hom hm i)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
s : Cocone S.arrows.diagram
Y₁ : C
⊢ ∀ ⦃Y₂ Z : C⦄ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : S.arrows f₁) (h₂ : S.arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom ((yoneda.obj s.pt).map g₁.op)) (S.arrows.yonedaFamilyOfElements_fromCocone s f₁ h₁) =
        (ConcreteCategory.hom ((yoneda.obj s.pt).map g₂.op)) (S.arrows.yonedaFamilyOfElements_fromCocone s f₂ h₂)

Tactic:
Y₂

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
s : Cocone S.arrows.diagram
Y₁ Y₂ : C
⊢ ∀ ⦃Z : C⦄ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : S.arrows f₁) (h₂ : S.arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom ((yoneda.obj s.pt).map g₁.op)) (S.arrows.yonedaFamilyOfElements_fromCocone s f₁ h₁) =
        (ConcreteCategory.hom ((yoneda.obj s.pt).map g₂.op)) (S.arrows.yonedaFamilyOfElements_fromCocone s f₂ h₂)