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

Goal state before:
pp: case inr
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑y ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
rw [h1] at hq
    rw [trinomial_def] at hp
    rw [← neg_inj, neg_add, neg_add, ← neg_mul, ← neg_mul, ← neg_mul, ← C_neg, ← C_neg, ← C_neg]
      at hp
    rw [← neg_mul_neg, ← mirror_neg] at hpq
    rcases irreducible_aux3 hkm hmn hkm' hmn' (-u) (-v) (-w) x z hp hq hpq with (rfl | rfl)
    · exact Or.inr (Or.inl rfl)
    · exact Or.inr (Or.inr (Or.inr p.mirror_neg))

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoid R
⊢ AddCommMonoid (QuadraticAlgebra R a b)

Tactic:
refine (equivProd a b).injective.addCommMonoid _ rfl ?_ ?_ <;> intros <;> rfl

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ z ^ 2 - trace z • z + (algebraMap R (QuadraticAlgebra R a b)) (norm z) = 0

Tactic:
by
  rw [Algebra.smul_def, algebraMap_trace_eq_add_star, algebraMap_norm_eq_mul_star]; ring

Goal state after:
Module: Mathlib.Algebra.Quandle

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

Tactic:
by
  rw [← left_cancel (x ◃ x)]
  rw [right_inv]
  rw [self_act_act_eq]
  rw [right_inv]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
x✝ y✝ : EnvelGroup R
x y : PreEnvelGroup R
⊢ Quotient.liftOn (⟦x⟧ * ⟦y⟧) (mapAux f) ⋯ = ⟦x⟧.liftOn (mapAux f) ⋯ * ⟦y⟧.liftOn (mapAux f) ⋯

Tactic:
by
          change Quotient.liftOn ⟦mul x y⟧ (toEnvelGroup.mapAux f) _ = _
          simp [toEnvelGroup.mapAux]

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

Goal state before:
pp: case e_toAddCommGroup
R : Type u
toAddCommGroup✝¹ : AddCommGroup R
mul✝¹ : 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
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
toAddCommGroup✝ : AddCommGroup R
mul✝ : 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
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ toAddCommGroup✝¹ = toAddCommGroup✝

Tactic:
(ext : 1; assumption)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsFormallyReal R
⊢ IsReduced R

Tactic:
rw [isReduced_iff_pow_one_lt 2 (by lia)]

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsFormallyReal R
⊢ ∀ (x : R), x ^ 2 = 0 → x = 0
Module: Mathlib.Algebra.Ring.Subring.IntPolynomial

Goal state before:
pp: K : Type u_1
inst✝ : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
n : ℕ
⊢ n ∈ P.support ↔ ⟨P.coeff n, ⋯⟩ ≠ 0

Tactic:
rw [ne_eq, ← Subring.coe_eq_zero_iff, mem_support_iff]

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 : CentroidHom α
f' : α → α
h : f' = ⇑f
a b : α
⊢ f' (a * b) = f' a * b

Tactic:
by simp_rw [h, map_mul_right]

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 α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
z : ↥(NonUnitalSubsemiring.center α)
g : CentroidHom α
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext a

Goal state after:
F : Type u_1
M : Type u_2
N : Type u_3
R✝ : Type u_4
α : Type u_5
inst✝¹⁶ : NonUnitalNonAssocSemiring α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
z : ↥(NonUnitalSubsemiring.center α)
g : CentroidHom α
a : α
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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 α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
z₁ z₂ : ↥(NonUnitalSubsemiring.center α)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext a

Goal state after:
F : Type u_1
M : Type u_2
N : Type u_3
R✝ : Type u_4
α : Type u_5
inst✝¹⁶ : NonUnitalNonAssocSemiring α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
z₁ z₂ : ↥(NonUnitalSubsemiring.center α)
a : α
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst✝² : Semiring k
inst✝¹ : AddCommMonoid A
inst✝ : Module k A
e : G ≃ H
c : k
x : SkewMonoidAlgebra A G
⊢ (mapDomain ⇑e) (c • x) = c • (mapDomain ⇑e) x

Tactic:
mapDomain_smul

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : IsRightCancelMul G
r : k
x : G
hrx : ∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0
⊢ (f * single x r).support = map (mulRightEmbedding x) f.support

Tactic:
ext a

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : IsRightCancelMul G
r : k
x : G
hrx : ∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0
a : G
⊢ a ∈ (f * single x r).support ↔ a ∈ map (mulRightEmbedding x) f.support
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mpr.mul
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ w✝ x✝ y✝ z✝ : R
a✝¹ : RingConGen.Rel r w✝ x✝
a✝ : RingConGen.Rel r y✝ z✝
a_ih✝¹ : Relation.EqvGen (Rel r) w✝ x✝
a_ih✝ : Relation.EqvGen (Rel r) y✝ z✝
⊢ Relation.EqvGen (Rel r) (w✝ * y✝) (x✝ * z✝)

Tactic:
exact (RingQuot.ringCon r).mul ‹_› ‹_›

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : IsLeftCancelMul G
r : k
x : G
hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0
⊢ (single x r * f).support = map (mulLeftEmbedding x) f.support

Tactic:
ext a

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : IsLeftCancelMul G
r : k
x : G
hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0
a : G
⊢ a ∈ (single x r * f).support ↔ a ∈ map (mulLeftEmbedding x) f.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
x : α
⊢ (f.update a b).coeff x = ((erase a) f + single a b).coeff x

Tactic:
by_cases hx : x = a <;> aesop (add norm coeff_single_apply)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : SkewPolynomial R
⊢ (p + q).support ⊆ p.support ∪ q.support

Tactic:
by
  simpa [support, ← Finset.map_union, Finset.map_subset_map] using SkewMonoidAlgebra.support_add

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: 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
f : A ≃ₐ[S] B
rel : A → A → Prop
⊢ ((liftAlgHom S) ⟨(mkAlgHom S rel).comp ↑f.symm, ⋯⟩).comp ((liftAlgHom S) ⟨(mkAlgHom S (rel on ⇑f.symm)).comp ↑f, ⋯⟩) =
    AlgHom.id S (RingQuot rel)

Tactic:
ext a

Goal state after:
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
f : A ≃ₐ[S] B
rel : A → A → Prop
a : A
⊢ ((((liftAlgHom S) ⟨(mkAlgHom S rel).comp ↑f.symm, ⋯⟩).comp
            ((liftAlgHom S) ⟨(mkAlgHom S (rel on ⇑f.symm)).comp ↑f, ⋯⟩)).comp
        (mkAlgHom S rel))
      a =
    ((AlgHom.id S (RingQuot rel)).comp (mkAlgHom S rel)) a
Module: Mathlib.Algebra.Star.CentroidHom

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

Tactic:
ext a

Goal state after:
α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
a : α
⊢ ↑(star (f * g)) a = ↑(star g * star f) a
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
⊢ star (centerToCentroidCenter z) = centerToCentroidCenter (star z)

Tactic:
ext a

Goal state after:
α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ ↑(star (centerToCentroidCenter z)) a = ↑(centerToCentroidCenter (star z)) a
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
x : TrivSqZeroExt R M
⊢ x ∈ kerIdeal R M ↔ x = inr x.snd

Tactic:
by
  obtain ⟨r, m⟩ := x
  simp only [kerIdeal, RingHom.mem_ker, fstHom_apply, fst_mk]
  exact ⟨fun hr => by rw [hr]; rfl, fun hrm => by rw [← fst_mk r m, hrm, fst_inr]⟩

Goal state after:
Module: Mathlib.Algebra.Tropical.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
this : Set.range untrop = Set.univ
hs : BddAbove (untrop '' s)
⊢ BddAbove s

Tactic:
change BddAbove (tropOrderIso.symm '' s) at hs

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
this : Set.range untrop = Set.univ
hs : BddAbove (⇑tropOrderIso.symm '' s)
⊢ BddAbove s
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
X✝ : X.Opens
⊢ CoverPreserving (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Y) (opensFunctor f)

Tactic:
exact Scheme.Hom.coverPreserving_opensFunctor f

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
this : limit.lift (cospan f.base g.base) s' ≫ limit.π (cospan f.base g.base) WalkingCospan.right = s.snd.base
⊢ ⇑(TopCat.Hom.hom (limit.lift (cospan f.base g.base) (PullbackCone.mk s.fst.base s.snd.base ⋯))) ⁻¹'
      ⇑(TopCat.Hom.hom (limit.π (cospan f.base g.base) WalkingCospan.right)) ⁻¹'
        ⇑(ConcreteCategory.hom (pullback.snd f.base g.base)) '' ↑(unop U) =
    ⇑(ConcreteCategory.hom (pullback.lift s.fst.base s.snd.base ⋯)) ⁻¹' ↑(unop U)

Tactic:
Set.preimage_image_eq _
                    (TopCat.snd_isOpenEmbedding_of_left hf.base_open g.base).injective

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
this : limit.lift (cospan f.base g.base) s' ≫ limit.π (cospan f.base g.base) WalkingCospan.right = s.snd.base
⊢ ⇑(TopCat.Hom.hom (limit.lift (cospan f.base g.base) (PullbackCone.mk s.fst.base s.snd.base ⋯))) ⁻¹' ↑(unop U) =
    ⇑(ConcreteCategory.hom (pullback.lift s.fst.base s.snd.base ⋯)) ⁻¹' ↑(unop U)
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Presieve.ofArrows P p₁ ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings Y

Tactic:
by
    rw [Precoverage.mem_comap_iff, Presieve.map_ofArrows,
      Types.ofArrows_mem_jointlySurjectivePrecoverage_iff] at hf ⊢
    intro x
    obtain ⟨i, hi⟩ := hf (F.map g x)
    have : HasPullback g (f i) := (h i).hasPullback
    use i
    have : F.map (p₁ i) = F.map ((h i).isoPullback.hom) ≫ pullbackComparison F g (f i) ≫
        pullback.fst _ _ := by simp [← Functor.map_comp]
    rwa [this, types_comp, types_comp, Function.comp_assoc, Set.range_comp,
      Function.Surjective.range_eq <| (H _ _).comp (surjective_of_epi _), Set.image_univ,
      Types.range_pullbackFst]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : MorphismProperty C
⊢ (P ⊓ Q).precoverage = P.precoverage ⊓ Q.precoverage

Tactic:
ext X R
  exact ⟨fun hS ↦ ⟨fun _ _ hf ↦ (hS hf).left, fun _ _ hf ↦ (hS hf).right⟩,
    fun h ↦ fun _ _ hf ↦ ⟨h.left hf, h.right hf⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
⊢ Scheme

Tactic:
apply LocallyRingedSpace.IsOpenImmersion.scheme (toLocallyRingedSpace _ f)
  intro x
  obtain ⟨R, i, _, h₁, h₂⟩ :=
    Scheme.exists_affine_mem_range_and_range_subset (U := ⟨_, H.base_open.isOpen_range⟩) ⟨x, rfl⟩
  refine ⟨R, LocallyRingedSpace.IsOpenImmersion.lift (toLocallyRingedSpaceHom _ f) _ h₂, ?_, ?_⟩
  · rw [LocallyRingedSpace.IsOpenImmersion.lift_range]; exact h₁
  · delta LocallyRingedSpace.IsOpenImmersion.lift; infer_instance

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

Goal state before:
pp: K : Precoverage Scheme
inst✝ : JointlySurjective K
X : Scheme
𝒰 : Cover K X
⊢ ⋃ i, Set.range ⇑(𝒰.f i) = Set.univ

Tactic:
by
  rw [Set.eq_univ_iff_forall]
  intro x
  rw [Set.mem_iUnion]
  exact 𝒰.exists_eq x

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: U V X Y : Scheme
g : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
f : X ⟶ Y
inst✝¹ : IsOpenImmersion iU
inst✝ : IsOpenImmersion iV
H : iU ≫ f = g ≫ iV
H' : f ⁻¹ᵁ Scheme.Hom.opensRange iV = Scheme.Hom.opensRange iU
⊢ Set.range ⇑(pullback.snd iV f) = Set.range ⇑iU

Tactic:
simpa [range_pullbackSnd] using congr(($H').1)

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
this :
  Function.Bijective
    ⇑((algebraMap ((structureSheafInType R R).obj.obj (op (basicOpen f)))
          (Module.End ((structureSheafInType R R).obj.obj (op (basicOpen f)))
            ((structureSheafInType R M).obj.obj (op (basicOpen f)))))
        ((algebraMap R ((structureSheafInType R R).obj.obj (op (basicOpen f)))) f))
⊢ ⇑((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))) f) =
    ⇑((algebraMap ((structureSheafInType R R).obj.obj (op (basicOpen f)))
          (Module.End ((structureSheafInType R R).obj.obj (op (basicOpen f)))
            ((structureSheafInType R M).obj.obj (op (basicOpen f)))))
        ((algebraMap R ((structureSheafInType R R).obj.obj (op (basicOpen f)))) f))

Tactic:
ext a

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
this :
  Function.Bijective
    ⇑((algebraMap ((structureSheafInType R R).obj.obj (op (basicOpen f)))
          (Module.End ((structureSheafInType R R).obj.obj (op (basicOpen f)))
            ((structureSheafInType R M).obj.obj (op (basicOpen f)))))
        ((algebraMap R ((structureSheafInType R R).obj.obj (op (basicOpen f)))) f))
a : (structureSheafInType R M).obj.obj (op (basicOpen f))
⊢ ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))) f) a =
    ((algebraMap ((structureSheafInType R R).obj.obj (op (basicOpen f)))
          (Module.End ((structureSheafInType R R).obj.obj (op (basicOpen f)))
            ((structureSheafInType R M).obj.obj (op (basicOpen f)))))
        ((algebraMap R ((structureSheafInType R R).obj.obj (op (basicOpen f)))) f))
      a
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
⊢ (X.homOfLE e).base = (Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e)

Tactic:
ext a

Goal state after:
X : Scheme
U V : X.Opens
e : U ≤ V
a : ↥↑U
⊢ (X.homOfLE e) a = (ConcreteCategory.hom ((Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e))) a
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Tactic:
by
  have e₁ := Scheme.Hom.congr_app (X.homOfLE_ι e) (V.ι ''ᵁ W)
  have : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W := W.map_functor_eq (U := V)
  have e₂ := (X.homOfLE e).naturality (eqToIso this).hom.op
  have e₃ := e₂.symm.trans e₁
  dsimp at e₃ ⊢
  rw [← IsIso.eq_comp_inv, ← Functor.map_inv, ← Functor.map_comp] at e₃
  rw [e₃, ← Functor.map_comp]
  congr 1

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
W' : (↑U).Opens
e' : W' ≤ X.homOfLE e ⁻¹ᵁ W
⊢ Hom.appLE (X.homOfLE e) W W' e' = X.presheaf.map (homOfLE ⋯).op

Tactic:
by
  simp [Scheme.Hom.appLE, Scheme.homOfLE_app, ← Functor.map_comp, ← op_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
X : Scheme
U V : X.Opens
e : U = V
⊢ Set.range ⇑U.ι = Set.range ⇑V.ι

Tactic:
rw [e]

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:
by
  simp only [RingedSpace.zeroLocus]
  have (i : LocallyRingedSpace.Γ.obj (op X)) (_ : i ∈ s) :
      (SetLike.coe (X.toRingedSpace.basicOpen i))ᶜ =
        X.toΓSpec.base ⁻¹' ((PrimeSpectrum.basicOpen i).carrier)ᶜ := by
    symm
    rw [Set.preimage_compl, Opens.carrier_eq_coe]
    erw [X.toΓSpec_preimage_basicOpen_eq i]
  erw [Set.iInter₂_congr this]
  simp_rw [← Set.preimage_iInter₂, Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl,
    compl_compl]
  rw [← PrimeSpectrum.zeroLocus_iUnion₂]
  simp

Goal state after:
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)
f : R
hf : x ∈ basicOpen f
this :
  Function.Bijective
    ⇑((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
          (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
        ((ConcreteCategory.hom (toStalk R x)) f))
⊢ ⇑((algebraMap R (Module.End R ↑((structurePresheafInModuleCat R M).stalk x))) f) =
    ⇑((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
          (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
        ((ConcreteCategory.hom (toStalk R x)) f))

Tactic:
ext a

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
this :
  Function.Bijective
    ⇑((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
          (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
        ((ConcreteCategory.hom (toStalk R x)) f))
a : ↑((structurePresheafInModuleCat R M).stalk x)
⊢ ((algebraMap R (Module.End R ↑((structurePresheafInModuleCat R M).stalk x))) f) a =
    ((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
          (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
        ((ConcreteCategory.hom (toStalk R x)) f))
      a
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.app hU.fromSpec U = (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op

Tactic:
← hU.ΓSpecIso_hom_fromSpec_app,

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥V
m : Localizations R (PrimeSpectrum.comap f ↑p)
⊢ (Localizations.comapFun f.toSemilinearMap ↑p) m =
    (Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯) m

Tactic:
induction m using LocalizedModule.induction_on with

Goal state after: