mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case exists_of_eq.zero
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
a : A
m : ℕ
b : A
k : ℕ
hc : ↑⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ * (x ^ m * (a * g ^ n)) = ↑⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ * (x ^ n * (b * g ^ m))
hf : f ∈ 𝒜 0
hd : 0 ≠ 0
ha : a ∈ 𝒜 (n • 0)
hb : b ∈ 𝒜 (m • 0)
⊢ (fun x ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ 0) ^ (k + m + n) * a)) =
    (fun x ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ 0) ^ (k + m + n) * b))

pp: case exists_of_eq.succ
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
a : A
m : ℕ
b : A
k : ℕ
hc : ↑⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ * (x ^ m * (a * g ^ n)) = ↑⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ * (x ^ n * (b * g ^ m))
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
ha : a ∈ 𝒜 (n • (d + 1))
hb : b ∈ 𝒜 (m • (d + 1))
⊢ (fun x ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ (d + 1)) ^ (k + m + n) * a)) =
    (fun x ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ (d + 1)) ^ (k + m + n) * b))

Tactic:
· contradiction

Goal state after:
case exists_of_eq.succ
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
a : A
m : ℕ
b : A
k : ℕ
hc : ↑⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ * (x ^ m * (a * g ^ n)) = ↑⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ * (x ^ n * (b * g ^ m))
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
ha : a ∈ 𝒜 (n • (d + 1))
hb : b ∈ 𝒜 (m • (d + 1))
⊢ (fun x ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ (d + 1)) ^ (k + m + n) * a)) =
    (fun x ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ (d + 1)) ^ (k + m + n) * b))
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
⊢ Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x} = ⊤

Tactic:
by
  by_cases HH : Subsingleton (HomogeneousLocalization.Away 𝒜 f)
  · exact Subsingleton.elim _ _
  rw [← top_le_iff]
  rintro x -
  obtain ⟨⟨n, ⟨a, ha⟩, ⟨b, hb'⟩, ⟨j, (rfl : _ = b)⟩⟩, rfl⟩ := mk_surjective x
  by_cases hfj : f ^ j = 0
  · exact (HH (HomogeneousLocalization.subsingleton _ ⟨_, hfj⟩)).elim
  have : DirectSum.decompose 𝒜 a n = ⟨a, ha⟩ := Subtype.ext (DirectSum.decompose_of_mem_same 𝒜 ha)
  simp_rw [← this]
  clear this ha
  have : a ∈ Submodule.span (𝒜 0) (Submonoid.closure (Set.range v)) := by
    rw [← Algebra.adjoin_eq_span, hx]
    trivial
  induction this using Submodule.span_induction with
  | mem a ha' =>
    obtain ⟨ai, rfl⟩ := Submonoid.exists_of_mem_closure_range _ _ ha'
    clear ha'
    by_cases H : ∑ i, ai i • dv i = n
    · apply Submodule.subset_span
      refine ⟨j, ai, H.trans ?_, ?_⟩
      · exact DirectSum.degree_eq_of_mem_mem 𝒜 hb'
          (SetLike.pow_mem_graded j hf) hfj
      · ext
        simp only [val_mk, Away.val_mk]
        congr
        refine (DirectSum.decompose_of_mem_same _ ?_).symm
        exact H ▸ SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i
    · convert! zero_mem (Submodule.span (𝒜 0) _)
      ext
      have : (DirectSum.decompose 𝒜 (∏ i : ι', v i ^ ai i) n).1 = 0 := by
        refine DirectSum.decompose_of_mem_ne _ ?_ H
        exact SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i
      simp [this, Localization.mk_zero]
  | zero =>
    convert! zero_mem (Submodule.span (𝒜 0) _)
    ext; simp [Localization.mk_zero]
  | add s t hs ht hs' ht' =>
    convert! add_mem hs' ht'
    ext; simp [← Localization.add_mk_self]
  | smul r x hx hx' =>
    convert! Submodule.smul_mem _ r hx'
    ext
    simp [Algebra.smul_def, algebraMap_eq, fromZeroRingHom, Localization.mk_mul,
      -decompose_mul, coe_decompose_mul_of_left_mem_zero 𝒜 r.2]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec (CommRingCat.of ↑R)).Modules
f : M ⟶ N
r : (InducedCategory (TopologicalSpace.Opens ↥(Spec (CommRingCat.of ↑R))) PrimeSpectrum.basicOpen)ᵒᵖ
⊢ tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop r)) ≫
      (modulesSpecToSheaf.map (tilde.map ((modulesSpecToSheaf.map f).hom.app (op ⊤))) ≫
              modulesSpecToSheaf.map N.fromTildeΓ).hom.app
        (op (PrimeSpectrum.basicOpen (unop r))) =
    tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop r)) ≫
      (modulesSpecToSheaf.map M.fromTildeΓ ≫ modulesSpecToSheaf.map f).hom.app (op (PrimeSpectrum.basicOpen (unop r)))

Tactic:
tilde.toOpen_map_app_assoc,

Goal state after:
case h
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec (CommRingCat.of ↑R)).Modules
f : M ⟶ N
r : (InducedCategory (TopologicalSpace.Opens ↥(Spec (CommRingCat.of ↑R))) PrimeSpectrum.basicOpen)ᵒᵖ
⊢ (modulesSpecToSheaf.map f).hom.app (op ⊤) ≫
      tilde.toOpen ((modulesSpecToSheaf.obj N).obj.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop r)) ≫
        (modulesSpecToSheaf.map N.fromTildeΓ).hom.app (op (PrimeSpectrum.basicOpen (unop r))) =
    tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop r)) ≫
      (modulesSpecToSheaf.map M.fromTildeΓ ≫ modulesSpecToSheaf.map f).hom.app (op (PrimeSpectrum.basicOpen (unop r)))
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
⊢ Algebra.FiniteType (↥(𝒜 0)) (Away 𝒜 f)

Tactic:
constructor
  obtain ⟨s, hs, hs'⟩ := GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero 𝒜
  choose dx hdx hxd using Subtype.forall'.mp hs'
  simp_rw [Subalgebra.fg_def, ← top_le_iff,
    ← Away.adjoin_mk_prod_pow_eq_top hf (ι' := s) Subtype.val (by simpa) dx hxd]
  rcases d.eq_zero_or_pos with hd | hd
  · let f' := Away.mk 𝒜 hf 1 1 (by simp [hd, GradedOne.one_mem])
    refine ⟨{f'}, Set.finite_singleton f', ?_⟩
    rw [Algebra.adjoin_le_iff]
    rintro _ ⟨a, ai, hai, hai', rfl⟩
    obtain rfl : ai = 0 := funext <| by simpa [hd, hdx] using hai
    simp only [Finset.univ_eq_attach, Pi.zero_apply, pow_zero, Finset.prod_const_one, mem_coe]
    convert! pow_mem (Algebra.self_mem_adjoin_singleton (𝒜 0) f') a using 1
    ext
    simp [f', Localization.mk_pow]
  refine ⟨_, ?_, le_rfl⟩
  let b := ∑ i, dx i
  let s' : Set ((Fin (b + 1)) × (s → Fin (d + 1))) := { ai | ∑ i, (ai.2 i).1 * dx i = ai.1 * d }
  let F : s' → Away 𝒜 f := fun ai ↦ Away.mk 𝒜 hf ai.1.1.1 (∏ i, i ^ (ai.1.2 i).1)
    (by convert! SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i; exact ai.2.symm)
  apply (Set.finite_range F).subset
  rintro _ ⟨a, ai, hai, hai', rfl⟩
  refine ⟨⟨⟨⟨a, ?_⟩, fun i ↦ ⟨ai i, (hai' i).trans_lt d.lt_succ_self⟩⟩, hai⟩, rfl⟩
  rw [Nat.lt_succ_iff, ← mul_le_mul_iff_of_pos_right hd, ← smul_eq_mul, ← hai, Finset.sum_mul]
  simp_rw [smul_eq_mul, mul_comm _ d]
  gcongr
  exact hai' _

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
⊢ ⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) 0, ⋯⟩ = 0

Tactic:
by ext; simp only [map_zero, HomogeneousLocalization.val_zero, Proj.zero_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
⊢ (Scheme.ΓSpecIso (CommRingCat.of (A⁰_ f))).inv ≫
      (toSpec 𝒜 f).c.app (op ⊤) ≫ (Proj.restrict ⋯).presheaf.germ ((Opens.map (toSpec 𝒜 f).base).obj ⊤) x ⋯ =
    awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x

Tactic:
toOpen_toSpec_val_c_app_assoc

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
⊢ (awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.map (homOfLE ⋯).op) ≫
      (Proj.restrict ⋯).presheaf.germ ((Opens.map (toSpec 𝒜 f).base).obj ⊤) x ⋯ =
    awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case e'_4.zero
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
hf : f ∈ 𝒜 0
hd : 0 < 0
this : n = j * (0 + e)
⊢ j * (0 * (e + 1)) = j * (0 + e) + (j * (0 - 1)) • e

pp: case e'_4.succ
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
n✝ : ℕ
hf : f ∈ 𝒜 (n✝ + 1)
hd : 0 < n✝ + 1
this : n = j * (n✝ + 1 + e)
⊢ j * ((n✝ + 1) * (e + 1)) = j * (n✝ + 1 + e) + (j * (n✝ + 1 - 1)) • e

Tactic:
· contradiction

Goal state after:
case e'_4.succ
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
n✝ : ℕ
hf : f ∈ 𝒜 (n✝ + 1)
hd : 0 < n✝ + 1
this : n = j * (n✝ + 1 + e)
⊢ j * ((n✝ + 1) * (e + 1)) = j * (n✝ + 1 + e) + (j * (n✝ + 1 - 1)) • e
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case h.zero
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
hf : f ∈ 𝒜 0
hd : 0 < 0
this : n = j * (0 + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (0 * (e + 1)), num := ⟨a * g ^ (j * (0 - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * (0 * e), num := ⟨f ^ (j * e), ⋯⟩, den := ⟨g ^ (j * 0), ⋯⟩, den_mem := ⋯ }
⊢ x ^ j * (a * g ^ (j * (0 - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * 0))) =
    x ^ (j * (e + 1)) * x ^ (j * 0) * a

pp: case h.succ
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
n✝ : ℕ
hf : f ∈ 𝒜 (n✝ + 1)
hd : 0 < n✝ + 1
this : n = j * (n✝ + 1 + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * ((n✝ + 1) * (e + 1)), num := ⟨a * g ^ (j * (n✝ + 1 - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩,
    den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * ((n✝ + 1) * e), num := ⟨f ^ (j * e), ⋯⟩, den := ⟨g ^ (j * (n✝ + 1)), ⋯⟩, den_mem := ⋯ }
⊢ x ^ j * (a * g ^ (j * (n✝ + 1 - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * (n✝ + 1)))) =
    x ^ (j * (e + 1)) * x ^ (j * (n✝ + 1)) * a

Tactic:
· contradiction

Goal state after:
case h.succ
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
n✝ : ℕ
hf : f ∈ 𝒜 (n✝ + 1)
hd : 0 < n✝ + 1
this : n = j * (n✝ + 1 + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * ((n✝ + 1) * (e + 1)), num := ⟨a * g ^ (j * (n✝ + 1 - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩,
    den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * ((n✝ + 1) * e), num := ⟨f ^ (j * e), ⋯⟩, den := ⟨g ^ (j * (n✝ + 1)), ⋯⟩, den_mem := ⋯ }
⊢ x ^ j * (a * g ^ (j * (n✝ + 1 - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * (n✝ + 1)))) =
    x ^ (j * (e + 1)) * x ^ (j * (n✝ + 1)) * a
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
g : ↑R
a : R ⟶ CommRingCat.of (Localization.Away g) := CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))
ψ : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec (CommRingCat.of ↑R) := Spec.map a
M' : (Spec (CommRingCat.of (Localization.Away g))).Modules := M.restrict ψ
h : Aux M' ⊤
heq : ∀ (f : ↑R), basicOpen f ≤ basicOpen g → basicOpen f = ψ ''ᵁ basicOpen ((ConcreteCategory.hom a) f)
iso : Γ(M.restrict ψ, ⊤) ≅ Γ(M, basicOpen g) :=
  Scheme.Modules.restrictAppIso ψ M ⊤ ≪≫ Functor.mapIso M.presheaf (eqToIso ⋯).op
e : (f : ↑R) → basicOpen f ≤ basicOpen g → (Γ(M', basicOpen ((ConcreteCategory.hom a) f)) ≅ Γ(M, basicOpen f)) :=
  fun f hf ↦
    Scheme.Modules.restrictAppIso ψ M (basicOpen ((ConcreteCategory.hom a) f)) ≪≫
      Functor.mapIso M.presheaf (eqToIso ⋯).op
f : ↑R
hf : basicOpen f ≤ basicOpen g
t : ↑Γ(M, basicOpen g)
ht : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
⊢ (ConcreteCategory.hom (M'.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom iso.inv) t) = 0

Tactic:
simpa [M', iso, ← M.presheaf.map_comp_apply, homOfLE_op_comp_eqToHom, e] using
        congr((e _ hf).inv $ht)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.obj.obj (op X)
⊢ (ConcreteCategory.hom ((J.uliftYonedaEquiv.symm x).hom.app (op X')))
      (J.uliftYonedaEquiv ((uliftYoneda.{v', v, u} J).map f)) =
    (ConcreteCategory.hom (F.obj.map f.op)) x

Tactic:
uliftYonedaEquiv_uliftYoneda_map

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.obj.obj (op X)
⊢ (ConcreteCategory.hom ((J.uliftYonedaEquiv.symm x).hom.app (op X'))) { down := f } =
    (ConcreteCategory.hom (F.obj.map f.op)) x
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (f.hom.app (op Y))) (J.uliftYonedaEquiv ((uliftYoneda.{v', v, u} J).map g)) =
    (ConcreteCategory.hom (f.hom.app (op Y))) { down := g }

Tactic:
uliftYonedaEquiv_uliftYoneda_map

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (f.hom.app (op Y))) { down := g } = (ConcreteCategory.hom (f.hom.app (op Y))) { down := g }
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (f.hom.app (op (unop Y)))) (J.uliftYonedaEquiv ((uliftYoneda.{v', v, u} J).map g.unop)) =
    (ConcreteCategory.hom (f.hom.app Y)) { down := g.unop }

Tactic:
uliftYonedaEquiv_uliftYoneda_map

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (f.hom.app (op (unop Y)))) { down := g.unop } =
    (ConcreteCategory.hom (f.hom.app Y)) { down := g.unop }
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : W f
hg : W g
i : Fin 2
⊢ W ((ComposableArrows.mk₂ f g).map (homOfLE ⋯))

Tactic:
by fin_cases i <;> assumption

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : HasPushouts C
inst✝ : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
g : Arrow C
⊢ Arrow.Hom.left (Arrow.homMk (functorMap f (𝟙 g)) (Arrow.Hom.right (𝟙 g)) ⋯) =
    Arrow.Hom.left (𝟙 (Arrow.mk (πFunctorObj f g.hom)))

Tactic:
apply functorMap_id

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
val : F.obj (op j)
map_zero : (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val = val₀
map_succ :
  ∀ (i : J) (hi : i < j),
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val)
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
j✝ j'✝ : { x // x ∈ Set.Iio i }ᵒᵖ
f : j✝ ⟶ j'✝
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op ≫ F.map (⋯.functor.map f.unop).op)) val =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val

Tactic:
← map_comp

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
val : F.obj (op j)
map_zero : (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val = val₀
map_succ :
  ∀ (i : J) (hi : i < j),
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val)
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
j✝ j'✝ : { x // x ∈ Set.Iio i }ᵒᵖ
f : j✝ ⟶ j'✝
⊢ (ConcreteCategory.hom (F.map ((homOfLE ⋯).op ≫ (⋯.functor.map f.unop).op))) val =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op ≫ F.map (homOfLE ⋯).op)) e.val = val₀

Tactic:
← map_comp

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
⊢ (ConcreteCategory.hom (F.map ((homOfLE hij).op ≫ (homOfLE ⋯).op))) e.val = val₀
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case e_x
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
l : J
hl : l ∈ Set.Iio k
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val =
    (ConcreteCategory.hom (F.map (homOfLE hij).op ≫ F.map (homOfLE ⋯).op)) e.val

Tactic:
← map_comp

Goal state after:
case e_x
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
l : J
hl : l ∈ Set.Iio k
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val =
    (ConcreteCategory.hom (F.map ((homOfLE hij).op ≫ (homOfLE ⋯).op))) e.val
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op ≫ F.map (homOfLE ⋯).op)) (d.succ j hj e.val)

Tactic:
← map_comp

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    (ConcreteCategory.hom (F.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) (d.succ j hj e.val)
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : LinearOrder J
inst✝¹ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝ : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ sqFunctor c p f g).sections
x✝ : ↑(Set.Iio j)
i : J
hij : i ∈ Set.Iio j
this : (↑s (Opposite.op ⟨i, hij⟩)).f' ≫ p = c.ι.app i ≫ g
⊢ F.map (homOfLE ⋯) ≫ liftHom hj s ≫ p = F.map (homOfLE ⋯) ≫ c.ι.app j ≫ g

Tactic:
liftHom_fac_assoc _ _ _ hij,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : LinearOrder J
inst✝¹ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝ : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ sqFunctor c p f g).sections
x✝ : ↑(Set.Iio j)
i : J
hij : i ∈ Set.Iio j
this : (↑s (Opposite.op ⟨i, hij⟩)).f' ≫ p = c.ι.app i ≫ g
⊢ (↑s (Opposite.op ⟨i, hij⟩)).f' ≫ p = F.map (homOfLE ⋯) ≫ c.ι.app j ≫ g
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case e_x
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
this :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val,
        ⋯⟩
l : J
hl : l ∈ Set.Iio i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op ≫ F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val)

Tactic:
← map_comp

Goal state after:
case e_x
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
this :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val,
        ⋯⟩
l : J
hl : l ∈ Set.Iio i
⊢ (ConcreteCategory.hom (F.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) (d.succ j hj e.val) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val)