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

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

pp: 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✝)

pp: 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✝)

Tactic:
· refine ⟨u, by rw [trinomial_trailing_coeff' hkm hmn]⟩

Goal state after:
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.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'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ Disjoint (range q) (Ico q (p.natDegree + 1))

Tactic:
rw [range_eq_Ico, disjoint_iff_inter_eq_empty, eq_empty_iff_forall_notMem]

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)
this : range q = range (q - 1 + 1)
⊢ ∀ (x : ℕ), x ∉ Ico 0 q ∩ Ico q (p.natDegree + 1)
Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
i : Fin 2
⊢ ((basis a b).repr ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) w)) i =
    !![z.re, a * z.im; z.im, z.re + b * z.im].mulVec (⇑((basis a b).repr w)) i

Tactic:
fin_cases i

Goal state after:
case «0»
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ ((basis a b).repr ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) w)) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![z.re, a * z.im; z.im, z.re + b * z.im].mulVec (⇑((basis a b).repr w)) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ ((basis a b).repr ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) w)) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![z.re, a * z.im; z.im, z.re + b * z.im].mulVec (⇑((basis a b).repr w)) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
h : star z ∈ (QuadraticAlgebra R a b)⁰
⊢ z ∈ (QuadraticAlgebra R a b)⁰

Tactic:
rw [← star_involutive z]

Goal state after:
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
h : star z ∈ (QuadraticAlgebra R a b)⁰
⊢ star (star z) ∈ (QuadraticAlgebra R a b)⁰
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (x.imI * y.imI) • (c₁ • 1 + c₂ • q.i) +
                        (x.imI * y.imJ) • q.k +
                      (x.imI * y.imK) • (c₁ • q.j + c₂ • q.k) +
                    (x.imJ * y.re) • q.j +
                  (x.imJ * y.imI) • (c₂ • q.j + -q.k) +
                (x.imJ * y.imJ * c₃) • 1 +
              (x.imJ * y.imK) • ((c₂ * c₃) • 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((x.imK * y.imI * c₁) • q.j) +
        (x.imK * y.imJ * c₃) • q.i +
      -((c₁ * c₃ * x.imK * y.imK) • 1)

Tactic:
simp only [mul_comm _ c₁]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (x.imI * y.imI) • (c₁ • 1 + c₂ • q.i) +
                        (x.imI * y.imJ) • q.k +
                      (x.imI * y.imK) • (c₁ • q.j + c₂ • q.k) +
                    (x.imJ * y.re) • q.j +
                  (x.imJ * y.imI) • (c₂ • q.j + -q.k) +
                (x.imJ * y.imJ * c₃) • 1 +
              (x.imJ * y.imK) • ((c₂ * c₃) • 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((c₁ * (x.imK * y.imI)) • q.j) +
        (x.imK * y.imJ * c₃) • q.i +
      -((c₁ * c₃ * x.imK * y.imK) • 1)
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid
h_zero' : inst₁.toZero = inst₂.toZero
h_one' : inst₁.toOne = inst₂.toOne
⊢ NatCast.natCast = NatCast.natCast

Tactic:
funext n

Goal state after:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid
h_zero' : inst₁.toZero = inst₂.toZero
h_one' : inst₁.toOne = inst₂.toOne
n : ℕ
⊢ ↑n = ↑n
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
h_one' : inst₁.toMulZeroOneClass.toOne = inst₂.toMulZeroOneClass.toOne
h_one : One.one = One.one
⊢ inst₁ = inst₂

Tactic:
have : inst₁.toAddCommMonoidWithOne = inst₂.toAddCommMonoidWithOne := by
    ext : 1 <;> assumption

Goal state after:
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
h_one' : inst₁.toMulZeroOneClass.toOne = inst₂.toMulZeroOneClass.toOne
h_one : One.one = One.one
this : inst₁.toAddCommMonoidWithOne = inst₂.toAddCommMonoidWithOne
⊢ inst₁ = inst₂
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
⊢ IntCast.intCast = IntCast.intCast

Tactic:
funext n

Goal state after:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
n : ℤ
⊢ IntCast.intCast n = IntCast.intCast n
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

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
⊢ f.coeff a ≠ 0

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
⊢ p ((erase a) f)

Tactic:
· rw [support_erase, Finset.mem_erase]
      exact fun H ↦ H.1 rfl

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
⊢ f.coeff a ≠ 0

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
⊢ p ((erase a) f)
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 → R → Prop
⊢ ∀ (a b c : RingQuot r), (a + b) * c = a * c + b * c

Tactic:
by
    rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp only [mul_quot, add_quot, right_distrib]

Goal state after:
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₁
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2

Tactic:
let P := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
  have i₁ : 0 ≤ P := by
    have idem : P * P = 4 * P := CHSH_id T.A₀_inv T.A₁_inv T.B₀_inv T.B₁_inv
    have idem' : P = (1 / 4 : ℝ) • (P * P) := by
      have h : 4 * P = (4 : ℝ) • P := by simp [map_ofNat, Algebra.smul_def]
      rw [idem, h, ← mul_smul]
      simp
    have sa : star P = P := by
      dsimp [P]
      simp only [star_add, star_sub, star_mul, star_ofNat, T.A₀_sa, T.A₁_sa, T.B₀_sa,
        T.B₁_sa, mul_comm B₀, mul_comm B₁]
    simpa only [← idem', sa]
      using smul_nonneg (by simp : (0 : ℝ) ≤ 1 / 4) (star_mul_self_nonneg P)
  apply le_of_sub_nonneg
  simpa only [sub_add_eq_sub_sub, ← sub_add] using i₁

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ X * p = (p.sum fun a b ↦ (monomial a) (φ b)) * X

Tactic:
simp only [X, mul_def]
  rw [sum_monomial_index (by simp), sum_sum_index (by simp) (by simp)]
  simp [add_comm]

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

Goal state before:
pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g h : SkewMonoidAlgebra k G
x : G
a : k
⊢ single x a * g * h = single x a * (g * h)

Tactic:
| single x a =>

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

Goal state before:
pp: case add
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g h : SkewMonoidAlgebra k G
f✝ g✝ : SkewMonoidAlgebra k G
a✝¹ : f✝ * g * h = f✝ * (g * h)
a✝ : g✝ * g * h = g✝ * (g * h)
⊢ (f✝ + g✝) * g * h = (f✝ + g✝) * (g * h)

Tactic:
simp_all [add_mul]

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
f g h : SkewMonoidAlgebra k G
⊢ f * g * h = f * (g * h)

Tactic:
induction f with

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
f : SkewMonoidAlgebra k G
⊢ 1 * f = f

Tactic:
induction f with

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

Goal state before:
pp: case add
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
a✝¹ : f * 1 = f
a✝ : g * 1 = g
⊢ (f + g) * 1 = f + g

Tactic:
simp_all [add_mul]

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
f : SkewMonoidAlgebra k G
⊢ f * 1 = f

Tactic:
induction f with

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
g : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
gc : Y.presheaf ⟶ (pushforward C g).obj X.presheaf
h : { hom := { base := f, c := fc } }.hom.base = { hom := { base := g, c := gc } }.hom.base
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap { hom := { base := f, c := fc } }.hom x =
      (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap { hom := { base := g, c := gc } }.hom x
⊢ { hom := { base := f, c := fc } } = { hom := { base := g, c := gc } }

Tactic:
obtain rfl : f = g := h

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc gc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap { hom := { base := f, c := fc } }.hom x =
      (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap { hom := { base := f, c := gc } }.hom x
⊢ { hom := { base := f, c := fc } } = { hom := { base := f, c := gc } }
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_2
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)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).obj U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))),
    (fun s ↦ IsGluing (X.sheafToTypes T).obj U sf' s) y → y = gl
⊢ (fun s ↦ (subpresheafToTypes P.toPrelocalPredicate).IsGluing U sf s) ⟨gl, ⋯⟩

Tactic:
exact fun i ↦ Subtype.ext (gl_spec i)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
f : ↑R
⊢ (Spec R).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) f) = PrimeSpectrum.basicOpen f

Tactic:
ext x
  simp only [SetLike.mem_coe, Scheme.mem_basicOpen_top]
  suffices IsUnit (algebraMap _ ((structurePresheafInCommRingCat ↑R).stalk x) f) ↔
    f ∉ PrimeSpectrum.asIdeal x by exact this
  rw [← isUnit_map_iff (StructureSheaf.stalkIso R x).symm, AlgEquiv.commutes]
  exact IsLocalization.AtPrime.isUnit_to_map_iff _ (PrimeSpectrum.asIdeal x) 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
| (fun x ↦
      (TopCat.Hom.hom (limit.π (cospan f.base g.base) WalkingCospan.right))
        ((TopCat.Hom.hom (limit.lift (cospan f.base g.base) (PullbackCone.mk s.fst.base s.snd.base ⋯))) x)) ⁻¹'
    ⇑(ConcreteCategory.hom (pullback.snd f.base g.base)) '' ↑(unop U)

Tactic:
← Set.preimage_preimage

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 ⋯))) ⁻¹'
    ⇑(TopCat.Hom.hom (limit.π (cospan f.base g.base) WalkingCospan.right)) ⁻¹'
      ⇑(ConcreteCategory.hom (pullback.snd f.base g.base)) '' ↑(unop U)
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
X : C
R : Presieve X
h : ∀ (x : F.obj X), ∃ Y f, R f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom (F.map f))
x : F.obj X
⊢ ∃ Y g, map F R g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)

Tactic:
obtain ⟨Y, g, hg, hi⟩ := h x
    exact ⟨_, _, ⟨hg⟩, hi⟩

Goal state after:
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)
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (p₁ i)))

Tactic:
have : F.map (p₁ i) = F.map ((h i).isoPullback.hom) ≫ pullbackComparison F g (f i) ≫
        pullback.fst _ _ := by simp [← Functor.map_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 ∈ Set.range ⇑(ConcreteCategory.hom (F.map (p₁ i)))
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
⊢ ∀ {X Y S : Type u_2} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison (𝟭 (Type u_2)) f g))

Tactic:
intro X Y S f g _

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
F : C ⥤ Type u
X Y S : Type u_2
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
⊢ Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison (𝟭 (Type u_2)) f g))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan f g ⋙ forget) LocallyRingedSpace.forgetToTop

Tactic:
refine @preservesLimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoCospan.{u} _).symm ?_

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))
    LocallyRingedSpace.forgetToTop
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion (pullback.snd f g)

Tactic:
rw [SheafedSpace.isOpenImmersion_iff_hom]
  have : _ = (pullback.snd f g).hom := preservesLimitIso_hom_π forget (cospan f g) right
  rw [← this]
  have := HasLimit.isoOfNatIso_hom_π (diagramIsoCospan (cospan f g ⋙ forget)) right
  dsimp at this
  rw [Category.comp_id] at this
  rw [← this]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.OverClass

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
X Y : C
f : X ⟶ Y
S S' : C
inst✝⁷ : OverClass X S
inst✝⁶ : OverClass X S'
inst✝⁵ : OverClass Y S
inst✝⁴ : OverClass Y S'
inst✝³ : OverClass S S'
inst✝² : IsOverTower X S S'
inst✝¹ : IsOverTower Y S S'
inst✝ : HomIsOver f S
⊢ HomIsOver f S'

Tactic:
by
  constructor
  rw [← comp_over (Y ↘ S), comp_over_assoc f, comp_over]

Goal state after: