mathlib-initiative/mathlib-tactics huggingface dataset:
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
i : n'
j : m'
⊢ (∑ i_1,
      ((Pi.basisFun R m).repr (r (Pi.single j 1))).sum fun j yj ↦
        ((Pi.basisFun R n).repr (l (Pi.single i 1))) i_1 •> yj •> (B ((Pi.basisFun R n) i_1)) ((Pi.basisFun R m) j)) =
    ∑ y,
      ∑ x,
        of (fun i j ↦ l (Pi.single j 1) i) y i * (B (Pi.single y 1)) (Pi.single x 1) *
          of (fun i j ↦ r (Pi.single j 1) i) x j

Tactic:
apply sum_congr rfl
    rintro i' -
    rw [Finsupp.sum_fintype]
    · apply sum_congr rfl
      rintro j' -
      simp only [smul_eq_mul, Pi.basisFun_repr, mul_assoc, mul_comm, mul_left_comm,
        Pi.basisFun_apply, of_apply]
    · intros
      simp only [zero_smul, smul_zero]

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

Goal state before:
pp: n : Type u_11
m : Type u_12
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 m'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (m' → R) →ₗ[R] m → R
⊢ (toMatrix₂' R) (B.compl₂ f) = (toMatrix₂' R) B * toMatrix' f

Tactic:
rw [← LinearMap.comp_id B, ← LinearMap.compl₁₂]
  simp

Goal state after:
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
⊢ ↑0 = 0

Tactic:
simp only [NatCast.natCast, GSemiring.natCast_zero, map_zero]

Goal state after:
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:
by
    simp_rw [NatCast.natCast, GSemiring.natCast_succ]
    rw [map_add]
    rfl

Goal state after:
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
a : A 0
⊢ (of A 0) 1 = 1

Tactic:
DirectSum.of_zero_one

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a : A 0
⊢ 1 = 1
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
⊢ Function.Injective polarBilin

Tactic:
intro Q₁ Q₂ h₁₂

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
⊢ Q₁ = Q₂
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ A₁ ∈ pairSelfAdjointMatricesSubmodule J J₂ ↔ J.IsAdjointPair J₂ A₁ A₁

Tactic:
simp only [pairSelfAdjointMatricesSubmodule, Submodule.mem_map_equiv,
    mem_isPairSelfAdjointSubmodule, toMatrix'_symm, ← isAdjointPair_toLinearMap₂',
    IsPairSelfAdjoint, toLin'_apply']

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

Goal state before:
pp: R : Type u_3
N : Type u_5
P : Type u_6
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
m : Type w
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : AddCommGroup P
inst✝ : Module R P
b' : Basis m R P
Q : QuadraticForm R P
f : N →ₗ[R] P
⊢ toMatrix b (QuadraticMap.comp Q f) = ((LinearMap.toMatrix b b') f)ᵀ * toMatrix b' Q * (LinearMap.toMatrix b b') f

Tactic:
by
  simp only [QuadraticMap.associated_comp, LinearMap.toMatrix₂_compl₁₂ b' b', toMatrix]

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
n : ZMod 2
⊢ Submodule.comap reverse (evenOdd Q n) = evenOdd Q n

Tactic:
by
  rw [← submodule_map_reverse_eq_comap, evenOdd_map_reverse]

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₂ : M
⊢ (ι Q) m₁ * (ι Q) m₂ ∈ (ι Q).range ^ ↑⟨2, ⋯⟩

Tactic:
by
      rw [Subtype.coe_mk, pow_two]
      exact
        Submodule.mul_mem_mul (LinearMap.mem_range_self (ι Q) m₁)
          (LinearMap.mem_range_self (ι Q) m₂)

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
⊢ ∀ (val : ℕ) (property : ↑val = n) (x : CliffordAlgebra Q) (hx : x ∈ (ι Q).range ^ val), motive x ⋯

Tactic:
ZMod.natCast_eq_iff,

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
⊢ ∀ (val : ℕ) (property : ∃ k, val = n.val + 2 * k) (x : CliffordAlgebra Q) (hx : x ∈ (ι Q).range ^ val), motive x ⋯
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: n : ℕ
β : Type u_2
s : Finset β
hs : s ∈ powersetCard β n
⊢ Fintype.card ?m.22 = #?m.25

Tactic:
hs,

Goal state after:
n : ℕ
β : Type u_2
s : Finset β
hs : s ∈ powersetCard β n
⊢ Fintype.card ?m.22 = n
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem_mul_mem.add
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 a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n✝.val
x y : CliffordAlgebra Q
n : ℕ
hx : x ∈ ((ι Q).range ^ 2) ^ n
hy : y ∈ ((ι Q).range ^ 2) ^ n
ihx : motive (x * b) ⋯
ihy : motive (y * b) ⋯
⊢ motive ((x + y) * b) ⋯

Tactic:
simp_rw [add_mul]

Goal state after:
case mem_mul_mem.add
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 a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n✝.val
x y : CliffordAlgebra Q
n : ℕ
hx : x ∈ ((ι Q).range ^ 2) ^ n
hy : y ∈ ((ι Q).range ^ 2) ^ n
ihx : motive (x * b) ⋯
ihy : motive (y * b) ⋯
⊢ motive (x * b + y * b) ⋯
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: case inr.succ
α : Type u_1
val✝ : Infinite α
n : ℕ
⊢ Nat.card ↑(powersetCard α (n + 1)) = (Nat.card α).choose (n + 1)

Tactic:
Nat.card_eq_zero_of_infinite (α := α),

Goal state after:
case inr.succ
α : Type u_1
val✝ : Infinite α
n : ℕ
⊢ Nat.card ↑(powersetCard α (n + 1)) = Nat.choose 0 (n + 1)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem_mul_mem.mem_mul.add
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 a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x✝ : CliffordAlgebra Q
n'' : ℕ
y✝ : CliffordAlgebra Q
hy✝ : y✝ ∈ ((ι Q).range ^ 2) ^ n''
ihy✝ : motive (y✝ * b) ⋯
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range * (ι Q).range
y : CliffordAlgebra Q
hy : y ∈ (ι Q).range * (ι Q).range
ihx : motive (x * y✝ * b) ⋯
ihy : motive (y * y✝ * b) ⋯
⊢ motive ((x + y) * y✝ * b) ⋯

Tactic:
simp_rw [add_mul]

Goal state after:
case mem_mul_mem.mem_mul.add
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 a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x✝ : CliffordAlgebra Q
n'' : ℕ
y✝ : CliffordAlgebra Q
hy✝ : y✝ ∈ ((ι Q).range ^ 2) ^ n''
ihy✝ : motive (y✝ * b) ⋯
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range * (ι Q).range
y : CliffordAlgebra Q
hy : y ∈ (ι Q).range * (ι Q).range
ihx : motive (x * y✝ * b) ⋯
ihy : motive (y * y✝ * b) ⋯
⊢ motive (x * y✝ * b + y * y✝ * b) ⋯
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case refine_1
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
h : (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r
this : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
⊢ x = 0 ∧ r = 0

Tactic:
have : IsCentralScalar R M := ⟨fun r m => rfl⟩

Goal state after:
case refine_1
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
h : (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R M
⊢ x = 0 ∧ r = 0
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
f : M →ₗ[R] N
this : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
⊢ ιInv ∘ₗ (map f).toLinearMap = f ∘ₗ ιInv

Tactic:
have : IsCentralScalar R M := ⟨fun r m => rfl⟩

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
f : M →ₗ[R] N
this✝ : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R M
⊢ ιInv ∘ₗ (map f).toLinearMap = f ∘ₗ ιInv
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
⊢ Module.rank R ↑S.X₂ = Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃

Tactic:
have := free_shortExact hS'
  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]
  exact ⟨Basis.indexEquiv (Module.Free.chooseBasis R S.X₂) (Basis.ofShortExact hS'
    (Module.Free.chooseBasis R S.X₁) (Module.Free.chooseBasis R S.X₃))⟩

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : Small.{v, u} R
inst✝ : Small.{v', u} R
M : ModuleCat R
N : ModuleCat R
e : ↑M ≃ₗ[R] ↑N
n : ℕ
⊢ HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n

Tactic:
by
  let eM : M ≃ₗ[R] ModuleCat.of R (ULift.{v'} M) := ULift.moduleEquiv.symm
  rw [hasInjectiveDimensionLE_iff_of_linearEquiv_aux eM,
    ← hasInjectiveDimensionLE_iff_of_linearEquiv_aux (e.symm.trans eM)]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Submonoid R
M₁ M₂ M₃ : ModuleCat R
f₁ : M₁ ⟶ M₂
f₂ : M₂ ⟶ M₃
h₁ : IsLocalizedModule S (Hom.hom f₁)
h₂ : IsLocalizedModule S (Hom.hom (f₁ ≫ f₂))
⊢ IsIso f₂

Tactic:
have : Function.Bijective f₂.hom := by
    rw [← IsLocalizedModule.linearEquiv_of_isLocalizedModule_comp S f₁.hom f₂.hom]
    exact (IsLocalizedModule.linearEquiv ..).bijective

Goal state after:
R : Type u
inst✝ : CommRing R
S : Submonoid R
M₁ M₂ M₃ : ModuleCat R
f₁ : M₁ ⟶ M₂
f₂ : M₂ ⟶ M₃
h₁ : IsLocalizedModule S (Hom.hom f₁)
h₂ : IsLocalizedModule S (Hom.hom (f₁ ≫ f₂))
this : Function.Bijective ⇑(Hom.hom f₂)
⊢ IsIso f₂
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
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
this : IsFiltered P.FullSubcategory
G : FinalModel C₀ ⥤ P.FullSubcategory :=
  { obj := fun X ↦ { obj := (fromFinalModel C₀).obj X, property := ⋯ },
    map := fun {X Y} f ↦ ObjectProperty.homMk ((fromFinalModel C₀).map f), map_id := ⋯, map_comp := ⋯ }
⊢ ∃ D, ∃ (_ : Small.{w, u} D), ∃ x, ∃ (_ : IsFiltered D), ∃ F, F.Final

Tactic:
have : (G ⋙ P.ι).Final := inferInstanceAs (fromFinalModel.{w} C₀).Final

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
this✝ : IsFiltered P.FullSubcategory
G : FinalModel C₀ ⥤ P.FullSubcategory :=
  { obj := fun X ↦ { obj := (fromFinalModel C₀).obj X, property := ⋯ },
    map := fun {X Y} f ↦ ObjectProperty.homMk ((fromFinalModel C₀).map f), map_id := ⋯, map_comp := ⋯ }
this : (G ⋙ P.ι).Final
⊢ ∃ D, ∃ (_ : Small.{w, u} D), ∃ x, ∃ (_ : IsFiltered D), ∃ F, F.Final
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 : Type u
w✝² : Small.{w, u} D
w✝¹ : Category.{w, u} D
w✝ : IsFiltered D
F : D ⥤ C₀
h✝ : F.Final
e : D ≌ SmallModel.{w, w, u} D := equivSmallModel D
⊢ ∃ D x, ∃ (_ : IsFiltered D), ∃ F, F.Final

Tactic:
exact ⟨_, _, of_equivalence e, e.inverse ⋙ F, inferInstance⟩

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₃₀
τ₀₁₂ : G₂₀ ⟶ G₂₁ ⋙ G₁₀
τ₀₂₃ : G₃₀ ⟶ G₃₂ ⋙ G₂₀
⊢ (F₀₁.associator F₁₂ F₂₃).inv ≫
      whiskerRight (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ τ₀₁₂) F₂₃ ≫
        adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ τ₀₂₃ =
    (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm
      (τ₀₂₃ ≫ G₃₂.whiskerLeft τ₀₁₂ ≫ (G₃₂.associator G₂₁ G₁₀).inv)

Tactic:
obtain ⟨τ₀₁₂, rfl⟩ := (conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)).surjective τ₀₁₂
  obtain ⟨τ₀₂₃, rfl⟩ := (conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃)).surjective τ₀₂₃
  apply (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).injective
  simp only [Equiv.apply_symm_apply, Equiv.symm_apply_apply, leftAdjointCompNatTrans]
  rw [← cancel_mono (associator G₃₂ G₂₁ G₁₀).hom, Category.assoc, Category.assoc,
    Iso.inv_hom_id, Category.comp_id, ← conjugateEquiv_associator_hom adj₀₁ adj₁₂ adj₂₃,
    ← conjugateEquiv_whiskerRight _ _ adj₂₃, conjugateEquiv_comp, Iso.hom_inv_id_assoc,
    conjugateEquiv_comp]

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 : Cᵒᵖ
⊢ (𝟙 x✝¹ ▷ x✝).app X = (𝟙 (x✝¹ ⊗ x✝)).app X

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

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
⊢ (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ J.coverings S

Tactic:
let σ' (i : ι') : Type (max u v) := (Presieve.ofArrows (Y i.2.idx) (g i.2.idx)).uncurry

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
σ' : ι' → Type (max u v) :=
  fun i ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯))).uncurry
⊢ (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ J.coverings S
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : (fun J X ↦ J.sieves X) J₁ = (fun J X ↦ J.sieves X) J₂
⊢ J₁ = J₂

Tactic:
cases J₁; cases J₂; congr

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J✝ : GrothendieckTopology C
T : Set (GrothendieckTopology C)
X Y : C
S : Sieve X
hS : Y ⟶ X
f : S ∈ sInf (sieves '' T) X
J : GrothendieckTopology C
hJ : J ∈ T
⊢ Sieve.pullback hS S ∈ (fun f ↦ ↑f Y) ⟨J.sieves, ⋯⟩

Tactic:
apply J.pullback_stable _ (f _ ⟨⟨_, _, hJ, rfl⟩, rfl⟩)

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
s : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
Y✝ Y : C
u : Y ⟶ X
hu : s u
⊢ ⟨(limit.cone (cospan u b)).1, (limit.cone (cospan u b)).π.1 WalkingCospan.right⟩ ∈
    (fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) '' s.uncurry

Tactic:
exact ⟨⟨Y, u⟩, hu, rfl⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z : C
f : Y✝ ⟶ X✝
S R : Sieve X✝
I : Type u_1
Y : I → C
X : C
⊢ ∀ {Y_1 Z : C} {f : Y_1 ⟶ X}, (∃ i, Nonempty (Y_1 ⟶ Y i)) → ∀ (g : Z ⟶ Y_1), ∃ i, Nonempty (Z ⟶ Y i)

Tactic:
by
    rintro Z₁ Z₂ p ⟨i, ⟨f⟩⟩ g
    exact ⟨i, ⟨g ≫ f⟩⟩

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

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
⊢ (ConcreteCategory.hom (firstMap P R)) x = (ConcreteCategory.hom (secondMap P R)) x →
    Presieve.FamilyOfElements.PullbackCompatible ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x)

Tactic:
intro t Y Z f g hf hg
    rw [Types.limit_ext_iff'] at t
    simpa [firstMap, secondMap] using t ⟨⟨⟨Y, f, hf⟩, Z, g, hg⟩⟩

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

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x →
    Arrows.PullbackCompatible P π ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x)

Tactic:
· intro t i j
    apply_fun Pi.π (fun (ij : I × I) ↦ P.obj (op (pullback (π ij.1) (π ij.2)))) ⟨i, j⟩ at t
    simpa [firstMap, secondMap] using t

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.plusObj P ⟶ Q
hγ : J.toPlus P ≫ γ = η
⊢ γ = J.plusMap η ≫ (J.isoToPlus Q hQ).inv

Tactic:
Iso.eq_comp_inv,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.plusObj P ⟶ Q
hγ : J.toPlus P ≫ γ = η
⊢ γ ≫ (J.isoToPlus Q hQ).hom = J.plusMap η
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G : Subfunctor F
f : F ⟶ F'
Δ Δ' : C
φ : Δ ⟶ Δ'
x : F.obj Δ
hx : x ∈ G.obj Δ
⊢ (ConcreteCategory.hom (f.app Δ')) ((ConcreteCategory.hom (F.map φ)) x) =
    (ConcreteCategory.hom (F'.map φ)) ((ConcreteCategory.hom (f.app Δ)) x)

Tactic:
apply NatTrans.naturality_apply

Goal state after: