mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
hxy : x ≠ y
h : (r x y ∧ ∀ (a : α), a ∈ xs → r x a) ∧ (∀ (a' : α), a' ∈ xs → r y a') ∧ Pairwise r xs
this : ¬x ∈ xs
⊢ ¬x ∈ y :: xs

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case monomial
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
n✝ a n : ℕ
⊢ a • ↑n ^ n✝ = ↑(a • n ^ n✝)

Tactic:
nsmul_eq_mul,

Goal state after:
case monomial
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
n✝ a n : ℕ
⊢ ↑a * ↑n ^ n✝ = ↑(a • n ^ n✝)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝ : Semiring R
k n : ℕ
u v w : R
hw : w ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ ↑i ≤ ↑n

pp: case inr.inr
R : Type u_1
inst✝ : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hw : w ≠ 0
i : ℕ
hmn : m < i
⊢ ↑i ≤ ↑i

Tactic:
· exact WithBot.coe_le_coe.mpr hmn.le

Goal state after:
case inr.inr
R : Type u_1
inst✝ : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hw : w ≠ 0
i : ℕ
hmn : m < i
⊢ ↑i ≤ ↑i
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ∑ n_1 ∈ {k, m, n}, (trinomial k m n ↑u ↑v ↑w).coeff n_1 ^ 2 = 3

Tactic:
sum_insert (mt mem_insert.mp (not_or_intro hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),

Goal state after:
case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ (trinomial k m n ↑u ↑v ↑w).coeff k ^ 2 + ∑ x ∈ {m, n}, (trinomial k m n ↑u ↑v ↑w).coeff x ^ 2 = 3
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
r : A
⊢ (aeval r) ((q + k)! • p') = q ! • (aeval r) (↑((q + k).descFactorial k) * p')

Tactic:
nsmul_eq_mul,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
r : A
⊢ (aeval r) (↑(q + k)! * p') = ↑q ! * (aeval r) (↑((q + k).descFactorial k) * p')
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
⊢ ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) (sumIDeriv p) = q ! • (aeval r) gp

Tactic:
by
  have h (k) :
      ∃ gp : R[X], gp.natDegree ≤ p.natDegree - q ∧
        ∀ (r : A), (X - C r) ^ q ∣ p.map (algebraMap R A) →
          aeval r (derivative^[k] p) = q ! • aeval r gp := by
    cases lt_or_ge k q with
    | inl hk =>
      use 0
      rw [natDegree_zero]
      use Nat.zero_le _
      intro r ⟨p', hp⟩
      rw [map_zero, smul_zero, aeval_iterate_derivative_of_lt p q r hp hk]
    | inr hk =>
      obtain ⟨gp, gp_le, h⟩ := aeval_iterate_derivative_of_ge A p q hk
      exact ⟨gp, gp_le.trans (tsub_le_tsub_left hk _), fun r _ => h r⟩
  choose c h using h
  choose c_le hc using h
  refine ⟨(range (p.natDegree + 1)).sum c, ?_, ?_⟩
  · refine (natDegree_sum_le _ _).trans ?_
    rw [fold_max_le]
    exact ⟨Nat.zero_le _, fun i _ => c_le i⟩
  intro r ⟨p', hp⟩
  rw [sumIDeriv_apply, map_sum]; simp_rw [hc _ r ⟨_, hp⟩, map_sum, smul_sum]

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r✝ : R
x✝ y : QuadraticAlgebra R a b
inst✝² : Semiring S
inst✝¹ : AddCommMonoid R
inst✝ : Module S R
r s : S
x : QuadraticAlgebra R a b
⊢ (r + s) • x = r • x + s • x

Tactic:
ext <;> simp [add_smul]

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : ι → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j, r' i j * g i ^ ↑j
⊢ ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k =
    ∑ x ∈ s, (q' x * ∏ i ∈ s, g i ^ n i + ∑ j, r' x j * g x ^ ↑j * ∏ k ∈ s.erase x, g k ^ n k)

Tactic:
refine Finset.sum_congr rfl fun i hi => ?_

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : ι → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j, r' i j * g i ^ ↑j
i : ι
hi : i ∈ s
⊢ r i * ∏ k ∈ s.erase i, g k ^ n k = q' i * ∏ i ∈ s, g i ^ n i + ∑ j, r' i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
⊢ ∑ i ∈ s, (algebraMap R[X] K) (∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k) * ∏ i ∈ s, gi i ^ n i =
    ∑ i ∈ s, ∑ j, (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)

Tactic:
refine Finset.sum_congr rfl fun i hi => ?_

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
⊢ (algebraMap R[X] K) (∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k) * ∏ i ∈ s, gi i ^ n i =
    ∑ j, (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ ((algebraMap R[X] K) (r i j.rev * g i ^ ↑j.rev) * ∏ x ∈ s.erase i, (algebraMap R[X] K) (g x ^ n x)) *
      ∏ i ∈ s, gi i ^ n i =
    (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)

Tactic:
← Finset.prod_erase_mul s _ hi,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ ((algebraMap R[X] K) (r i j.rev * g i ^ ↑j.rev) * ∏ x ∈ s.erase i, (algebraMap R[X] K) (g x ^ n x)) *
      ((∏ x ∈ s.erase i, gi x ^ n x) * gi i ^ n i) =
    (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y ↔ x = y

Tactic:
by
  constructor; swap
  · rintro rfl; rfl
  intro h
  trans (x ◃ x) ◃⁻¹ x ◃ x
  · rw [← left_cancel (x ◃ x), right_inv, self_act_act_eq]
  · rw [h, ← left_cancel (y ◃ y), right_inv, self_act_act_eq]

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
a b : R
⊢ single (ofAdd m) a = single (ofAdd n) b ↔ single m a = single n b

Tactic:
simp only [← ofCoeff_single, SkewMonoidAlgebra.ofCoeff_inj, Finsupp.single_eq_single_iff,
    EmbeddingLike.apply_eq_iff_eq]

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ erase n 0 = 0

Tactic:
by
  simp [erase, zero_def]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
⊢ (liftNC ↑f ⇑g) (a * b) = (liftNC ↑f ⇑g) a * (liftNC ↑f ⇑g) b

Tactic:
conv_rhs => rw [← sum_single a, ← sum_single b]

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
⊢ (liftNC ↑f ⇑g) (a * b) = (liftNC ↑f ⇑g) (a.sum single) * (liftNC ↑f ⇑g) (b.sum single)
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Surjective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Mono (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
gc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
h : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
hc : Z.presheaf ⟶ (pushforward C h).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := h, c := hc } }).hom
y : ↑↑Y.toPresheafedSpace
⊢ (ConcreteCategory.hom g) y = (ConcreteCategory.hom h) y

Tactic:
rw [← (h₁ y).choose_spec]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Surjective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Mono (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
gc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
h : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
hc : Z.presheaf ⟶ (pushforward C h).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := h, c := hc } }).hom
y : ↑↑Y.toPresheafedSpace
⊢ (ConcreteCategory.hom g) ((ConcreteCategory.hom f.hom.base) ⋯.choose) =
    (ConcreteCategory.hom h) ((ConcreteCategory.hom f.hom.base) ⋯.choose)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
⊢ (Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c).app (op U) ≫ H.hom.c.app (op U) =
    (𝟙 ((Presheaf.pushforward C H.hom.base).obj X.presheaf)).app (op U)

Tactic:
NatTrans.id_app

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
⊢ (Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c).app (op U) ≫ H.hom.c.app (op U) =
    𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ Hom.stalkMap (e.inv ≫ e.hom) y = Y.presheaf.stalkSpecializes ⋯

Tactic:
LocallyRingedSpace.stalkMap_congr_hom (e.inv ≫ e.hom) (𝟙 _) (by simp)

Goal state after:
X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (𝟙 Y) y = Y.presheaf.stalkSpecializes ⋯
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_1.refine_1
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : (ConcreteCategory.hom ((P.cocone x).ι.app U)) ⟨fU, hU⟩ = (ConcreteCategory.hom ((P.cocone x).ι.app V)) ⟨fV, hV⟩
W : OpenNhds x
iU : W ⟶ unop U
iV : W ⟶ unop V
w : ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
⊢ ↑(unop (op W)) ⟶ ↑(unop U)

pp: case refine_1.refine_2
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : (ConcreteCategory.hom ((P.cocone x).ι.app U)) ⟨fU, hU⟩ = (ConcreteCategory.hom ((P.cocone x).ι.app V)) ⟨fV, hV⟩
W : OpenNhds x
iU : W ⟶ unop U
iV : W ⟶ unop V
w : ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
⊢ (ConcreteCategory.hom
          (colimit.ι
            (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
              (subpresheafToTypes P.toPrelocalPredicate))
            U))
        ⟨fU, hU⟩ =
      (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop (op W))) x ⋯)) ⟨fun w ↦ fU (iU w), ⋯⟩ ∧
    (ConcreteCategory.hom
          (colimit.ι
            (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
              (subpresheafToTypes P.toPrelocalPredicate))
            V))
        ⟨fV, hV⟩ =
      (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop (op W))) x ⋯)) ⟨fun w ↦ fU (iU w), ⋯⟩

Tactic:
· rcases W with ⟨W, m⟩
    exact iU

Goal state after:
case refine_1.refine_2
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : (ConcreteCategory.hom ((P.cocone x).ι.app U)) ⟨fU, hU⟩ = (ConcreteCategory.hom ((P.cocone x).ι.app V)) ⟨fV, hV⟩
W : OpenNhds x
iU : W ⟶ unop U
iV : W ⟶ unop V
w : ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
⊢ (ConcreteCategory.hom
          (colimit.ι
            (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
              (subpresheafToTypes P.toPrelocalPredicate))
            U))
        ⟨fU, hU⟩ =
      (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop (op W))) x ⋯)) ⟨fun w ↦ fU (iU w), ⋯⟩ ∧
    (ConcreteCategory.hom
          (colimit.ι
            (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
              (subpresheafToTypes P.toPrelocalPredicate))
            V))
        ⟨fV, hV⟩ =
      (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop (op W))) x ⋯)) ⟨fun w ↦ fU (iU w), ⋯⟩
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
⊢ f ≫ toSpecΓ S = toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op

Tactic:
by
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` failed to pick up one of the three lemmas
  ext : 2
  refine Subtype.ext <| funext fun x' => ?_; symm
  erw [comap_apply]
  apply Localization.localRingHom_to_map

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Mono f

Tactic:
rw [← H.isoRestrict_hom_ofRestrict]; apply mono_comp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝¹ }.base = { toLRSHom' := toLRSHom'✝ }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom'✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toLRSHom' := toLRSHom'✝ }.app U
U : TopologicalSpace.Opens ↥Y
⊢ (toLRSHom'✝¹.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf).app (op U) = toLRSHom'✝.c.app (op U)

Tactic:
by simpa using! h_app U

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
U : (Opens ↑↑X)ᵒᵖ
⊢ (Opens.map g.base).op.obj (op (⋯.functor.obj (unop U))) =
    ⋯.functor.op.obj ((Opens.map (pullback.fst f.base g.base)).op.obj U)

Tactic:
simp only [IsOpenMap.functor, op_inj_iff, Opens.map,
                    Functor.op_obj]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
U : (Opens ↑↑X)ᵒᵖ
⊢ (↑(TopCat.Hom.frameHom g.base)).toFunctor.obj
      { carrier := ⇑(ConcreteCategory.hom f.base) '' ↑(unop U), is_open' := ⋯ } =
    {
      carrier :=
        ⇑(ConcreteCategory.hom (pullback.snd f.base g.base)) ''
          ↑((↑(TopCat.Hom.frameHom (pullback.fst f.base g.base))).toFunctor.obj (unop U)),
      is_open' := ⋯ }
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : MorphismProperty C
S✝ : C
E : P.precoverage.ZeroHypercover S✝
⊢ E.Small

Tactic:
constructor
    use PEmpty, PEmpty.elim
    simp

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this : U = ⋯.functor.obj ((Opens.map f.base).obj U)
⊢ IsIso (f.c.app (op U))

Tactic:
convert! H.c_iso ((Opens.map f.base).obj U)

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑(pullback.fst g f) = ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)

Tactic:
by
  rw [← show _ = (pullback.fst g f).base from
    PreservesPullback.iso_hom_fst Scheme.forgetToTop g f, TopCat.coe_comp, Set.range_comp,
    Set.range_eq_univ.mpr, ← @Set.preimage_univ _ _ (pullback.snd g.base f.base)]
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11224): was `rw`
  · erw [TopCat.pullback_fst_image_snd_preimage]
    rw [Set.image_univ]
    rfl
  rw [← TopCat.epi_iff_surjective]
  infer_instance

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i j : Discrete ι
h : i ≠ j
U : Opens ↑↑(F.obj i).toPresheafedSpace
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
y : ↑↑(F.obj i).toPresheafedSpace
hy : y ∈ ↑U
eq :
  (ConcreteCategory.hom (colimit.ι F i).hom.base) y =
    (ConcreteCategory.hom (preservesColimitIso forgetToPresheafedSpace F).inv.base)
      ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base) x)
⊢ False

Tactic:
replace eq := ConcreteCategory.congr_arg (preservesColimitIso (SheafedSpace.forget C) F ≪≫
    HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫ TopCat.sigmaIsoSigma.{v, v} _).hom eq

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i j : Discrete ι
h : i ≠ j
U : Opens ↑↑(F.obj i).toPresheafedSpace
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
y : ↑↑(F.obj i).toPresheafedSpace
hy : y ∈ ↑U
eq :
  (ConcreteCategory.hom
        (preservesColimitIso (forget C) F ≪≫
            HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫
              TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom)
      ((ConcreteCategory.hom (colimit.ι F i).hom.base) y) =
    (ConcreteCategory.hom
        (preservesColimitIso (forget C) F ≪≫
            HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫
              TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom)
      ((ConcreteCategory.hom (preservesColimitIso forgetToPresheafedSpace F).inv.base)
        ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base) x))
⊢ False
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f✝ : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f✝) g
𝒱 : X.OpenCover
f : 𝒰 ⟶ 𝒱
i : 𝒰.I₀
⊢ IsOpenImmersion (f.h₀ i ≫ 𝒱.f (f.s₀ i))

Tactic:
f.w₀

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f✝ : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f✝) g
𝒱 : X.OpenCover
f : 𝒰 ⟶ 𝒱
i : 𝒰.I₀
⊢ IsOpenImmersion (𝒰.f i)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥U
⊢ ∀ (U_1 : TopologicalSpace.Opens ↥↑U) (hxU : x ∈ U_1),
    (↑U).presheaf.germ U_1 x hxU ≫ 𝟙 ((↑U).presheaf.stalk x) =
      (↑U).presheaf.germ U_1 x hxU ≫ (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x

Tactic:
intro W

Goal state after:
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↥↑U
⊢ ∀ (hxU : x ∈ W),
    (↑U).presheaf.germ W x hxU ≫ 𝟙 ((↑U).presheaf.stalk x) =
      (↑U).presheaf.germ W x hxU ≫ (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen s))))) s ^ n)
      ((toBasicOpenₗ R M s) (LocalizedModule.mk f ⟨(fun x ↦ s ^ x) n, ⋯⟩)) =
    ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen s))))) s ^ n)
      (const f (↑⟨(fun x ↦ s ^ x) n, ⋯⟩) (basicOpen s) ⋯)

Tactic:
← map_pow

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen s))))) (s ^ n))
      ((toBasicOpenₗ R M s) (LocalizedModule.mk f ⟨(fun x ↦ s ^ x) n, ⋯⟩)) =
    ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen s))))) (s ^ n))
      (const f (↑⟨(fun x ↦ s ^ x) n, ⋯⟩) (basicOpen s) ⋯)
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
x✝ : ↑(unop X)
⊢ (ConcreteCategory.hom (0 ≫ (forget₂ TopCommRingCat TopCat).map φ)) x✝ = (ConcreteCategory.hom 0) x✝

Tactic:
exact φ.1.map_zero

Goal state after: