mathlib-initiative/mathlib-tactics huggingface dataset:
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

pp: R✝ : Type u_1
inst✝⁴ : Ring R✝
inst✝³ : LinearOrder R✝
η✝ : R✝
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
P : R[X]
hx : η ≠ 0
hx2 : 0 < η
⊢ (C η * P).signVariations = P.signVariations

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

Goal state after:
R✝ : Type u_1
inst✝⁴ : Ring R✝
inst✝³ : LinearOrder R✝
η✝ : R✝
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
P : R[X]
hx : η ≠ 0
hx2 : 0 < η
⊢ (C η * P).signVariations = P.signVariations
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
this : ((X - C η) * P).eraseLead.eraseLead = ((X - C η) * P.eraseLead).eraseLead
⊢ ((X - C η) * P).eraseLead.signVariations = ((X - C η) * P.eraseLead).signVariations

Tactic:
suffices (coeffList (eraseLead ((X - C η) * P))).map SignType.sign =
      (coeffList ((X - C η) * P.eraseLead)).map SignType.sign by
        rw [signVariations, signVariations, this]
    have : 0 < natDegree ((X - C η) * P.eraseLead) := by lia
    grind [leadingCoeff_mul, leadingCoeff_X_sub_C, one_mul, leadingCoeff_eraseLead_eq_nextCoeff,
      LT.lt.ne, sign_neg, coeffList_eraseLead, ne_zero_of_natDegree_gt,
      nextCoeff_eq_zero_of_eraseLead_eq_zero]

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

Goal state before:
pp: p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
h : p * p.mirror = q * q.mirror
⊢ q = p ∨ q = p.mirror

Tactic:
let f (p : ℤ[X]) : ℤ[X] := ⟨.ofCoeff <| .filter (· ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp.coeff⟩

Goal state after:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
h : p * p.mirror = q * q.mirror
f : ℤ[X] → ℤ[X] :=
  fun p ↦
    { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp.coeff) }
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
h₇ : ((X - C η) * P).natDegree = P.natDegree + 1
h₈ : ((X - C η) * P.eraseLead).eraseLead = (X - C η) * P.eraseLead - (monomial P.natDegree) P.nextCoeff
this✝³ : P.eraseLead.natDegree + 2 = ((X - C η) * P.eraseLead).coeffList.length
this✝² : P.natDegree + 2 = ((X - C η) * P).coeffList.length
this✝¹ : ((X - C η) * P).leadingCoeff = P.leadingCoeff
h₉ : ((X - C η) * P).nextCoeff = 0
this✝ : ((X - C η) * P).eraseLead = ((X - C η) * P.eraseLead).eraseLead
this :
  ((X - C η) * P).coeffList =
    ((X - C η) * P).leadingCoeff ::
      (List.replicate (((X - C η) * P).natDegree - ((X - C η) * P).eraseLead.degree.succ) 0 ++
        ((X - C η) * P).eraseLead.coeffList)
⊢ ((X - C η) * P).coeffList =
    P.leadingCoeff :: ((X - C η) * P).nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)

Tactic:
#adaptation_note
        /--
        Moving from `nightly-2025-10-13` to `nightly-2025-10-19`
        we now need to provide an intermediate step.
        -/

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
h₇ : ((X - C η) * P).natDegree = P.natDegree + 1
h₈ : ((X - C η) * P.eraseLead).eraseLead = (X - C η) * P.eraseLead - (monomial P.natDegree) P.nextCoeff
this✝³ : P.eraseLead.natDegree + 2 = ((X - C η) * P.eraseLead).coeffList.length
this✝² : P.natDegree + 2 = ((X - C η) * P).coeffList.length
this✝¹ : ((X - C η) * P).leadingCoeff = P.leadingCoeff
h₉ : ((X - C η) * P).nextCoeff = 0
this✝ : ((X - C η) * P).eraseLead = ((X - C η) * P.eraseLead).eraseLead
this :
  ((X - C η) * P).coeffList =
    ((X - C η) * P).leadingCoeff ::
      (List.replicate (((X - C η) * P).natDegree - ((X - C η) * P).eraseLead.degree.succ) 0 ++
        ((X - C η) * P).eraseLead.coeffList)
⊢ ((X - C η) * P).coeffList =
    P.leadingCoeff :: ((X - C η) * P).nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case zero
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid
h_zero' : inst₁.toZero = inst₂.toZero
h_one' : inst₁.toOne = inst₂.toOne
⊢ 0 = 0

Tactic:
exact congrArg (@Zero.zero R) h_zero'

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime : IsCoprime g₁ g₂
q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : R[X]
hr₁₁ : r₁₁.degree < g₁.degree
hr₁₂ : r₁₂.degree < g₁.degree
hr₂₁ : r₂₁.degree < g₂.degree
hr₂₂ : r₂₂.degree < g₂.degree
hf : ↑q₁ + ↑r₁₁ / ↑g₁ + ↑r₂₁ / ↑g₂ = ↑q₂ + ↑r₁₂ / ↑g₁ + ↑r₂₂ / ↑g₂
⊢ q₁ = q₂ ∧ r₁₁ = r₁₂ ∧ r₂₁ = r₂₂

Tactic:
by
  let g : Bool → R[X] := Bool.rec g₂ g₁
  let r₁ : Bool → R[X] := Bool.rec r₂₁ r₁₁
  let r₂ : Bool → R[X] := Bool.rec r₂₂ r₁₂
  have hg (i : Bool) (_ : i ∈ Finset.univ) : (g i).Monic := Bool.rec hg₂ hg₁ i
  have hcoprime : Set.Pairwise (Finset.univ : Finset Bool) fun i j => IsCoprime (g i) (g j) := by
    simp [g, Set.pairwise_insert, hcoprime, hcoprime.symm]
  have hr₁ (i : Bool) (_ : i ∈ Finset.univ) : (r₁ i).degree < (g i).degree := Bool.rec hr₂₁ hr₁₁ i
  have hr₂ (i : Bool) (_ : i ∈ Finset.univ) : (r₂ i).degree < (g i).degree := Bool.rec hr₂₂ hr₁₂ i
  refine (quo_add_sum_rem_div_unique K hg hcoprime hr₁ hr₂ ?_).imp_right fun h =>
    ⟨h true (Finset.mem_univ true), h false (Finset.mem_univ false)⟩
  simpa [g, r₁, r₂, add_assoc] using hf

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddCommMonoid R
inst✝ : Mul R
hz : ∀ {a : R}, a * a = 0 → a = 0
ha : ∀ {s₁ s₂ : R}, IsSumSq s₁ → IsSumSq s₂ → s₁ + s₂ = 0 → s₁ = 0
⊢ ¬IsSumNonzeroSq 0

Tactic:
suffices ∀ (x : R), IsSumNonzeroSq x → x ≠ 0 by grind

Goal state after:
R : Type u_1
inst✝¹ : AddCommMonoid R
inst✝ : Mul R
hz : ∀ {a : R}, a * a = 0 → a = 0
ha : ∀ {s₁ s₂ : R}, IsSumSq s₁ → IsSumSq s₂ → s₁ + s₂ = 0 → s₁ = 0
⊢ ∀ (x : R), IsSumNonzeroSq x → x ≠ 0
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0
⊢ ¬IsSumNonzeroSq 0

Tactic:
suffices ∀ (x : R), IsSumNonzeroSq x → x ≠ 0 by grind

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0
⊢ ∀ (x : R), IsSumNonzeroSq x → x ≠ 0
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
⊢ X ^ n * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n

Tactic:
by
  induction n generalizing p with
  | zero      => simp only [pow_zero, one_mul, Function.iterate_zero, id_eq, sum_monomial, mul_one]
  | succ n ih =>
    conv_lhs => rw [pow_succ]
    rw [mul_assoc, X_mul, ← mul_assoc, ih, mul_assoc, ← pow_succ, sum_sum_index (by simp) (by simp)]
    simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
S : Type u_2
inst✝ : Ring S
p : SkewPolynomial R
f g : ℕ → R → S
⊢ (p.sum fun n x ↦ f n x - g n x) = p.sum f - p.sum g

Tactic:
by
  simp only [sub_eq_add_neg, sum_add, sum_neg]

Goal state after:
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ (conjStarAlgAut S R) v = (conjStarAlgAut S R) u ↔ ∃ α, ↑u = α • ↑v

Tactic:
StarAlgEquiv.ext_iff,

Goal state after:
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ (∀ (a : R), ((conjStarAlgAut S R) v) a = ((conjStarAlgAut S R) u) a) ↔ ∃ α, ↑u = α • ↑v
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ ↑(toUnits v)⁻¹ * ↑(toUnits u) ∈ Set.range ⇑(algebraMap S R) ↔ ∃ α, ↑(toUnits u) = α • ↑(toUnits v)

Tactic:
Set.mem_range,

Goal state after:
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ (∃ y, (algebraMap S R) y = ↑(toUnits v)⁻¹ * ↑(toUnits u)) ↔ ∃ α, ↑(toUnits u) = α • ↑(toUnits v)
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ (conjStarAlgAut S R) v = (conjStarAlgAut S R) u ↔ ∃ α, u = α • v

Tactic:
StarAlgEquiv.ext_iff,

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ (∀ (a : R), ((conjStarAlgAut S R) v) a = ((conjStarAlgAut S R) u) a) ↔ ∃ α, u = α • v
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ ↑(toUnits v)⁻¹ * ↑(toUnits u) ∈ Set.range ⇑(algebraMap S R) ↔ ∃ α, u = α • v

Tactic:
Set.mem_range,

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ (∃ y, (algebraMap S R) y = ↑(toUnits v)⁻¹ * ↑(toUnits u)) ↔ ∃ α, u = α • v
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case e_6.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ unsym a * (unsym b + unsym c) + (unsym b * unsym a + unsym c * unsym a) =
    unsym a * unsym b + unsym b * unsym a + (unsym a * unsym c + unsym c * unsym a)

Tactic:
mul_add

Goal state after:
case e_6.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ unsym a * unsym b + unsym a * unsym c + (unsym b * unsym a + unsym c * unsym a) =
    unsym a * unsym b + unsym b * unsym a + (unsym a * unsym c + unsym c * unsym a)
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case e_6.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ unsym a * unsym c + unsym b * unsym c + unsym c * (unsym a + unsym b) =
    unsym a * unsym c + unsym c * unsym a + (unsym b * unsym c + unsym c * unsym b)

Tactic:
mul_add

Goal state after:
case e_6.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ unsym a * unsym c + unsym b * unsym c + (unsym c * unsym a + unsym c * unsym b) =
    unsym a * unsym c + unsym c * unsym a + (unsym b * unsym c + unsym c * unsym b)
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: case inl
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
x y : Tropical R
n : ℕ
h : x ≤ y
⊢ (x + y) ^ n = x ^ n + y ^ n

Tactic:
add_eq_left h,

Goal state after:
case inl
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
x y : Tropical R
n : ℕ
h : x ≤ y
⊢ x ^ n = x ^ n + y ^ n
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a : αˢʸᵐ
⊢ unsym (a * a) = unsym a * unsym a

Tactic:
rw [mul_def, unsym_sym, ← two_mul, invOf_mul_cancel_left]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
a₁ a₂ : G
b₁ b₂ : k
⊢ ((single a₂ b₂).sum fun a₂ b₂ ↦ single (a₁ * a₂) (0 * a₁ • b₂)) = 0

Tactic:
simp [zero_mul, single_zero, sum_zero]

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

Goal state before:
pp: X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ ↑(X.presheaf.1 U) →+* PUnit.{u + 1}

Tactic:
refine ⟨⟨⟨0, ?_⟩, ?_⟩, ?_, ?_⟩ <;> intros <;> rfl

Goal state after:
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
eq₁ : (H.hom ≫ H.inv).c.app (op ((Opens.map H.hom.base).obj U)) = X.presheaf.map (eqToHom ⋯)
eq₂ :
  Y.presheaf.map (eqToHom ⋯).op ≫ H.hom.c.app (op ((Opens.map ((forget C).map (𝟙 Y))).obj U)) =
    H.hom.c.app (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) ≫
      ((Presheaf.pushforward C H.hom.base).obj X.presheaf).map (eqToHom ⋯).op
⊢ H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫ eqToHom ⋯ ≫ H.hom.c.app (op U) =
    𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))

Tactic:
eqToHom_map,

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ X.presheaf.map (⋯.adjunction.counit.app U✝).op = (eqToHom ⋯).app (op U✝)

Tactic:
eqToHom_map,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ eqToHom ⋯ = (eqToHom ⋯).app (op U✝)

case p
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ op U✝ = op (⋯.functor.obj ((Opens.map ⊤.inclusion').obj U✝))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑(X.restrict ⋯)
⊢ (eqToHom ⋯ ≫ (Presheaf.pushforward C X.toRestrictTop.base).map (eqToHom ⋯)).app (op U✝) =
    (𝟙 (X.restrict ⋯)).c.app (op U✝)

Tactic:
eqToHom_map,

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑(X.restrict ⋯)
⊢ (eqToHom ⋯ ≫ eqToHom ⋯).app (op U✝) = (𝟙 (X.restrict ⋯)).c.app (op U✝)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ ((eqToHom ⋯ ≫ (Presheaf.pushforward C (X.ofRestrict ⋯).base).map (eqToHom ⋯)) ≫
          whiskerRight (eqToHom ⋯) X.presheaf).app
      (op U✝) =
    (𝟙 X).c.app (op U✝)

Tactic:
eqToHom_map,

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ ((eqToHom ⋯ ≫ eqToHom ⋯) ≫ whiskerRight (eqToHom ⋯) X.presheaf).app (op U✝) = (𝟙 X).c.app (op U✝)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i ↦ ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
⊢ IsCompatible (X.sheafToTypes T).obj U sf'

Tactic:
exact sf'_comp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
this :
  IsIso (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M x.asIdeal).toRingEquiv.toCommRingCatIso.hom
⊢ Function.Bijective
    ⇑(Localization.localRingHom (Ideal.comap (algebraMap (↑R) (Localization M)) x.asIdeal) x.asIdeal
        (algebraMap (↑R) (Localization M)) ⋯)

Tactic:
by
    rwa [ConcreteCategory.isIso_iff_bijective] at this

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

Goal state before:
pp: case x
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ ↑((Opens.map g.base).obj (h.functor.obj U)) = ↑((opensFunctor f).obj U)

Tactic:
dsimp only [Opens.map_coe, IsOpenMap.coe_functor_obj, comp_base, TopCat.coe_comp]

Goal state after:
case x
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ ⇑(ConcreteCategory.hom g.base) ⁻¹' ⇑(ConcreteCategory.hom g.base) ∘ ⇑(ConcreteCategory.hom f.base) '' ↑U =
    ⇑(ConcreteCategory.hom f.base) '' ↑U
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
⊢ (pullbackConeOfLeftFst f g ≫ f).base = (Y.ofRestrict ⋯ ≫ g).base

Tactic:
simpa using! pullback.condition

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
e : X ≅ Y
y : ↥Y
⊢ e.hom (e.inv y) = y

Tactic:
change (e.inv ≫ e.hom) y = 𝟙 Y.toPresheafedSpace y

Goal state after:
X Y : Scheme
e : X ≅ Y
y : ↥Y
⊢ (e.inv ≫ e.hom) y = (ConcreteCategory.hom (𝟙 Y.toPresheafedSpace).base) y
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 : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst = s.fst

Tactic:
refine PresheafedSpace.Hom.ext _ _ ?_ <| NatTrans.ext <| funext fun x => ?_
  · change pullback.lift _ _ _ ≫ pullback.fst _ _ = _
    simp
  · induction x with | op x => ?_
    change ((_ ≫ _) ≫ _ ≫ _) ≫ _ = _
    simp_rw [Category.assoc]
    erw [← s.pt.presheaf.map_comp]
    erw [s.snd.c.naturality_assoc]
    have := congr_app s.condition (op (opensFunctor f |>.obj x))
    dsimp only [comp_c_app, unop_op] at this
    rw [← IsIso.comp_inv_eq] at this
    replace this := reassoc_of% this
    erw [← this, hf.invApp_app_assoc, s.fst.c.naturality_assoc]
    simp [eqToHom_map]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P✝ P : MorphismProperty Scheme
inst✝ : P.IsStableUnderComposition
⊢ (precoverage P).IsStableUnderComposition

Tactic:
dsimp only [precoverage]; infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P✝ P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ (precoverage P).HasIsos

Tactic:
dsimp only [precoverage]; infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (limit.π (cospan f g) left ≫ (cospan f g).map Hom.inl)

Tactic:
change IsOpenImmersion (_ ≫ f)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (limit.π (cospan f g) left ≫ f)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (eqToHom ⋯ ≫ (Opens.map f.base).map (eqToHom ⋯)).op

Tactic:
eqToHom_map,

Goal state after:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯).op
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasLimits C
inst✝⁴ : HasColimits 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✝² : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)
X Y : SheafedSpace C
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f.hom.base)
H : ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.Hom.stalkMap f.hom x)
U : Opens ↑↑X.toPresheafedSpace
⊢ IsIso (f.hom.c.app (op (hf.functor.obj U)))

Tactic:
by
      apply +allowSynthFailures TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso
          (show Y.sheaf ⟶ (TopCat.Sheaf.pushforward _ f.hom.base).obj X.sheaf from ⟨f.hom.c⟩)
      rintro ⟨_, y, hy, rfl⟩
      specialize H y
      delta PresheafedSpace.Hom.stalkMap at H
      have H' := TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing C
        hf.toIsInducing X.presheaf y
      have := IsIso.comp_isIso' H (@IsIso.inv_isIso _ _ _ _ _ H')
      rwa [Category.assoc, IsIso.hom_inv_id, Category.comp_id] at this

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
H : ∀ (i : 𝒰.I₀), CompactSpace ↥(𝒰.X i)
⊢ CompactSpace ↥X

Tactic:
cases nonempty_fintype 𝒰.I₀

Goal state after:
case intro
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
H : ∀ (i : 𝒰.I₀), CompactSpace ↥(𝒰.X i)
val✝ : Fintype 𝒰.I₀
⊢ CompactSpace ↥X
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : U ≤ basicOpen f
x : ↥(unop (op U))
⊢ ↑(const 0 f U hu) x = ↑0 x

Tactic:
simp; rfl

Goal state after: