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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ p.natDegree + p.natTrailingDegree - n ≤ p.natDegree

Tactic:
tsub_le_iff_tsub_le,

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ p.natDegree + p.natTrailingDegree - p.natDegree ≤ n
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a₁ ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a₁ ≠ 0 →
      ∀ a₂ ∈ Finset.range (p.natDegree + 1),
        p.mirror.coeff a₂ ≠ 0 →
          (revAt (p.natDegree + p.natTrailingDegree)) a₁ = (revAt (p.natDegree + p.natTrailingDegree)) a₂ → a₁ = a₂

pp: case refine_4
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ b ∈ Finset.range (p.natDegree + 1),
    p.coeff b ≠ 0 →
      ∃ a,
        ∃ (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
          (revAt (p.natDegree + p.natTrailingDegree)) a = b

pp: case refine_5
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a ≠ 0 → p.mirror.coeff a = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) a)

Tactic:
· exact fun n₁ _ _ _ _ _ h => by rw [← @revAt_invol _ n₁, h, revAt_invol]

Goal state after:
case refine_4
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ b ∈ Finset.range (p.natDegree + 1),
    p.coeff b ≠ 0 →
      ∃ a,
        ∃ (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
          (revAt (p.natDegree + p.natTrailingDegree)) a = b

case refine_5
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a ≠ 0 → p.mirror.coeff a = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) a)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ p.natDegree + p.natTrailingDegree - n ≤ p.natDegree

Tactic:
tsub_le_iff_tsub_le,

Goal state after:
case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ p.natDegree + p.natTrailingDegree - p.natDegree ≤ n
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
⊢ (p.toTupleMvPolynomial ((fun i ↦ i) ⟨1, ⋯⟩)).IsHomogeneous p.natDegree

Tactic:
· simpa [toTupleMvPolynomial] using MvPolynomial.isHomogeneous_X_pow 1 p.natDegree

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

Goal state before:
pp: case add
R : Type u_1
inst✝³ : Semiring R
p✝ : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
r : R
p q : R[X]
ph : (r • p).smeval x = r • p.smeval x
qh : (r • q).smeval x = r • q.smeval x
⊢ (r • (p + q)).smeval x = r • (p + q).smeval x

Tactic:
smul_add,

Goal state after:
case add
R : Type u_1
inst✝³ : Semiring R
p✝ : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
r : R
p q : R[X]
ph : (r • p).smeval x = r • p.smeval x
qh : (r • q).smeval x = r • q.smeval x
⊢ (r • p + r • q).smeval x = r • (p + q).smeval x
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ ((X - C η) * P).eraseLead - (monomial ((X - C η) * P).eraseLead.natDegree) ((X - C η) * P).eraseLead.leadingCoeff =
    ((X - C η) * P.eraseLead).eraseLead

Tactic:
leadingCoeff_eraseLead_eq_nextCoeff hQ₁.ne

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ ((X - C η) * P).eraseLead - (monomial ((X - C η) * P).eraseLead.natDegree) ((X - C η) * P).nextCoeff =
    ((X - C η) * P.eraseLead).eraseLead
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ (X - C η) * P - (monomial (P.natDegree + 1)) P.leadingCoeff -
      (monomial P.natDegree) (P.coeff d - η * P.coeff (d + 1)) =
    (X - C η) * P - (X - C η) * (monomial P.natDegree) P.leadingCoeff - (monomial P.natDegree) P.nextCoeff

Tactic:
sub_mul,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ X * P - C η * P - (monomial (P.natDegree + 1)) P.leadingCoeff -
      (monomial P.natDegree) (P.coeff d - η * P.coeff (d + 1)) =
    X * P - C η * P - (X - C η) * (monomial P.natDegree) P.leadingCoeff - (monomial P.natDegree) P.nextCoeff
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ X * P - C η * P - (monomial (P.natDegree + 1)) P.leadingCoeff -
      (monomial P.natDegree) (P.coeff d - η * P.coeff (d + 1)) =
    X * P - C η * P - (X - C η) * (monomial P.natDegree) P.leadingCoeff - (monomial P.natDegree) P.nextCoeff

Tactic:
sub_mul,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ X * P - C η * P - (monomial (P.natDegree + 1)) P.leadingCoeff -
      (monomial P.natDegree) (P.coeff d - η * P.coeff (d + 1)) =
    X * P - C η * P - (X * (monomial P.natDegree) P.leadingCoeff - C η * (monomial P.natDegree) P.leadingCoeff) -
      (monomial P.natDegree) P.nextCoeff
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

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

Tactic:
rw [trinomial_def] at hp

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 = C ↑u * X ^ k + C ↑v * X ^ m + C ↑w * X ^ n
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Module: Mathlib.Algebra.PresentedMonoid.Basic

Goal state before:
pp: α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
⊢ closure (range (of rels)) = ⊤

Tactic:
Submonoid.eq_top_iff'

Goal state after:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
⊢ ∀ (x : PresentedMonoid rels), x ∈ closure (range (of rels))
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : Zero R
r : R
⊢ QuadraticAlgebra.C r = QuadraticAlgebra.C 0 ↔ r = 0

Tactic:
C_inj

Goal state after:
R : Type u_1
a b : R
inst✝ : Zero R
r : R
⊢ r = 0 ↔ r = 0
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : Zero R
inst✝ : One R
r : R
⊢ QuadraticAlgebra.C r = QuadraticAlgebra.C 1 ↔ r = 1

Tactic:
C_inj

Goal state after:
R : Type u_1
a b : R
inst✝¹ : Zero R
inst✝ : One R
r : R
⊢ r = 1 ↔ r = 1
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ ((algebraMap R (QuadraticAlgebra R a b)) (norm z)).re = (z * star z).re

Tactic:
simp [norm, star, mul_comm]

Goal state after:
case re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ z.re * z.re + z.im * (b * z.re) - z.im * (a * z.im) = z.re * (z.re + b * z.im) + -(z.im * (a * z.im))
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ ((algebraMap R (QuadraticAlgebra R a b)) (norm z)).im = (z * star z).im

Tactic:
simp [norm, star, mul_comm]

Goal state after:
case im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ 0 = -(z.re * z.im) + z.im * (z.re + b * z.im) + -(z.im * (b * z.im))
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
simp [Rat.cast_def]

Goal state after:
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₃
⊢ (c₂ • q.j - q.k) * q.j = (c₂ * c₃) • 1 - c₃ • q.i

Tactic:
sub_mul,

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₃
⊢ c₂ • q.j * q.j - q.k * q.j = (c₂ * c₃) • 1 - c₃ • q.i
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₃
⊢ (q.i * c₂ • q.j - (c₁ • q.j + c₂ • q.i * q.j)) * q.j = -((c₁ * c₃) • 1)

Tactic:
sub_mul,

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₃
⊢ q.i * c₂ • q.j * q.j - (c₁ • q.j + c₂ • q.i * q.j) * q.j = -((c₁ * c₃) • 1)
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✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a✝ r : α
⊢ ((f * g) a✝ - (g * f) a✝) * (r * ((f * g) a✝ - (g * f) a✝)) = 0

Tactic:
sub_mul,

Goal state after:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a✝ r : α
⊢ (f * g) a✝ * (r * ((f * g) a✝ - (g * f) a✝)) - (g * f) a✝ * (r * ((f * g) a✝ - (g * f) a✝)) = 0
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:
rw [sum_def , Finset.sum_subset hs]
  intro _ _ hx
  simp only [mem_support_iff, ne_eq, not_not] at hx
  simp [hx, hf]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
G' : Type u_3
f : G → G'
v : SkewMonoidAlgebra k G
⊢ ((mapDomain f) v).coeff = Finsupp.mapDomain f v.coeff

Tactic:
mapDomain_apply,

Goal state after:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
G' : Type u_3
f : G → G'
v : SkewMonoidAlgebra k G
⊢ (v.sum fun a ↦ single (f a)).coeff = Finsupp.mapDomain f v.coeff
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 α
inst✝ : AddCommMonoid k
g a✝ : G
⊢ (g • 0).coeff a✝ = (coeff 0) a✝

Tactic:
simp [comapSMul_def, mapDomain]

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

Goal state before:
pp: case inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
⊢ x + y ≤ x + z

Tactic:
· rw [add_eq_right hy]
      rcases le_total x z with hx | hx
      · rwa [add_eq_left hx]
      · rwa [add_eq_right hx]

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

Goal state before:
pp: case inr
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
x y : Tropical R
n : ℕ
h : y ≤ x
⊢ (x + y) ^ n = x ^ n + y ^ n

Tactic:
rw [add_eq_right h, add_eq_right (pow_le_pow_left' h _)]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
x : Tropical R
n : ℕ
IH : (n + 1) • x = x
⊢ x + x = x

Tactic:
add_self

Goal state after:
case succ
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
x : Tropical R
n : ℕ
IH : (n + 1) • x = x
⊢ x = x
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
A : VertexOperator R V
n : ℤ
x : V
h : n < ((HahnModule.of R).symm (A x)).order
⊢ (coeff A n) x = 0

Tactic:
rw [coeff_eq_ncoeff, ncoeff_eq_zero_of_lt_order A (-n - 1) x]

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
n : ℤ
x : V
h : n < ((HahnModule.of R).symm (A x)).order
⊢ -(-n - 1) - 1 < ((HahnModule.of R).symm (A x)).order
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case h
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
V : Opens ↑↑(X.restrict hf)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
⊢ (g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V) = g₂.c.app (op V)

Tactic:
have :
      IsIso (hf.isOpenMap.adjunction.counit.app (unop (op (hf.functor.obj V)))) :=
        NatIso.isIso_app_of_isIso
          (whiskerLeft hf.functor hf.isOpenMap.adjunction.counit) V

Goal state after:
case h
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
V : Opens ↑↑(X.restrict hf)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
this : IsIso (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))
⊢ (g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V) = g₂.c.app (op V)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case x
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ ⇑(ConcreteCategory.hom g.base) ⁻¹' ⇑(ConcreteCategory.hom g.base) '' ⇑(ConcreteCategory.hom f.base) '' ↑U =
    ⇑(ConcreteCategory.hom f.base) '' ↑U

Tactic:
Set.preimage_image_eq _ hg.base_open.injective

Goal state after:
case x
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ ⇑(ConcreteCategory.hom f.base) '' ↑U = ⇑(ConcreteCategory.hom f.base) '' ↑U
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
I : Ideal ↑Γ(X, U)
⊢ X.zeroLocus ↑I.radical = X.zeroLocus ↑I

Tactic:
refine (X.zeroLocus_mono I.le_radical).antisymm ?_

Goal state after:
X : Scheme
U : X.Opens
I : Ideal ↑Γ(X, U)
⊢ X.zeroLocus ↑I ⊆ X.zeroLocus ↑I.radical
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : Opens ↥X
x : ↥U
f s : ↑Γ(X, U)
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s)
n : ℕ
hf : s ^ n * f = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0

Tactic:
have hu : IsUnit (X.presheaf.germ _ x x.2 (s ^ n)) := by
    rw [map_pow]
    exact IsUnit.pow n hx

Goal state after:
X : Scheme
U : Opens ↥X
x : ↥U
f s : ↑Γ(X, U)
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s)
n : ℕ
hf : s ^ n * f = 0
hu : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) (s ^ n))
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
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
⊢ IsLimit (pullbackConeOfLeft f g)

Tactic:
by
  apply PullbackCone.isLimitAux'
  intro s
  use pullbackConeOfLeftLift f g s
  use pullbackConeOfLeftLift_fst f g s
  use pullbackConeOfLeftLift_snd f g s
  intro m _ h₂
  rw [← cancel_mono (pullbackConeOfLeft f g).snd]
  exact h₂.trans (pullbackConeOfLeftLift_snd f g s).symm

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

Goal state before:
pp: K : Precoverage Scheme
X : Scheme
inst✝ : JointlySurjective K
𝒰 : Cover K X
x : ↥X
⊢ ∃ i y, (𝒰.f i) y = x

Tactic:
by
  obtain ⟨Y, g, ⟨i⟩, y, hy⟩ := JointlySurjective.exists_eq 𝒰.presieve₀ 𝒰.mem₀ x
  use i, y

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

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

Tactic:
← show _ = (pullback.fst g f).base from
    PreservesPullback.iso_hom_fst Scheme.forgetToTop g f,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range
      ⇑(ConcreteCategory.hom
          ((PreservesPullback.iso Scheme.forgetToTop g f).hom ≫
            pullback.fst (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))) =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange 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
X Y : Scheme
𝒰 : Cover (precoverage P) X
f : Y ⟶ X
hf : P f
⊢ (𝒰.add f).presieve₀ ∈ (precoverage P).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ⟨some <| 𝒰.idx x, 𝒰.covers x⟩, ?_⟩
    rintro (i | i) <;> simp [hf, 𝒰.map_prop]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i j : Discrete ι
h : i ≠ j
U : Opens ↑↑(F.obj i).toPresheafedSpace
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
y : ↑↑(F.obj i).toPresheafedSpace
hy : y ∈ ↑U
eq :
  (ConcreteCategory.hom
        (preservesColimitIso (forget C) F ≪≫
            HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫
              TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom)
      ((ConcreteCategory.hom (colimit.ι F i).hom.base) y) =
    (ConcreteCategory.hom
        (preservesColimitIso (forget C) F ≪≫
            HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫
              TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom)
      ((ConcreteCategory.hom (preservesColimitIso forgetToPresheafedSpace F).inv.base)
        ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base) x))
⊢ False

Tactic:
CategoryTheory.Iso.trans_hom,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i j : Discrete ι
h : i ≠ j
U : Opens ↑↑(F.obj i).toPresheafedSpace
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
y : ↑↑(F.obj i).toPresheafedSpace
hy : y ∈ ↑U
eq :
  (ConcreteCategory.hom
        ((preservesColimitIso (forget C) F).hom ≫
          (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      ((ConcreteCategory.hom (colimit.ι F i).hom.base) y) =
    (ConcreteCategory.hom
        ((preservesColimitIso (forget C) F).hom ≫
          (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      ((ConcreteCategory.hom (preservesColimitIso forgetToPresheafedSpace F).inv.base)
        ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base) x))
⊢ False
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
⊢ Epi
    ((inv (pullback.snd f g)).base ≫
      (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom)

Tactic:
show (inv (pullback.snd f g)).base = _ from
        (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _).map_inv _

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
⊢ Epi
    (inv ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map (pullback.snd f g)) ≫
      (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R A : Type u
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : U ≤ basicOpen f
x✝ : ↥(unop (op U))
⊢ 1 • 1 • (algebraMap R A) f = 1 • ⟨f, ⋯⟩ • 1

Tactic:
simp [Algebra.smul_def, Submonoid.smul_def]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
X : Scheme
U V : X.Opens
e : U ≤ V
⊢ IsOpenImmersion (X.homOfLE e)

Tactic:
delta Scheme.homOfLE

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
X : Scheme
U V : X.Opens
e : U ≤ V
⊢ IsOpenImmersion (IsOpenImmersion.lift V.ι U.ι ⋯)