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
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticMap.IsometryEquiv Q₁ Q₂
⊢ e.symm.toIsometry.comp e.toIsometry = QuadraticMap.Isometry.id Q₁

Tactic:
ext m

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 : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticMap.IsometryEquiv Q₁ Q₂
m : M₁
⊢ (e.symm.toIsometry.comp e.toIsometry) m = (QuadraticMap.Isometry.id Q₁) m
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
n : ℕ
⊢ ↑(n + 1) = ↑n + 1

Tactic:
simp_rw [NatCast.natCast, GSemiring.natCast_succ]
    rw [map_add]
    rfl

Goal state after:
Module: Mathlib.Algebra.DirectSum.Algebra

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ (of A 0) (GAlgebra.toFun r) * (of A i) xi = (of A i) xi * (of A 0) (GAlgebra.toFun r)

Tactic:
rw [of_mul_of, of_mul_of]

Goal state after:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ (of A (0 + i)) (GradedMonoid.GMul.mul (GAlgebra.toFun r) xi) =
    (of A (i + 0)) (GradedMonoid.GMul.mul xi (GAlgebra.toFun r))
Module: Mathlib.Algebra.DirectSum.Decomposition

Goal state before:
pp: ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid M
inst✝⁴ : SetLike σ M
inst✝³ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝² : Decomposition ℳ
P : Type u_5
inst✝¹ : SetLike P M
inst✝ : AddSubmonoidClass P M
p : P
hp : SetLike.IsHomogeneous ℳ p
x : M
⊢ x ∈ p ↔ ∀ (i : ι), ↑(((decompose ℳ) x) i) ∈ p

Tactic:
by
  classical
  refine ⟨fun hx i ↦ hp i hx, fun hx ↦ ?_⟩
  rw [← DirectSum.sum_support_decompose ℳ x]
  exact sum_mem (fun i _ ↦ hx i)

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✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : IsUnit 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ Q₁ = Q₂

Tactic:
apply h.smul_left_cancel.mp

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : IsUnit 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ 2 • Q₁ = 2 • Q₂
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✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Invertible 2
⊢ ⟨⅟2, ⋯⟩ • 1 * 2 = 1

Tactic:
ext m

Goal state after:
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✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Invertible 2
m : M
⊢ (⟨⅟2, ⋯⟩ • 1 * 2) m = 1 m
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✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Invertible 2
⊢ 2 * ⟨⅟2, ⋯⟩ • 1 = 1

Tactic:
ext m

Goal state after:
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✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Invertible 2
m : M
⊢ (2 * ⟨⅟2, ⋯⟩ • 1) m = 1 m
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case zero
K : Type v
inst✝³ : Field K
hK : Invertible 2
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hd : finrank K V = 0
⊢ ∃ v, IsOrthoᵢ B ⇑v

Tactic:
exact ⟨basisOfFinrankZero hd, fun _ _ _ => map_zero _⟩

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

Goal state before:
pp: case mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * (ι Q) m)
x✝ : CliffordAlgebra Q
i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
⊢ P x

Tactic:
induction hx using Submodule.pow_induction_on_right' with
    | algebraMap r => exact algebraMap r
    | add _x _y _i _ _ ihx ihy => exact add _ _ ihx ihy
    | mul_mem _i x _hx px m hm =>
      obtain ⟨m, rfl⟩ := hm
      exact mul_ι _ _ px

Goal state after:
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₂
f : MultilinearMap R M M₂
x y : M 0
⊢ mk' (fun m ↦ f (Fin.cons (x + y) m)) ⋯ ⋯ = mk' (fun m ↦ f (Fin.cons x m)) ⋯ ⋯ + mk' (fun m ↦ f (Fin.cons y m)) ⋯ ⋯

Tactic:
ext m

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₂
f : MultilinearMap R M M₂
x y : M 0
m : (i : Fin n) → M i.succ
⊢ (mk' (fun m ↦ f (Fin.cons (x + y) m)) ⋯ ⋯) m =
    (mk' (fun m ↦ f (Fin.cons x m)) ⋯ ⋯ + mk' (fun m ↦ f (Fin.cons y m)) ⋯ ⋯) m
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₂
f : MultilinearMap R M M₂
c : R
x : M 0
⊢ mk' (fun m ↦ f (Fin.cons (c • x) m)) ⋯ ⋯ = (RingHom.id R) c • mk' (fun m ↦ f (Fin.cons x m)) ⋯ ⋯

Tactic:
ext m

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₂
f : MultilinearMap R M M₂
c : R
x : M 0
m : (i : Fin n) → M i.succ
⊢ (mk' (fun m ↦ f (Fin.cons (c • x) m)) ⋯ ⋯) m = ((RingHom.id R) c • mk' (fun m ↦ f (Fin.cons x m)) ⋯ ⋯) m
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₂
f : MultilinearMap R M M₂
⊢ f.curryLeft.uncurryLeft = f

Tactic:
ext m

Goal state after:
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₂
f : MultilinearMap R M M₂
m : (i : Fin n.succ) → M i
⊢ f.curryLeft.uncurryLeft m = f m
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
⊢ (DirectSum.coeAlgHom (evenOdd Q)).comp ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) = AlgHom.id R (CliffordAlgebra Q)

Tactic:
ext m

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
m : M
⊢ (((DirectSum.coeAlgHom (evenOdd Q)).comp ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩)).toLinearMap ∘ₗ ι Q) m =
    ((AlgHom.id R (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q) m
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₂
f : MultilinearMap R M M₂
⊢ f.curryRight.uncurryRight = f

Tactic:
ext m

Goal state after:
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₂
f : MultilinearMap R M M₂
m : (i : Fin n.succ) → M i
⊢ f.curryRight.uncurryRight m = f m
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : ↑(powersetCard α n)
⊢ ↑(map n f s) = ⇑f '' ↑s

Tactic:
by
  ext
  simp [mem_map_iff_mem_range]

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

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

Tactic:
apply Finset.orderEmbOfFin_unique'

Goal state after:
n : ℕ
I : Type u_1
inst✝ : LinearOrder I
f : Fin n ↪o I
⊢ ∀ (x : Fin n), f x ∈ ↑((fun f ↦ ofFinEmb n I f.toEmbedding) f)
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 : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] N
⊢ (map f).toLinearMap.compAlternatingMap (ιMulti R n) = (ιMulti R n).compLinearMap f

Tactic:
ext m

Goal state after:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] N
m : Fin n → M
⊢ ((map f).toLinearMap.compAlternatingMap (ιMulti R n)) m = ((ιMulti R n).compLinearMap f) m
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: case h
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (hom ((F ⋙ forget (ModuleCat R)).map f)) x.snd = (hom ((F ⋙ forget (ModuleCat R)).map g)) y.snd
⊢ (hom (F.map f)) ⟨x.fst, r • x.snd⟩.snd = (hom (F.map g)) ⟨y.fst, r • y.snd⟩.snd

Tactic:
simp only [Functor.comp_obj, Functor.comp_map, ConcreteCategory.hom_ofHom,
    TypeCat.Fun.coe_mk] at hfg

Goal state after:
case h
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (hom (F.map f)) x.snd = (hom (F.map g)) y.snd
⊢ (hom (F.map f)) ⟨x.fst, r • x.snd⟩.snd = (hom (F.map g)) ⟨y.fst, r • y.snd⟩.snd
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₃ n
h₂ : HasInjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₁ : Ext Y S.X₃ i
⊢ x₁.comp hS.extClass ⋯ = 0

Tactic:
x₁.eq_zero_of_hasInjectiveDimensionLT n (by lia),

Goal state after:
case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₃ n
h₂ : HasInjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₁ : Ext Y S.X₃ i
⊢ Ext.comp 0 hS.extClass ⋯ = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: case bot
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hd : injectiveDimension X = ⊥
⊢ ∃ n, HasInjectiveDimensionLE X n

Tactic:
exact ⟨0, by simp [← injectiveDimension_le_iff, hd]⟩

Goal state after:
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
I : Type u_4
inst✝ : LinearOrder I
v : I → M
hv : Submodule.span R (Set.range v) = ⊤
y✝ : ↑(Set.powersetCard I n)
⊢ (Subtype.val ∘ ιMulti_family R n v) y✝ ∈ ⋀[R]^n M

Tactic:
comp_apply

Goal state after:
case a
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 (Set.range v) = ⊤
y✝ : ↑(Set.powersetCard I n)
⊢ ↑(ιMulti_family R n v y✝) ∈ ⋀[R]^n M
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
M : ModuleCat R
⊢ (λ_ ((extendScalars f).obj M)).inv =
    (extendScalars f).map (λ_ M).inv ≫
      (AlgebraTensorModule.distribBaseChange R S ↑(𝟙_ (ModuleCat R)) ↑M).symm.toModuleIso.inv ≫
        (AlgebraTensorModule.rid R S S).symm.toModuleIso.inv ▷ (extendScalars f).obj M

Tactic:
ext m

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
M : ModuleCat R
m : ↑M
⊢ (ConcreteCategory.hom (λ_ ((extendScalars f).obj M)).inv) (1 ⊗ₜ[R] m) =
    (ConcreteCategory.hom
        ((extendScalars f).map (λ_ M).inv ≫
          (AlgebraTensorModule.distribBaseChange R S ↑(𝟙_ (ModuleCat R)) ↑M).symm.toModuleIso.inv ≫
            (AlgebraTensorModule.rid R S S).symm.toModuleIso.inv ▷ (extendScalars f).obj M))
      (1 ⊗ₜ[R] m)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
M : ModuleCat R
⊢ (ρ_ ((extendScalars f).obj M)).inv =
    (extendScalars f).map (ρ_ M).inv ≫
      (AlgebraTensorModule.distribBaseChange R S ↑M ↑(𝟙_ (ModuleCat R))).symm.toModuleIso.inv ≫
        (extendScalars f).obj M ◁ (AlgebraTensorModule.rid R S S).symm.toModuleIso.inv

Tactic:
ext m

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
M : ModuleCat R
m : ↑M
⊢ (ConcreteCategory.hom (ρ_ ((extendScalars f).obj M)).inv) (1 ⊗ₜ[R] m) =
    (ConcreteCategory.hom
        ((extendScalars f).map (ρ_ M).inv ≫
          (AlgebraTensorModule.distribBaseChange R S ↑M ↑(𝟙_ (ModuleCat R))).symm.toModuleIso.inv ≫
            (extendScalars f).obj M ◁ (AlgebraTensorModule.rid R S S).symm.toModuleIso.inv))
      (1 ⊗ₜ[R] m)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: case left
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
X Y : J ⥤ C
j : J
⊢ (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).π.app { as := WalkingPair.left } =
    (Iso.refl (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).pt).hom ≫
      ((Cone.postcompose
                  (mapPairIso (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.left }))
                      (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.right }))).hom).obj
              (((evaluation J C).obj j).mapCone
                (BinaryFan.mk { app := fun x ↦ fst (X.obj x) (Y.obj x), naturality := ⋯ }
                  { app := fun x ↦ snd (X.obj x) (Y.obj x), naturality := ⋯ }))).π.app
        { as := WalkingPair.left }

pp: case right
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
X Y : J ⥤ C
j : J
⊢ (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).π.app { as := WalkingPair.right } =
    (Iso.refl (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).pt).hom ≫
      ((Cone.postcompose
                  (mapPairIso (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.left }))
                      (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.right }))).hom).obj
              (((evaluation J C).obj j).mapCone
                (BinaryFan.mk { app := fun x ↦ fst (X.obj x) (Y.obj x), naturality := ⋯ }
                  { app := fun x ↦ snd (X.obj x) (Y.obj x), naturality := ⋯ }))).π.app
        { as := WalkingPair.right }

Tactic:
all_goals cat_disch

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

Goal state before:
pp: case refine_1.refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
⊢ f ⟶ StructuredArrow.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t))

Tactic:
exact StructuredArrow.homMk (IsFiltered.leftToMax _ _ ≫ t) rfl

Goal state after:
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
d : D
inst✝ : IsCofiltered (CostructuredArrow F d)
c₁ c₂ : C
s₁ : F.obj c₁ ⟶ d
s₂ : F.obj c₂ ⟶ d
⊢ ∃ c t₁ t₂, F.map t₁ ≫ s₁ = F.map t₂ ≫ s₂

Tactic:
by
  obtain ⟨W, p₁, p₂, -⟩ := IsCofilteredOrEmpty.cone_objs
    (CostructuredArrow.mk s₁) (CostructuredArrow.mk s₂)
  exact ⟨W.left, p₁.left, p₂.left, (CostructuredArrow.w p₁).trans (CostructuredArrow.w p₂).symm⟩

Goal state after:
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✝² : IsCofiltered D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
⊢ Nonempty C

Tactic:
have : Nonempty D := IsCofiltered.nonempty
      obtain ⟨c, -⟩ := h (Classical.arbitrary D)
      exact ⟨c⟩

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

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : FinallySmall J
i : J
⊢ ∃ j ∈ Set.range (fromFinalModel J).obj, Nonempty (i ⟶ j)

Tactic:
obtain ⟨f⟩ : Nonempty (StructuredArrow i (fromFinalModel J)) := IsConnected.is_nonempty

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : FinallySmall J
i : J
f : StructuredArrow i (fromFinalModel J)
⊢ ∃ j ∈ Set.range (fromFinalModel J).obj, Nonempty (i ⟶ j)
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✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
Q : DiagramOfCones (curry.obj G) := DiagramOfCones.mkOfHasLimits (curry.obj G)
Q' : (j : J) → IsLimit (Q.obj j) := fun j ↦ limit.isLimit ((curry.obj G).obj j)
c' : Cone G
f : c'.pt ⟶ (coneOfHasLimitCurryCompLim G).pt
h : ∀ (j : J × K), f ≫ (coneOfHasLimitCurryCompLim G).π.app j = c'.π.app j
⊢ f = limit.lift (curry.obj G ⋙ lim) (coneOfConeCurry G Q' c')

Tactic:
dsimp [coneOfHasLimitCurryCompLim] at f h ⊢
      refine limit.hom_ext (F := curry.obj G ⋙ lim) (fun j ↦ limit.hom_ext (fun k ↦ ?_))
      simp [h ⟨j, k⟩, Q']

Goal state after:
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
φ : F ⟶ G.presheaf ⋙ forget Ab
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (freeObj F).map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (ModuleCat.freeDesc (φ.app Y)) =
    ModuleCat.freeDesc (φ.app X) ≫ G.map f

Tactic:
dsimp
    ext x
    simpa using! NatTrans.naturality_apply φ f x

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
⊢ map hcR hcM hcM (𝟙 M) = LinearMap.id

Tactic:
ext m

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 : ModuleColimit hcR hcM
⊢ (map hcR hcM hcM (𝟙 M)) m = LinearMap.id m
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'
f : M ⟶ M'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
g : M' ⟶ M''
⊢ map hcR hcM' hcM'' g ∘ₗ map hcR hcM hcM' f = map hcR hcM hcM'' (f ≫ g)

Tactic:
ext m

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'
f : M ⟶ M'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
g : M' ⟶ M''
m : ModuleColimit hcR hcM
⊢ (map hcR hcM' hcM'' g ∘ₗ map hcR hcM hcM' f) m = (map hcR hcM hcM'' (f ≫ g)) m
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
inst✝¹ : Category.{v_1, u_1} C₀
inst✝ : Category.{v_2, u_2} C₁
F₀₀' : C₀ ⥤ C₀
F₀'₁ : C₀ ⥤ C₁
G₀'₀ : C₀ ⥤ C₀
G₁₀' : C₁ ⥤ C₀
adj₀₀' : F₀₀' ⊣ G₀'₀
adj₀'₁ : F₀'₁ ⊣ G₁₀'
e₀'₀ : G₀'₀ ≅ 𝟭 C₀
X₀ : C₀
h₁ :
  F₀'₁.map (F₀₀'.map (G₀'₀.map (adj₀'₁.unit.app X₀))) ≫ F₀'₁.map (adj₀₀'.counit.app (G₁₀'.obj (F₀'₁.obj X₀))) =
    F₀'₁.map (adj₀₀'.counit.app X₀) ≫ F₀'₁.map (adj₀'₁.unit.app X₀)
h₂ :
  F₀'₁.map (F₀₀'.map (adj₀'₁.unit.app X₀)) ≫ F₀'₁.map (F₀₀'.map (e₀'₀.inv.app (G₁₀'.obj (F₀'₁.obj X₀)))) =
    F₀'₁.map (F₀₀'.map (e₀'₀.inv.app X₀)) ≫ F₀'₁.map (F₀₀'.map (G₀'₀.map (adj₀'₁.unit.app X₀)))
⊢ (adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ (G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor)).hom.app X₀ =
    (isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor).hom.app X₀

Tactic:
simp [leftAdjointCompIso_hom_app, leftAdjointIdIso_hom_app,
    reassoc_of% h₂, reassoc_of% h₁]

Goal state after: