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

Goal state before:
pp: case inr.refine_2.e_a.e_a
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)
⊢ (aeval r) ((⇑derivative)^[q - 1] p) = (q - 1)! • eval r p'

pp: case inr.refine_2.e_a
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)
⊢ ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) ((⇑derivative)^[x] p) = q ! • ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) (c x)

Tactic:
· rw [← aeval_iterate_derivative_self _ _ _ hp]

Goal state after:
case inr.refine_2.e_a
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)
⊢ ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) ((⇑derivative)^[x] p) = q ! • ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) (c x)
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝ : CommRing R
x✝ : QuadraticAlgebra R a b
⊢ star (star x✝) = x✝

Tactic:
refine QuadraticAlgebra.ext (by simp) (neg_neg _)

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝ : CommRing R
z w : QuadraticAlgebra R a b
⊢ (z * w).re * (z * w).re + b * (z * w).re * (z * w).im - a * (z * w).im * (z * w).im =
    (z.re * z.re + b * z.re * z.im - a * z.im * z.im) * (w.re * w.re + b * w.re * w.im - a * w.im * w.im)

Tactic:
by simp only [re_mul, im_mul]; ring

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
η : 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

Tactic:
suffices SignType.sign ((X - C η) * P).nextCoeff = -1 by
        simp +decide [signVariations_eq_eraseLead_add_ite h_mul, h_lC,
          leadingCoeff_eraseLead_eq_nextCoeff, ← sign_eq_zero_iff, this]
      grind [← sign_eq_neg_one_iff, coeff_X_sub_C_mul, nextCoeff]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y z : Rᵐᵒᵖ
⊢ op (unop x ◃⁻¹ unop (op (unop y ◃⁻¹ unop z))) = op (unop (op (unop x ◃⁻¹ unop y)) ◃⁻¹ unop (op (unop x ◃⁻¹ unop z)))

Tactic:
induction x

Goal state after:
case h
R : Type u_1
inst✝ : Rack R
y z : Rᵐᵒᵖ
X✝ : R
⊢ op (unop (op X✝) ◃⁻¹ unop (op (unop y ◃⁻¹ unop z))) =
    op (unop (op (unop (op X✝) ◃⁻¹ unop y)) ◃⁻¹ unop (op (unop (op X✝) ◃⁻¹ unop z)))
Module: Mathlib.Algebra.Quandle

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

Tactic:
induction x

Goal state after:
case h
Q : Type u_1
inst✝ : Quandle Q
X✝ : Q
⊢ op X✝ ◃ op X✝ = op X✝
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ F ((algebraMap R ℍ[R,c₁,c₂,c₃]) x✝.re) + x✝.imI • F { re := 0, imI := 1, imJ := 0, imK := 0 } +
        x✝.imJ • F { re := 0, imI := 0, imJ := 1, imK := 0 } +
      x✝.imK • F { re := 0, imI := 0, imJ := 0, imK := 1 } =
    F x✝

Tactic:
simp only [← map_smul, ← map_add, mk_add_mk, smul_mk, smul_zero, algebraMap_eq]

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ F
      { re := x✝.re + 0 + 0 + 0, imI := 0 + x✝.imI • 1 + 0 + 0, imJ := 0 + 0 + x✝.imJ • 1 + 0,
        imK := 0 + 0 + 0 + x✝.imK • 1 } =
    F x✝
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: case refine_1.inl
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
a : α
⊢ L a * (toEndRingHom α) f = (toEndRingHom α) f * L a

Tactic:
exact AddMonoidHom.ext fun b ↦ (map_mul_left f a b).symm

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

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
⊢ a ∈ NonUnitalSubsemiring.center α ↔ R a = L a ∧ L a ∈ (toEndRingHom α).rangeS

Tactic:
by
  constructor
  · exact fun ha ↦ ⟨AddMonoidHom.ext <| fun _ => (IsMulCentral.comm ha _).symm,
      ⟨centerToCentroid ⟨a, ha⟩, rfl⟩⟩
  · rintro ⟨hc, ⟨T, hT⟩⟩
    have e1 (d : α) : T d = a * d := congr($hT d)
    have e2 (d : α) : T d = d * a := congr($(hT.trans hc.symm) d)
    constructor
    case comm => exact (congr($hc.symm ·))
    case left_assoc => simpa [e1] using (map_mul_right T · ·)
    case right_assoc => simpa [e2] using (map_mul_left T · ·)

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

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

Tactic:
by
  rw [← monomial_one_one_eq_X, monomial_mul_monomial, iterate_map_one, mul_one]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
p : SkewMonoidAlgebra k G
⊢ p.support = ∅ ↔ p = 0

Tactic:
rcases p
  simp only [support, Finsupp.support_eq_empty, ofCoeff_eq_zero]

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✝ : ∃ α, u = α • v
y : ↥(unitary S)
h : u = y • v
⊢ ↑y • 1 = star ↑v * ↑u

Tactic:
by
    simp only [h, coe_smul, mul_smul_comm, SetLike.coe_mem, star_mul_self_of_mem]; rfl

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : CommMonoid G
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
hgk : ∀ (g : G) (r : k), g • r = r
⊢ (b.coeff.sum fun x' v' ↦ a.coeff.sum fun x v ↦ single (x * x') (v * v')) =
    b.coeff.sum fun a₁ b₁ ↦ a.coeff.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * b₂)

Tactic:
exact Finsupp.sum_congr (fun x _ ↦ Finsupp.sum_congr
      (fun y _ ↦ by rw [mul_comm, mul_comm (a.coeff y) _]))

Goal state after:
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
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
⊢ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x} = {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support}

Tactic:
by ext; simp [Finset.mem_filter, Finset.mem_product, hs, and_comm]

Goal state after:
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:
simp only [max_def, untrop_le_iff, untrop_trop]; split_ifs <;> simp

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

Goal state before:
pp: R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
H : Type u_9
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : AddCommMonoid E
inst✝¹⁴ : StarAddMonoid E
inst✝¹³ : Module R E
inst✝¹² : StarModule R E
inst✝¹¹ : AddCommMonoid F
inst✝¹⁰ : StarAddMonoid F
inst✝⁹ : Module R F
inst✝⁸ : StarModule R F
inst✝⁷ : AddCommMonoid G
inst✝⁶ : StarAddMonoid G
inst✝⁵ : Module R G
inst✝⁴ : StarModule R G
inst✝³ : AddCommMonoid H
inst✝² : StarAddMonoid H
inst✝¹ : Module R H
inst✝ : StarModule R H
f : WithConv (E →ₗ[R] F)
g : WithConv (G →ₗ[R] H)
x : TensorProduct R E G
⊢ star ((TensorProduct.map f.ofConv g.ofConv) x) = (TensorProduct.map (star f).ofConv (star g).ofConv) (star x)

Tactic:
simpa using congr($(TensorProduct.intrinsicStar_map f g) (star x))

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

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommMonoid E
inst✝² : Module R E
inst✝¹ : StarAddMonoid E
inst✝ : StarModule R E
f : WithConv (End R E)
hf : IsUnit f.ofConv
⊢ IsUnit (star f).ofConv

Tactic:
have ⟨u, hu⟩ := hf
  have : IsUnit (star (toConv (u : End R E))).ofConv := (star (toConv u)).ofConv.isUnit
  simpa [hu] using this

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 : X.presheaf ⟶ (pushforward C g).obj Z.presheaf
h : ↑Z.toPresheafedSpace ⟶ ↑X.toPresheafedSpace
hc : X.presheaf ⟶ (pushforward C h).obj Z.presheaf
e : { hom := { base := g, c := gc } } ≫ f = { hom := { base := h, c := hc } } ≫ f
⊢ { hom := { base := g, c := gc } } = { hom := { base := h, c := hc } }

Tactic:
obtain rfl : g = h := ConcreteCategory.hom_ext _ _ fun x ↦ h₁ congr(($e).hom.base x)

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
⊢ { hom := { base := g, c := gc } } = { hom := { base := g, c := hc } }
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ (𝟙 X.toSheafedSpace).hom = 𝟙 X.toPresheafedSpace

Tactic:
SheafedSpace.id_hom

Goal state after:
X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ 𝟙 X.toPresheafedSpace = 𝟙 X.toPresheafedSpace
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ (𝟙 Y.toSheafedSpace).hom = 𝟙 Y.toPresheafedSpace

Tactic:
SheafedSpace.id_hom

Goal state after:
X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ 𝟙 Y.toPresheafedSpace = 𝟙 Y.toPresheafedSpace
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

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

Tactic:
eqToHom_op,

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

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

Tactic:
SetLike.mem_coe,

Goal state after:
case mp
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom f.base) x ∈ U
hx : IsUnit ((ConcreteCategory.hom (Y.toRingedSpace.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
⊢ x ∈ X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case app
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj (unop U))) = U

Tactic:
induction U with | op U => ?_

Goal state after:
case app.op
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U : Opens ↑↑(Y.restrict ⋯)
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj (unop (op U)))) = op U
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op V ⟶ op V'
⊢ appLE f U V e ≫ X.presheaf.map i = appLE f U V' ⋯

Tactic:
Hom.appLE,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op V ⟶ op V'
⊢ (app f U ≫ X.presheaf.map (homOfLE e).op) ≫ X.presheaf.map i = appLE f U V' ⋯
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op U' ⟶ op U
⊢ Y.presheaf.map i ≫ appLE f U V e = appLE f U' V ⋯

Tactic:
Hom.appLE,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op U' ⟶ op U
⊢ Y.presheaf.map i ≫ app f U ≫ X.presheaf.map (homOfLE e).op = appLE f U' 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
h' : Epi f.base
U : (Opens ↑↑Y)ᵒᵖ
⊢ U = op ((opensFunctor f).obj ((Opens.map f.base).obj (unop U)))

Tactic:
induction U with | op U => ?_

Goal state after:
case op
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
U : Opens ↑↑Y
⊢ op U = op ((opensFunctor f).obj ((Opens.map f.base).obj (unop (op U))))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U V : X.Opens
i : op U ⟶ op V
⊢ Y.presheaf.map ((opensFunctor f).map i.unop).op ≫ (appIso f V).hom = (appIso f U).hom ≫ X.presheaf.map i

Tactic:
simp [← cancel_mono (f.appIso V).inv]

Goal state after:
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 (algebraMap R S)))

Tactic:
← e,

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
        ((↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).comp
          (algebraMap R (Localization.Away f)))))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (pullback.snd (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))) '' Set.univ =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)

pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop f g).hom)

Tactic:
← @Set.preimage_univ _ _ (pullback.fst f.base g.base)

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (pullback.snd (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))) ''
      ⇑(ConcreteCategory.hom (pullback.fst f.base g.base)) ⁻¹' Set.univ =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)

X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop f g).hom)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

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

Tactic:
eqToHom_op,

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = X.basicOpen r
⊢ f ''ᵁ X.basicOpen r = Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)

Tactic:
← e,

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = X.basicOpen r
⊢ f ''ᵁ f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) =
    Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : Epi f.base
⊢ IsIso f

Tactic:
by
  rw [← isIso_iff_of_reflects_iso _ LocallyRingedSpace.forgetToSheafedSpace]
  have : Epi (forgetToSheafedSpace.map f).hom.base := by assumption
  apply SheafedSpace.IsOpenImmersion.to_iso

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
y : ↥X
hyU : y ∈ U
hyW : ⟨y, hyU⟩ ∈ ↑(X.homOfLE e ⁻¹ᵁ W)
⊢ ⟨y, ⋯⟩ ∈ ↑W

Tactic:
by simpa [homOfLE_apply'] using hyW

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
y : ↥↑V
hyW : y ∈ ↑W
hyU : (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom V.ι)).hom.base) y ∈ ↑U
⊢ ⟨↑y, hyU⟩ ∈ ↑(X.homOfLE e ⁻¹ᵁ W)

Tactic:
by simpa [homOfLE_apply'] using hyW

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

Goal state before:
pp: case mpr.refine_3
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
y : ↑(F.obj.obj (op W))
e₁ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
⊢ (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (F.obj.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) =
    (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y

Tactic:
rw [← e₂, ← TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd]
      simp only [← CommRingCat.comp_apply, ← Functor.map_comp, ← op_comp,
        homOfLE_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s = X.toRingedSpace.zeroLocus s

Tactic:
simp only [RingedSpace.zeroLocus]

Goal state after:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s = ⋂ f ∈ s, (↑(X.toRingedSpace.basicOpen f))ᶜ