mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ ∃ a, det a = r

Tactic:
refine ⟨⟨diagonal fun j ↦ if j = i then r else 1, diagonal fun j ↦ if j = i then r⁻¹.1 else 1,
    ?_, ?_⟩, by simp [det]⟩

Goal state after:
case refine_1
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ ((diagonal fun j ↦ if j = i then ↑r else 1) * diagonal fun j ↦ if j = i then ↑r⁻¹ else 1) = 1

case refine_2
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ ((diagonal fun j ↦ if j = i then ↑r⁻¹ else 1) * diagonal fun j ↦ if j = i then ↑r else 1) = 1
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
M N : Matrix n n A
h : M.det ≠ 0
⊢ M.det * N.det ≠ 0 ↔ N.det ≠ 0

Tactic:
exact mul_ne_zero_iff_left h

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

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
hn : IsEmpty n
⊢ ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)

Tactic:
by
    rw [center_eq_bot_of_subsingleton, Fintype.card_eq_zero, max_eq_right_of_lt zero_lt_one,
      rootsOfUnity_one]
    exact MulEquiv.ofUnique

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
⊢ (List.ofFn r).prod ∈ A (List.map i (List.finRange n)).sum

Tactic:
List.ofFn_eq_map

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
⊢ (List.map r (List.finRange n)).prod ∈ A (List.map i (List.finRange n)).sum
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
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
N₂ : Type u_10
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
ι : Type u_15
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring S₁
inst✝⁷ : Semiring R₂
inst✝⁶ : Semiring S₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module S₁ N₂
inst✝³ : Module S₂ N₂
inst✝² : SMulCommClass S₂ S₁ N₂
inst✝¹ : Fintype n
inst✝ : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
f : Matrix n m N₂
x✝ : R₂
v : n → R₁
w : m → R₂
⊢ ∑ i, ∑ j, σ₂ ((x✝ •> w) j) •> σ₁ (v i) •> f i j = σ₂ x✝ •> ∑ i, ∑ j, σ₂ (w j) •> σ₁ (v i) •> f i j

Tactic:
by simp only [Pi.smul_apply, smul_eq_mul, map_mul, mul_smul, smul_sum]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x : M
⊢ Q (x + x) = 4 • Q x

Tactic:
rw [← two_smul R x, Q.map_smul, ← Nat.cast_smul_eq_nsmul R]
  norm_num

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₂' : Type u_9
n : Type u_11
m : Type u_12
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₂'
b₂' : Basis m' R M₂'
inst✝¹ : Fintype m'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
M : Matrix m m' R
⊢ (toMatrix₂ b₁ b₂) B * M = (toMatrix₂ b₁ b₂') (B.compl₂ ((toLin b₂' b₂) M))

Tactic:
by
  rw [LinearMap.toMatrix₂_compl₂ b₁ b₂, toMatrix_toLin]

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

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q Q' : QuadraticMap R M N
a : R
x : M
⊢ (⇑Q + ⇑Q') (a • x) = (a * a) • (⇑Q + ⇑Q') x

Tactic:
by simp only [Pi.add_apply, smul_add, QuadraticMap.map_smul]

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

Goal state before:
pp: case e'_2.e'_2
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ⁻¹ * A₁ᵀ * Pᵀ * J = ↑v⁻¹ * x

Tactic:
rw [mul_assoc, mul_assoc, ← mul_assoc _ _ J]
      rfl

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)
i j : n
⊢ ((QuadraticMap.associated Q) (Pi.single j 1)) (Pi.single i 1) =
    ((QuadraticMap.associated Q) (Pi.single i 1)) (Pi.single j 1)

Tactic:
← QuadraticMap.associated_isSymm

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
⊢ (((QuadraticMap.associatedHom R) Q) (Pi.single i 1)) (Pi.single j 1) =
    ((QuadraticMap.associated Q) (Pi.single i 1)) (Pi.single j 1)
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
i j : n
⊢ ((QuadraticMap.associated Q) (b j)) (b i) = ((QuadraticMap.associated Q) (b i)) (b j)

Tactic:
← QuadraticMap.associated_isSymm

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
⊢ (((QuadraticMap.associatedHom R) Q) (b i)) (b j) = ((QuadraticMap.associated Q) (b i)) (b j)
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
a b : α
hab : a ≠ b
ha' : ↑n ≤ {b}ᶜ.encard
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = ↑n
this : s.Finite
⊢ #this.toFinset = n

Tactic:
← ENat.natCast_inj,

Goal state after:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
a b : α
hab : a ≠ b
ha' : ↑n ≤ {b}ᶜ.encard
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = ↑n
this : s.Finite
⊢ ↑(#this.toFinset) = ↑n
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Infinite α
finite : Finite ↑(powersetCard α n)
⊢ ⋃₀ (SetLike.coe '' powersetCard α n) = univ

Tactic:
sUnion_eq_univ_iff

Goal state after:
α : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Infinite α
finite : Finite ↑(powersetCard α n)
⊢ ∀ (a : α), ∃ b ∈ SetLike.coe '' powersetCard α n, a ∈ b
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁹ : CommSemiring R
inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : Module R M'
inst✝³ : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝² : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝¹ : (i : ι ⊕ ι') → Module R (N i)
f : MultilinearMap R N M₂
inst✝ : DecidableEq ι
u : (i : ι) → N (Sum.inl i)
i : ι
x y : N (Sum.inl i)
x✝ : (i : ι') → N (Sum.inr i)
⊢ { toFun := fun v ↦ f fun t ↦ Sum.rec (update u i (x + y)) v t, map_update_add' := ⋯, map_update_smul' := ⋯ } x✝ =
    ({ toFun := fun v ↦ f fun t ↦ Sum.rec (update u i x) v t, map_update_add' := ⋯, map_update_smul' := ⋯ } +
        { toFun := fun v ↦ f fun t ↦ Sum.rec (update u i y) v t, map_update_add' := ⋯, map_update_smul' := ⋯ })
      x✝

Tactic:
let := Classical.decEq ι'

Goal state after:
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁹ : CommSemiring R
inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : Module R M'
inst✝³ : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝² : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝¹ : (i : ι ⊕ ι') → Module R (N i)
f : MultilinearMap R N M₂
inst✝ : DecidableEq ι
u : (i : ι) → N (Sum.inl i)
i : ι
x y : N (Sum.inl i)
x✝ : (i : ι') → N (Sum.inr i)
this : DecidableEq ι' := Classical.decEq ι'
⊢ { toFun := fun v ↦ f fun t ↦ Sum.rec (update u i (x + y)) v t, map_update_add' := ⋯, map_update_smul' := ⋯ } x✝ =
    ({ toFun := fun v ↦ f fun t ↦ Sum.rec (update u i x) v t, map_update_add' := ⋯, map_update_smul' := ⋯ } +
        { toFun := fun v ↦ f fun t ↦ Sum.rec (update u i y) v t, map_update_add' := ⋯, map_update_smul' := ⋯ })
      x✝
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁹ : CommSemiring R
inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : Module R M'
inst✝³ : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝² : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝¹ : (i : ι ⊕ ι') → Module R (N i)
f : MultilinearMap R N M₂
inst✝ : DecidableEq ι
u : (i : ι) → N (Sum.inl i)
i : ι
c : R
x : N (Sum.inl i)
x✝ : (i : ι') → N (Sum.inr i)
⊢ { toFun := fun v ↦ f fun t ↦ Sum.rec (update u i (c • x)) v t, map_update_add' := ⋯, map_update_smul' := ⋯ } x✝ =
    (c • { toFun := fun v ↦ f fun t ↦ Sum.rec (update u i x) v t, map_update_add' := ⋯, map_update_smul' := ⋯ }) x✝

Tactic:
let := Classical.decEq ι'

Goal state after:
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁹ : CommSemiring R
inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : Module R M'
inst✝³ : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝² : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝¹ : (i : ι ⊕ ι') → Module R (N i)
f : MultilinearMap R N M₂
inst✝ : DecidableEq ι
u : (i : ι) → N (Sum.inl i)
i : ι
c : R
x : N (Sum.inl i)
x✝ : (i : ι') → N (Sum.inr i)
this : DecidableEq ι' := Classical.decEq ι'
⊢ { toFun := fun v ↦ f fun t ↦ Sum.rec (update u i (c • x)) v t, map_update_add' := ⋯, map_update_smul' := ⋯ } x✝ =
    (c • { toFun := fun v ↦ f fun t ↦ Sum.rec (update u i x) v t, map_update_add' := ⋯, map_update_smul' := ⋯ }) x✝
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
g : MultilinearMap R (fun i ↦ N (Sum.inl i)) (MultilinearMap R (fun i ↦ N (Sum.inr i)) M₂)
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ [inst : DecidableEq (ι ⊕ ι')] (m : (i : ι ⊕ ι') → N i) (i : ι ⊕ ι') (x y : N i),
    ((g fun i_1 ↦ update m i (x + y) (Sum.inl i_1)) fun i' ↦ update m i (x + y) (Sum.inr i')) =
      ((g fun i_1 ↦ update m i x (Sum.inl i_1)) fun i' ↦ update m i x (Sum.inr i')) +
        (g fun i_1 ↦ update m i y (Sum.inl i_1)) fun i' ↦ update m i y (Sum.inr i')

Tactic:
let := Classical.decEq ι'

Goal state after:
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
g : MultilinearMap R (fun i ↦ N (Sum.inl i)) (MultilinearMap R (fun i ↦ N (Sum.inr i)) M₂)
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq ι' := Classical.decEq ι'
⊢ ∀ [inst : DecidableEq (ι ⊕ ι')] (m : (i : ι ⊕ ι') → N i) (i : ι ⊕ ι') (x y : N i),
    ((g fun i_1 ↦ update m i (x + y) (Sum.inl i_1)) fun i' ↦ update m i (x + y) (Sum.inr i')) =
      ((g fun i_1 ↦ update m i x (Sum.inl i_1)) fun i' ↦ update m i x (Sum.inr i')) +
        (g fun i_1 ↦ update m i y (Sum.inl i_1)) fun i' ↦ update m i y (Sum.inr i')
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
g : MultilinearMap R (fun i ↦ N (Sum.inl i)) (MultilinearMap R (fun i ↦ N (Sum.inr i)) M₂)
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ [inst : DecidableEq (ι ⊕ ι')] (m : (i : ι ⊕ ι') → N i) (i : ι ⊕ ι') (c : R) (x : N i),
    ((g fun i_1 ↦ update m i (c • x) (Sum.inl i_1)) fun i' ↦ update m i (c • x) (Sum.inr i')) =
      c • (g fun i_1 ↦ update m i x (Sum.inl i_1)) fun i' ↦ update m i x (Sum.inr i')

Tactic:
let := Classical.decEq ι'

Goal state after:
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
g : MultilinearMap R (fun i ↦ N (Sum.inl i)) (MultilinearMap R (fun i ↦ N (Sum.inr i)) M₂)
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq ι' := Classical.decEq ι'
⊢ ∀ [inst : DecidableEq (ι ⊕ ι')] (m : (i : ι ⊕ ι') → N i) (i : ι ⊕ ι') (c : R) (x : N i),
    ((g fun i_1 ↦ update m i (c • x) (Sum.inl i_1)) fun i' ↦ update m i (c • x) (Sum.inr i')) =
      c • (g fun i_1 ↦ update m i x (Sum.inl i_1)) fun i' ↦ update m i x (Sum.inr i')
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Fin 0 → M
⊢ (ιMulti R 0) v = 1

Tactic:
simp [ιMulti]

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

Goal state before:
pp: 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

Tactic:
· rw [ExteriorAlgebra.ιMulti_apply]
      apply congrArg (List.prod ∘ List.ofFn)
      ext i
      obtain ⟨m, -, hm⟩ := (Set.mem_image _ _ _).mp (f i).2
      rw [Function.comp_apply, Function.comp_apply, ← hm, ExteriorAlgebra.ι_leftInverse]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasInjectiveDimensionLT X n
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT X i}, a < ↑n

Tactic:
· obtain _ | n := n
    · exact ⟨⊥, fun _ _ ↦ hasInjectiveDimensionLT_of_ge _ 0 _ (by simp), by decide⟩
    · exact ⟨n, fun i hi ↦ hasInjectiveDimensionLT_of_ge _ (n + 1) _ (by simpa using hi),
        by simp [ENat.WithBot.lt_add_one_iff]⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
inst✝² : Free R ↑S.X₁
inst✝¹ : Free R ↑S.X₃
inst✝ : StrongRankCondition R
this : Free R ↑S.X₂
⊢ Module.rank R ↑S.X₂ = Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃

Tactic:
rw [Module.Free.rank_eq_card_chooseBasisIndex, Module.Free.rank_eq_card_chooseBasisIndex R S.X₁,
    Module.Free.rank_eq_card_chooseBasisIndex R S.X₃, Cardinal.add_def, Cardinal.eq]

Goal state after:
R : Type u_3
inst✝³ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
inst✝² : Free R ↑S.X₁
inst✝¹ : Free R ↑S.X₃
inst✝ : StrongRankCondition R
this : Free R ↑S.X₂
⊢ Nonempty (Free.ChooseBasisIndex R ↑S.X₂ ≃ Free.ChooseBasisIndex R ↑S.X₁ ⊕ Free.ChooseBasisIndex R ↑S.X₃)
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : IsFiltered C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : FinallySmall C
this :
  ∀ (C₀ : Type u) [inst : Category.{w, u} C₀] [IsFiltered C₀] [FinallySmall C₀],
    ∃ D, ∃ (_ : Small.{w, u} D), ∃ x, ∃ (_ : IsFiltered D), ∃ F, F.Final
C₀ : Type u
inst✝ : Category.{w, u} C₀
x✝¹ : IsFiltered C₀
x✝ : FinallySmall C₀
⊢ ∃ D x, ∃ (_ : IsFiltered D), ∃ F, F.Final

Tactic:
obtain ⟨D, _, _, _, F, _⟩ := this C₀

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : IsFiltered C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : FinallySmall C
this :
  ∀ (C₀ : Type u) [inst : Category.{w, u} C₀] [IsFiltered C₀] [FinallySmall C₀],
    ∃ D, ∃ (_ : Small.{w, u} D), ∃ x, ∃ (_ : IsFiltered D), ∃ F, F.Final
C₀ : Type u
inst✝ : Category.{w, u} C₀
x✝¹ : IsFiltered C₀
x✝ : FinallySmall C₀
D : Type u
w✝² : Small.{w, u} D
w✝¹ : Category.{w, u} D
w✝ : IsFiltered D
F : D ⥤ C₀
h✝ : F.Final
⊢ ∃ D x, ∃ (_ : IsFiltered D), ∃ F, F.Final
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator

Goal state before:
pp: C : Type u
inst✝ : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
m : M.Elements
⊢ (ConcreteCategory.hom (M.fromFreeYonedaCoproduct.app m.fst))
      ((ConcreteCategory.hom ((M.ιFreeYonedaCoproduct m).app m.fst)) (ModuleCat.freeMk (𝟙 (Opposite.unop m.fst)))) =
    m.snd

Tactic:
M.ι_fromFreeYonedaCoproduct_apply m,

Goal state after:
C : Type u
inst✝ : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
m : M.Elements
⊢ (ConcreteCategory.hom (m.fromFreeYoneda.app m.fst)) (ModuleCat.freeMk (𝟙 (Opposite.unop m.fst))) = m.snd
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Free

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
ψ : freeObj F ⟶ G
⊢ (fun φ ↦ freeObjDesc φ)
      ((fun ψ ↦ freeAdjunctionUnit R F ≫ Functor.whiskerRight ((toPresheaf R).map ψ) (forget Ab)) ψ) =
    ψ

Tactic:
ext1 X; dsimp; ext x; simp [toPresheaf]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X : F.PartialLeftAdjointSource
⊢ F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap (𝟙 X)) =
    F.partialLeftAdjointHomEquiv (𝟙 (F.partialLeftAdjointObj X))

Tactic:
simp [partialLeftAdjointHomEquiv_map]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
N : ModuleCat ↑cR.pt
ψ : M ⟶ (constFunctor cR).obj N
φ : ModuleColimit hcR hcM →+ N.1
hφ : (homEquiv' hcR hcM) φ = (toPresheaf R).map ψ
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
⊢ (ConcreteCategory.hom (((toPresheaf R).map ψ).app U)) (r • m) =
    (ConcreteCategory.hom (cR.ι.app U)) r • (ConcreteCategory.hom (((toPresheaf R).map ψ).app U)) m

Tactic:
erw [toPresheaf_map_app_apply]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
N : ModuleCat ↑cR.pt
ψ : M ⟶ (constFunctor cR).obj N
φ : ModuleColimit hcR hcM →+ N.1
hφ : (homEquiv' hcR hcM) φ = (toPresheaf R).map ψ
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
⊢ (ConcreteCategory.hom (ψ.app U)) (r • m) =
    (ConcreteCategory.hom (cR.ι.app U)) r • (ConcreteCategory.hom (((toPresheaf R).map ψ).app U)) m
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
J K : Precoverage D
inst✝¹ : CreatesLimitsOfShape WalkingCospan F
inst✝ : J.HasPullbacks
X Y : C
R : Presieve Y
f : X ⟶ Y
hR : R ∈ (comap F J).coverings Y
Z : C
g : Z ⟶ Y
hg : R g
this : (Presieve.map F R).HasPullbacks (F.map f)
⊢ HasPullback g f

Tactic:
have : HasPullback (F.map g) (F.map f) := (R.map F).hasPullback _ (R.map_map hg)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
J K : Precoverage D
inst✝¹ : CreatesLimitsOfShape WalkingCospan F
inst✝ : J.HasPullbacks
X Y : C
R : Presieve Y
f : X ⟶ Y
hR : R ∈ (comap F J).coverings Y
Z : C
g : Z ⟶ Y
hg : R g
this✝ : (Presieve.map F R).HasPullbacks (F.map f)
this : HasPullback (F.map g) (F.map f)
⊢ HasPullback g f
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ ∀ (s : Cocone S.arrows.diagram) (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Exists.choose ⋯ = s.ι.app j

Tactic:
by
        intro s f
        replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
          (yonedaFamily_fromCocone_compatible S s)
        have ht := H.choose_spec.1 f.obj.hom f.property
        cat_disch

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
U : ι → C
X Y : C
g : (i : ι) → U i ⟶ X
f : X ⟶ Y
⊢ pushforward f (ofArrows U g) ≤ ofArrows U fun x ↦ g x ≫ f

Tactic:
rintro _ _ ⟨u, rfl, ⟨i⟩⟩
    exact ⟨i⟩

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
s : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
Z : C
v : Z ⟶ B
⊢ ⟨Z, v⟩ ∈ (fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) '' s.uncurry →
    ⟨Z, v⟩ ∈ (pullbackArrows b s).uncurry

Tactic:
· rintro ⟨⟨Y, u⟩, hu, h⟩
    rw [Sigma.ext_iff] at h
    obtain ⟨rfl, h⟩ := h
    rw [heq_iff_eq] at h; subst h
    exact ⟨Y, u, hu⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
R : Presieve X
Y✝ : C
f✝ : Y✝ ⟶ Y
⊢ (generate (Presieve.pushforward f R)).arrows f✝ ↔ (pushforward f (generate R)).arrows f✝

Tactic:
grind [generate_apply, Presieve.pushforward, pushforward_apply]

Goal state after: