mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_7
inst✝ : CommMonoid M
x✝ : Mˣ
⊢ x✝ ∈ rootsOfUnity 0 M ↔ x✝ ∈ ⊤

Tactic:
simp only [mem_rootsOfUnity, pow_zero, Subgroup.mem_top]

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

Goal state before:
pp: n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : Basis n R M
inst✝ : DecidableEq n
A : Matrix n n R
hA : IsUnit A.det
x : M
⊢ ((toLin b b) A⁻¹) (((toLin b b) A) x) = x

Tactic:
simp_rw [← LinearMap.comp_apply, ← Matrix.toLin_mul b b b, Matrix.nonsing_inv_mul _ hA,
      toLin_one, LinearMap.id_apply]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S✝ : Type u_5
F : Type u_6
inst✝⁷ : CommMonoid M
inst✝⁶ : CommMonoid N
inst✝⁵ : DivisionCommMonoid G
k l : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
L : Type u_7
inst✝¹ : LeftCancelMonoid L
inst✝ : Finite L
S : Subgroup Rˣ := rootsOfUnity (Monoid.exponent L) R
this : Finite (L →* ↥S)
f : L →* Rˣ
a : L
⊢ f 1 = 1

Tactic:
map_one

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S✝ : Type u_5
F : Type u_6
inst✝⁷ : CommMonoid M
inst✝⁶ : CommMonoid N
inst✝⁵ : DivisionCommMonoid G
k l : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
L : Type u_7
inst✝¹ : LeftCancelMonoid L
inst✝ : Finite L
S : Subgroup Rˣ := rootsOfUnity (Monoid.exponent L) R
this : Finite (L →* ↥S)
f : L →* Rˣ
a : L
⊢ 1 = 1
Module: Mathlib.LinearAlgebra.Basis.Bilinear

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
Rₗ : Type u_10
Mₗ : Type u_11
Nₗ : Type u_12
Pₗ : Type u_13
inst✝⁶ : CommSemiring Rₗ
inst✝⁵ : AddCommMonoid Mₗ
inst✝⁴ : AddCommMonoid Nₗ
inst✝³ : AddCommMonoid Pₗ
inst✝² : Module Rₗ Mₗ
inst✝¹ : Module Rₗ Nₗ
inst✝ : Module Rₗ Pₗ
b₁' : Basis ι₁ Rₗ Mₗ
b₂' : Basis ι₂ Rₗ Nₗ
B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ
x : Mₗ
y : Nₗ
⊢ ((b₁'.repr x).sum fun i xi ↦ (b₂'.repr y).sum fun j yj ↦ xi • yj • (B (b₁' i)) (b₂' j)) =
    (B ((Finsupp.linearCombination Rₗ ⇑b₁') (b₁'.repr x))) ((Finsupp.linearCombination Rₗ ⇑b₂') (b₂'.repr y))

Tactic:
simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum₂, map_sum, map_smul₂, map_smul]

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

Goal state before:
pp: n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
⊢ (∃ v, v ≠ 0 ∧ M *ᵥ v = 0) ↔ M.det = 0

Tactic:
by
  have : (∃ v ≠ 0, (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ _ :=
    exists_mulVec_eq_zero_iff_aux
  rw [← RingHom.map_det, IsFractionRing.to_map_eq_zero_iff] at this
  refine Iff.trans ?_ this; constructor <;> rintro ⟨v, hv, mul_eq⟩
  · refine ⟨fun i => algebraMap _ _ (v i), mt (fun h => funext fun i => ?_) hv, ?_⟩
    · exact IsFractionRing.to_map_eq_zero_iff.mp (congr_fun h i)
    · ext i
      refine (RingHom.map_mulVec _ _ _ i).symm.trans ?_
      rw [mul_eq, Pi.zero_apply, map_zero, Pi.zero_apply]
  · let := Classical.decEq K
    obtain ⟨⟨b, hb⟩, ba_eq⟩ :=
      IsLocalization.exist_integer_multiples_of_finset (nonZeroDivisors A) (Finset.univ.image v)
    choose f hf using ba_eq
    refine
      ⟨fun i => f _ (Finset.mem_image.mpr ⟨i, Finset.mem_univ i, rfl⟩),
        mt (fun h => funext fun i => ?_) hv, ?_⟩
    · have := congr_arg (algebraMap A K) (congr_fun h i)
      rw [hf, Subtype.coe_mk, Pi.zero_apply, map_zero, Algebra.smul_def, mul_eq_zero,
        IsFractionRing.to_map_eq_zero_iff] at this
      exact this.resolve_left (nonZeroDivisors.ne_zero hb)
    · ext i
      refine IsFractionRing.injective A K ?_
      calc
        algebraMap A K ((M *ᵥ (fun i : n => f (v i) _)) i) =
            ((algebraMap A K).mapMatrix M *ᵥ algebraMap _ K b • v) i := ?_
        _ = 0 := ?_
        _ = algebraMap A K 0 := (map_zero _).symm
      · simp_rw [RingHom.map_mulVec, mulVec, dotProduct, Function.comp_apply, hf,
          RingHom.mapMatrix_apply, Pi.smul_apply, smul_eq_mul, Algebra.smul_def]
      · rw [mulVec_smul, mul_eq, Pi.smul_apply, Pi.zero_apply, smul_zero]

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 : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : { f // ∀ (m : M), f m * f m = (algebraMap R A) (Q m) }
⊢ (fun F ↦ ⟨F.toLinearMap ∘ₗ ι Q, ⋯⟩) ((fun f ↦ (ringCon Q).liftₐ ((TensorAlgebra.lift R) ↑f) ⋯) f) = f

Tactic:
by
    ext x
    dsimp
    exact (RingCon.liftₐ_mk _ _ _ _).trans (TensorAlgebra.lift_ι_apply _ x)

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c : F
⊢ SpecialLinearGroup.transvection ⋯ c ∈ commutator SL(2, F)

Tactic:
by
  rw [← commutator_diag2_transvection a ha (c / (a ^ 2 - 1)) c
    (div_mul_cancel₀ c (sub_ne_zero_of_ne hasq)).symm]
  exact Subgroup.commutator_mem_commutator (Subgroup.mem_top _) (Subgroup.mem_top _)

Goal state after:
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
⊢ mul.comp (mulLeft 0) = 0

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
⊢ mul.compr₂ (mulLeft 0) = 0

Tactic:
ext; simp

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

Goal state before:
pp: n : ℤ
⊢ ↑(T ^ n) = !![1, n; 0, 1]

Tactic:
by
  induction n with
  | zero => rw [zpow_zero, coe_one, Matrix.one_fin_two]
  | succ n h =>
    simp_rw [zpow_add, zpow_one, coe_mul, h, coe_T, Matrix.mul_fin_two]
    congrm !![_, ?_; _, _]
    rw [mul_one, mul_one, add_comm]
  | pred n h =>
    simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, Matrix.mul_fin_two]
    congrm !![?_, ?_; _, _] <;> ring

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

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
⊢ involute.comp involute = AlgHom.id R (CliffordAlgebra Q)

Tactic:
ext; simp

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

Goal state before:
pp: case ι_mul_ι_mul
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
m₁ m₂ : M
x : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 0
ihx : involute x = x
⊢ involute ((ι Q) m₁ * (ι Q) m₂ * x) = (ι Q) m₁ * (ι Q) m₂ * x

Tactic:
| ι_mul_ι_mul m₁ m₂ x _hx ihx =>

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

Goal state before:
pp: case ι_mul_ι_mul
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
m₁ m₂ : M
x : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 1
ihx : involute x = -x
⊢ involute ((ι Q) m₁ * (ι Q) m₂ * x) = -((ι Q) m₁ * (ι Q) m₂ * x)

Tactic:
| ι_mul_ι_mul m₁ m₂ x _hx ihx =>

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

Goal state before:
pp: case mem.algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x : CliffordAlgebra Q
i : ℕ
r : R
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) ((algebraMap R (CliffordAlgebra Q)) r) =
    (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑0) ⟨(algebraMap R (CliffordAlgebra Q)) r, ⋯⟩

Tactic:
rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl

Goal state after:
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
⊢ ∀ (m : M), (GradedAlgebra.ι Q) m * (GradedAlgebra.ι Q) m = (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i))) (Q m)

Tactic:
by apply GradedAlgebra.ι_sq_scalar Q

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
s : ↑(powersetCard α 1)
⊢ (fun a ↦ ⟨{a}, ⋯⟩) ((fun s ↦ ⋯.choose) s) = s

Tactic:
← Subtype.val_inj,

Goal state after:
α : Type u_1
n : ℕ
s : ↑(powersetCard α 1)
⊢ ↑((fun a ↦ ⟨{a}, ⋯⟩) ((fun s ↦ ⋯.choose) s)) = ↑s
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
i : Fin (n + 1)
f : M i →ₗ[R] MultilinearMap R (fun j ↦ M (i.succAbove j)) M₂
⊢ curryMid i (uncurryMid i f) = f

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
i : Fin (n + 1)
f : MultilinearMap R M M₂
⊢ LinearMap.uncurryMid i (curryMid i f) = f

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Fintype α
⊢ powersetCard α n = ↑(Finset.powersetCard n Finset.univ)

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u_8
inst✝⁴ : Fintype ι
R : Type u_9
M : Type u_10
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
w : ι → R
j : ι
hj : j ∈ univ
i : ι
a✝ : i ∈ univ
hij : i ≠ j
⊢ w j • w i • 0 = 0

Tactic:
module

Goal state after:
Module: Mathlib.Order.Hom.PowersetCard

Goal state before:
pp: n : ℕ
I : Type u_1
inst✝ : LinearOrder I
s : ↑(powersetCard I n)
⊢ (fun f ↦ ofFinEmb n I f.toEmbedding) ((fun s ↦ (↑s).orderEmbOfFin ⋯) s) = s

Tactic:
ext; simp

Goal state after:
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
hxv : xv ∈ ((ι Q).range ^ 2) ^ k * (ι Q).range ^ n.val
⊢ motive xv ⋯

Tactic:
induction hxv using Submodule.mul_induction_on' with

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
this : ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ M [⋀^Fin 0]→ₗ[R] N ≃ₗ[R] N

Tactic:
exact AlternatingMap.constLinearEquivOfIsEmpty.symm

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
⊢ ∀ (m : M) (x : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    ((LinearMap.mk₂ R (fun m f i ↦ (f i.succ).curryLeft m) ⋯ ⋯ ⋯ ⋯) m)
        (((LinearMap.mk₂ R (fun m f i ↦ (f i.succ).curryLeft m) ⋯ ⋯ ⋯ ⋯) m) x) =
      0 m • x

Tactic:
intro m x
    ext
    simp

Goal state after:
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
n : ℕ
m : M
⊢ (ιMulti R n.succ).curryLeft m = (LinearMap.mulLeft R ((ι R) m)).compAlternatingMap (ιMulti R n)

Tactic:
ext; simp

Goal state after:
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
⊢ Submodule.span R (range ⇑(ιMulti R n)) = ⊤

Tactic:
apply LinearMap.map_injective (Submodule.ker_subtype (⋀[R]^n M))

Goal state after:
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Submodule.map (⋀[R]^n M).subtype (Submodule.span R (range ⇑(ιMulti R n))) = Submodule.map (⋀[R]^n M).subtype ⊤
Module: Mathlib.Algebra.Category.ModuleCat.InjectiveDimension

Goal state before:
pp: case succ
R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
I' : ModuleCat R'
injective✝ : Injective I'
f' : N ⟶ I'
mono✝ : Mono f'
this✝ : Module.Injective R' ↑I'
injf' : Function.Injective ⇑(Hom.hom f')
S' : ShortComplex (ModuleCat R') := shortComplexOfCompEqZero (Hom.hom f') (Hom.hom f').range.mkQ ⋯
exactS' : S'.ShortExact
I : ModuleCat R :=
  let this := Module.compHom (↑I') eR.toRingHom;
  of R ↑I'
eI : ↑I ≃ₛₗ[↑eR] ↑I' :=
  let __spread.0 := AddEquiv.refl ↑I;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
this : Injective (of R ↑I)
f : ↑M →ₗ[R] ↑I := ↑eI.symm ∘ₛₗ Hom.hom f' ∘ₛₗ ↑e
injf : Function.Injective ⇑f
S : ShortComplex (ModuleCat R) := shortComplexOfCompEqZero f f.range.mkQ ⋯
exactS : S.ShortExact
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)

Tactic:
let eCoker : ModuleCat.of R (I ⧸ f.range) ≃ₛₗ[RingHomClass.toRingHom eR]
      ModuleCat.of R' (I' ⧸ f'.hom.range) :=
      Submodule.Quotient.equiv _ _ eI
        (by simp [f, ← Submodule.map_symm_eq_iff eI, LinearMap.range_comp])

Goal state after:
case succ
R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
I' : ModuleCat R'
injective✝ : Injective I'
f' : N ⟶ I'
mono✝ : Mono f'
this✝ : Module.Injective R' ↑I'
injf' : Function.Injective ⇑(Hom.hom f')
S' : ShortComplex (ModuleCat R') := shortComplexOfCompEqZero (Hom.hom f') (Hom.hom f').range.mkQ ⋯
exactS' : S'.ShortExact
I : ModuleCat R :=
  let this := Module.compHom (↑I') eR.toRingHom;
  of R ↑I'
eI : ↑I ≃ₛₗ[↑eR] ↑I' :=
  let __spread.0 := AddEquiv.refl ↑I;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
this : Injective (of R ↑I)
f : ↑M →ₗ[R] ↑I := ↑eI.symm ∘ₛₗ Hom.hom f' ∘ₛₗ ↑e
injf : Function.Injective ⇑f
S : ShortComplex (ModuleCat R) := shortComplexOfCompEqZero f f.range.mkQ ⋯
exactS : S.ShortExact
eCoker : ↑(of R (↑I ⧸ f.range)) ≃ₛₗ[↑eR] ↑(of R' (↑I' ⧸ (Hom.hom f').range)) :=
  Submodule.Quotient.equiv f.range (Hom.hom f').range eI ⋯
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)
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
hv : Submodule.span R (range v) = ⊤
⊢ Submodule.span R (range (ιMulti_family R n v)) = ⊤

Tactic:
apply LinearMap.map_injective (Submodule.ker_subtype (⋀[R]^n M))

Goal state after:
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
hv : Submodule.span R (range v) = ⊤
⊢ Submodule.map (⋀[R]^n M).subtype (Submodule.span R (range (ιMulti_family R n v))) = Submodule.map (⋀[R]^n M).subtype ⊤
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)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
⊢ ((evaluation R X).mapCocone c).ι.app j ≫
      c.pt.map f ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).desc ((evaluation R Y).mapCocone s)) =
    ((evaluation R X).mapCocone c).ι.app j ≫ (hc X).desc ((evaluation R X).mapCocone s) ≫ s.pt.map f

Tactic:
rw [(hc X).fac_assoc ((evaluation R X).mapCocone s) j]
        have h₁ := (c.ι.app j).naturality f
        have h₂ := (hc Y).fac ((evaluation R Y).mapCocone s)
        dsimp at h₁ h₂ ⊢
        simp only [← reassoc_of% h₁, ← Functor.map_comp, h₂, Hom.naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Types

Goal state before:
pp: C✝ : Type v₂
inst✝¹ : Category.{v₁, v₂} C✝
C : Type v₁
inst✝ : SmallCategory C
F : C ⥤ Type v₁
this : ∀ (X : Type v₁), PreservesColimits (tensorLeft X)
⊢ Closed F

Tactic:
letI : PreservesColimits (tensorLeft F) := ⟨by infer_instance⟩

Goal state after:
C✝ : Type v₂
inst✝¹ : Category.{v₁, v₂} C✝
C : Type v₁
inst✝ : SmallCategory C
F : C ⥤ Type v₁
this✝ : ∀ (X : Type v₁), PreservesColimits (tensorLeft X)
this : PreservesColimits (tensorLeft F) :=
  { preservesColimitsOfShape := @instMonoidalClosedFunctorType._proof_2 C inst✝ F }
⊢ Closed F
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsSifted C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
e : D ≌ C
this : D × D ≌ C × C := e.prod e
c : C
⊢ (e.inverse ⋙ Functor.diag D ⋙ this.functor).obj c ≅ (Functor.diag C).obj c

Tactic:
dsimp [this]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsSifted C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
e : D ≌ C
this : D × D ≌ C × C := e.prod e
c : C
⊢ (e.functor.obj (e.inverse.obj c), e.functor.obj (e.inverse.obj c)) ≅ (c, 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
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
m : (coconeOfCoconeUncurry Q c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfCoconeUncurry Q c).ι.app j ≫ m = s.ι.app j
⊢ m = P.desc { pt := s.pt, ι := { app := fun p ↦ (D.obj p.1).ι.app p.2 ≫ s.ι.app p.1, naturality := ⋯ } }

Tactic:
refine P.uniq
      { pt := s.pt
        ι := _ } m ?_

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
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
m : (coconeOfCoconeUncurry Q c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfCoconeUncurry Q c).ι.app j ≫ m = s.ι.app j
⊢ ∀ (j : J × K),
    c.ι.app j ≫ m = { pt := s.pt, ι := { app := fun p ↦ (D.obj p.1).ι.app p.2 ≫ s.ι.app p.1, naturality := ⋯ } }.ι.app j
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 : C ⥤ D
h : F.rightAdjointObjIsDefined = ⊤
⊢ F.IsLeftAdjoint

Tactic:
replace h : ∀ X, IsRepresentable (F.op ⋙ yoneda.obj X) := fun X ↦ by
    simp only [← rightAdjointObjIsDefined_iff, h, Pi.top_apply, Prop.top_eq_true]
  exact (Adjunction.adjunctionOfEquivRight
    (fun X Y ↦ (F.op ⋙ yoneda.obj Y).representableBy.homEquiv.symm)
    (fun X Y Y' g f ↦ (RepresentableBy.comp_homEquiv_symm ..).symm)).isLeftAdjoint

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

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₁₂ : F₀₁ ⋙ F₁₂ ⟶ F₀₂
τ₀₂₃ : F₀₂ ⋙ F₂₃ ⟶ F₀₃
⊢ (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))) ((F₀₁.associator F₁₂ F₂₃).inv ≫ whiskerRight τ₀₁₂ F₂₃ ≫ τ₀₂₃) ≫
      (conjugateEquiv (adj₀₁.comp (adj₁₂.comp adj₂₃)) ((adj₀₁.comp adj₁₂).comp adj₂₃)) (F₀₁.associator F₁₂ F₂₃).hom =
    (conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃)) τ₀₂₃ ≫ G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)) τ₀₁₂)

Tactic:
← conjugateEquiv_whiskerRight _ _ adj₂₃,

Goal state after:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₁₂ : F₀₁ ⋙ F₁₂ ⟶ F₀₂
τ₀₂₃ : F₀₂ ⋙ F₂₃ ⟶ F₀₃
⊢ (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))) ((F₀₁.associator F₁₂ F₂₃).inv ≫ whiskerRight τ₀₁₂ F₂₃ ≫ τ₀₂₃) ≫
      (conjugateEquiv (adj₀₁.comp (adj₁₂.comp adj₂₃)) ((adj₀₁.comp adj₁₂).comp adj₂₃)) (F₀₁.associator F₁₂ F₂₃).hom =
    (conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃)) τ₀₂₃ ≫
      (conjugateEquiv (adj₀₂.comp adj₂₃) ((adj₀₁.comp adj₁₂).comp adj₂₃)) (whiskerRight τ₀₁₂ F₂₃)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X : Cᵒᵖ
x : ↑(M.obj (F.op.obj X))
⊢ (ModuleCat.Hom.hom (M.map (F.op.map (𝟙 X)))) x =
    (ModuleCat.Hom.hom
        ((ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((F.op ⋙ R).map (𝟙 X))) ⋯).inv.app
          (ModuleCat.of ↑((F.op ⋙ R).obj X) ↑(M.obj (F.op.obj X)))))
      x

Tactic:
exact (M.congr_map_apply (F.op.map_id X) x).trans (by simp)

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✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ 𝟙 x✝¹ ▷ x✝ = 𝟙 (x✝¹ ⊗ x✝)

Tactic:
by
    ext1 X
    apply MonoidalCategory.id_whiskerRight (C := ModuleCat (R.obj X))

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
X : C
S : Sieve X
⊢ S ∈ (sInf s) X ↔ ∀ t ∈ s, S ∈ t X

Tactic:
change S ∈ sInf (sieves '' s) X ↔ _

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
X : C
S : Sieve X
⊢ S ∈ sInf (sieves '' s) X ↔ ∀ t ∈ s, S ∈ t X
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
⊢ K.toGrothendieck ≤ J ↔ K ≤ J.toPretopology

Tactic:
by
    constructor
    · intro h X R hR
      exact h _ ⟨_, hR, Sieve.le_generate R⟩
    · rintro h X S ⟨R, hR, RS⟩
      apply J.superset_covering _ (h _ hR)
      rwa [Sieve.giGenerate.gc]

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

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y✝ : ι → C
f : (i : ι) → Y✝ i ⟶ X
Y : C
i : ι
⊢ ∃ y, Y✝ y = Y✝ i ∧ f y ≍ f i

Tactic:
exact ⟨_, rfl, HEq.refl _⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x y : FamilyOfElements P R
H : ∀ {Y : C} (f : Y ⟶ X) (hf : R f), x f hf = y f hf
⊢ x = y

Tactic:
funext Z f hf
  exact H f hf

Goal state after: