mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹² : DivisionRing K
inst✝¹¹ : LinearOrder K
inst✝¹⁰ : IsOrderedRing K
inst✝⁹ : Archimedean K
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
inst✝⁵ : Module K M
inst✝⁴ : IsOrderedModule K M
R : Type u_3
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : Module K R
seed : Seed K M R
inst✝ : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x y : ↥(sSupFun hc).domain
h : x < y
hyx : ↑(y - x) ∈ (sSupFun hc).domain
⊢ 0 < ↑(sSupFun hc) (y - x)

Tactic:
sSupFun,

Goal state after:
K : Type u_1
inst✝¹² : DivisionRing K
inst✝¹¹ : LinearOrder K
inst✝¹⁰ : IsOrderedRing K
inst✝⁹ : Archimedean K
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
inst✝⁵ : Module K M
inst✝⁴ : IsOrderedModule K M
R : Type u_3
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : Module K R
seed : Seed K M R
inst✝ : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x y : ↥(sSupFun hc).domain
h : x < y
hyx : ↑(y - x) ∈ (LinearPMap.sSup ((fun x ↦ ↑x) '' c) ⋯).domain
⊢ 0 < ↑(sSupFun hc) (y - x)
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
c✝ : Set (Partial seed)
hnonempty : c✝.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c✝
x : ↥(sSupFun hc).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ (sSupFun hc).domain
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑(sSupFun hc) x))) ∈ (sSupFun hc).toFun.range

Tactic:
sSupFun,

Goal state after:
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
c✝ : Set (Partial seed)
hnonempty : c✝.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c✝
x : ↥(sSupFun hc).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ (LinearPMap.sSup ((fun x ↦ ↑x) '' c✝) ⋯).domain
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑(sSupFun hc) x))) ∈ (sSupFun hc).toFun.range
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Subsingleton R
⊢ (p * q).IsMonicOfDegree (m + n)

pp: case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
⊢ (p * q).IsMonicOfDegree (m + n)

Tactic:
· simp only [isMonicOfDegree_iff_of_subsingleton, Nat.add_eq_zero_iff] at hp hq ⊢
    exact ⟨hp, hq⟩

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
⊢ (p * q).IsMonicOfDegree (m + n)
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
l : List α
a b : α
hab : R a b
⊢ IsChain R (a :: destutter' R b l)

Tactic:
simpa [destutter'_cons, hab] using isChain_destutter' R (b :: l) a

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
⊢ ((p.homogenize p.natDegree).coeff.sum fun x c ↦ f c) = p.sum fun x c ↦ f c

Tactic:
rw [MvPolynomial.sum_def, sum_def p]

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
⊢ ∑ m ∈ (p.homogenize p.natDegree).support, f (MvPolynomial.coeff m (p.homogenize p.natDegree)) =
    ∑ n ∈ p.support, f (p.coeff n)
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

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

Tactic:
Function.iterate_succ_apply'

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

Goal state before:
pp: p : ℤ[X]
hp : p.IsUnitTrinomial
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
hq : q.IsUnitTrinomial
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
obtain ⟨k, m, n, hkm, hmn, u, v, w, hp⟩ := hp

Goal state after:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
hq : q.IsUnitTrinomial
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case neg
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
⊢ (monomial P.natDegree) ((X - C η) * P).nextCoeff =
    (monomial P.natDegree) P.nextCoeff - C η * (monomial P.natDegree) P.leadingCoeff

Tactic:
grind [coeff_X_sub_C_mul, nextCoeff_of_natDegree_pos, leadingCoeff]

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

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
r : R
hr : norm x * r = 1
hr' : r * norm x = 1
⊢ ∃ b_1, x * b_1 = 1 ∧ b_1 * x = 1

Tactic:
← C_inj (R := R) (a := a) (b := b),

Goal state after:
case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
r : R
hr : QuadraticAlgebra.C (norm x * r) = QuadraticAlgebra.C 1
hr' : r * norm x = 1
⊢ ∃ b_1, x * b_1 = 1 ∧ b_1 * x = 1
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case succ.inl.refine_2
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 : P.eraseLead.signVariations + 1 ≤ ((X - C η) * P.eraseLead).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
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 = -1
h₁ : P.nextCoeff ≠ 0
this : P.signVariations = P.eraseLead.signVariations + 1
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
trans ((X - C η) * P).eraseLead.signVariations + 1

Goal state after:
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 : P.eraseLead.signVariations + 1 ≤ ((X - C η) * P.eraseLead).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
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 = -1
h₁ : P.nextCoeff ≠ 0
this : P.signVariations = P.eraseLead.signVariations + 1
⊢ P.signVariations + 1 ≤ ((X - C η) * P).eraseLead.signVariations + 1

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 : P.eraseLead.signVariations + 1 ≤ ((X - C η) * P.eraseLead).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
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 = -1
h₁ : P.nextCoeff ≠ 0
this : P.signVariations = P.eraseLead.signVariations + 1
⊢ ((X - C η) * P).eraseLead.signVariations + 1 ≤ ((X - C η) * P).signVariations
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
ih : ∀ (P : R[X]), Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ → n✝ ≤ P.signVariations
η : R
η_pos : 0 < η
Q : R[X]
h : Multiset.countP (fun x ↦ 0 < x) ((X - C η) * Q).roots = n✝ + 1
hp : (X - C η) * Q ≠ 0
η_root : η ∈ ((X - C η) * Q).roots
⊢ Multiset.countP (fun x ↦ 0 < x) Q.roots = n✝

Tactic:
· simp [← h, roots_mul (ne_zero_of_mem_roots η_root), η_pos, ← Nat.succ.injEq]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝ : Quandle Q
⊢ ∀ {x : Qᵐᵒᵖ}, x ◃ x = x

Tactic:
by
    intro x
    induction x
    simp

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : DecidableEq G
r : k
a : G
⊢ image₂ (fun x1 x2 ↦ x1 * x2) f.support {a} ⊆ image (fun x ↦ x * a) f.support

Tactic:
by
    rw [Finset.image₂_singleton_right]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
⊢ ∑ x ∈ p.coeff.support, f (toAdd x) (p.coeff x) = ∑ n ∈ p.support, f n (p.coeff n)

Tactic:
apply Finset.sum_of_injOn (toAdd) (Injective.injOn fun ⦃a₁ a₂⦄ a ↦ a) (fun _ ↦ ?_)

Goal state after:
case h'
R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
⊢ ∀ i ∈ p.support, i ∉ ⇑toAdd '' ↑p.coeff.support → f i (p.coeff i) = 0

case h
R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
⊢ ∀ i ∈ p.coeff.support, f (toAdd i) (p.coeff i) = f (toAdd i) (p.coeff (toAdd i))

R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
x✝ : Multiplicative ℕ
⊢ x✝ ∈ ↑p.coeff.support → toAdd x✝ ∈ ↑p.support
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
p : SkewMonoidAlgebra k G → Prop
f : SkewMonoidAlgebra k G
zero : p 0
single : ∀ (g : G) (a : k), p (SkewMonoidAlgebra.single g a)
add : ∀ (f g : SkewMonoidAlgebra k G), p f → p g → p (f + g)
⊢ p (f.sum SkewMonoidAlgebra.single)

Tactic:
sum_def'

Goal state after:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
p : SkewMonoidAlgebra k G → Prop
f : SkewMonoidAlgebra k G
zero : p 0
single : ∀ (g : G) (a : k), p (SkewMonoidAlgebra.single g a)
add : ∀ (f g : SkewMonoidAlgebra k G), p f → p g → p (f + g)
⊢ p (∑ a ∈ f.support, SkewMonoidAlgebra.single a (f.coeff a))
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 = ∑ i ∈ this.toFinset, f.coeff i.1 * i.1 • g.coeff i.2

Tactic:
let s := Set.Finite.toFinset (s := ({p : G × G | p.1 * p.2 = x}
    ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2)) 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
s : Finset (G × G) := this.toFinset
⊢ (f * g).coeff x = ∑ i ∈ this.toFinset, f.coeff i.1 * i.1 • g.coeff i.2
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: case inr.inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
hx : z ≤ x
⊢ y ≤ x + z

Tactic:
rwa [add_eq_right hx]

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

Goal state before:
pp: X✝ X Y Z : LocallyRingedSpace
f : X.Hom Y
g : Y.Hom Z
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (f.toHom ≫ g.toHom) x))

Tactic:
by
    rw [PresheafedSpace.stalkMap.comp]
    apply +allowSynthFailures RingHom.isLocalHom_comp
    all_goals apply isLocalHomValStalkMap

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

Goal state before:
pp: case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this✝ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
this : g₁.base = g₂.base
⊢ g₁.base = g₂.base

Tactic:
exact this

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

Goal state before:
pp: case mpr
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s)) →
    x ∈ ↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s))

Tactic:
· rintro ⟨hxU, hx⟩
    simp only [Opens.map_coe, Set.mem_preimage, SetLike.mem_coe, toRingedSpace] at hx ⊢
    rw [RingedSpace.mem_basicOpen _ s (f.base x) hxU]
    rw [← stalkMap_germ_apply] at hx
    exact (isUnit_map_iff (f.stalkMap x).hom _).mp hx

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

Goal state before:
pp: case mpr
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑(unop V)
w✝ : x ∈ unop U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop U) x w✝)) f)
⊢ x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f))

Tactic:
refine ⟨hxV, ?_⟩

Goal state after:
case mpr
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑(unop V)
w✝ : x ∈ unop U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop U) x w✝)) f)
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop V) x hxV)) ((ConcreteCategory.hom (X.presheaf.map i)) f))
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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ ((sheafIsoOfIso
                (colimit.isoColimitCocone
                    { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm).app
            (op U) ≪≫
          limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
              ((Opens.map
                      (colimit.isoColimitCocone
                              { cocone := colimitCocone F,
                                isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
                (op U)) ≪≫
            lim.mapIso (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫
      (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)

Tactic:
Iso.trans_inv,

Goal state after:
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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ ((limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
              ((Opens.map
                      (colimit.isoColimitCocone
                              { cocone := colimitCocone F,
                                isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
                (op U)) ≪≫
            lim.mapIso (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫
        ((sheafIsoOfIso
                (colimit.isoColimitCocone
                    { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm).app
            (op U)).inv) ≫
      (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)
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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ ((limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
              ((Opens.map
                      (colimit.isoColimitCocone
                              { cocone := colimitCocone F,
                                isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
                (op U)) ≪≫
            lim.mapIso (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫
        ((sheafIsoOfIso
                (colimit.isoColimitCocone
                    { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm).app
            (op U)).inv) ≫
      (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)

Tactic:
Iso.trans_inv,

Goal state after:
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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ (((lim.mapIso (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫
          (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
              ((Opens.map
                      (colimit.isoColimitCocone
                              { cocone := colimitCocone F,
                                isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
                (op U))).inv) ≫
        ((sheafIsoOfIso
                (colimit.isoColimitCocone
                    { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm).app
            (op U)).inv) ≫
      (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
f : ↑R
x : ↥(Spec R)
this : IsUnit ((algebraMap ↑R ↑((structurePresheafInCommRingCat ↑R).stalk x)) f) ↔ f ∉ x.asIdeal
⊢ IsUnit
      ((ConcreteCategory.hom ((Spec R).presheaf.germ ⊤ x _root_.trivial))
        ((ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) f)) ↔
    x ∈ PrimeSpectrum.basicOpen f

Tactic:
exact this

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : Opens ↥X
x : ↥U
f s : ↑Γ(X, U)
hx : ↑x ∈ X.basicOpen s
n : ℕ
hf : s ^ n * f = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0

Tactic:
rw [Scheme.mem_basicOpen X s x x.2] at hx

Goal state after:
X : Scheme
U : Opens ↥X
x : ↥U
f s : ↑Γ(X, U)
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s)
n : ℕ
hf : s ^ n * f = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
s : Set ↑R
x : ↥(Spec R)
⊢ x ∈ (Spec R).zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) '' s) ↔ x ∈ PrimeSpectrum.zeroLocus s

Tactic:
suffices (∀ a ∈ s, x ∉ PrimeSpectrum.basicOpen a) ↔ x ∈ PrimeSpectrum.zeroLocus s by simpa

Goal state after:
R : CommRingCat
s : Set ↑R
x : ↥(Spec R)
⊢ (∀ a ∈ s, x ∉ PrimeSpectrum.basicOpen a) ↔ x ∈ PrimeSpectrum.zeroLocus s
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
⊢ Presieve.singleton f ∈ jointlySurjectivePrecoverage.coverings Y ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
rw [mem_jointlySurjectivePrecoverage_iff]

Goal state after:
X Y : Type u
f : X ⟶ Y
⊢ (∀ (x : Y), ∃ Y_1 g, Presieve.singleton f g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)) ↔
    Function.Surjective ⇑(ConcreteCategory.hom f)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ V ≤ U

Tactic:
preimage_image_eq

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : V ≤ U
⊢ V ≤ U
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
⊢ IsLimit
    ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
      ((forget C).mapCone (pullbackConeOfLeft f g)))

Tactic:
refine (IsLimit.equivIsoLimit ?_).toFun (limit.isLimit (cospan f.base g.base))

Goal state after:
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
⊢ limit.cone (cospan f.base g.base) ≅
    (Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj ((forget C).mapCone (pullbackConeOfLeft f g))
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
fn : 𝒰.I₀ → ℕ
hfn : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s ^ fn i = 0
⊢ IsNilpotent s

Tactic:
have : Fintype 𝒰.I₀ := Fintype.ofFinite 𝒰.I₀

Goal state after:
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
fn : 𝒰.I₀ → ℕ
hfn : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s ^ fn i = 0
this : Fintype 𝒰.I₀
⊢ IsNilpotent s
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case h.h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : const a (↑b) (basicOpen f) ⋯ = const c (↑d) (basicOpen f) ⋯
⊢ ∀ x ∈ PrimeSpectrum.zeroLocus ↑(⊥.colon {d • a - b • c}), f ∈ x.asIdeal

Tactic:
intro p

Goal state after:
case h.h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : const a (↑b) (basicOpen f) ⋯ = const c (↑d) (basicOpen f) ⋯
p : PrimeSpectrum R
⊢ p ∈ PrimeSpectrum.zeroLocus ↑(⊥.colon {d • a - b • c}) → f ∈ p.asIdeal
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
⊢ resLE f U V e ⁻¹ᵁ O = resLE f U V e ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ O

Tactic:
preimage_image_eq

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
⊢ resLE f U V e ⁻¹ᵁ O = resLE f U V e ⁻¹ᵁ O