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

Goal state before:
pp: case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
⊢ map (algebraMap R A) p = (X - C r) ^ (q - 1) * p' →
    (aeval r) (sumIDeriv p) = (q - 1)! • eval r p' + q ! • (aeval r) (∑ x ∈ Ico q (p.natDegree + 1), c x)

Tactic:
hp

Goal state after:
case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
⊢ (aeval r) (sumIDeriv p) = (q - 1)! • eval r p' + q ! • (aeval r) (∑ x ∈ Ico q (p.natDegree + 1), c x)
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
⊢ (aeval r) (sumIDeriv p) = (q - 1)! • eval r p' + q ! • (aeval r) (∑ x ∈ Ico q (p.natDegree + 1), c x)

Tactic:
have : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1) := by
    rw [range_eq_Ico, range_eq_Ico, Ico_union_Ico_eq_Ico hq.le]
    rw [← tsub_le_iff_right]
    calc
      q - 1 ≤ q - 1 + p'.natDegree := le_self_add
      _ = (p.map <| algebraMap R A).natDegree := by
        rw [hp, natDegree_mul, natDegree_pow, natDegree_X_sub_C, mul_one,
          ← Nat.sub_add_comm (Nat.one_le_of_lt hq)]
        · exact pow_ne_zero _ (X_sub_C_ne_zero r)
        · rintro rfl
          rw [mul_zero, Polynomial.map_eq_zero_iff inj_amap] at hp
          exact p0 hp
      _ ≤ p.natDegree := natDegree_map_le

Goal state after:
case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
⊢ (aeval r) (sumIDeriv p) = (q - 1)! • eval r p' + q ! • (aeval r) (∑ x ∈ Ico q (p.natDegree + 1), c x)
Module: Mathlib.Algebra.Regular.Pi

Goal state before:
pp: ι : Type u_1
R : ι → Type u_3
inst✝ : (i : ι) → Mul (R i)
a : (i : ι) → R i
⊢ IsRegular a ↔ ∀ (i : ι), IsRegular (a i)

Tactic:
by
  simp [_root_.isRegular_iff, forall_and]

Goal state after:
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
⊢ ((Basis.self R).compHom F).liftHom = F

Tactic:
ext
    dsimp [Basis.lift]
    rw [← F.commutes]
    simp only [← map_smul, ← map_add, mk_add_mk, smul_mk, smul_zero, algebraMap_eq]
    congr <;> simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x : R
hx : x ∈ sumNonzeroSq R
⊢ x ∈ closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x}

Tactic:
induction hx with
  | sq ha => aesop
  | sq_add ha hs ih =>
    -- `aesop` times out
    apply add_mem
    · apply AddSubsemigroup.mem_closure_of_mem
      aesop
    aesop

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case rel.trans
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
a b x✝¹ y✝¹ : R
hab : Rel r x✝¹ y✝¹
c d x✝ y✝ z✝ : R
a✝¹ : Relation.EqvGen (Rel r) x✝ y✝
a✝ : Relation.EqvGen (Rel r) y✝ z✝
h : Relation.EqvGen (Rel r) (y✝¹ * x✝) (y✝¹ * y✝)
h' : Relation.EqvGen (Rel r) (y✝¹ * y✝) (y✝¹ * z✝)
⊢ Relation.EqvGen (Rel r) (y✝¹ * x✝) (y✝¹ * z✝)

Tactic:
| trans _ _ _ _ _ h h' =>

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refl.trans
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
a b x✝¹ c d x✝ y✝ z✝ : R
a✝¹ : Relation.EqvGen (Rel r) x✝ y✝
a✝ : Relation.EqvGen (Rel r) y✝ z✝
h : Relation.EqvGen (Rel r) (x✝¹ * x✝) (x✝¹ * y✝)
h' : Relation.EqvGen (Rel r) (x✝¹ * y✝) (x✝¹ * z✝)
⊢ Relation.EqvGen (Rel r) (x✝¹ * x✝) (x✝¹ * z✝)

Tactic:
| trans _ _ _ _ _ h h' =>

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case rel.trans
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
a b x✝¹ y✝¹ : R
hab : Rel r x✝¹ y✝¹
c d x✝ y✝ z✝ : R
a✝¹ : Relation.EqvGen (Rel r) x✝ y✝
a✝ : Relation.EqvGen (Rel r) y✝ z✝
h : Relation.EqvGen (Rel r) (y✝¹ + x✝) (y✝¹ + y✝)
h' : Relation.EqvGen (Rel r) (y✝¹ + y✝) (y✝¹ + z✝)
⊢ Relation.EqvGen (Rel r) (y✝¹ + x✝) (y✝¹ + z✝)

Tactic:
| trans _ _ _ _ _ h h' =>

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refl.trans
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
a b x✝¹ c d x✝ y✝ z✝ : R
a✝¹ : Relation.EqvGen (Rel r) x✝ y✝
a✝ : Relation.EqvGen (Rel r) y✝ z✝
h : Relation.EqvGen (Rel r) (x✝¹ + x✝) (x✝¹ + y✝)
h' : Relation.EqvGen (Rel r) (x✝¹ + y✝) (x✝¹ + z✝)
⊢ Relation.EqvGen (Rel r) (x✝¹ + x✝) (x✝¹ + z✝)

Tactic:
| trans _ _ _ _ _ h h' =>

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

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

Tactic:
by
  induction n with
  | zero      => simp only [pow_zero, monomial_zero_left, ← CRingHom_eq_C, map_one]
  | succ n hn =>
    rw [pow_succ', hn, X, monomial_mul_monomial]
    simp [add_comm]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
S : Type u_3
inst✝¹ : DecidableEq G
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f + g).sum h = f.sum h + g.sum h

Tactic:
rw [show f + g = ⟨f.coeff + g.coeff⟩ by rw [ofCoeff_add, eta]]
  exact Finsupp.sum_add_index h_zero h_add

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

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

Tactic:
simp_rw [mul_def, map_sum, liftNC_single, sum_mul, mul_sum]

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
⊢ (a.sum fun a b_1 ↦ b.sum fun a_1 b ↦ ↑f (b_1 * a • b) * g (a * a_1)) =
    a.sum fun a c ↦ b.sum fun a_1 c_1 ↦ ↑f c * g a * (↑f c_1 * g a_1)
Module: Mathlib.Topology.Sheaves.Functors

Goal state before:
pp: case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
X✝ Y✝ : TopCat.Sheaf A Y
u : X✝ ⟶ Y✝
⊢ (presheafToSheaf (Opens.grothendieckTopology ↑X) A).map
        ((Presheaf.pullback A f).map ((Sheaf.forget A Y).map u) ≫ ⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj Y✝)) ≫
      ObjectProperty.homMk (isoSheafify (Opens.grothendieckTopology ↑X) ⋯).inv =
    ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj X✝)) ≫
        ObjectProperty.homMk (isoSheafify (Opens.grothendieckTopology ↑X) ⋯).inv) ≫
      (sheafPullback A hf).map u

Tactic:
hf.isOpenMap.pullbackIso.hom.naturality,

Goal state after:
case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
X✝ Y✝ : TopCat.Sheaf A Y
u : X✝ ⟶ Y✝
⊢ (presheafToSheaf (Opens.grothendieckTopology ↑X) A).map
        (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj X✝) ≫
          ((Functor.whiskeringLeft (Opens ↑X)ᵒᵖ (Opens ↑Y)ᵒᵖ A).obj ⋯.functor.op).map ((Sheaf.forget A Y).map u)) ≫
      ObjectProperty.homMk (isoSheafify (Opens.grothendieckTopology ↑X) ⋯).inv =
    ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj X✝)) ≫
        ObjectProperty.homMk (isoSheafify (Opens.grothendieckTopology ↑X) ⋯).inv) ≫
      (sheafPullback A hf).map u
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
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
⊢ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } ≫ { base := H.hom, c := α.inv } = 𝟙 Y

Tactic:
ext
    · dsimp
      exact H.inv_hom_id_apply _
    dsimp
    simp only [Presheaf.toPushforwardOfIso_app, assoc, ← α.hom.naturality]
    simp only [eqToHom_map, eqToHom_app, eqToHom_trans_assoc, eqToHom_refl, id_comp]
    apply Iso.inv_hom_id_app

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

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑(X.restrict ⋯)
⊢ ((X.ofRestrict ⋯ ≫ X.toRestrictTop).c ≫ whiskerRight (eqToHom ⋯) (X.restrict ⋯).presheaf).app (op U✝) =
    (𝟙 (X.restrict ⋯)).c.app (op U✝)

Tactic:
comp_c,

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑(X.restrict ⋯)
⊢ ((X.toRestrictTop.c ≫ (Presheaf.pushforward C X.toRestrictTop.base).map (X.ofRestrict ⋯).c) ≫
          whiskerRight (eqToHom ⋯) (X.restrict ⋯).presheaf).app
      (op U✝) =
    (𝟙 (X.restrict ⋯)).c.app (op U✝)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ ((X.toRestrictTop ≫ X.ofRestrict ⋯).c ≫ whiskerRight (eqToHom ⋯) X.presheaf).app (op U✝) = (𝟙 X).c.app (op U✝)

Tactic:
comp_c,

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ (((X.ofRestrict ⋯).c ≫ (Presheaf.pushforward C (X.ofRestrict ⋯).base).map X.toRestrictTop.c) ≫
          whiskerRight (eqToHom ⋯) X.presheaf).app
      (op U✝) =
    (𝟙 X).c.app (op U✝)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ ((X.toRestrictTop ≫ X.ofRestrict ⋯).c ≫ whiskerRight (eqToHom ⋯) X.presheaf).app (op U✝) = (𝟙 X).c.app (op U✝)

Tactic:
· erw [comp_c, ofRestrict_top_c, toRestrictTop_c, eqToHom_map, whiskerRight_id', comp_id,
        eqToHom_trans, eqToHom_refl]
      rfl

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

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
⊢ ∃! s, (subpresheafToTypes P.toPrelocalPredicate).IsGluing U sf s

Tactic:
let sf' (i : ι) : (presheafToTypes X T).obj (op (U i)) := (sf i).val

Goal state after:
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i ↦ ↑(sf i)
⊢ ∃! s, (subpresheafToTypes P.toPrelocalPredicate).IsGluing U sf s
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: case h
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 : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
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)
x : F.obj Y
i : ι
hi : (ConcreteCategory.hom (F.map g)) x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
this✝ : HasPullback g (f i)
this : F.map (p₁ i) = F.map ⋯.isoPullback.hom ≫ pullbackComparison F g (f i) ≫ pullback.fst (F.map g) (F.map (f i))
⊢ x ∈
    Set.range
      (⇑(ConcreteCategory.hom (pullback.fst (F.map g) (F.map (f i)))) ∘
        ⇑(ConcreteCategory.hom (pullbackComparison F g (f i))) ∘ ⇑(ConcreteCategory.hom (F.map ⋯.isoPullback.hom)))

Tactic:
Set.range_comp,

Goal state after:
case h
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 : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
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)
x : F.obj Y
i : ι
hi : (ConcreteCategory.hom (F.map g)) x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
this✝ : HasPullback g (f i)
this : F.map (p₁ i) = F.map ⋯.isoPullback.hom ≫ pullbackComparison F g (f i) ≫ pullback.fst (F.map g) (F.map (f i))
⊢ x ∈
    ⇑(ConcreteCategory.hom (pullback.fst (F.map g) (F.map (f i)))) ''
      Set.range
        (⇑(ConcreteCategory.hom (pullbackComparison F g (f i))) ∘ ⇑(ConcreteCategory.hom (F.map ⋯.isoPullback.hom)))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

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

Tactic:
Set.range_comp,

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))) ''
      Set.range ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop f g).hom) =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

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

Tactic:
Set.range_comp,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (pullback.fst (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))) ''
      Set.range ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop g f).hom) =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

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

Tactic:
Set.range_comp,

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

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

Tactic:
Set.range_comp,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑g '' Set.range ⇑(pullback.fst g f) = Set.range ⇑g ∩ Set.range ⇑f
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 ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)
⊢ f ''ᵁ X.basicOpen r = Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)

Tactic:
Scheme.basicOpen_res,

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) = f ⁻¹ᵁ f ''ᵁ U ⊓ X.basicOpen r
⊢ f ''ᵁ X.basicOpen r = Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)
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
U : (x : ↑X.toTopCat) → OpenNhds x
R : ↑X.toTopCat → CommRingCat
h : ∀ (x : ↑X.toTopCat), Nonempty (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)))
e : (x : ↑X.toTopCat) → X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)) := fun x ↦ ⋯.some
x : ↥X
⊢ ({ I₀ := ↥X, X := fun x ↦ Spec (R x), f := fun x ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }.f x)
      ((ConcreteCategory.hom (e x).hom.base) ⟨x, ⋯⟩) =
    x

Tactic:
change ((((e x).hom ≫ (e x).inv).base ≫ (X.ofRestrict _).base)) ⟨x, _⟩ = x

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
U : (x : ↑X.toTopCat) → OpenNhds x
R : ↑X.toTopCat → CommRingCat
h : ∀ (x : ↑X.toTopCat), Nonempty (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)))
e : (x : ↑X.toTopCat) → X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)) := fun x ↦ ⋯.some
x : ↥X
⊢ (ConcreteCategory.hom (((e x).hom ≫ (e x).inv).base ≫ (X.ofRestrict ⋯).base)) ⟨x, ⋯⟩ = x
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
⊢ ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
    m ≫ (pullbackConeOfLeft f g).fst = s.fst →
      m ≫ (pullbackConeOfLeft f g).snd = s.snd →
        m =
          {
            toHom :=
              PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯),
            prop := ⋯ }

Tactic:
· intro m _ h₂
      rw [← cancel_mono (pullbackConeOfLeft f g).snd]
      exact h₂.trans <| LocallyRingedSpace.Hom.ext'
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd f.1 g.1 <|
          PullbackCone.mk s.fst.1 s.snd.1 <| congr_arg
            LocallyRingedSpace.Hom.toHom s.condition).symm

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

Goal state before:
pp: X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
⊢ Set.range
      (⇑(ConcreteCategory.hom
            (pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
              ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g))) ∘
        ⇑(ConcreteCategory.hom
            ((inv (pullback.snd f g)).base ≫
              (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom))) =
    ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
Set.range_comp,

Goal state after:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
⊢ ⇑(ConcreteCategory.hom
          (pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
            ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g))) ''
      Set.range
        ⇑(ConcreteCategory.hom
            ((inv (pullback.snd f g)).base ≫
              (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom)) =
    ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)
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 :
  IsUnit
    ((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))
⊢ IsUnit ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))) f)

Tactic:
rw [Module.End.isUnit_iff] at this ⊢

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))
⊢ Function.Bijective ⇑((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))) f)