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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a ≠ 0 → (revAt (p.natDegree + p.natTrailingDegree)) a ∈ Finset.range (p.natDegree + 1)

pp: case refine_3
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a₁ ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a₁ ≠ 0 →
      ∀ a₂ ∈ Finset.range (p.natDegree + 1),
        p.mirror.coeff a₂ ≠ 0 →
          (revAt (p.natDegree + p.natTrailingDegree)) a₁ = (revAt (p.natDegree + p.natTrailingDegree)) a₂ → a₁ = a₂

pp: case refine_4
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ b ∈ Finset.range (p.natDegree + 1),
    p.coeff b ≠ 0 →
      ∃ a,
        ∃ (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
          (revAt (p.natDegree + p.natTrailingDegree)) a = b

pp: case refine_5
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a ≠ 0 → p.mirror.coeff a = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) a)

Tactic:
· intro n hn hp
    rw [Finset.mem_range_succ_iff] at *
    rw [revAt_le (hn.trans (Nat.le_add_right _ _))]
    rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right, ← mirror_natTrailingDegree]
    exact natTrailingDegree_le_of_ne_zero hp

Goal state after:
case refine_3
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a₁ ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a₁ ≠ 0 →
      ∀ a₂ ∈ Finset.range (p.natDegree + 1),
        p.mirror.coeff a₂ ≠ 0 →
          (revAt (p.natDegree + p.natTrailingDegree)) a₁ = (revAt (p.natDegree + p.natTrailingDegree)) a₂ → a₁ = a₂

case refine_4
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ b ∈ Finset.range (p.natDegree + 1),
    p.coeff b ≠ 0 →
      ∃ a,
        ∃ (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
          (revAt (p.natDegree + p.natTrailingDegree)) a = b

case refine_5
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a ≠ 0 → p.mirror.coeff a = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) a)
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : ¬R b a
⊢ (if R b a then b :: destutter' R a l else destutter' R b l) = destutter' R b l

Tactic:
if_neg h

Goal state after:
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : ¬R b a
⊢ destutter' R b l = destutter' R b l
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case neg
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
hac : ¬R a c
⊢ (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length

Tactic:
case neg =>
        simp only [if_neg hac]
        exact length_destutter'_cotrans_ge hba

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

Goal state before:
pp: R : Type u_3
inst✝ : Semiring R
r : R
x✝ : R[X]
⊢ (leval r) x✝ = (smeval.linearMap R r) x✝

Tactic:
rw [leval_apply, smeval.linearMap_apply, eval_eq_smeval]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ 3 / 2 ≤ p.natDegree / 2

Tactic:
by apply Nat.div_le_div_right (c := 2) hp2

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ Irreducible (p * C p.leadingCoeff⁻¹) ↔ p.roots = 0

Tactic:
(monic_mul_leadingCoeff_inv hp0).irreducible_iff_roots_eq_zero_of_degree_le_three,

Goal state after:
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ (p * C p.leadingCoeff⁻¹).roots = 0 ↔ p.roots = 0

case hp2
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ 2 ≤ (p * C p.leadingCoeff⁻¹).natDegree

case hp3
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ (p * C p.leadingCoeff⁻¹).natDegree ≤ 3
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ sumIDeriv (derivative p) = derivative (sumIDeriv p)

Tactic:
rw [sumIDeriv_apply_of_le ((natDegree_derivative_le p).trans tsub_le_self), sumIDeriv_apply,
    derivative_sum]
  simp_rw [← Function.iterate_succ_apply, Function.iterate_succ_apply']

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

Goal state before:
pp: p : ℤ[X]
⊢ p.IsUnitTrinomial ↔ (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3

Tactic:
rw [natDegree_mul_mirror, natTrailingDegree_mul_mirror, ← mul_add,
    Nat.mul_div_right _ zero_lt_two, coeff_mul_mirror]

Goal state after:
p : ℤ[X]
⊢ p.IsUnitTrinomial ↔ (p.sum fun x x_1 ↦ x_1 ^ 2) = 3
Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ ⇑((basis a b).repr ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) w)) =
    ⇑((basis a b).repr
        (((LinearMap.toMatrix (basis a b) (basis a b)).symm !![z.re, a * z.im; z.im, z.re + b * z.im]) w))

Tactic:
rw [LinearMap.toMatrix_symm, Matrix.repr_toLin]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ ⇑((basis a b).repr ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) w)) =
    !![z.re, a * z.im; z.im, z.re + b * z.im].mulVec ⇑((basis a b).repr w)
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
hz : z ∈ (QuadraticAlgebra R a b)⁰
⊢ star z ∈ (QuadraticAlgebra R a b)⁰

Tactic:
by
  rw [mem_nonZeroDivisors_iff_right] at hz ⊢
  intro w hw
  apply star_involutive.injective
  rw [star_zero]
  apply hz
  rw [← star_involutive z, ← star_mul, mul_comm, hw, star_zero]

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

Goal state before:
pp: R : Type u
inst₂ : Distrib R
mul✝ add✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ { mul := mul✝, add := add✝, left_distrib := left_distrib✝, right_distrib := right_distrib✝ } = inst₂

Tactic:
rcases inst₂ with @⟨⟨⟩, ⟨⟩⟩

Goal state after:
R : Type u
mul✝¹ add✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
mul✝ add✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ { mul := mul✝¹, add := add✝¹, left_distrib := left_distrib✝¹, right_distrib := right_distrib✝¹ } =
    { mul := mul✝, add := add✝, left_distrib := left_distrib✝, right_distrib := right_distrib✝ }
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
h_group :
  { toAddMonoid := inst₁.toAddMonoid, toNeg := inst₁.toNeg, toSub := inst₁.toSub, toZSMul := inst₁.toZSMul,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ } =
    { toAddMonoid := inst₂.toAddMonoid, toNeg := inst₂.toNeg, toSub := inst₂.toSub, toZSMul := inst₂.toZSMul,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
⊢ inst₁ = inst₂

Tactic:
injection h_group

Goal state after:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
⊢ inst₁ = inst₂
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:
by
    suffices ∀ (x : R), IsSumNonzeroSq x → x ≠ 0 by grind
    intro x hx
    induction hx with
    | sq ha => grind
    | @sq_add b s hb hs ih => grind [ha (IsSumSq.mul_self b) hs.isSumSq]

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

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

Tactic:
by
  ext; simp [ coeff_add, Finsupp.single_add_erase]

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

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a' : α
b : M
h : a' ≠ a
⊢ (if a' = a then b else f.coeff a') = f.coeff a'

Tactic:
if_neg h

Goal state after:
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a' : α
b : M
h : a' ≠ a
⊢ f.coeff a' = f.coeff a'
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : NonAssocSemiring T
r : R → R → Prop
f g : RingQuot r →+* T
w : f.comp (mkRingHom r) = g.comp (mkRingHom r)
x : R
⊢ f ((mkRingHom r) x) = g ((mkRingHom r) x)

Tactic:
exact (RingHom.congr_fun w x :)

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mul_right
R : Type uR
inst✝⁴ : Semiring R
S : Type uS
inst✝³ : CommSemiring S
T : Type uT
A : Type uA
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
inst✝ : Semiring T
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → f x = f y
x : RingQuot r
a✝² b✝¹ a✝¹ b✝ c✝ : R
a✝ : Rel r b✝ c✝
r' : f b✝ = f c✝
⊢ f (a✝¹ * b✝) = f (a✝¹ * c✝)

Tactic:
| mul_right _ r' =>

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mul_right
R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → f x = f y
x : RingQuot s
a✝² b✝¹ a✝¹ b✝ c✝ : A
a✝ : Rel s b✝ c✝
r' : f b✝ = f c✝
⊢ f (a✝¹ * b✝) = f (a✝¹ * c✝)

Tactic:
| mul_right _ r' =>

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : (monomial n) 1 = X ^ n
⊢ (monomial (n + 1)) 1 = X ^ (n + 1)

Tactic:
rw [pow_succ', ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial]

Goal state after:
case succ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : (monomial n) 1 = X ^ n
⊢ (monomial (n + 1)) 1 = (monomial (1 + n)) (1 * (⇑φ)^[1] 1)
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
⊢ star ((star g * ↑f) (star a)) = star ((↑f * star g) (star a))

Tactic:
rw [f.property.comm]

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

Goal state before:
pp: R : Type u_1
n : ℕ
inst✝ : Semiring R
a : R
h : n ≠ 0
⊢ (if n = 0 then a else 0) = 0

Tactic:
if_neg h

Goal state after:
R : Type u_1
n : ℕ
inst✝ : Semiring R
a : R
h : n ≠ 0
⊢ 0 = 0
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n i : ℕ
a : R
h : i ≠ n
⊢ (if i = n then a else p.coeff i) = p.coeff i

Tactic:
if_neg h

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n i : ℕ
a : R
h : i ≠ n
⊢ p.coeff i = p.coeff i
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst✝ : AddCommMonoid k'
f : G →₀ k
g : G → k → G' →₀ k'
⊢ { coeff := f.sum g } = { coeff := f }.sum fun x1 x2 ↦ { coeff := g x1 x2 }

Tactic:
by
  apply coeff_injective; simp only [coeff_sum']

Goal state after:
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
rw [← mul_def, ← mul_def]

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

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (End R E)ˣ
⊢ (End R E)ˣ

Tactic:
by
    refine ⟨(star (toConv ↑f.ofConv : WithConv (End R E))).ofConv,
      (star (toConv ↑(f.ofConv⁻¹ : (End R E)ˣ))).ofConv, ?_, ?_⟩
    all_goals
      rw [mul_eq_comp, ← toConv_injective.eq_iff, ← LinearMap.intrinsicStar_comp']
      simp [← mul_eq_comp, one_eq_id]

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u : U
g' : Γ'
hg' : ¬A (((of R).symm (B u)).coeff g') = 0
hAB : ((of R).symm (B u)).coeff g' = 0
⊢ False

Tactic:
exact hg' (by simp [hAB])

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ ∃ inv,
    Hom.stalkMap α x ≫ inv = 𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x)) ∧
      inv ≫ Hom.stalkMap α x = 𝟙 (X.presheaf.stalk x)

Tactic:
refine
      ⟨eqToHom (show X.presheaf.stalk x = X.presheaf.stalk ((α ≫ β).base x) by rw [h_eq]) ≫
          (β.stalkMap (α.base x) :),
        ?_, ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ Hom.stalkMap α x ≫ eqToHom ⋯ ≫ Hom.stalkMap β ((ConcreteCategory.hom α.base) x) =
    𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x))

case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ (eqToHom ⋯ ≫ Hom.stalkMap β ((ConcreteCategory.hom α.base) x)) ≫ Hom.stalkMap α x = 𝟙 (X.presheaf.stalk x)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : x ∈ V
hf : IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)
y : ↑↑X.toPresheafedSpace
⊢ y ∈ V.carrier → y ∈ {x | ∃ (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)}

Tactic:
hy

Goal state after:
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : x ∈ V
hf : IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)
y : ↑↑X.toPresheafedSpace
hy : y ∈ V.carrier
⊢ y ∈ {x | ∃ (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)}
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case h
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)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
this✝ : IsIso (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))
this :
  g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) =
    g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯)
h :
  g₁.c.app (op V) ≫ ((Presheaf.pushforward C g₁.base).obj Z.presheaf).map (eqToHom hV).op =
    g₂.c.app (op V) ≫ ((Presheaf.pushforward C g₂.base).obj Z.presheaf).map (eqToHom hV).op ≫ Z.presheaf.map (eqToHom ⋯)
⊢ (g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V) = g₂.c.app (op V)

Tactic:
simp only [eqToHom_op, eqToHom_map, eqToHom_trans,
      ← IsIso.comp_inv_eq, inv_eqToHom, Category.assoc] at h

Goal state after:
case h
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)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
this✝ : IsIso (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))
this :
  g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) =
    g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯)
h : g₁.c.app (op V) ≫ eqToHom ⋯ = g₂.c.app (op V)
⊢ (g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V) = g₂.c.app (op V)
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 : (Opens ↑↑Y)ᵒᵖ
⊢ f.c.app x ≫ X.presheaf.map ((Opens.map f.base).op.map (⋯.adjunction.counit.app (unop x)).op ≫ (eqToIso ⋯).hom) =
    f.c.app x

Tactic:
trans f.c.app x ≫ X.presheaf.map (𝟙 _)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
x : (Opens ↑↑Y)ᵒᵖ
⊢ f.c.app x ≫ X.presheaf.map ((Opens.map f.base).op.map (⋯.adjunction.counit.app (unop x)).op ≫ (eqToIso ⋯).hom) =
    f.c.app x ≫ X.presheaf.map (𝟙 ((Opens.map f.base).op.obj x))

C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
x : (Opens ↑↑Y)ᵒᵖ
⊢ f.c.app x ≫ X.presheaf.map (𝟙 ((Opens.map f.base).op.obj x)) = f.c.app x
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 ↑↑X
⊢ X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj U))) ≫ f.c.app (op ((opensFunctor f).obj U)) =
    X.presheaf.map (eqToHom ⋯)

Tactic:
IsIso.inv_hom_id,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ X.presheaf.map (eqToHom ⋯) ≫ 𝟙 (X.presheaf.obj ((Opens.map f.base).op.obj (op ((opensFunctor f).obj U)))) =
    X.presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
f : R
inst✝ : IsLocalization.Away f S
e :
  (↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).comp
      (algebraMap R (Localization.Away f)) =
    algebraMap R S
⊢ IsOpenImmersion
    (Spec.map
      (CommRingCat.ofHom
        ((↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).comp
          (algebraMap R (Localization.Away f)))))

Tactic:
CommRingCat.ofHom_comp,

Goal state after:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
f : R
inst✝ : IsLocalization.Away f S
e :
  (↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).comp
      (algebraMap R (Localization.Away f)) =
    algebraMap R S
⊢ IsOpenImmersion
    (Spec.map
      (CommRingCat.ofHom (algebraMap R (Localization.Away f)) ≫
        CommRingCat.ofHom ↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case w.some.left
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
⊢ ((forget C).mapCone (pullbackConeOfLeft f g)).π.app (some WalkingPair.left) ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.left) =
    (limit.cone (cospan f.base g.base)).π.app (some WalkingPair.left)

pp: case w.some.right
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
⊢ ((forget C).mapCone (pullbackConeOfLeft f g)).π.app (some WalkingPair.right) ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.right) =
    (limit.cone (cospan f.base g.base)).π.app (some WalkingPair.right)

Tactic:
· exact Category.comp_id _

Goal state after:
case w.some.right
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
⊢ ((forget C).mapCone (pullbackConeOfLeft f g)).π.app (some WalkingPair.right) ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.right) =
    (limit.cone (cospan f.base g.base)).π.app (some WalkingPair.right)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case w.some.right
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
⊢ ((forget C).mapCone (pullbackConeOfLeft f g)).π.app (some WalkingPair.right) ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.right) =
    (limit.cone (cospan f.base g.base)).π.app (some WalkingPair.right)

Tactic:
· exact Category.comp_id _

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case pos
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥U
⊢ iU x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W) ↔ iU x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)

Tactic:
simp only [SetLike.mem_coe, Opens.map_coe, Set.mem_preimage, ← Scheme.Hom.comp_apply, ← H.w]

Goal state after:
case pos
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥U
⊢ iU x ∈ iU ''ᵁ f' ⁻¹ᵁ W ↔ (f' ≫ iV) x ∈ iV ''ᵁ W
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₀
⊢ (pullbackCoverAffineRefinementObjIso f 𝒰 i).inv ≫ Cover.pullbackHom 𝒰.affineRefinement.openCover f i =
    Cover.pullbackHom (𝒰.X i.fst).affineCover (Cover.pullbackHom 𝒰 f i.fst) i.snd

Tactic:
simp only [Cover.pullbackHom, pullbackCoverAffineRefinementObjIso, Iso.trans_inv, asIso_inv,
    Iso.symm_inv, Category.assoc, pullbackSymmetry_inv_comp_snd, IsIso.inv_comp_eq, limit.lift_π,
    PullbackCone.mk_π_app, Category.comp_id]
  convert! pullbackSymmetry_inv_comp_fst ((𝒰.X i.1).affineCover.f i.2) (pullback.fst _ _)
  exact pullbackRightPullbackFstIso_hom_fst _ _ _

Goal state after: