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

Goal state before:
pp: case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
⊢ ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k =
    ∑ x ∈ s,
      (r x * b x %ₘ g i * ∏ x ∈ s, g x +
        ((r x * b x /ₘ g i + r x * a x /ₘ g x) * (g i * ∏ x ∈ s, g x) +
          Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) x *
            ∏ k ∈ (Finset.cons i s hi).erase x, g k))

Tactic:
refine Finset.sum_congr rfl fun j hj => ?_

Goal state after:
case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
⊢ r j * ∏ k ∈ s.erase j, g k =
    r j * b j %ₘ g i * ∏ x ∈ s, g x +
      ((r j * b j /ₘ g i + r j * a j /ₘ g j) * (g i * ∏ x ∈ s, g x) +
        Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) j *
          ∏ k ∈ (Finset.cons i s hi).erase j, g k)
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
⊢ eval r
        (∑ k ∈ range q,
          (q.choose (k + 1) * q.descFactorial (q - (k + 1))) • (X - C r) ^ (q - (q - (k + 1))) *
            (⇑derivative)^[k + 1] p') +
      q ! • eval r p' =
    q ! • eval r p'

Tactic:
convert! zero_add _

Goal state after:
case e'_2.e'_5
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
⊢ eval r
      (∑ k ∈ range q,
        (q.choose (k + 1) * q.descFactorial (q - (k + 1))) • (X - C r) ^ (q - (q - (k + 1))) *
          (⇑derivative)^[k + 1] p') =
    0
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
P : R[X]
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) (-P).coeffList))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) P.coeffList))).length -
      1

Tactic:
coeffList_neg

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
P : R[X]
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0))
            (List.map (⇑SignType.sign) (List.map (fun x ↦ -x) P.coeffList)))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) P.coeffList))).length -
      1
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inl
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

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
    rcases irreducible_aux3 hkm hmn hkm' hmn' u v w x z hp hq hpq with (h2 | h2)
    · exact Or.inl h2
    · exact Or.inr (Or.inr (Or.inl h2))

Goal state after:
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
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), (domCongr e) (c • x) = c • (domCongr e) x

Tactic:
simp only [domCongr_apply]
    intro c x
    simp_rw [equivMapDomain_eq_mapDomain, mapDomain_smul]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : MulSemiringAction G k
V : Type u_4
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : Module (SkewMonoidAlgebra k G) V
inst✝ : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, (of k G) g • v ∈ W
f : SkewMonoidAlgebra k G
v : V
hv : v ∈ ↑W
⊢ f.coeff.sum single • v ∈ ↑W

Tactic:
Finsupp.sum,

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : MulSemiringAction G k
V : Type u_4
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : Module (SkewMonoidAlgebra k G) V
inst✝ : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, (of k G) g • v ∈ W
f : SkewMonoidAlgebra k G
v : V
hv : v ∈ ↑W
⊢ (∑ a ∈ f.coeff.support, single a (f.coeff a)) • v ∈ ↑W
Module: Mathlib.Algebra.Star.CHSH

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : IsOrderedModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
h : 4 * P = 4 • P
⊢ P = (1 / 4) • (P * P)

Tactic:
idem,

Goal state after:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : IsOrderedModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
h : 4 * P = 4 • P
⊢ P = (1 / 4) • (4 * P)
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
⊢ p.sum f = ∑ n ∈ p.support, f n (p.coeff n)

Tactic:
by
  simp only [sum_def', SkewMonoidAlgebra.sum_def, Finsupp.sum]
  apply Finset.sum_of_injOn (toAdd) (Injective.injOn fun ⦃a₁ a₂⦄ a ↦ a) (fun _ ↦ ?_) <;>
  simp +contextual [coeff]

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₁
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1

Tactic:
have M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = ((m : ℝ) * a) • x := fun m a x => by
    rw [← Int.cast_smul_eq_zsmul ℝ, ← mul_smul]
  let P := (√2)⁻¹ • (A₁ + A₀) - B₀
  let Q := (√2)⁻¹ • (A₁ - A₀) + B₁
  have w : √2 ^ 3 • (1 : R) - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2) := by
    dsimp [P, Q]
    -- distribute out all the powers and products appearing on the RHS
    simp only [sq, sub_mul, mul_sub, add_mul, mul_add, smul_add, smul_sub]
    -- pull all coefficients out to the front, and combine `√2`s where possible
    simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, ← mul_smul, sqrt_two_inv_mul_self]
    -- replace Aᵢ * Aᵢ = 1 and Bᵢ * Bᵢ = 1
    simp only [← sq, T.A₀_inv, T.A₁_inv, T.B₀_inv, T.B₁_inv]
    -- move Aᵢ to the left of Bᵢ
    simp only [← T.A₀B₀_commutes, ← T.A₀B₁_commutes, ← T.A₁B₀_commutes, ← T.A₁B₁_commutes]
    -- collect terms, simplify coefficients, and collect terms again:
    abel_nf
    -- all terms coincide, but the last one. Simplify all other terms
    simp only [M]
    simp only [neg_mul, mul_inv_cancel_of_invertible, add_assoc, add_comm,
      add_left_comm, one_smul, Int.cast_neg, neg_smul, Int.cast_ofNat, ← add_smul]
    grind
  have pos : 0 ≤ (√2)⁻¹ • (P ^ 2 + Q ^ 2) := by
    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]
    have Q_sa : star Q = Q := by
      simp only [Q, star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₁_sa]
    have P2_nonneg : 0 ≤ P ^ 2 := by simpa only [P_sa, sq] using star_mul_self_nonneg P
    have Q2_nonneg : 0 ≤ Q ^ 2 := by simpa only [Q_sa, sq] using star_mul_self_nonneg Q
    positivity
  apply le_of_sub_nonneg
  simpa only [sub_add_eq_sub_sub, ← sub_add, w, Nat.cast_zero] using pos

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
c : R
h : c ≠ 0
⊢ (C c * X).support = {1}

Tactic:
by
  rw [C_mul_X_eq_monomial, support_monomial 1 h]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ X.support = {1}

Tactic:
← pow_one X,

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (X ^ 1).support = {1}
Module: Mathlib.Algebra.Star.TransferInstance

Goal state before:
pp: R : Type u_1
S : Type u_2
e : R ≃ S
𝕜 : Type u_3
inst✝³ : Star 𝕜
inst✝² : Star S
inst✝¹ : SMul 𝕜 S
inst✝ : StarModule 𝕜 S
this : Star R := e.star
⊢ StarModule 𝕜 R

Tactic:
let := e.smul 𝕜

Goal state after:
R : Type u_1
S : Type u_2
e : R ≃ S
𝕜 : Type u_3
inst✝³ : Star 𝕜
inst✝² : Star S
inst✝¹ : SMul 𝕜 S
inst✝ : StarModule 𝕜 S
this✝ : Star R := e.star
this : SMul 𝕜 R := Equiv.smul 𝕜 e
⊢ StarModule 𝕜 R
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
a a' : G
b : k
h : b ≠ 0
⊢ single a b = single a' b ↔ a = a'

Tactic:
by
  rw [← coeff_inj]
  exact Finsupp.single_left_inj h

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

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst✝² : Monoid G
inst✝¹ : AddCommMonoid M
inst✝ : MulAction G α
f : SkewMonoidAlgebra M α
⊢ 1 • f = f

Tactic:
by rw [comapSMul_def, one_smul_eq_id, mapDomain_id]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := this.toFinset
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
⊢ ∑ p ∈ f.support ×ˢ g.support with p.1 * p.2 = x, f.coeff p.1 * p.1 • g.coeff p.2 =
    ∑ p ∈ s with p.1 ∈ f.support ∧ p.2 ∈ g.support, f.coeff p.1 * p.1 • g.coeff p.2

Tactic:
by
        apply Finset.sum_congr_of_eq_on_inter <;> aesop

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
a₁ a₂ : G
b₁ b₂ : k
⊢ single (a₁ * a₂) (b₁ * a₁ • 0) = 0

Tactic:
by simp [smul_zero, mul_zero, single_zero]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), BddBelow (Function.support fun y ↦ (f y) x)
n : ℤ
⊢ ncoeff (of_coeff f hf) n = f (-n - 1)

Tactic:
by
  ext v
  rw [ncoeff_apply, coeff_apply_apply, of_coeff_apply_coeff]

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

Goal state before:
pp: S T : Type u_1
f : S ⟶ T
hf : IsIso f
x : T
⊢ ∃ Y g, Presieve.singleton f g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)

Tactic:
use S, f, ⟨⟩
    exact surjective_of_epi f x

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

Goal state before:
pp: P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
⊢ Presieve.singleton f ∈ (precoverage P).coverings S ↔ Function.Surjective ⇑f ∧ P f

Tactic:
rw [← Presieve.ofArrows_pUnit.{0}, ofArrows_mem_precoverage_iff]

Goal state after:
P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
⊢ ((∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑f) ∧ ∀ (i : PUnit.{1}), P f) ↔ Function.Surjective ⇑f ∧ P f
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ IsIso (f.c.app (op U))

Tactic:
have : U = H.base_open.functor.obj ((Opens.map f.base).obj U) := by
    ext1
    exact (Set.inter_eq_left.mpr hU).symm.trans Set.image_preimage_eq_inter_range.symm

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this : U = ⋯.functor.obj ((Opens.map f.base).obj U)
⊢ IsIso (f.c.app (op U))
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : M
g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
h : g₂ • f₁ = g₁ • f₂
x : ↥(unop (op U))
⊢ ∃ u, u • ⟨g₂, ⋯⟩ • f₁ = u • ⟨g₁, ⋯⟩ • f₂

Tactic:
by simp [h, Submonoid.smul_def]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
⊢ Hom.app (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V) = Hom.app f (U.ι ''ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
simpa [← Functor.map_comp_assoc, ← Functor.map_comp] using!
    congr(Y.presheaf.map (eqToHom (congr_arg (U.ι ''ᵁ ·) (U.ι.preimage_image_eq V).symm)).op ≫
      $(Scheme.Hom.congr_app (morphismRestrict_ι f U) (U.ι ''ᵁ V)))

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
⊢ Arrow.mk (f ∣_ U ∣_ V) ≅ Arrow.mk (f ∣_ U.ι ''ᵁ V)

Tactic:
by
  refine Arrow.isoMk' _ _ ((Scheme.Opens.ι _).isoImage _ ≪≫ Scheme.isoOfEq _ ?_)
    ((Scheme.Opens.ι _).isoImage _) ?_
  · exact image_morphismRestrict_preimage f U V
  · simp [← cancel_mono (Scheme.Opens.ι _)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
V V' : X.Opens
i : V ≤ V'
⊢ resLE (𝟙 X) V' V i = X.homOfLE i

Tactic:
simp only [resLE, morphismRestrict_id]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
⊢ resLE f U V e ⁻¹ᵁ O = V.ι ⁻¹ᵁ f ⁻¹ᵁ U.ι ''ᵁ O

Tactic:
rw [← comp_preimage, ← resLE_comp_ι f e, comp_preimage, preimage_image_eq]

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
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
n : ℕ
c : ι →₀ R
hc : ∑ i, c i • b i = f ^ (n + 1)
i : ι
x : ↥(unop (op (basicOpen (b i))))
⊢ ⟨b i, ⋯⟩ • ∑ i, c i • a i = ⟨f ^ (n + 1), ⋯⟩ • a i

Tactic:
Finset.smul_sum,

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
n : ℕ
c : ι →₀ R
hc : ∑ i, c i • b i = f ^ (n + 1)
i : ι
x : ↥(unop (op (basicOpen (b i))))
⊢ ∑ x_1, ⟨b i, ⋯⟩ • c x_1 • a x_1 = ⟨f ^ (n + 1), ⋯⟩ • a i
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v, u₁} C
C' : Type u₂
inst✝¹ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j k : D.J
⊢ ((PreservesPullback.iso F (D.f i j) (D.f i k)).inv ≫
        F.map (D.t' i j k) ≫ (PreservesPullback.iso F (D.f j k) (D.f j i)).hom) ≫
      pullback.snd (F.map (D.f j k)) (F.map (D.f j i)) =
    pullback.fst (F.map (D.f i j)) (F.map (D.f i k)) ≫ F.map (D.t i j)

Tactic:
by simpa [Iso.inv_comp_eq] using congr_arg (fun f => F.map f) (D.t_fac i j k)

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
U✝ : X.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X, U✝)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩) := Y.presheaf.algebra_section_stalk ⟨f x, ⋯⟩
⊢ Arrow.mk (Scheme.Hom.stalkMap f x) ≅
    Arrow.mk
      (CommRingCat.ofHom
        (Localization.localRingHom (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal (hV.primeIdealOf ⟨x, hx⟩).asIdeal
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯))

Tactic:
have := hU.isLocalization_stalk ⟨f x, hVU hx⟩

Goal state after:
X Y : Scheme
U✝ : X.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X, U✝)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝ : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩) := Y.presheaf.algebra_section_stalk ⟨f x, ⋯⟩
this : IsLocalization.AtPrime (↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩)) (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
⊢ Arrow.mk (Scheme.Hom.stalkMap f x) ≅
    Arrow.mk
      (CommRingCat.ofHom
        (Localization.localRingHom (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal (hV.primeIdealOf ⟨x, hx⟩).asIdeal
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ U ≤ ⨆ f, X.basicOpen ↑f ↔ Ideal.span s = ⊤

Tactic:
rw [← hU.iSup_basicOpen_eq_self_iff, @comm _ Eq]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ U ≤ ⨆ f, X.basicOpen ↑f ↔ U = ⨆ f, X.basicOpen ↑f
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case refine_1
D : GlueData
h : MkCore
i j k : h.J
x : ↑(h.U i)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
⊢ ↑((ConcreteCategory.hom (h.t i j)) (↑⟨(⟨x, hx⟩, ⟨x, hx'⟩), ⋯⟩).1) ∈ h.V j k

Tactic:
exact h.t_inter _ ⟨x, hx⟩ hx'

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h
X : Scheme
𝒰✝ : X.OpenCover
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf : ∀ (x y : 𝒰.I₀), pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x = pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y
i j : (ulift 𝒰).gluedCover.J
⊢ (ulift 𝒰).gluedCover.diagram.fst (i, j) ≫ f (idx 𝒰 i) = (ulift 𝒰).gluedCover.diagram.snd (i, j) ≫ f (idx 𝒰 j)

Tactic:
change pullback.fst _ _ ≫ f _ = (_ ≫ _) ≫ f _

Goal state after:
case h
X : Scheme
𝒰✝ : X.OpenCover
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf : ∀ (x y : 𝒰.I₀), pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x = pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y
i j : (ulift 𝒰).gluedCover.J
⊢ pullback.fst ((ulift 𝒰).f i) ((ulift 𝒰).f j) ≫ f (idx 𝒰 i) =
    ((ulift 𝒰).gluedCover.t i j ≫ (ulift 𝒰).gluedCover.f j i) ≫ f (idx 𝒰 j)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i j : 𝒰.I₀
⊢ pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
    (gluing 𝒰 f g).V (i, j)

Tactic:
refine (pullbackRightPullbackFstIso _ _ _).hom ≫ ?_
  refine pullback.map _ _ _ _ ?_ (𝟙 _) (𝟙 _) ?_ ?_
  · exact (pullbackSymmetry _ _).hom ≫
      pullback.map _ _ _ _ (𝟙 _) s.snd f (Category.id_comp _).symm s.condition
  · simpa using! pullback.condition
  · simp only [Category.comp_id, Category.id_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ (∀ (x : ↥(X ⨿ Y)),
      ∃ i,
        x ∈
          Set.range
            ⇑({ I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1}, X := fun x ↦ Sum.elim (fun x ↦ X) (fun x ↦ Y) x,
                    f := fun x ↦ Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr) x }.f
                i)) ∧
    ∀
      (i :
        { I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1}, X := fun x ↦ Sum.elim (fun x ↦ X) (fun x ↦ Y) x,
            f := fun x ↦ Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr) x }.I₀),
      IsOpenImmersion
        ({ I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1}, X := fun x ↦ Sum.elim (fun x ↦ X) (fun x ↦ Y) x,
              f := fun x ↦ Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr) x }.f
          i)

Tactic:
refine ⟨fun x ↦ ?_, fun x ↦ x.rec (fun _ ↦ inferInstance) (fun _ ↦ inferInstance)⟩

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥(X ⨿ Y)
⊢ ∃ i,
    x ∈
      Set.range
        ⇑({ I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1}, X := fun x ↦ Sum.elim (fun x ↦ X) (fun x ↦ Y) x,
                f := fun x ↦ Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr) x }.f
            i)