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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
⊢ (trinomial k m n u v w).natTrailingDegree = k

Tactic:
by
  refine
    natTrailingDegree_eq_of_trailingDegree_eq_some
      ((Finset.le_inf fun i h => ?_).antisymm <|
          trailingDegree_le_of_ne_zero <| by rwa [trinomial_trailing_coeff' hkm hmn]).symm
  replace h := support_trinomial_subset k m n u v w h
  rw [mem_insert, mem_insert, mem_singleton] at h
  rcases h with (rfl | rfl | rfl)
  · exact le_rfl
  · exact WithTop.coe_le_coe.mpr hkm.le
  · exact WithTop.coe_le_coe.mpr (hkm.trans hmn).le

Goal state after:
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'
k : ℕ
hk : k < q
h : ∀ (x : ℕ), (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1)
⊢ eval r (∑ k_1 ∈ range k.succ, k.choose k_1 • ((⇑derivative)^[k - k_1] ((X - C r) ^ q) * (⇑derivative)^[k_1] p')) = 0

Tactic:
iterate_derivative_X_sub_pow,

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'
k : ℕ
hk : k < q
h : ∀ (x : ℕ), (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1)
⊢ eval r
      (∑ x ∈ range k.succ, k.choose x • (q.descFactorial (k - x) • (X - C r) ^ (q - (k - x)) * (⇑derivative)^[x] p')) =
    0
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.succ, q.choose k • ((⇑derivative)^[q - k] ((X - C r) ^ q) * (⇑derivative)^[k] p')) =
    q ! • eval r p'

Tactic:
iterate_derivative_X_sub_pow,

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
      (∑ x ∈ range q.succ, q.choose x • (q.descFactorial (q - x) • (X - C r) ^ (q - (q - x)) * (⇑derivative)^[x] p')) =
    q ! • eval r p'
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial

Tactic:
replace hx := hp.2 k (mem_insert_self k {m, n})

Goal state after:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hy : y ≠ 0
hz : z ≠ 0
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hx : IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inr.refine_2
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)
⊢ Disjoint (range q) (Ico q (p.natDegree + 1))

Tactic:
· rw [range_eq_Ico, disjoint_iff_inter_eq_empty, eq_empty_iff_forall_notMem]
    intro x hx
    rw [mem_inter, mem_Ico, mem_Ico] at hx
    exact hx.1.2.not_ge hx.2.1

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝ : Quandle Q
n : ℕ
x y z : Dihedral n
⊢ dihedralAct n x (dihedralAct n y z) = dihedralAct n (dihedralAct n x y) (dihedralAct n x z)

Tactic:
simp only [dihedralAct]

Goal state after:
Q : Type u_1
inst✝ : Quandle Q
n : ℕ
x y z : Dihedral n
⊢ 2 * x - (2 * y - z) = 2 * (2 * x - y) - (2 * x - z)
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝ : Quandle Q
n : ℕ
x : Dihedral n
⊢ dihedralAct n x x = x

Tactic:
simp only [dihedralAct]

Goal state after:
Q : Type u_1
inst✝ : Quandle Q
n : ℕ
x : Dihedral n
⊢ 2 * x - x = x
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y : R
⊢ act' (x ◃ y) = act' x ◃ act' y

Tactic:
exact ad_conj x y

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f g : CentroidHom α
a b : α
⊢ (↑(↑f + ↑g)).toFun (a * b) = (↑(↑f + ↑g)).toFun a * b

Tactic:
by
        simp [map_mul_right, add_mul]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : MulSemiringAction G k
V : Type u_4
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : Module (SkewMonoidAlgebra k G) V
inst✝ : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, (of k G) g • v ∈ W
f : SkewMonoidAlgebra k G
v : V
hv : v ∈ ↑W
⊢ f • v ∈ ↑W

Tactic:
← sum_single f,

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : MulSemiringAction G k
V : Type u_4
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : Module (SkewMonoidAlgebra k G) V
inst✝ : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, (of k G) g • v ∈ W
f : SkewMonoidAlgebra k G
v : V
hv : v ∈ ↑W
⊢ f.sum single • v ∈ ↑W
Module: Mathlib.Algebra.SkewMonoidAlgebra.Support

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommGroup k
p : SkewMonoidAlgebra k G
⊢ (-p.coeff).support = p.support

Tactic:
Finsupp.support_neg,

Goal state after:
k : Type u_1
G : Type u_2
inst✝ : AddCommGroup k
p : SkewMonoidAlgebra k G
⊢ p.coeff.support = p.support
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
⊢ (f.update a b).coeff a = b

Tactic:
by
  classical
  rw [f.coeff_update_apply, if_pos rfl]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
motive : SkewPolynomial R → Prop
p : SkewPolynomial R
h0 : motive 0
ha : ∀ (n : ℕ) (r : R) (q : SkewPolynomial R), n ∉ q.support → r ≠ 0 → motive q → motive ((monomial n) r + q)
⊢ motive p

Tactic:
apply SkewMonoidAlgebra.induction

Goal state after:
case h0
R : Type u_1
inst✝ : Semiring R
motive : SkewPolynomial R → Prop
p : SkewPolynomial R
h0 : motive 0
ha : ∀ (n : ℕ) (r : R) (q : SkewPolynomial R), n ∉ q.support → r ≠ 0 → motive q → motive ((monomial n) r + q)
⊢ motive 0

case ha
R : Type u_1
inst✝ : Semiring R
motive : SkewPolynomial R → Prop
p : SkewPolynomial R
h0 : motive 0
ha : ∀ (n : ℕ) (r : R) (q : SkewPolynomial R), n ∉ q.support → r ≠ 0 → motive q → motive ((monomial n) r + q)
⊢ ∀ (a : Multiplicative ℕ) (b : R) (f : SkewMonoidAlgebra R (Multiplicative ℕ)),
    a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
a b : R
n : ℕ
⊢ (monomial n) (a - b) = (monomial n) a - (monomial n) b

Tactic:
by
  rw [sub_eq_add_neg, monomial_add, monomial_neg, sub_eq_add_neg]

Goal state after:
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

Tactic:
← sum_single f,

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 (f.sum SkewMonoidAlgebra.single)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ (f.sum fun a₁ b₁ ↦ (g + h).sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
    (f.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) +
      f.sum fun a₁ b₁ ↦ h.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)

Tactic:
refine Eq.trans (congr_arg (sum f) (funext₂ fun _ _ ↦ sum_add_index ?_ ?_)) ?_ <;>
      simp only [smul_zero, smul_add, mul_add, mul_zero, single_zero, single_add,
        forall_true_iff, sum_add]

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

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

Tactic:
rw [mul_assoc, ← mul_assoc (f (y • b.coeff x)), h_comm hy, mul_assoc, mul_assoc]

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
this : star y * y = 1
⊢ u = ⟨y, ⋯⟩ • v

Tactic:
by ext; exact huv

Goal state after:
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 (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * (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:
← mul_assoc

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 (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * 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.Algebra.Symmetrized

Goal state before:
pp: case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟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) =
    ⅟2 *
      (⅟2 *
        (unsym a * (unsym b * unsym (a * a) + unsym (a * a) * unsym b) +
          (unsym b * unsym (a * a) + unsym (a * a) * unsym b) * unsym a))

Tactic:
← mul_assoc

Goal state after:
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟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) =
    ⅟2 * ⅟2 *
      (unsym a * (unsym b * unsym (a * a) + unsym (a * a) * unsym b) +
        (unsym b * unsym (a * a) + unsym (a * a) * unsym b) * unsym a)
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟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) =
    ⅟2 * ⅟2 *
      (unsym a * unsym b * unsym (a * a) + unsym a * (unsym (a * a) * unsym b) + unsym b * unsym (a * a) * unsym a +
        unsym (a * a) * unsym b * unsym a)

Tactic:
← mul_assoc

Goal state after:
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟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) =
    ⅟2 * ⅟2 *
      (unsym a * unsym b * unsym (a * a) + unsym a * unsym (a * a) * unsym b + unsym b * unsym (a * a) * unsym a +
        unsym (a * a) * unsym b * unsym a)
Module: Mathlib.Algebra.Vertex.VertexOperator

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), BddBelow (Function.support fun y ↦ (f y) x)
n : ℤ
⊢ ncoeff (of_coeff f hf) n = f (-n - 1)

Tactic:
ext v

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), BddBelow (Function.support fun y ↦ (f y) x)
n : ℤ
v : V
⊢ (ncoeff (of_coeff f hf) n) v = (f (-n - 1)) v
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : OpenNhds ((TopCat.Hom.hom f.base) y)
⊢ colimit.ι ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) y)).op ⋙ Y.presheaf) (op j) ≫
      colimit.desc ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) y)).op ⋙ Y.presheaf)
          { pt := colimit ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) x)).op ⋙ Y.presheaf),
            ι :=
              {
                app := fun U ↦
                  colimit.ι ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) x)).op ⋙ Y.presheaf) (op ⟨↑(unop U), ⋯⟩),
                naturality := ⋯ } } ≫
        colimMap ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) x)).op.whiskerLeft f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map f.base x).op =
    colimit.ι ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) y)).op ⋙ Y.presheaf) (op j) ≫
      (colimMap ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) y)).op.whiskerLeft f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion y).op ⋙ X.presheaf) (OpenNhds.map f.base y).op) ≫
        colimit.desc ((OpenNhds.inclusion y).op ⋙ X.presheaf)
          { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
            ι :=
              { app := fun U ↦ colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf) (op ⟨↑(unop U), ⋯⟩),
                naturality := ⋯ } }

Tactic:
simp only [colimit.ι_desc_assoc, ι_colimMap_assoc, whiskerLeft_app,
    whiskerRight_app, NatTrans.id_app, colimit.ι_pre, assoc,
    colimit.pre_desc, colimit.map_desc, colimit.ι_desc, Cocone.precompose_obj_ι,
    Cocone.whisker_ι, NatTrans.comp_app]

Goal state after:
case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : OpenNhds ((TopCat.Hom.hom f.base) y)
⊢ f.c.app ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) x)).op.obj (op ⟨↑j, ⋯⟩)) ≫
      X.presheaf.map (𝟙 ((OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op.obj (op ⟨↑j, ⋯⟩))) ≫
        colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf) ((OpenNhds.map f.base x).op.obj (op ⟨↑j, ⋯⟩)) =
    f.c.app ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) y)).op.obj (op j)) ≫
      X.presheaf.map (𝟙 ((OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op.obj (op j))) ≫
        colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf) (op ⟨↑(unop ((OpenNhds.map f.base y).op.obj (op j))), ⋯⟩)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: 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
V : Opens ↑↑(X.restrict hf)
⊢ ↑((Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V)) = ↑V

Tactic:
exact Set.preimage_image_eq _ hf.injective

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ X.zeroLocus {f} = (X.basicOpen f).carrierᶜ

Tactic:
by
  simp [zeroLocus]

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
⊢ X.zeroLocus ∅ = Set.univ

Tactic:
by
  simp [zeroLocus]

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ X.zeroLocus s ↔ ∀ f ∈ s, x ∉ X.basicOpen f

Tactic:
by
  simp [zeroLocus]

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

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

Tactic:
apply IsIso.comp_isIso'

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)
⊢ IsIso (g.c.app (op (h.functor.obj U)))

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)
⊢ IsIso (f.c.app (op ((Opens.map g.base).obj (h.functor.obj U))))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

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

Tactic:
simp only [app_invApp, Opens.carrier_eq_coe,
    homOfLE_leOfHom, eqToHom_op]
  tauto

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
⊢ ↑((Opens.map f).obj (hf.functor.obj U)) = ↑U

Tactic:
exact Set.preimage_image_eq _ hf.injective

Goal state after:
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
⊢ (opensFunctor f).PreservesOneHypercovers (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Y)

Tactic:
by
  refine Functor.PreservesOneHypercovers.of_coverPreserving ?_
  exact Scheme.Hom.coverPreserving_opensFunctor f

Goal state after:
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
X Y : Type u_2
⊢ ∀ {S : Type u_2} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison (𝟭 (Type u_2)) f g))

Tactic:
S

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
X Y S : Type u_2
⊢ ∀ (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison (𝟭 (Type u_2)) f g))
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : f x = g y
⊢ ∃ a, (pullback.snd f g) a = y

Tactic:
by
  let iso := pullbackSymmetry f g
  have : HasPullback g f := hasPullback_symmetry f g
  obtain ⟨a, ha⟩ := exists_preimage_fst_triplet_of_prop hf y x h.symm
  use (pullbackSymmetry f g).inv a
  rwa [← Scheme.Hom.comp_apply, pullbackSymmetry_inv_comp_snd]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

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

Tactic:
Scheme.Hom.coe_opensRange

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑f ∩ Set.range ⇑g = Set.range ⇑f ∩ Set.range ⇑g
Module: Mathlib.AlgebraicGeometry.OpenImmersion

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

Tactic:
Scheme.Hom.coe_opensRange

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑g ∩ Set.range ⇑f = Set.range ⇑g ∩ Set.range ⇑f
Module: Mathlib.AlgebraicGeometry.Cover.Open

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

Tactic:
by
  choose U R h using X.local_affine
  let e (x) := (h x).some
  exact
  { I₀ := X
    X x := Spec (R x)
    f x := ⟨(e x).inv ≫ X.toLocallyRingedSpace.ofRestrict _⟩
    mem₀ := by
      rw [presieve₀_mem_precoverage_iff]
      refine ⟨fun x ↦ ⟨x, ⟨(e x).hom.base ⟨x, (U x).2⟩, ?_⟩⟩, inferInstance⟩
      change ((((e x).hom ≫ (e x).inv).base ≫ (X.ofRestrict _).base)) ⟨x, _⟩ = x
      cat_disch }

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀
⊢ (pullbackSymmetry ((𝒰.X i.fst).affineCover.f i.snd) (pullback.fst (𝒰.f i.fst) f)).inv ≫
      (pullbackRightPullbackFstIso (𝒰.f i.fst) f ((𝒰.X i.fst).affineCover.f i.snd)).hom ≫
        pullback.snd (𝒰.affineRefinement.f i) f =
    pullback.fst (pullback.fst (𝒰.f i.fst) f) ((𝒰.X i.fst).affineCover.f i.snd) ≫ pullback.snd (𝒰.f i.fst) f

Tactic:
convert!
    pullbackSymmetry_inv_comp_snd_assoc ((𝒰.X i.1).affineCover.f i.2) (pullback.fst _ _) _ using 2

Goal state after:
case e'_2
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀
e_1✝ :
  (pullback (pullback.fst (𝒰.f i.fst) f) ((𝒰.X i.fst).affineCover.f i.snd) ⟶ X) =
    (pullback (pullback.fst (𝒰.f i.fst) f) ((𝒰.X i.fst).affineCover.f i.snd) ⟶ X)
⊢ (pullbackRightPullbackFstIso (𝒰.f i.fst) f ((𝒰.X i.fst).affineCover.f i.snd)).hom ≫
      pullback.snd (𝒰.affineRefinement.f i) f =
    pullback.snd ((𝒰.X i.fst).affineCover.f i.snd) (pullback.fst (𝒰.f i.fst) f) ≫ pullback.snd (𝒰.f i.fst) f