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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
this : ↑z ≠ x
hzy : z < y
⊢ ↑z - ↑y ≠ 0

Tactic:
apply sub_ne_zero_of_ne

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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
this : ↑z ≠ x
hzy : z < y
⊢ ↑z ≠ ↑y
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : stabilizer G s ≤ stabilizer G t
hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G t
⊢ stabilizer G (s ∪ t) = stabilizer G s

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : stabilizer G s ≤ stabilizer G t
hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G t
⊢ stabilizer G (s ∪ t) ≤ stabilizer G s

case refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : stabilizer G s ≤ stabilizer G t
hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G t
⊢ stabilizer G s ≤ stabilizer G (s ∪ t)
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: case refine_1
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : stabilizer G s ≤ stabilizer G t
hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G t
⊢ stabilizer G (s ∪ t) ≤ stabilizer G s

pp: case refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : stabilizer G s ≤ stabilizer G t
hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G t
⊢ stabilizer G s ≤ stabilizer G (s ∪ t)

Tactic:
· calc
      stabilizer G (s ∪ t)
        ≤ stabilizer G (s ∪ t) ⊓ stabilizer G t := by simpa
      _ ≤ stabilizer G ((s ∪ t) \ t) := stabilizer_inf_stabilizer_le_stabilizer_sdiff
      _ = stabilizer G s := by rw [union_sdiff_cancel_right]; simpa [← disjoint_iff_inter_eq_empty]

Goal state after:
case refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : stabilizer G s ≤ stabilizer G t
hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G t
⊢ stabilizer G s ≤ stabilizer G (s ∪ t)
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ coeffList 0 = []

Tactic:
simp [coeffList]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
⊢ P.coeffList = [] ↔ P = 0

Tactic:
simp [coeffList]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
⊢ P.coeffList.length = P.degree.succ

Tactic:
simp [coeffList]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
P : R[X]
hp : ¬P = 0
⊢ (-P).coeffList = List.map (fun x ↦ -x) P.coeffList

Tactic:
simp [coeffList]

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
n : ℕ
x : A
⊢ d.mapCoeffs ((monomial n) x) = PolynomialModule.single A n (d x)

Tactic:
by
  ext; simp [coeff_monomial, apply_ite d, Finsupp.single_apply]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Irreducible

Goal state before:
pp: case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ b.leadingCoeff * ?refine_2.b = 1

pp: case refine_2.b
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ R

Tactic:
· rw [mul_comm]
    exact q

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
h : 1 ≤ n
v : Fin n → R
⊢ ((ofFn n) v).natDegree < n

Tactic:
rw [Nat.lt_iff_le_pred h, natDegree_le_iff_coeff_eq_zero]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
h : 1 ≤ n
v : Fin n → R
⊢ ∀ (N : ℕ), n - 1 < N → ((ofFn n) v).coeff N = 0
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : Semiring R
p q : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
x✝² : ℕ
x✝¹ x✝ : R
⊢ smul_pow x x✝² (x✝¹ + x✝) = smul_pow x x✝² x✝¹ + smul_pow x x✝² x✝

Tactic:
rw [smul_pow, smul_pow, smul_pow, add_smul]

Goal state after:
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
hw : w ≠ 0
⊢ C w * X ^ k + C v * X ^ (n - m + k) + C u * X ^ n = trinomial k (n - m + k) n w v u

Tactic:
← trinomial_def

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
⊢ trinomial k (n - m + k) n w v u = trinomial k (n - m + k) n w v u
Module: Mathlib.Algebra.PresentedMonoid.Basic

Goal state before:
pp: α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
⊢ closure (range (of rels)) = ⊤

Tactic:
rw [Submonoid.eq_top_iff']
  intro x
  induction x with | _ a
  induction a with
  | one => exact Submonoid.one_mem _
  | of x => exact subset_closure <| by simp [range, of]
  | mul x y hx hy => exact Submonoid.mul_mem _ hx hy

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
a b : QuadraticAlgebra R a✝ b✝
⊢ star (a * b) = star b * star a

Tactic:
ext <;>
    simp only [re_star, re_mul, im_mul, im_star, mul_neg, neg_mul, neg_neg] <;> ring

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
⊢ LinearMap.det (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) = norm z

Tactic:
← LinearMap.det_toMatrix <| basis ..

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
⊢ ((LinearMap.toMatrix (basis a b) (basis a b)) (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z)).det = norm z
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocSemiring R)

Tactic:
intro _ _ h
  -- Use above extensionality lemma to prove injectivity by showing that `h_add` and `h_mul` hold.
  ext x y
  · exact congrArg (·.toAdd.add x y) h
  · exact congrArg (·.toMul.mul x y) h

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

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ 0 ≤ (√2)⁻¹ • (P ^ 2 + Q ^ 2)

Tactic:
have P_sa : star P = P := by
      simp only [P, star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa]

Goal state after:
R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
⊢ 0 ≤ (√2)⁻¹ • (P ^ 2 + Q ^ 2)
Module: Mathlib.Algebra.TrivSqZeroExt.Ideal

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
r : R
m : M
hrm : (r, m) = inr (snd (r, m))
⊢ r = 0

Tactic:
rw [← fst_mk r m, hrm, fst_inr]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_3
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : SkewMonoidAlgebra k G
⊢ (liftNC ↑f ⇑g) (c • φ) = f c * (liftNC ↑f ⇑g) φ

Tactic:
by
  suffices this :
    (liftNC ↑f g).comp (smulAddHom k (SkewMonoidAlgebra k G) c) =
      (AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f g) by simpa using congr($this φ)
  refine addHom_ext' fun a => AddMonoidHom.ext fun b => ?_
  simp [smul_single, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
add_sub_add_right_eq_sub,

Goal state after:
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ unsym a * unsym b * unsym a * unsym a + unsym b * unsym a * unsym a * unsym a +
        unsym a * unsym a * unsym a * unsym b -
      (unsym a * unsym b * unsym a * unsym a + unsym a * unsym a * unsym a * unsym b +
        unsym b * unsym a * unsym a * unsym a) =
    0
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
add_sub_add_right_eq_sub,

Goal state after:
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ unsym a * unsym a * unsym a * unsym b - unsym a * unsym a * unsym a * unsym b = 0
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:
← mul_def,

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
⊢ Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x = Hom.stalkMap f y ≫ X.presheaf.stalkSpecializes h

Tactic:
dsimp [stalkSpecializes, Hom.stalkMap, stalkFunctor, stalkPushforward]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
⊢ 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 =
    (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 := ⋯ } }
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
h : f.toHom = g.toHom
⊢ f = g

Tactic:
cases f; cases g; congr

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

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ (ConcreteCategory.hom e.hom.base) ((ConcreteCategory.hom e.inv.base) y) = y

Tactic:
change (e.inv.base ≫ e.hom.base) y = 𝟙 Y.toPresheafedSpace y
  simp

Goal state after:
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:
rw [Hom.appLE, f.naturality_assoc, ← Functor.map_comp]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ app (f ≫ inv f) U = X.presheaf.map (eqToHom ⋯).op

Tactic:
congr_app (IsIso.hom_inv_id f),

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ app (𝟙 X) U ≫ X.presheaf.map (eqToHom ⋯).op = X.presheaf.map (eqToHom ⋯).op
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h₂
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ ∀
    (y :
      ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).stalk
          p)),
    ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1

pp: case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ ∀ (x : ↑S), (toPushforwardStalkAlgHom R S p) x = 0 → ∃ m, m • x = 0

Tactic:
· apply isLocalizedModule_toPushforwardStalkAlgHom_aux

Goal state after:
case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ ∀ (x : ↑S), (toPushforwardStalkAlgHom R S p) x = 0 → ∃ m, m • x = 0
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsOpenImmersion g
⊢ g ''ᵁ opensRange f = opensRange g

Tactic:
opensRange_of_isIso,

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsOpenImmersion g
⊢ g ''ᵁ ⊤ = opensRange g
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑(pullback.fst g f ≫ g) = Set.range ⇑g ∩ Set.range ⇑f

Tactic:
by
  rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp, range_pullbackFst,
    Opens.map_obj, Opens.coe_mk, Set.image_preimage_eq_inter_range,
    Set.inter_comm, Opens.carrier_eq_coe, Scheme.Hom.coe_opensRange]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ IsIso f

Tactic:
isIso_iff_isOpenImmersion_and_epi_base

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ IsOpenImmersion f ∧ Epi f.base
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i : Discrete ι
this :
  colimit.ι (F ⋙ forget C) i =
    (Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (((Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫
          (preservesColimitIso (forget C) F).inv))

Tactic:
have : colimit.ι _ _ ≫ _ = _ :=
    TopCat.sigmaIsoSigma_hom_ι.{v, v} ((F ⋙ SheafedSpace.forget C).obj ∘ Discrete.mk) i.as

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i : Discrete ι
this✝ :
  colimit.ι (F ⋙ forget C) i =
    (Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
this :
  colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := i.as } ≫
      (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom =
    TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) i.as
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (((Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫
          (preservesColimitIso (forget C) F).inv))
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
H : CompactSpace ↥X
this : ∃ t, ⋃ x ∈ t, Set.range ⇑(𝒰.f (Cover.idx 𝒰 x)) = ⊤
t : Finset ↥X := this.choose
x : ↥X
h' : x ∈ ⊤
⊢ ∃ y, x ∈ Set.range ⇑(𝒰.f (Cover.idx 𝒰 ↑y))

Tactic:
← Classical.choose_spec this,

Goal state after:
X✝ Y Z : Scheme
𝒰✝ : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
X : Scheme
𝒰 : X.OpenCover
H : CompactSpace ↥X
this : ∃ t, ⋃ x ∈ t, Set.range ⇑(𝒰.f (Cover.idx 𝒰 x)) = ⊤
t : Finset ↥X := this.choose
x : ↥X
h' : x ∈ ⋃ x ∈ Classical.choose this, Set.range ⇑(𝒰.f (Cover.idx 𝒰 x))
⊢ ∃ y, x ∈ Set.range ⇑(𝒰.f (Cover.idx 𝒰 ↑y))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsLimit ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).mapCone (pullbackConeOfLeft f g))

Tactic:
apply (isLimitMapConePullbackConeEquiv _ _).symm.toFun
    exact PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit f.1 g.1

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
⊢ Opens.IsBasis X.affineOpens

Tactic:
by
  rw [Opens.isBasis_iff_nbhd]
  rintro U x (hU : x ∈ (U : Set X))
  obtain ⟨S, hS, hxS, hSU⟩ := X.affineBasisCover_is_basis.exists_subset_of_mem_open hU U.isOpen
  refine ⟨⟨S, X.affineBasisCover_is_basis.isOpen hS⟩, ?_, hxS, hSU⟩
  rcases hS with ⟨i, rfl⟩
  exact isAffineOpen_opensRange _

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s
he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ IsUnit ((algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r)

Tactic:
refine IsLocalization.map_units S (⟨r, ?_⟩ : p.asIdeal.primeCompl)

Goal state after:
X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s
he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ r ∈ p.asIdeal.primeCompl
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.appTop hU.isoSpec.inv ≫ Scheme.Hom.appTop hU.isoSpec.hom =
    (U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv) ≫ Scheme.Hom.appTop hU.isoSpec.hom

Tactic:
← Scheme.Hom.comp_appTop,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.appTop (hU.isoSpec.hom ≫ hU.isoSpec.inv) =
    (U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv) ≫ Scheme.Hom.appTop hU.isoSpec.hom
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
r : R
m : ↑((structurePresheafInModuleCat R M).stalk x)
⊢ (ConcreteCategory.hom (toStalk R x)) r • m = r • m

Tactic:
change modulePresheafStalkIso R M x (toStalk R x r • (modulePresheafStalkIso R M x).symm m) = _

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
r : R
m : ↑((structurePresheafInModuleCat R M).stalk x)
⊢ (modulePresheafStalkIso R M x) ((ConcreteCategory.hom (toStalk R x)) r • (modulePresheafStalkIso R M x).symm m) =
    r • m
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case w
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace
⊢ PrimeSpectrum.comap ((CommRingCat.Hom.hom (X.presheaf.Γgerm x)).comp (CommRingCat.Hom.hom (f.c.app (op ⊤))))
      (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)) =
    PrimeSpectrum.comap
      ((CommRingCat.Hom.hom (Hom.stalkMap f x)).comp
        (CommRingCat.Hom.hom (Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x))))
      (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))

Tactic:
← CommRingCat.hom_comp,

Goal state after:
case w
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace
⊢ PrimeSpectrum.comap (CommRingCat.Hom.hom (f.c.app (op ⊤) ≫ X.presheaf.Γgerm x))
      (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)) =
    PrimeSpectrum.comap
      ((CommRingCat.Hom.hom (Hom.stalkMap f x)).comp
        (CommRingCat.Hom.hom (Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x))))
      (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))