mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteResidueField K
h : x ≤ y
z : FiniteResidueField K
⊢ x + z ≤ y + z

Tactic:
induction x with | mk x

Goal state after:
case mk
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
y z : FiniteResidueField K
x : FiniteElement K
h : mk x ≤ y
⊢ mk x + z ≤ y + z
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
⊢ ⋃ a ∈ s, a • ↑(lowerClosure t) = ↑(lowerClosure (⋃ a ∈ s, a • t))

Tactic:
lowerClosure_iUnion,

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
⊢ ⋃ a ∈ s, a • ↑(lowerClosure t) = ↑(⨆ i ∈ s, lowerClosure (i • t))
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteResidueField K
hy : 0 < y
⊢ ∃ n, x ≤ n • y

Tactic:
induction x with | mk x

Goal state after:
case mk
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
y : FiniteResidueField K
hy : 0 < y
x : FiniteElement K
⊢ ∃ n, mk x ≤ n • y
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 < mk x
hy : mk y < 0
⊢ mk y ≠ 0

Tactic:
exact hy.ne

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬(monomial n) x = 0
h₁✝ : 0 < ((monomial n) x).coeffList.length
h₁ : 0 < (x :: List.replicate n 0).length
⊢ ((monomial n) x).coeffList.get ⟨0, h₁✝⟩ = (x :: List.replicate n 0).get ⟨0, h₁⟩

Tactic:
exact (coeffList_eq_cons_leadingCoeff h).rec (by simp_all)

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

Goal state before:
pp: case ha
A : Type u_1
inst✝¹¹ : CommRing A
inst✝¹⁰ : Differential A
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Differential R
inst✝⁷ : Algebra A R
inst✝⁶ : DifferentialAlgebra A R
R' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : Differential R'
inst✝³ : Algebra A R'
inst✝² : DifferentialAlgebra A R'
inst✝¹ : IsDomain R'
inst✝ : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective ⇑f
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
⊢ (f.comp (aeval x)) (derivative p) ≠ 0

Tactic:
simp only [AlgHom.coe_comp, Function.comp_apply, ne_eq, map_eq_zero_iff f hf]

Goal state after:
case ha
A : Type u_1
inst✝¹¹ : CommRing A
inst✝¹⁰ : Differential A
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Differential R
inst✝⁷ : Algebra A R
inst✝⁶ : DifferentialAlgebra A R
R' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : Differential R'
inst✝³ : Algebra A R'
inst✝² : DifferentialAlgebra A R'
inst✝¹ : IsDomain R'
inst✝ : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective ⇑f
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
⊢ ¬(aeval x) (derivative p) = 0
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ (equivMvPolynomial R) (C (C a)) = MvPolynomial.C a

Tactic:
by
  simp [equivMvPolynomial]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ (equivMvPolynomial R) (C X) = MvPolynomial.X 0

Tactic:
by
  simp [equivMvPolynomial]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ (equivMvPolynomial R) Y = MvPolynomial.X 1

Tactic:
by
  simp [equivMvPolynomial]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ (equivMvPolynomial R).symm (MvPolynomial.X 0) = C X

Tactic:
by
  simp [equivMvPolynomial]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ (equivMvPolynomial R).symm (MvPolynomial.X 1) = Y

Tactic:
by
  simp [equivMvPolynomial]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ (equivMvPolynomial R).symm (MvPolynomial.C a) = C (C a)

Tactic:
by
  simp [equivMvPolynomial]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n ∧ p.coeff n = 1
hq : q.natDegree ≤ n ∧ q.coeff n = 1
m : ℕ
hm : n ≤ m
a✝ : Nontrivial R
⊢ p.coeff m = q.coeff m

Tactic:
rcases eq_or_lt_of_le hm with rfl | hm

Goal state after:
case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n ∧ p.coeff n = 1
hq : q.natDegree ≤ n ∧ q.coeff n = 1
a✝ : Nontrivial R
hm : n ≤ n
⊢ p.coeff n = q.coeff n

case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n ∧ p.coeff n = 1
hq : q.natDegree ≤ n ∧ q.coeff n = 1
m : ℕ
hm✝ : n ≤ m
a✝ : Nontrivial R
hm : n < m
⊢ p.coeff m = q.coeff m
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a + r
⊢ ∃ q, q.IsMonicOfDegree (m - n) ∧ a = q * b - r

Tactic:
obtain ⟨q, hq⟩ := exists_eq_mul_left_of_dvd h
  refine ⟨q, hb.of_mul_right ?_, eq_sub_iff_add_eq.mpr hq⟩
  rw [← hq, show m - n + n = m by lia]
  exact ha.add_right hr

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

Goal state before:
pp: case monomial.inl
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ MvPolynomial.coeff m (((monomial k) c).homogenize n) = if m 0 + m 1 = n then ((monomial k) c).coeff (m 0) else 0

Tactic:
rw [homogenize_monomial hkn, coeff_monomial, MvPolynomial.coeff_monomial]

Goal state after:
case monomial.inl
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ (if (fun₀ | 0 => k | 1 => n - k) = m then c else 0) = if m 0 + m 1 = n then if k = m 0 then c else 0 else 0
Module: Mathlib.Data.List.Destutter

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

Tactic:
simp only [if_pos hac, length_cons]
        exact Nat.le_succ_of_le (length_destutter'_cotrans_ge hbc)

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ s 0 ∈ p.support

Tactic:
simpa [coeff_homogenize, sum_eq_natDegree_of_mem_support_homogenize p hs] using hs

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

Goal state before:
pp: k✝ k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k✝ ∈ (trinomial k m n ↑u ↑v ↑w).support
this : k✝ = k ∨ k✝ = m ∨ k✝ = n
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k✝)

Tactic:
rcases this with (rfl | rfl | rfl)

Goal state after:
case inl
k m n : ℕ
hmn : m < n
u v w : ℤˣ
hkm : k < m
hk : k ∈ (trinomial k m n ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k)

case inr.inl
k✝ k n : ℕ
u v w : ℤˣ
hkm : k < k✝
hmn : k✝ < n
hk : k✝ ∈ (trinomial k k✝ n ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k k✝ n ↑u ↑v ↑w).coeff k✝)

case inr.inr
k✝ k m : ℕ
hkm : k < m
u v w : ℤˣ
hmn : m < k✝
hk : k✝ ∈ (trinomial k m k✝ ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k m k✝ ↑u ↑v ↑w).coeff k✝)
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✝² : SMul S R
inst✝¹ : SMul T R
s✝ : S
inst✝ : SMulCommClass S T R
s : S
t : T
z : QuadraticAlgebra R a b
⊢ s • t • z = t • s • z

Tactic:
ext <;> exact smul_comm _ _ _

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
⊢ (algebraMap R[X] K) (∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k) * ∏ i ∈ s, gi i ^ n i =
    ∑ j, (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)

Tactic:
rw [map_sum, Finset.sum_mul, ← Equiv.sum_comp Fin.revPerm]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
⊢ ∑ i_1,
      (algebraMap R[X] K) (r i (Fin.revPerm i_1) * g i ^ ↑(Fin.revPerm i_1) * ∏ k ∈ s.erase i, g k ^ n k) *
        ∏ i ∈ s, gi i ^ n i =
    ∑ j, (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)
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
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F q.j * F q.j = c₃ • 1

Tactic:
rw [← map_mul, q.j_mul_j, map_smul, map_one]

Goal state after:
Module: Mathlib.Algebra.Ring.Pointwise.Set

Goal state before:
pp: α : Type u_1
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
x✝¹ x✝ : Set α
⊢ (fun x ↦ -x) '' x✝¹ * x✝ = (fun x ↦ -x) '' (x✝¹ * x✝)

Tactic:
exact image2_image_left_comm neg_mul

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✝ : NonAssocSemiring α
T : CentroidHom α
x✝ : α
⊢ (centerToCentroid.toMulHom ((fun T ↦ ⟨T 1, ⋯⟩) T)) x✝ = T x✝

Tactic:
NonUnitalRingHom.coe_toMulHom,

Goal state after:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
x✝ : α
⊢ (centerToCentroid ((fun T ↦ ⟨T 1, ⋯⟩) T)) x✝ = T x✝
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ a ∉ ((erase a) f).support

Tactic:
rw [support_erase, Finset.mem_erase]

Goal state after:
case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ ¬(a ≠ a ∧ a ∈ f.support)
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
s : Finset ℕ
hs : p.support ⊆ s
⊢ p.sum f = ∑ n ∈ s, f n (p.coeff n)

Tactic:
sum_def ,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
s : Finset ℕ
hs : p.support ⊆ s
⊢ ∑ n ∈ p.support, f n (p.coeff n) = ∑ n ∈ s, f n (p.coeff n)
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroup R
x✝¹ x✝ : Tropical R
⊢ untrop (x✝¹ / x✝) = untrop (x✝¹ * x✝⁻¹)

Tactic:
by simp [sub_eq_add_neg]

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

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
a₁✝ a₂✝ : HVertexOperator Γ R V W
h : coeff a₁✝ = coeff a₂✝
v : V
n : Γ
⊢ ((of R).symm (a₁✝ v)).coeff n = ((of R).symm (a₂✝ v)).coeff n

Tactic:
exact congrFun (congrArg DFunLike.coe (congrFun h n)) v

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
α β : X.Hom Y
w : α.base = β.base
h : α.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = β.c
⊢ α = β

Tactic:
by
  rcases α with ⟨base, c⟩
  rcases β with ⟨base', c'⟩
  dsimp at w
  subst w
  dsimp at h
  erw [whiskerRight_id', comp_id] at h
  subst h
  rfl

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

Goal state before:
pp: case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
⊢ g₁.base = g₂.base

Tactic:
have := congr_arg PresheafedSpace.Hom.base eq
    simp only [PresheafedSpace.comp_base, PresheafedSpace.ofRestrict_base] at this
    rw [cancel_mono] at this
    exact this

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : ↑↑(locallyRingedSpaceObj S).toPresheafedSpace
a : ↑((locallyRingedSpaceObj R).presheaf.stalk ((ConcreteCategory.hom (sheafedSpaceMap f).hom.base) p))
ha : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (sheafedSpaceMap f).hom p)) a)
⊢ IsUnit a

Tactic:
rw [← localRingHom_comp_stalkIso] at ha

Goal state after:
R S : CommRingCat
f : R ⟶ S
p : ↑↑(locallyRingedSpaceObj S).toPresheafedSpace
a : ↑((locallyRingedSpaceObj R).presheaf.stalk ((ConcreteCategory.hom (sheafedSpaceMap f).hom.base) p))
ha :
  IsUnit
    ((CommRingCat.Hom.hom
        (CommRingCat.ofHom (stalkIso (↑R) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).symm.toRingEquiv.toRingHom ≫
          CommRingCat.ofHom
              (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
                (CommRingCat.Hom.hom f) ⋯) ≫
            CommRingCat.ofHom (stalkIso (↑S) p).toRingEquiv.toRingHom))
      a)
⊢ IsUnit a
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:
by
  rw [Hom.appLE, Category.assoc, ← Functor.map_comp]
  rfl

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
Y : TopCat
f : Y ⟶ TopCat.of ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(X.restrict h)
⊢ invApp (X.ofRestrict h) U = 𝟙 ((X.restrict h).presheaf.obj (op U))

Tactic:
by
  delta invApp
  rw [IsIso.comp_inv_eq, Category.id_comp]
  change X.presheaf.map _ = X.presheaf.map _
  congr 1

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

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

Tactic:
ext X Y f

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ P.precoverage.morphismProperty f ↔ P f
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: case h
P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : f x = g y
iso : pullback f g ≅ pullback g f := ⋯
this : HasPullback g f
a : ↥(pullback g f)
ha : (pullback.fst g f) a = y
⊢ (pullback.snd f g) ((pullbackSymmetry f g).inv a) = y

Tactic:
← Scheme.Hom.comp_apply,

Goal state after:
case h
P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : f x = g y
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
this : HasPullback g f
a : ↥(pullback g f)
ha : (pullback.fst g f) a = y
⊢ ((pullbackSymmetry f g).inv ≫ pullback.snd f g) a = y
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 : IsOpenImmersion f
g : Y ⟶ Z
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f.base g.base)
this : IsIso (pullback.snd f g).base
⊢ IsIso (pullback.snd f g)

Tactic:
apply to_iso

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑g '' ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier = Set.range ⇑f ∩ Set.range ⇑g

Tactic:
Set.image_preimage_eq_inter_range,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ (Scheme.Hom.opensRange f).carrier ∩ Set.range ⇑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
⊢ ⇑g '' ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier = Set.range ⇑g ∩ Set.range ⇑f

Tactic:
Set.image_preimage_eq_inter_range,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ (Scheme.Hom.opensRange f).carrier ∩ Set.range ⇑g = Set.range ⇑g ∩ Set.range ⇑f
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : P.RespectsIso
X : Scheme
𝒰 : Cover (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : J ≃ 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f (e₁ i)
⊢ { I₀ := J, X := obj, f := map }.presieve₀ ∈ (precoverage P).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, ?_⟩
    · obtain ⟨i, y, rfl⟩ := 𝒰.exists_eq x
      obtain ⟨i, rfl⟩ := e₁.surjective i
      use i, (e₂ i).inv y
      simp [h]
    · simp_rw [h, MorphismProperty.cancel_left_of_respectsIso]
      intro i
      exact 𝒰.map_prop _

Goal state after:
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✝
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsOpenImmersion g
p : ↥P
x : ↥X
hx : fst p = x
this : IsOpenImmersion fst
⊢ f (fst p) = g (snd p)

Tactic:
← Scheme.Hom.comp_apply,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsOpenImmersion g
p : ↥P
x : ↥X
hx : fst p = x
this : IsOpenImmersion fst
⊢ (fst ≫ f) p = g (snd p)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (isoRestrict f).hom ≫ Y.ofRestrict ⋯ = f

Tactic:
apply LocallyRingedSpace.forgetToSheafedSpace.map_injective

Goal state after:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ forgetToSheafedSpace.map ((isoRestrict f).hom ≫ Y.ofRestrict ⋯) = forgetToSheafedSpace.map f
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h_nhds.refine_2
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ ⇑(X.affineCover.f (Cover.idx X.affineCover a)) '' (PrimeSpectrum.basicOpen s).carrier ⊆ U

Tactic:
rw [Set.image_subset_iff]; exact hVU

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (TopCat.Hom.hom (Spec.map (X.presheaf.map (eqToHom ⋯).op)).base)
      ((Spec.map ((↑U).presheaf.germ ⊤ x True.intro)) (closedPoint ↑((↑U).presheaf.stalk x))) =
    (Spec.map (X.presheaf.germ U ↑x ⋯)) (closedPoint ↑(X.presheaf.stalk ↑x))

Tactic:
← Scheme.Hom.comp_apply,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (Spec.map ((↑U).presheaf.germ ⊤ x True.intro) ≫ Spec.map (X.presheaf.map (eqToHom ⋯).op))
      (closedPoint ↑((↑U).presheaf.stalk x)) =
    (Spec.map (X.presheaf.germ U ↑x ⋯)) (closedPoint ↑(X.presheaf.stalk ↑x))
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
x : ↑X.toTopCat
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x))

Tactic:
let p : PrimeSpectrum (Γ.obj (op X)) := X.toΓSpecFun x
    constructor
    -- show stalk map is local hom ↓
    let S := (structureSheaf _).presheaf.stalk p
    rintro (t : S) ht
    obtain ⟨⟨r, s⟩, he⟩ := IsLocalization.surj p.asIdeal.primeCompl t
    dsimp at he
    set t' := _
    change t * t' = _ at he
    apply isUnit_of_mul_isUnit_left (y := t')
    rw [he]
    refine IsLocalization.map_units S (⟨r, ?_⟩ : p.asIdeal.primeCompl)
    apply (notMem_prime_iff_unit_in_stalk _ _ _).mpr
    rw [← toStalk_stalkMap_toΓSpec, CommRingCat.comp_apply]
    erw [← he]
    rw [map_mul]
    exact ht.mul <| (IsLocalization.map_units (R := Γ.obj (op X)) S s).map _

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
⊢ CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).obj.obj (op U))) ≫
      (structurePresheafInCommRingCat R).germ U x hxU =
    CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).obj.obj (op ⊤))) ≫
      (structurePresheafInCommRingCat R).germ ⊤ x _root_.trivial

Tactic:
rw [← (structurePresheafInCommRingCat R).germ_res (homOfLE (le_top : U ≤ ⊤)) _ hxU]

Goal state after:
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
⊢ CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).obj.obj (op U))) ≫
      (structurePresheafInCommRingCat R).germ U x hxU =
    CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).obj.obj (op ⊤))) ≫
      (structurePresheafInCommRingCat R).map (homOfLE ⋯).op ≫ (structurePresheafInCommRingCat R).germ U x hxU
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ ⇑hU.fromSpec '' ⇑hU.fromSpec ⁻¹' ↑(X.basicOpen f) = ↑(X.basicOpen f)

Tactic:
Set.image_preimage_eq_inter_range,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ ↑(X.basicOpen f) ∩ Set.range ⇑hU.fromSpec = ↑(X.basicOpen f)