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

Goal state before:
pp: case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : ¬q.Monic
⊢ 1 * p.coeff i ∈ Mq ^ deg(p) * Mp

Tactic:
← one_pow p.natDegree

Goal state after:
case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : ¬q.Monic
⊢ 1 ^ deg(p) * p.coeff i ∈ Mq ^ deg(p) * Mp
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.reverse.natDegree + (X ^ p.natTrailingDegree).natDegree = p.natDegree

pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.reverse.leadingCoeff * (X ^ p.natTrailingDegree).leadingCoeff ≠ 0

Tactic:
reverse_natDegree,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.natDegree - p.natTrailingDegree + (X ^ p.natTrailingDegree).natDegree = p.natDegree

R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.reverse.leadingCoeff * (X ^ p.natTrailingDegree).leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n)

Tactic:
by_cases h2 : p.natDegree < n

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
⊢ p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n)

case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : ¬p.natDegree < n
⊢ p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n)
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
⊢ ∑ i ∈ range 1, (⇑derivative)^[i] (C a) = C a

Tactic:
sum_range_one,

Goal state after:
R : Type u_1
inst✝ : Semiring R
a : R
⊢ (⇑derivative)^[0] (C a) = C a
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: ⊢ ∑ x ∈ range 1, (⇑derivative)^[x] X + (⇑derivative)^[1] X = X + C 1

Tactic:
sum_range_one,

Goal state after:
⊢ (⇑derivative)^[0] X + (⇑derivative)^[1] X = X + C 1
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: ⊢ (⇑derivative)^[0] X + (⇑derivative)^[1] X = X + C 1

Tactic:
Function.iterate_zero_apply,

Goal state after:
⊢ X + (⇑derivative)^[1] X = X + C 1
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (⇑derivative)^[0] p + (∑ k ∈ range p.natDegree, (⇑derivative)^[k + 1] p + 0) =
    p + (∑ k ∈ range p.natDegree, (⇑derivative)^[k + 1] p + (⇑derivative)^[p.natDegree + 1] p)

Tactic:
Function.iterate_zero_apply,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p + (∑ k ∈ range p.natDegree, (⇑derivative)^[k + 1] p + 0) =
    p + (∑ k ∈ range p.natDegree, (⇑derivative)^[k + 1] p + (⇑derivative)^[p.natDegree + 1] 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 : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
⊢ eval r
      (∑ k ∈ range q,
          (q.choose (k + 1) * q.descFactorial (q - (k + 1))) • (X - C r) ^ (q - (q - (k + 1))) *
            (⇑derivative)^[k + 1] p' +
        q ! • (⇑derivative)^[0] p') =
    q ! • eval r p'

Tactic:
Function.iterate_zero_apply,

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 : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
⊢ eval r
      (∑ k ∈ range q,
          (q.choose (k + 1) * q.descFactorial (q - (k + 1))) • (X - C r) ^ (q - (q - (k + 1))) *
            (⇑derivative)^[k + 1] p' +
        q ! • p') =
    q ! • eval r p'
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

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

Tactic:
wlog! hx2 : 0 < η
  · simpa [lt_of_le_of_ne hx2, hx] using this (η := -η) (P := -P)
  rw [signVariations, signVariations]
  rw [coeffList_C_mul _ (lt_or_lt_iff_ne.mp (.inr hx2)), ← List.comp_map]
  congr 5
  funext
  simp [hx2, sign_mul]

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
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
this :
  List.map (⇑SignType.sign) ((X - C η) * P).eraseLead.coeffList =
    List.map (⇑SignType.sign) ((X - C η) * P.eraseLead).coeffList
⊢ ((X - C η) * P).eraseLead.signVariations = ((X - C η) * P.eraseLead).signVariations

Tactic:
by
        rw [signVariations, signVariations, this]

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
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
⊢ (X - C η) * P - (monomial (P.natDegree + 1)) P.leadingCoeff - (monomial P.natDegree) ((X - C η) * P).nextCoeff =
    (X - C η) * P.eraseLead - (monomial P.natDegree) P.nextCoeff

Tactic:
← self_sub_monomial_natDegree_leadingCoeff

Goal state after:
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
⊢ (X - C η) * P - (monomial (P.natDegree + 1)) P.leadingCoeff - (monomial P.natDegree) ((X - C η) * P).nextCoeff =
    (X - C η) * (P - (monomial P.natDegree) P.leadingCoeff) - (monomial P.natDegree) P.nextCoeff
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
f : SkewMonoidAlgebra k G
| F f

Tactic:
rw [lift_unique' F]

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
f : SkewMonoidAlgebra k G
| ((lift k G A) ((↑F).comp (of k G))) f
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mp
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ Relation.EqvGen (Rel r) x₁ x₂ → RingConGen.Rel r x₁ x₂

pp: case mpr
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ RingConGen.Rel r x₁ x₂ → Relation.EqvGen (Rel r) x₁ x₂

Tactic:
· intro h
    induction h with
    | rel _ _ h => induction h with
      | of => exact RingConGen.Rel.of _ _ ‹_›
      | add_left _ h => exact h.add (RingConGen.Rel.refl _)
      | mul_left _ h => exact h.mul (RingConGen.Rel.refl _)
      | mul_right _ h => exact (RingConGen.Rel.refl _).mul h
    | refl => exact RingConGen.Rel.refl _
    | symm => exact RingConGen.Rel.symm ‹_›
    | trans => exact RingConGen.Rel.trans ‹_› ‹_›

Goal state after:
case mpr
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ RingConGen.Rel r x₁ x₂ → Relation.EqvGen (Rel r) x₁ x₂
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝ : Semiring R
r : R → R → Prop
⊢ Relation.EqvGen (Rel r) = RingConGen.Rel r

Tactic:
by
  ext x₁ x₂
  constructor
  · intro h
    induction h with
    | rel _ _ h => induction h with
      | of => exact RingConGen.Rel.of _ _ ‹_›
      | add_left _ h => exact h.add (RingConGen.Rel.refl _)
      | mul_left _ h => exact h.mul (RingConGen.Rel.refl _)
      | mul_right _ h => exact (RingConGen.Rel.refl _).mul h
    | refl => exact RingConGen.Rel.refl _
    | symm => exact RingConGen.Rel.symm ‹_›
    | trans => exact RingConGen.Rel.trans ‹_› ‹_›
  · intro h
    induction h with
    | of => exact Relation.EqvGen.rel _ _ (Rel.of ‹_›)
    | refl => exact (RingQuot.ringCon r).refl _
    | symm => exact (RingQuot.ringCon r).symm ‹_›
    | trans => exact (RingQuot.ringCon r).trans ‹_› ‹_›
    | add => exact (RingQuot.ringCon r).add ‹_› ‹_›
    | mul => exact (RingQuot.ringCon r).mul ‹_› ‹_›

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : One G
inst✝ : AddMonoidWithOne k
n : ℕ
⊢ ↑n = single 1 ↑n

Tactic:
by
  induction n <;> simp_all

Goal state after:
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)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
hvy : (1 - star y * y) • ↑v = 0
⊢ ∃ α, u = α • v

Tactic:
smul_eq_zero,

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)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
hvy : 1 - star y * y = 0 ∨ ↑v = 0
⊢ ∃ α, u = α • v
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
a b : Tropical R
⊢ untrop (trop (max (untrop a) (untrop b))) = untrop (if a ≤ b then b else a)

Tactic:
by
      simp only [max_def, untrop_le_iff, untrop_trop]; split_ifs <;> simp

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

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a + b = 0 ↔ a = 0 ∧ b = 0

Tactic:
add_eq_iff

Goal state after:
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a ↔ a = 0 ∧ b = 0
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 g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
⊢ (f * g).coeff x = ∑ᶠ (p : G × G) (_ : p ∈ {p | p.1 * p.2 = x}), f.coeff p.1 * p.1 • g.coeff p.2

Tactic:
rw [← finsum_mem_inter_support, finsum_mem_eq_finite_toFinset_sum _ this]

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
⊢ (f * g).coeff x = ∑ i ∈ this.toFinset, f.coeff i.1 * i.1 • g.coeff i.2
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case calc_1
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ sym
      (⅟2 *
        (⅟2 * (unsym a * unsym b + unsym b * unsym a) * unsym (a * a) +
          unsym (a * a) * ⅟2 * (unsym a * unsym b + unsym b * unsym a))) =
    sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * unsym b * unsym a))

Tactic:
← commute_half_left (unsym (a * a)),

Goal state after:
case calc_1
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ sym
      (⅟2 *
        (⅟2 * (unsym a * unsym b + unsym b * unsym a) * unsym (a * a) +
          ⅟2 * unsym (a * a) * (unsym a * unsym b + unsym b * unsym a))) =
    sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * unsym b * unsym a))
Module: Mathlib.Topology.Sheaves.Limits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Category.{v_1, w} J
inst✝ : HasLimitsOfShape J C
X : TopCat
F : J ⥤ Presheaf C X
H : ∀ (j : J), (F.obj j).IsSheaf
c : Cone F
hc : IsLimit c
⊢ c.pt.IsSheaf

Tactic:
let F' : J ⥤ Sheaf C X :=
    { obj := fun j => ⟨F.obj j, H j⟩
      map := fun f => ⟨F.map f⟩ }
  let e : F' ⋙ Sheaf.forget C X ≅ F := NatIso.ofComponents fun _ => Iso.refl _
  exact Presheaf.isSheaf_of_iso
    ((isLimitOfPreserves (Sheaf.forget C X) (limit.isLimit F')).conePointsIsoOfNatIso hc e)
    (limit F').2

Goal state after:
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.Injective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Epi (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Z.toPresheafedSpace ⟶ ↑X.toPresheafedSpace
gc hc : X.presheaf ⟶ (pushforward C g).obj Z.presheaf
e : { hom := { base := g, c := gc } } ≫ f = { hom := { base := g, c := hc } } ≫ f
x : ↑↑Z.toPresheafedSpace
⊢ PresheafedSpace.Hom.stalkMap f.hom ((ConcreteCategory.hom g) x) ≫
      PresheafedSpace.Hom.stalkMap { hom := { base := g, c := gc } }.hom x =
    PresheafedSpace.Hom.stalkMap f.hom ((ConcreteCategory.hom g) x) ≫
      X.presheaf.stalkSpecializes ⋯ ≫ PresheafedSpace.Hom.stalkMap { hom := { base := g, c := hc } }.hom x

Tactic:
stalkSpecializes_refl,

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.Injective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Epi (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Z.toPresheafedSpace ⟶ ↑X.toPresheafedSpace
gc hc : X.presheaf ⟶ (pushforward C g).obj Z.presheaf
e : { hom := { base := g, c := gc } } ≫ f = { hom := { base := g, c := hc } } ≫ f
x : ↑↑Z.toPresheafedSpace
⊢ PresheafedSpace.Hom.stalkMap f.hom ((ConcreteCategory.hom g) x) ≫
      PresheafedSpace.Hom.stalkMap { hom := { base := g, c := gc } }.hom x =
    PresheafedSpace.Hom.stalkMap f.hom ((ConcreteCategory.hom g) x) ≫
      𝟙 (X.presheaf.stalk ((ConcreteCategory.hom { hom := { base := g, c := hc } }.hom.base) x)) ≫
        PresheafedSpace.Hom.stalkMap { hom := { base := g, c := hc } }.hom x
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 hc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := g, c := hc } }).hom
y : ↑↑Y.toPresheafedSpace
⊢ PresheafedSpace.Hom.stalkMap { hom := { base := g, c := gc } }.hom ((ConcreteCategory.hom f.hom.base) ⋯.choose) ≫
      PresheafedSpace.Hom.stalkMap f.hom ⋯.choose =
    (Z.presheaf.stalkSpecializes ⋯ ≫
        PresheafedSpace.Hom.stalkMap { hom := { base := g, c := hc } }.hom
          ((ConcreteCategory.hom f.hom.base) ⋯.choose)) ≫
      PresheafedSpace.Hom.stalkMap f.hom ⋯.choose

Tactic:
stalkSpecializes_refl,

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 hc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := g, c := hc } }).hom
y : ↑↑Y.toPresheafedSpace
⊢ PresheafedSpace.Hom.stalkMap { hom := { base := g, c := gc } }.hom ((ConcreteCategory.hom f.hom.base) ⋯.choose) ≫
      PresheafedSpace.Hom.stalkMap f.hom ⋯.choose =
    (𝟙
          (Z.presheaf.stalk
            ((ConcreteCategory.hom { hom := { base := g, c := hc } }.hom.base)
              ((ConcreteCategory.hom f.hom.base) ⋯.choose))) ≫
        PresheafedSpace.Hom.stalkMap { hom := { base := g, c := hc } }.hom
          ((ConcreteCategory.hom f.hom.base) ⋯.choose)) ≫
      PresheafedSpace.Hom.stalkMap f.hom ⋯.choose
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case mk.mk.w
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
⊢ toLRSHom'✝¹.base = toLRSHom'✝.base

pp: case h
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
⊢ toLRSHom'✝¹.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = toLRSHom'✝.c

Tactic:
· exact h_base

Goal state after:
case h
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
⊢ toLRSHom'✝¹.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = toLRSHom'✝.c
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✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
⊢ IsIso ((Y.ofRestrict hf).c.app (op (hf.functor.obj U)))

Tactic:
by
    dsimp
    have : (Opens.map f).obj (hf.functor.obj U) = U := by
      ext1
      exact Set.preimage_image_eq _ hf.injective
    convert_to IsIso (Y.presheaf.map (𝟙 _))
    · congr
    · -- Porting note: was `apply Subsingleton.helim; rw [this]`
      -- See https://github.com/leanprover/lean4/issues/2273
      congr
      · simp only
        congr
      apply Subsingleton.helim
      rw [this]
    · infer_instance

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.hom.base
⊢ IsIso f

Tactic:
have : IsIso (forgetToPresheafedSpace.map f) := PresheafedSpace.IsOpenImmersion.to_iso f.hom
  apply isIso_of_reflects_iso _ (SheafedSpace.forgetToPresheafedSpace)

Goal state after:
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let __src := ↑f;
  let __src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  { toFun := (↑↑__src).toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
⊢ f ≫ ⟨↑e_Ring.symm, ⋯⟩ = 𝟙 X

Tactic:
by
            ext x
            exact e_Ring.left_inv x

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

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U V W : (Opens ↑X)ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ CommRingCat.ofHom (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map (i ≫ j))) ⋯) =
    CommRingCat.ofHom (IsLocalization.map (Localization (G.obj V)) (CommRingCat.Hom.hom (F.map i)) ⋯) ≫
      CommRingCat.ofHom (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map j)) ⋯)

Tactic:
by
    delta CommRingCat.ofHom CommRingCat.of Bundled.of
    simp_rw [F.map_comp]
    ext : 1
    dsimp
    rw [IsLocalization.map_comp_map]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case refine_1
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
n : ↥U → ↥U → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : ↑U ⊆ ⋃ i ∈ t, ↑(basicOpen (g i))
N : ℕ := (t ×ˢ t).sup fun x ↦ n x.1 x.2 + 1
i j : ↥t
⊢ (fun i ↦ g ↑i ^ (N + 1)) j • (fun i ↦ g ↑i ^ N • f ↑i) i = (fun i ↦ g ↑i ^ (N + 1)) i • (fun i ↦ g ↑i ^ N • f ↑i) j

Tactic:
dsimp
    convert_to (g i * g ↑j) ^ N • g j • f i = (g i * g ↑j) ^ N • g i • f j
    · module
    · module
    have : n i j + 1 ≤ N := (t ×ˢ t).le_sup (f := fun x ↦ n x.1 x.2 + 1) (b := ⟨_, _⟩) (by simp)
    rw [← Nat.sub_add_cancel this, pow_add, mul_smul, mul_smul]
    congr 1
    convert! (hn i j).symm using 1 <;> module

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: case id.init
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
j : J
⊢ ∀ (b : F.obj none),
    ∃ l fli flj x,
      (ConcreteCategory.hom (F.map fli)) x = (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init j))) b ∧
        (ConcreteCategory.hom (F.map flj)) x = b

Tactic:
exact fun x ↦ ⟨_, .init _, 𝟙 _, x, by simp⟩

Goal state after: