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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : IsScalarTower R S S
n : ℕ
⊢ (p * X ^ (n + 1)).smeval x = p.smeval x * x ^ (n + 1)

Tactic:
by
    rw [npow_add, ← mul_assoc, npow_one, smeval_mul_X, smeval_mul_X_pow n, npow_add,
      ← smeval_assoc_X_pow, npow_one]

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

Goal state before:
pp: p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ C ↑v * (C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n)) =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
            (trinomial k m n ↑u ↑v ↑w * trinomial k (n - m + k) n ↑w ↑v ↑u).toFinsupp.coeff) }

Tactic:
simp_rw [trinomial_def, C_mul_X_pow_eq_monomial, add_mul, mul_add, monomial_mul_monomial,
    toFinsupp_add, toFinsupp_monomial, AddMonoidAlgebra.coeff_add, Finsupp.filter_add,
    AddMonoidAlgebra.coeff_single]

Goal state after:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + k) (↑u * ↑w)) +
                  Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + (n - m + k)) (↑u * ↑v)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + n) (↑u * ↑u)) +
              (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + k) (↑v * ↑w)) +
                  Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + (n - m + k)) (↑v * ↑v)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + n) (↑v * ↑u))) +
            (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + k) (↑w * ↑w)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + (n - m + k)) (↑w * ↑v)) +
              Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + n) (↑w * ↑u)))) }
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hf :
  r₁ i * ∏ x ∈ s, g x + g i * (q₁ * ∏ x ∈ s, g x + ∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x) =
    r₂ i * ∏ x ∈ s, g x + g i * (q₂ * ∏ x ∈ s, g x + ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
rw [← sub_eq_zero, add_sub_add_comm, ← sub_mul, ← mul_sub,
      ← neg_sub, neg_mul, neg_add_eq_sub, sub_eq_zero] at hf

Goal state after:
case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hf :
  g i *
      (q₁ * ∏ x ∈ s, g x + ∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x -
        (q₂ * ∏ x ∈ s, g x + ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x)) =
    (r₂ i - r₁ i) * ∏ x ∈ s, g x
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
⊢ norm (star x) = norm x

Tactic:
by
  simp only [norm, MonoidHom.coe_mk, OneHom.coe_mk, re_star, im_star, mul_neg, neg_mul, neg_neg,
    sub_left_inj]
  ring

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y z : R
⊢ x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z

Tactic:
by
  rw [← left_cancel (x ◃⁻¹ y), right_inv, ← left_cancel x, right_inv, self_distrib]
  repeat' rw [right_inv]

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

Tactic:
i_mul_j

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.k - (c₁ • q.j + c₂ • q.k) = -(c₁ • q.j)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddMonoid k
S : Type u_3
inst✝ : SMulZeroClass S k
s : S
a : G
b : k
⊢ (s • single a b).coeff = (single a (s • b)).coeff

Tactic:
simp;

Goal state after:
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ (∃ y, (algebraMap S R) y = ↑(toUnits v)⁻¹ * ↑(toUnits u)) ↔ ∃ α, ↑(toUnits u) = α • ↑(toUnits v)

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ (∃ y, y • 1 = ↑(toUnits v)⁻¹ * ↑(toUnits u)) ↔ ∃ α, ↑(toUnits u) = α • ↑(toUnits v)
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ (∃ y, (algebraMap S R) y = ↑(toUnits v)⁻¹ * ↑(toUnits u)) ↔ ∃ α, u = α • v

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ (∃ y, y • 1 = ↑(toUnits v)⁻¹ * ↑(toUnits u)) ↔ ∃ α, u = α • v
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : AddCommMonoid R
s : Multiset R
⊢ ∀ (a : List R), trop (sum ⟦a⟧) = (map trop ⟦a⟧).prod

Tactic:
by simpa using List.trop_sum

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a✝ b : αˢʸᵐ
a : α
⊢ ?m.16 a

Tactic:
by
      have := (Commute.one_left a).add_left (Commute.one_left a)
      rw [one_add_one_eq_two] at this
      exact this.invOf_left.eq

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

Goal state before:
pp: α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
⊢ ∀ (b : α₂) (m₁ m₂ : β),
    (((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (b * a₂) ((m₁ + m₂) * b • b₂)) =
      (((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (b * a₂) (m₁ * b • b₂)) +
        ((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (b * a₂) (m₂ * b • b₂)

Tactic:
simp [add_mul, single_add, sum_add]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
⊢ ∀ (s : Set (Tropical R)), ¬BddAbove s → sSup s = sSup ∅

Tactic:
intro s

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
⊢ ¬BddAbove s → sSup s = sSup ∅
Module: Mathlib.Algebra.Tropical.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
⊢ ∀ (s : Set (Tropical R)), ¬BddBelow s → sInf s = sInf ∅

Tactic:
intro s

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
⊢ ¬BddBelow s → sInf s = sInf ∅
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion g
inst✝ : IsOpenImmersion (f ≫ g)
x : ↥X
⊢ IsIso (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)

Tactic:
by
      rw [← Scheme.Hom.stalkMap_comp]
      infer_instance

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
⊢ (s : PullbackCone f g) →
    { l //
      l ≫ (pullbackConeOfLeft f g).fst = s.fst ∧
        l ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
          ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
            m ≫ (pullbackConeOfLeft f g).fst = s.fst → m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = l }

Tactic:
intro s

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✝ s : PullbackCone f g
⊢ { l //
    l ≫ (pullbackConeOfLeft f g).fst = s.fst ∧
      l ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
          m ≫ (pullbackConeOfLeft f g).fst = s.fst → m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = l }
Module: Mathlib.AlgebraicGeometry.OpenImmersion

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

pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop g f).hom)

Tactic:
← @Set.preimage_univ _ _ (pullback.snd g.base f.base)

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (pullback.fst (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))) ''
      ⇑(ConcreteCategory.hom (pullback.snd g.base f.base)) ⁻¹' Set.univ =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)

X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop g f).hom)
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
⊢ PreservesLimit (cospan f g ⋙ forget) (PresheafedSpace.forget C)

Tactic:
have : PreservesLimit
        (cospan ((cospan f g ⋙ forget).map Hom.inl)
          ((cospan f g ⋙ forget).map Hom.inr)) (PresheafedSpace.forget C) := by
        dsimp
        infer_instance

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this :
  PreservesLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))
    (PresheafedSpace.forget C)
⊢ PreservesLimit (cospan f g ⋙ forget) (PresheafedSpace.forget C)
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
S : (x : ↑X) → Submonoid ↑(F.stalk x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
⊢ ⨅ x, Submonoid.comap (CommRingCat.Hom.hom (F.germ (unop U) ↑x ⋯)) (S ↑x) ≤
    Submonoid.comap (CommRingCat.Hom.hom (F.map i))
      (⨅ x, Submonoid.comap (CommRingCat.Hom.hom (F.germ (unop V) ↑x ⋯)) (S ↑x))

Tactic:
intro s

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
S : (x : ↑X) → Submonoid ↑(F.stalk x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
s : ↑(F.obj U)
⊢ s ∈ ⨅ x, Submonoid.comap (CommRingCat.Hom.hom (F.germ (unop U) ↑x ⋯)) (S ↑x) →
    s ∈
      Submonoid.comap (CommRingCat.Hom.hom (F.map i))
        (⨅ x, Submonoid.comap (CommRingCat.Hom.hom (F.germ (unop V) ↑x ⋯)) (S ↑x))
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F✝ : Presheaf CommRingCat X
G : F✝.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ↑(F.presheaf.obj U) := (F.presheaf.submonoidPresheafOfStalk fun x ↦ (↑(F.presheaf.stalk x))⁰).obj U
⊢ m ≤ nonZeroDivisorsRight ↑(F.presheaf.obj U)

Tactic:
intro s

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F✝ : Presheaf CommRingCat X
G : F✝.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ↑(F.presheaf.obj U) := (F.presheaf.submonoidPresheafOfStalk fun x ↦ (↑(F.presheaf.stalk x))⁰).obj U
s : ↑(F.presheaf.obj U)
⊢ s ∈ m → s ∈ nonZeroDivisorsRight ↑(F.presheaf.obj U)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ Function.Injective ⇑(toBasicOpenₗ R M f)

Tactic:
intro s

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : LocalizedModule.Away f M
⊢ ∀ ⦃a₂ : LocalizedModule.Away f M⦄, (toBasicOpenₗ R M f) s = (toBasicOpenₗ R M f) a₂ → s = a₂
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : (toBasicOpenₗ R M f) (LocalizedModule.mk a b) = (toBasicOpenₗ R M f) (LocalizedModule.mk c d)
n : ℕ
hn : f ^ n ∈ ⊥.colon {d • a - b • c}
⊢ ⟨f ^ n, ⋯⟩ • d • a = ⟨f ^ n, ⋯⟩ • b • c

Tactic:
by simpa [sub_eq_zero, smul_sub] using! Submodule.mem_colon.mp hn _ rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ U : X.Opens
⊢ Over.homMk (X.homOfLE ⋯) ⋯ = 𝟙 (Over.mk U.ι)

Tactic:
by
    ext1
    exact Scheme.homOfLE_rfl _ _

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
⊢ Function.Surjective ⇑(toBasicOpenₗ R M f)

Tactic:
intro s

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))
⊢ ∃ a, (toBasicOpenₗ R M f) a = s
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
r s : (InducedCategory (Opens (PrimeSpectrum ↑(Γ.obj (op X)))) basicOpen)ᵒᵖ
f : r ⟶ s
⊢ CommRingCat.ofHom (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen (unop r))))) ≫
      ((inducedFunctor basicOpen).op ⋙ (structureSheaf ↑(Γ.obj (op X))).obj).map f ≫ X.toΓSpecCApp (unop s) =
    CommRingCat.ofHom
        (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen (unop r))))) ≫
      X.toΓSpecCApp (unop r) ≫
        ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).obj).map f

Tactic:
simp only [← Category.assoc]

Goal state after:
X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
r s : (InducedCategory (Opens (PrimeSpectrum ↑(Γ.obj (op X)))) basicOpen)ᵒᵖ
f : r ⟶ s
⊢ (CommRingCat.ofHom
          (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen (unop r))))) ≫
        ((inducedFunctor basicOpen).op ⋙ (structureSheaf ↑(Γ.obj (op X))).obj).map f) ≫
      X.toΓSpecCApp (unop s) =
    (CommRingCat.ofHom
          (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen (unop r))))) ≫
        X.toΓSpecCApp (unop r)) ≫
      ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).obj).map f
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : Category.{w', w} J
inst✝¹ : Small.{v, w} J
F : J ⥤ SheafedSpace C
inst✝ : HasLimits C
X Y : SheafedSpace C
f g : X ⟶ Y
⊢ Epi (coequalizer.π f g).hom.base

Tactic:
by
  rw [← show _ = (coequalizer.π f g).hom.base from
      ι_comp_coequalizerComparison f g (SheafedSpace.forget C),
      ← PreservesCoequalizer.iso_hom]
  apply epi_comp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
this : Ideal.span (Set.range f) = ⊤
t : Finset ↑Γ(X, ↑V)
ht₁ : ↑t ⊆ Set.range f
ht₂ : Ideal.span ↑t = ⊤
⊢ ∀ (f : ↥t), P (X.affineBasicOpen ↑f)

Tactic:
rintro ⟨i, hi⟩

Goal state after:
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
this : Ideal.span (Set.range f) = ⊤
t : Finset ↑Γ(X, ↑V)
ht₁ : ↑t ⊆ Set.range f
ht₂ : Ideal.span ↑t = ⊤
i : ↑Γ(X, ↑V)
hi : i ∈ t
⊢ P (X.affineBasicOpen ↑⟨i, hi⟩)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
a :
  ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
      ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x))
ha :
  IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom x)) a)
⊢ IsUnit a

Tactic:
rcases TopCat.Presheaf.exists_germ_eq _ a with ⟨U, hU, s, rfl⟩

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
hU : (ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x ∈ U
s : ToType ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
ha :
  IsUnit
    ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom x))
      ((ConcreteCategory.hom
          ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.germ U
            ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x) hU))
        s))
⊢ IsUnit
    ((ConcreteCategory.hom
        ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.germ U
          ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x) hU))
      s)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
⊢ IsOpenMap ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))

Tactic:
intro s

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
⊢ IsOpen s → IsOpen[inst✝] (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasPullbacks C
X A B R S Y Z : C
f : R ⟶ X
g : S ⟶ X
inst✝ : MonObj (mk f)
⊢ Hom.left (LaxMonoidal.μ (pullback (𝟙 X)) (mk f) (mk f)) ≫
      pullback.fst (pullback.fst f f ≫ f) (𝟙 X) ≫ Hom.left MonObj.mul =
    Hom.left (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯) ≫ Hom.left MonObj.mul

Tactic:
simp only [← Category.assoc]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasPullbacks C
X A B R S Y Z : C
f : R ⟶ X
g : S ⟶ X
inst✝ : MonObj (mk f)
⊢ (Hom.left (LaxMonoidal.μ (pullback (𝟙 X)) (mk f) (mk f)) ≫ pullback.fst (pullback.fst f f ≫ f) (𝟙 X)) ≫
      Hom.left MonObj.mul =
    Hom.left (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯) ≫ Hom.left MonObj.mul
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : 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
x : 𝒰.I₀
i : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift 𝒰)).I₀
⊢ pullback.snd (𝒰.f x) ((ulift 𝒰).f i) ≫
      (ulift 𝒰).gluedCover.ι i ≫ Multicoequalizer.desc (ulift 𝒰).gluedCover.diagram Y (fun i ↦ f (idx 𝒰 i)) ⋯ =
    pullback.fst (𝒰.f x) ((ulift 𝒰).f i) ≫ f x

Tactic:
ulift_f,

Goal state after:
X : Scheme
𝒰 : 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
x : 𝒰.I₀
i : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift 𝒰)).I₀
⊢ pullback.snd (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫
      (ulift 𝒰).gluedCover.ι i ≫ Multicoequalizer.desc (ulift 𝒰).gluedCover.diagram Y (fun i ↦ f (idx 𝒰 i)) ⋯ =
    pullback.fst (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫ f x
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case h.inr
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥Y
⊢ ∃ y,
    (Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr)
          (Sum.elim (fun x ↦ Sum.inl PUnit.unit) (fun x ↦ Sum.inr PUnit.unit) (Sum.inr x)))
        y =
      (coprodMk X Y) (Sum.inr x)

Tactic:
· simp only [Sum.elim_inr, coprodMk_inr, exists_apply_eq_apply]

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

Goal state before:
pp: case op.op
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
X Y : WalkingMultispan (MultispanShape.prod D.J)
f' : op X ⟶ op Y
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map f' ≫
      D.ιInvAppπApp U (unop (op Y)) =
    D.ιInvAppπApp U (unop (op X)) ≫ (D.diagramOverOpen U).map f'

Tactic:
| op Y =>

Goal state after:
case op.op
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
X Y : WalkingMultispan (MultispanShape.prod D.J)
f' : op X ⟶ op Y
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map f' ≫
      D.ιInvAppπApp U (unop (op Y)) =
    D.ιInvAppπApp U (unop (op X)) ≫ (D.diagramOverOpen U).map f'