mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ 1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|

Tactic:
by
  obtain ⟨ev, bi, bu, hF⟩ :=
    denomsClearable_natDegree (b := b) (algebraMap ℤ K) f a
      (by
        rw [eq_intCast, one_div_mul_cancel]
        rw [Int.cast_ne_zero]
        exact b0.ne.symm)
  obtain Fa := congr_arg abs hF
  rw [eq_one_div_of_mul_eq_one_left bu, eq_intCast, eq_intCast, abs_mul] at Fa
  rw [abs_of_pos (pow_pos (Int.cast_pos.mpr b0) _ : 0 < (b : K) ^ _), one_div, eq_intCast] at Fa
  rw [div_eq_mul_inv, ← Fa, ← Int.cast_abs, ← Int.cast_one, Int.cast_le]
  refine Int.le_of_lt_add_one ((lt_add_iff_pos_left 1).mpr (abs_pos.mpr fun F0 => fab ?_))
  rw [eq_one_div_of_mul_eq_one_left bu, F0, one_div, eq_intCast, Int.cast_zero, zero_eq_mul] at hF
  rcases hF with hF | hF
  · exact (not_le.mpr b0 (le_of_eq (Int.cast_eq_zero.mp (eq_zero_of_pow_eq_zero hF)))).elim
  · rwa [div_eq_mul_inv]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : ¬n = 0
⊢ (ofFn n) v = ∑ i, (monomial ↑i) (v i)

Tactic:
rw [as_sum_range' (ofFn n v) n <| ofFn_natDegree_lt (Nat.one_le_iff_ne_zero.mpr h) v]
    simp [Finset.sum_range]

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

Goal state before:
pp: case cons
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
p : ι → R[X]
n : ι → ℕ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ i ∈ s, (p i).natDegree ≤ n i) → (∏ i ∈ s, p i).homogenize (∑ i ∈ s, n i) = ∏ i ∈ s, (p i).homogenize (n i)
h : ∀ i_1 ∈ cons i s hi, (p i_1).natDegree ≤ n i_1
⊢ (∏ i ∈ cons i s hi, p i).homogenize (∑ i ∈ cons i s hi, n i) = ∏ i ∈ cons i s hi, (p i).homogenize (n i)

Tactic:
simp only [prod_cons, sum_cons, forall_mem_cons] at *
    rw [homogenize_mul _ _ h.1, ihs h.2]
    exact (natDegree_prod_le _ _).trans (sum_le_sum h.2)

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hb : ∀ {a : α}, IsChain R (a :: l) → destutter' R a l = a :: l
a : α
h✝ : IsChain R (a :: b :: l)
h : R a b
hc : IsChain R (b :: l)
⊢ destutter' R a (b :: l) = a :: b :: l

Tactic:
l.destutter'_cons_pos h,

Goal state after:
case cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hb : ∀ {a : α}, IsChain R (a :: l) → destutter' R a l = a :: l
a : α
h✝ : IsChain R (a :: b :: l)
h : R a b
hc : IsChain R (b :: l)
⊢ a :: destutter' R b l = a :: b :: l
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
R : α → α → Prop
inst✝¹ : DecidableRel R
R₂ : β → β → Prop
inst✝ : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
this : R a b ↔ R₂ (f a) (f b)
hr : R a b
⊢ map f (if R a b then a :: destutter' R b l else destutter' R a l) =
    if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)

Tactic:
simp [hr, ← destutter_cons', map_destutter fun c hc d hd ↦ hl _ (cons_subset_cons _
        (subset_cons_self _ _) hc) _ (cons_subset_cons _ (subset_cons_self _ _) hd),
        map_destutter fun c hc d hd ↦ hl _ (subset_cons_self _ _ hc) _ (subset_cons_self _ _ hd)]

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
R : α → α → Prop
inst✝¹ : DecidableRel R
R₂ : β → β → Prop
inst✝ : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
this : R a b ↔ R₂ (f a) (f b)
hr : ¬R a b
⊢ map f (if R a b then a :: destutter' R b l else destutter' R a l) =
    if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)

Tactic:
simp [hr, ← destutter_cons', map_destutter fun c hc d hd ↦ hl _ (cons_subset_cons _
        (subset_cons_self _ _) hc) _ (cons_subset_cons _ (subset_cons_self _ _) hd),
        map_destutter fun c hc d hd ↦ hl _ (subset_cons_self _ _ hc) _ (subset_cons_self _ _ hd)]

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

Goal state before:
pp: case succ.snoc
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
r₂ : Fin (n + 1) → R[X]
hr₂ : ∀ (i : Fin (n + 1)), (r₂ i).degree < g.degree
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
hf : q₁ * g ^ (n + 1) + ∑ i, Fin.snoc rs₁ r₁ i * g ^ ↑i = q₂ * g ^ (n + 1) + ∑ i, r₂ i * g ^ ↑i
⊢ q₁ = q₂ ∧ Fin.snoc rs₁ r₁ = r₂

Tactic:
cases r₂ using Fin.snocCases with | snoc rs₂ r₂

Goal state after:
case succ.snoc.snoc
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : q₁ * g ^ (n + 1) + ∑ i, Fin.snoc rs₁ r₁ i * g ^ ↑i = q₂ * g ^ (n + 1) + ∑ i, Fin.snoc rs₂ r₂ i * g ^ ↑i
⊢ q₁ = q₂ ∧ Fin.snoc rs₁ r₁ = Fin.snoc rs₂ r₂
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (map f p).natDegree p.natDegree
⊢ ∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), (⇑derivative)^[i] (map f p) = map f (sumIDeriv p)

Tactic:
sumIDeriv_apply_of_le (le_max_right _ _ : _ ≤ n)

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (map f p).natDegree p.natDegree
⊢ ∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), (⇑derivative)^[i] (map f p) =
    map f (∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), (⇑derivative)^[i] p)
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
P : R[X]
hx : η ≠ 0
this :
  ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {η : R} (P : R[X]),
    η ≠ 0 → 0 < η → (C η * P).signVariations = P.signVariations
hx2 : η ≤ 0
⊢ (C η * P).signVariations = P.signVariations

Tactic:
simpa [lt_of_le_of_ne hx2, hx] using this (η := -η) (P := -P)

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

Goal state before:
pp: case inr.refine_2.e_a
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
k : ℕ
hk : k ∈ Ico q (p.natDegree + 1)
⊢ (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)

Tactic:
exact hc k (mem_Ico.mp hk).1 r

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝ : CommRing R
x✝ : QuadraticAlgebra R a b
⊢ star (star x✝) = x✝

Tactic:
by
    refine QuadraticAlgebra.ext (by simp) (neg_neg _)

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = 0
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = -1
h✝ : ¬P.eraseLead = 0
⊢ ((X - C η) * P).eraseLead.signVariations + 1 = ((X - C η) * P).signVariations

Tactic:
simp [-leadingCoeff_mul, ← sign_ne_zero,
          signVariations_eq_eraseLead_add_ite h_mul, leadingCoeff_eraseLead_eq_nextCoeff,
          hs_nC_mul, h_mul_lC]

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

Goal state before:
pp: case coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a b : WithZero α
a✝ : α
⊢ (a + b) * ↑a✝ = a * ↑a✝ + b * ↑a✝

Tactic:
cases a <;> cases b

Goal state after:
case coe.zero.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝ : α
⊢ (0 + 0) * ↑a✝ = 0 * ↑a✝ + 0 * ↑a✝

case coe.zero.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝¹ a✝ : α
⊢ (0 + ↑a✝) * ↑a✝¹ = 0 * ↑a✝¹ + ↑a✝ * ↑a✝¹

case coe.coe.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝¹ a✝ : α
⊢ (↑a✝ + 0) * ↑a✝¹ = ↑a✝ * ↑a✝¹ + 0 * ↑a✝¹

case coe.coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝² a✝¹ a✝ : α
⊢ (↑a✝¹ + ↑a✝) * ↑a✝² = ↑a✝¹ * ↑a✝² + ↑a✝ * ↑a✝²
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : AddMonoid k
S : Type u_3
inst✝² : Monoid S
inst✝¹ : DistribMulAction S k
a : S
inst✝ : Nonempty G
inhabited_h : Inhabited G
ha : IsSMulRegular (SkewMonoidAlgebra k G) a
b₁ b₂ : k
inj✝ : (fun x ↦ a • x) b₁ = (fun x ↦ a • x) b₂
inj : a • single ?m.62 b₁ = a • single ?m.62 b₂
⊢ b₁ = b₂

pp: k : Type u_1
G : Type u_2
inst✝³ : AddMonoid k
S : Type u_3
inst✝² : Monoid S
inst✝¹ : DistribMulAction S k
a : S
inst✝ : Nonempty G
inhabited_h : Inhabited G
ha : IsSMulRegular (SkewMonoidAlgebra k G) a
b₁ b₂ : k
inj : (fun x ↦ a • x) b₁ = (fun x ↦ a • x) b₂
⊢ Type ?u.36

Tactic:
exact single_injective default (ha inj)

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

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst✝² : Monoid G
inst✝¹ : AddCommMonoid M
inst✝ : MulAction G α
f : SkewMonoidAlgebra M α
⊢ (mapDomain id) f = f

Tactic:
mapDomain_id

Goal state after:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst✝² : Monoid G
inst✝¹ : AddCommMonoid M
inst✝ : MulAction G α
f : SkewMonoidAlgebra M α
⊢ f = f
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case cons
R : Type u_1
inst✝ : AddMonoid R
hd : R
tl : List R
IH : trop tl.sum = (map trop tl).prod
⊢ trop (hd :: tl).sum = (map trop (hd :: tl)).prod

Tactic:
simp [← IH]

Goal state after:
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case cons
R : Type u_1
inst✝ : AddMonoid R
hd : Tropical R
tl : List (Tropical R)
IH : untrop tl.prod = (map untrop tl).sum
⊢ untrop (hd :: tl).prod = (map untrop (hd :: tl)).sum

Tactic:
simp [← IH]

Goal state after:
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : R
x : Multiset R
IH : trop x.inf = (map trop x).sum
⊢ trop (s ::ₘ x).inf = (map trop (s ::ₘ x)).sum

Tactic:
simp [← IH]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    ((single x r).sum fun a₂ b₂ ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) = if a₁ * x = z then b₁ * a₁ • r else 0
⊢ (f * single x r).coeff z = f.sum fun a b ↦ if a = y then b * y • r else 0

Tactic:
by simp [coeff_mul, A, H, sum_ite_eq']

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

Goal state before:
pp: k : Type u_1
G : Type u_2
A : Type u_6
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
inst✝ : DistribMulAction k A
φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A
h : ∀ (x : G), φ₁ (single x 1) = φ₂ (single x 1)
⊢ ↑φ₁ = ↑φ₂

Tactic:
apply distribMulActionHom_ext'

Goal state after:
k : Type u_1
G : Type u_2
A : Type u_6
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
inst✝ : DistribMulAction k A
φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A
h : ∀ (x : G), φ₁ (single x 1) = φ₂ (single x 1)
⊢ ∀ (a : G), (↑φ₁).comp (DistribMulActionHom.single a) = (↑φ₂).comp (DistribMulActionHom.single a)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : x ∈ W
heq :
  (ConcreteCategory.hom (X.presheaf.germ W x hxW))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom (X.presheaf.germ W x hxW)) 1
⊢ ∃ V i, ∃ (_ : x ∈ V), IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)

Tactic:
obtain ⟨W', hxW', i₁, i₂, heq'⟩ := X.presheaf.germ_eq x hxW hxW _ _ heq

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : x ∈ W
heq :
  (ConcreteCategory.hom (X.presheaf.germ W x hxW))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom (X.presheaf.germ W x hxW)) 1
W' : Opens ↑↑X.toPresheafedSpace
hxW' : x ∈ W'
i₁ i₂ : W' ⟶ W
heq' :
  (ConcreteCategory.hom (X.presheaf.map i₁.op))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom (X.presheaf.map i₂.op)) 1
⊢ ∃ V i, ∃ (_ : x ∈ V), IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : x ∈ W
heq :
  (ConcreteCategory.hom (X.presheaf.germ W x hxW))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom (X.presheaf.germ W x hxW)) 1
W' : Opens ↑↑X.toPresheafedSpace
hxW' : x ∈ W'
i₁ i₂ : W' ⟶ W
heq' :
  (ConcreteCategory.hom (X.presheaf.map i₁.op))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom (X.presheaf.map i₂.op)) 1
⊢ ∃ V i, ∃ (_ : x ∈ V), IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)

Tactic:
use W', i₁ ≫ Opens.infLELeft U V, hxW'

Goal state after:
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := ⋯
hxW : x ∈ W
heq :
  (ConcreteCategory.hom (X.presheaf.germ W x hxW))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom (X.presheaf.germ W x hxW)) 1
W' : Opens ↑↑X.toPresheafedSpace
hxW' : x ∈ W'
i₁ i₂ : W' ⟶ W
heq' :
  (ConcreteCategory.hom (X.presheaf.map i₁.op))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom (X.presheaf.map i₂.op)) 1
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.map (i₁ ≫ U.infLELeft V).op)) f)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: case refine_2
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
U : (Opens ↑↑s.pt)ᵒᵖ
j j' : Jᵒᵖ
f : j ⟶ j'
w :
  (Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
      ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)) =
    (Opens.map (((forget C).mapCocone s).ι.app (unop j))).obj (unop U)
⊢ 𝟙 (s.pt.presheaf.obj U) ≫
      ((F.map f.unop ≫ s.ι.app (unop j)).c.app U ≫ (F.obj (unop j')).presheaf.map (eqToHom ⋯)) ≫
        (F.obj (unop j')).presheaf.map (eqToHom ⋯) =
    ((s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫
      (F.map f.unop).c.app
          (op
            ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
              ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))) ≫
        𝟙
            ((F.obj (unop j')).presheaf.obj
              (op
                ((Opens.map (F.map f.unop).base).obj
                  ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
                    ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))))) ≫
          (pushforwardEq ⋯ (F.obj (unop j')).presheaf).hom.app
            (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))

Tactic:
replace w := congr_arg op w

Goal state after:
case refine_2
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
U : (Opens ↑↑s.pt)ᵒᵖ
j j' : Jᵒᵖ
f : j ⟶ j'
w :
  op
      ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
        ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U))) =
    op ((Opens.map (((forget C).mapCocone s).ι.app (unop j))).obj (unop U))
⊢ 𝟙 (s.pt.presheaf.obj U) ≫
      ((F.map f.unop ≫ s.ι.app (unop j)).c.app U ≫ (F.obj (unop j')).presheaf.map (eqToHom ⋯)) ≫
        (F.obj (unop j')).presheaf.map (eqToHom ⋯) =
    ((s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫
      (F.map f.unop).c.app
          (op
            ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
              ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))) ≫
        𝟙
            ((F.obj (unop j')).presheaf.obj
              (op
                ((Opens.map (F.map f.unop).base).obj
                  ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
                    ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))))) ≫
          (pushforwardEq ⋯ (F.obj (unop j')).presheaf).hom.app
            (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
⊢ e.inv.base ≫ e.hom.base = 𝟙 ↑Y.toPresheafedSpace

Tactic:
by
  simp only [← comp_base, Iso.inv_hom_id, id_toHom, PresheafedSpace.id_base]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
⊢ m = desc F s

Tactic:
by
    -- We need to use the identity on the continuous maps twice, so we prepare that first:
    have t :
      m.base =
        colimit.desc (F ⋙ PresheafedSpace.forget C) ((PresheafedSpace.forget C).mapCocone s) := by
      dsimp
      -- `colimit.hom_ext` used to be automatically applied by `ext` before https://github.com/leanprover-community/mathlib4/pull/21302
      apply colimit.hom_ext fun j => ?_
      ext
      rw [colimit.ι_desc, mapCocone_ι_app, ← w j]
      simp
    ext : 1
    · exact t
    · refine NatTrans.ext (funext fun U => limit_obj_ext fun j => ?_)
      simp [desc, descCApp,
        PresheafedSpace.congr_app (w (unop j)).symm U,
        NatTrans.congr (limit.π (pushforwardDiagramToColimit F).leftOp j)
        (congr_arg op (Functor.congr_obj (congr_arg Opens.map t) (unop U)))]

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T✝ : ↑X → Type u_1
T : Type ?u.10
inst✝ : TopologicalSpace T
U : Opens ↑X
f : ↥U → T
x : ↥U
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
w : ∀ (x : ↥V), ContinuousAt (fun x ↦ f (i x)) x
⊢ ContinuousAt f x

Tactic:
specialize w ⟨x, m⟩

Goal state after:
X : TopCat
T✝ : ↑X → Type u_1
T : Type ?u.10
inst✝ : TopologicalSpace T
U : Opens ↑X
f : ↥U → T
x : ↥U
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
w : ContinuousAt (fun x ↦ f (i x)) ⟨↑x, m⟩
⊢ ContinuousAt f x
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (comap (CommRingCat.Hom.hom (f ≫ g)) (unop (op U✝))
              ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj (unop (op U✝))) ⋯) ≫
          (sheafedSpaceObj T).presheaf.map
            ((𝟙 (TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).hom.base).op).app (op U✝))))
      x✝ =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c.app (op U✝))) x✝

Tactic:
(sheafedSpaceObj T).presheaf.map_id

Goal state after:
case h
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (comap (CommRingCat.Hom.hom (f ≫ g)) (unop (op U✝))
              ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj (unop (op U✝))) ⋯) ≫
          𝟙
            ((sheafedSpaceObj T).presheaf.obj
              ((TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).hom.base).op.obj (op U✝)))))
      x✝ =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c.app (op U✝))) x✝
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
this : ∀ (x : ↥X), ∀ f ∈ s, x ∈ X.basicOpen f → x ∈ U
⊢ Codisjoint (X.zeroLocus s) ↑U

Tactic:
simpa [codisjoint_iff_le_sup, Set.ext_iff, or_iff_not_imp_left]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
⊢ X.zeroLocus ↑(I * J) = X.zeroLocus ↑I ∪ X.zeroLocus ↑J

Tactic:
by
  rw [← X.zeroLocus_setMul, ← X.zeroLocus_span (U := U) (↑I * ↑J), ← Ideal.span_mul_span]
  simp

Goal state after: