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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → R[X]
⊢ span (Set.range (Function.update v j (v j - (v j /ₘ v i) • v i))) = span (Set.range v)

Tactic:
Ideal.span,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → R[X]
⊢ Submodule.span R[X] (Set.range (Function.update v j (v j - (v j /ₘ v i) • v i))) = span (Set.range v)
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → R[X]
⊢ Submodule.span R[X] (Set.range (Function.update v j (v j - (v j /ₘ v i) • v i))) = span (Set.range v)

Tactic:
Ideal.span,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → R[X]
⊢ Submodule.span R[X] (Set.range (Function.update v j (v j - (v j /ₘ v i) • v i))) = Submodule.span R[X] (Set.range v)
Module: Mathlib.Data.List.Destutter

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

Tactic:
by
    by_cases hbc : R b c
    case pos =>
      have hac : ¬Rᶜ a c := (mt (_root_.trans hba)) (not_not.2 hbc)
      simp_rw [destutter', if_pos (not_not.1 hac), if_pos hbc, length_cons, le_refl]
    case neg =>
      simp only [destutter', if_neg hbc]
      by_cases hac : R a c
      case pos =>
        simp only [if_pos hac, length_cons]
        exact Nat.le_succ_of_le (length_destutter'_cotrans_ge hbc)
      case neg =>
        simp only [if_neg hac]
        exact length_destutter'_cotrans_ge hba

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
p : R[X]
q : ℕ
hq : 0 < q
⊢ ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : R) {p' : R[X]},
        p = (X - C r) ^ (q - 1) * p' → eval r (sumIDeriv p) = (q - 1)! • eval r p' + q ! • eval r gp

Tactic:
simpa using aeval_sumIDeriv_of_pos R p hq Function.injective_id

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
u : { u // u * u = a • 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ (z.re • 1 + z.im • ↑u) * (w.re • 1 + w.im • ↑u) =
    (z.re * w.re) • 1 + (z.re * w.im) • ↑u + (z.im * w.re) • ↑u + (z.im * w.im) • (↑u * ↑u)

Tactic:
simp only [mul_add, mul_one, add_mul, one_mul, ← add_assoc, smul_mul_smul]

Goal state after:
K : Type u_1
R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
u : { u // u * u = a • 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ (z.re * w.re) • 1 + (z.im * w.re) • ↑u + (z.re * w.im) • ↑u + (z.im * w.im) • (↑u * ↑u) =
    (z.re * w.re) • 1 + (z.re * w.im) • ↑u + (z.im * w.re) • ↑u + (z.im * w.im) • (↑u * ↑u)
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
u : { u // u * u = a • 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ (z + w).re • 1 + (z + w).im • ↑u = z.re • 1 + z.im • ↑u + (w.re • 1 + w.im • ↑u)

Tactic:
simp only [re_add, im_add, add_smul, ← add_assoc]

Goal state after:
K : Type u_1
R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
u : { u // u * u = a • 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ z.re • 1 + w.re • 1 + z.im • ↑u + w.im • ↑u = z.re • 1 + z.im • ↑u + w.re • 1 + w.im • ↑u
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
⊢ IsUnit (norm x) → IsUnit x

Tactic:
· simp only [isUnit_iff_exists]
    rintro ⟨r, hr, hr'⟩
    rw [← C_inj (R := R) (a := a) (b := b), C_mul, C_eq_algebraMap, algebraMap_norm_eq_mul_star,
      mul_assoc, map_one] at hr
    refine ⟨_, hr, ?_⟩
    rw [mul_comm, hr]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_2
inst✝ : Rack R
x y z : R
⊢ x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z

Tactic:
rw [self_distrib]

Goal state after:
R : Type u_2
inst✝ : Rack R
x y z : R
⊢ (x ◃ y) ◃ x ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
Module: Mathlib.Algebra.Ring.Identities

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x₁ x₂ y₁ y₂ : R
⊢ (x₁ ^ 2 + x₂ ^ 2) * (y₁ ^ 2 + y₂ ^ 2) = (x₁ * y₁ - x₂ * y₂) ^ 2 + (x₁ * y₂ + x₂ * y₁) ^ 2

Tactic:
by
  ring

Goal state after:
Module: Mathlib.Algebra.Ring.Identities

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x₁ x₂ y₁ y₂ n : R
⊢ (x₁ ^ 2 + n * x₂ ^ 2) * (y₁ ^ 2 + n * y₂ ^ 2) = (x₁ * y₁ - n * x₂ * y₂) ^ 2 + n * (x₁ * y₂ + x₂ * y₁) ^ 2

Tactic:
by
  ring

Goal state after:
Module: Mathlib.Algebra.Ring.Identities

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
⊢ a ^ 4 + 4 * b ^ 4 = ((a - b) ^ 2 + b ^ 2) * ((a + b) ^ 2 + b ^ 2)

Tactic:
by
  ring

Goal state after:
Module: Mathlib.Algebra.Ring.Identities

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
⊢ a ^ 4 + 4 * b ^ 4 = (a ^ 2 - 2 * a * b + 2 * b ^ 2) * (a ^ 2 + 2 * a * b + 2 * b ^ 2)

Tactic:
by
  ring

Goal state after:
Module: Mathlib.Algebra.Ring.Identities

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x₁ x₂ x₃ x₄ y₁ y₂ y₃ y₄ : R
⊢ (x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 + x₄ ^ 2) * (y₁ ^ 2 + y₂ ^ 2 + y₃ ^ 2 + y₄ ^ 2) =
    (x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄) ^ 2 + (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃) ^ 2 +
        (x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂) ^ 2 +
      (x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁) ^ 2

Tactic:
by
  ring

Goal state after:
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s : R
h : IsSumNonzeroSq s
⊢ IsSumSq s

Tactic:
by
  induction h <;> aesop

Goal state after:
Module: Mathlib.Algebra.Ring.Identities

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ y₁ y₂ y₃ y₄ y₅ y₆ y₇ y₈ : R
⊢ (x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 + x₄ ^ 2 + x₅ ^ 2 + x₆ ^ 2 + x₇ ^ 2 + x₈ ^ 2) *
      (y₁ ^ 2 + y₂ ^ 2 + y₃ ^ 2 + y₄ ^ 2 + y₅ ^ 2 + y₆ ^ 2 + y₇ ^ 2 + y₈ ^ 2) =
    (x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄ - x₅ * y₅ - x₆ * y₆ - x₇ * y₇ - x₈ * y₈) ^ 2 +
                  (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃ + x₅ * y₆ - x₆ * y₅ - x₇ * y₈ + x₈ * y₇) ^ 2 +
                (x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂ + x₅ * y₇ + x₆ * y₈ - x₇ * y₅ - x₈ * y₆) ^ 2 +
              (x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁ + x₅ * y₈ - x₆ * y₇ + x₇ * y₆ - x₈ * y₅) ^ 2 +
            (x₁ * y₅ - x₂ * y₆ - x₃ * y₇ - x₄ * y₈ + x₅ * y₁ + x₆ * y₂ + x₇ * y₃ + x₈ * y₄) ^ 2 +
          (x₁ * y₆ + x₂ * y₅ - x₃ * y₈ + x₄ * y₇ - x₅ * y₂ + x₆ * y₁ - x₇ * y₄ + x₈ * y₃) ^ 2 +
        (x₁ * y₇ + x₂ * y₈ + x₃ * y₅ - x₄ * y₆ - x₅ * y₃ + x₆ * y₄ + x₇ * y₁ - x₈ * y₂) ^ 2 +
      (x₁ * y₈ - x₂ * y₇ + x₃ * y₆ + x₄ * y₅ - x₅ * y₄ - x₆ * y₃ + x₇ * y₂ + x₈ * y₁) ^ 2

Tactic:
by
  ring

Goal state after:
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f g : CentroidHom α
h : (fun f ↦ (↑f.toAddMonoidHom).toFun) f = (fun f ↦ (↑f.toAddMonoidHom).toFun) g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
g : CentroidHom α
toAddMonoidHom✝ : α →+ α
map_mul_left'✝ : ∀ (a b : α), (↑toAddMonoidHom✝).toFun (a * b) = a * (↑toAddMonoidHom✝).toFun b
map_mul_right'✝ : ∀ (a b : α), (↑toAddMonoidHom✝).toFun (a * b) = (↑toAddMonoidHom✝).toFun a * b
h :
  (fun f ↦ (↑f.toAddMonoidHom).toFun)
      { toAddMonoidHom := toAddMonoidHom✝, map_mul_left' := map_mul_left'✝, map_mul_right' := map_mul_right'✝ } =
    (fun f ↦ (↑f.toAddMonoidHom).toFun) g
⊢ { toAddMonoidHom := toAddMonoidHom✝, map_mul_left' := map_mul_left'✝, map_mul_right' := map_mul_right'✝ } = g
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✝¹⁶ : NonUnitalNonAssocSemiring α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
z : ↥(NonUnitalSubsemiring.center α)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
Subsemiring.mem_center_iff

Goal state after:
F : Type u_1
M : Type u_2
N : Type u_3
R✝ : Type u_4
α : Type u_5
inst✝¹⁶ : NonUnitalNonAssocSemiring α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
z : ↥(NonUnitalSubsemiring.center α)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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✝¹⁶ : NonUnitalNonAssocSemiring α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
f g : ↥(Subsemiring.center (CentroidHom α))
h : (fun f ↦ (↑(↑f).toAddMonoidHom).toFun) f = (fun f ↦ (↑(↑f).toAddMonoidHom).toFun) g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
F : Type u_1
M : Type u_2
N : Type u_3
R✝ : Type u_4
α : Type u_5
inst✝¹⁶ : NonUnitalNonAssocSemiring α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
g : ↥(Subsemiring.center (CentroidHom α))
val✝ : CentroidHom α
property✝ : val✝ ∈ Subsemiring.center (CentroidHom α)
h : (fun f ↦ (↑(↑f).toAddMonoidHom).toFun) ⟨val✝, property✝⟩ = (fun f ↦ (↑(↑f).toAddMonoidHom).toFun) g
⊢ ⟨val✝, property✝⟩ = g
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mk
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
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ { toQuot := Quot.mk (Rel r) a✝ } + 0 = { toQuot := Quot.mk (Rel r) a✝ }

Tactic:
simp only [add_quot, ← zero_quot, add_zero]

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 : G
a : k
⊢ single g a * 1 = single g a

Tactic:
rw [one_def, mul_def, sum_single_index, sum_single_index] <;> simp

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

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
h : f.toHom = g.toHom
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
X Y : LocallyRingedSpace
g : X ⟶ Y
toHom✝ : X.Hom Y.toPresheafedSpace
prop✝ : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom✝.stalkMap x))
h : { toHom := toHom✝, prop := prop✝ }.toHom = g.toHom
⊢ { toHom := toHom✝, prop := prop✝ } = g
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X✝ X : LocallyRingedSpace
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (𝟙 X.toPresheafedSpace) x))

Tactic:
rw [PresheafedSpace.stalkMap.id]

Goal state after:
X✝ X : LocallyRingedSpace
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (𝟙 (X.presheaf.stalk x)))
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)

Tactic:
exact RingHom.isUnit_map _ hf

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
U : TopologicalSpace.Opens ↑(Spec.topObj (CommRingCat.of ↑R))
hp : p ∈ U
s :
  ToType
    (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op U))
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          U p hp))
      s =
    y
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1

Tactic:
replace e :=
    ((Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).germ_res_apply
      (homOfLE hrU) p hpr _).trans e

Goal state after:
R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
U : TopologicalSpace.Opens ↑(Spec.topObj (CommRingCat.of ↑R))
hp : p ∈ U
s :
  ToType
    (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op U))
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      ((ConcreteCategory.hom
          (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).obj).map
            (homOfLE hrU).op))
        s) =
    y
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f g : X ⟶ Y
h_base : f.base = g.base
h_app : ∀ (U : Y.Opens), app f U ≫ X.presheaf.map (eqToHom ⋯).op = app g U
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
X Y : Scheme
g : X ⟶ Y
toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝ }.base = g.base
h_app : ∀ (U : Y.Opens), { toLRSHom' := toLRSHom'✝ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = app g U
⊢ { toLRSHom' := toLRSHom'✝ } = g
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f g : X ⟶ Y
h : toLRSHom f = toLRSHom g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
X Y : Scheme
g : X ⟶ Y
toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h : { toLRSHom' := toLRSHom'✝ }.toLRSHom = toLRSHom g
⊢ { toLRSHom' := toLRSHom'✝ } = g
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 V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map i ≫ invApp f (unop V) = invApp f (unop U) ≫ Y.presheaf.map ((opensFunctor f).op.map i)

Tactic:
simp only [invApp, ← Category.assoc]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ (X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯)) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop V)))) =
    (X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
      Y.presheaf.map ((opensFunctor f).op.map i)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case a
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
U : (Opens ↑↑X)ᵒᵖ
⊢ (↑(TopCat.Hom.frameHom g.base)).toFunctor.obj
      { carrier := ⇑(ConcreteCategory.hom f.base) '' ↑(unop U), is_open' := ⋯ } ≤
    {
      carrier :=
        ⇑(ConcreteCategory.hom (pullback.snd f.base g.base)) ''
          ↑((↑(TopCat.Hom.frameHom (pullback.fst f.base g.base))).toFunctor.obj (unop U)),
      is_open' := ⋯ }

Tactic:
rintro _ ⟨_, h₁, h₂⟩

Goal state after:
case a
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
U : (Opens ↑↑X)ᵒᵖ
x✝ : ↑↑Y
w✝ : ↑↑X
h₁ : w✝ ∈ ↑(unop U)
h₂ : (ConcreteCategory.hom f.base) w✝ = (ConcreteCategory.hom g.base) x✝
⊢ x✝ ∈
    {
      carrier :=
        ⇑(ConcreteCategory.hom (pullback.snd f.base g.base)) ''
          ↑((↑(TopCat.Hom.frameHom (pullback.fst f.base g.base))).toFunctor.obj (unop U)),
      is_open' := ⋯ }
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case inl
X : Scheme
U : X.Opens
I : Ideal ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ I, x ∉ X.basicOpen f
f : ↑Γ(X, U)
hx : x ∈ X.basicOpen f
hn : f ^ 0 ∈ I
⊢ False

pp: case inr
X : Scheme
U : X.Opens
I : Ideal ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ I, x ∉ X.basicOpen f
f : ↑Γ(X, U)
n : ℕ
hn : f ^ n ∈ I
hx : x ∈ X.basicOpen f
hn' : n > 0
⊢ False

Tactic:
· exact H f (by simpa using I.mul_mem_left f hn) hx

Goal state after:
case inr
X : Scheme
U : X.Opens
I : Ideal ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ I, x ∉ X.basicOpen f
f : ↑Γ(X, U)
n : ℕ
hn : f ^ n ∈ I
hx : x ∈ X.basicOpen f
hn' : n > 0
⊢ False
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
U : (Opens ↑↑Z)ᵒᵖ
⊢ ((pullbackConeOfLeftFst f g ≫ f).c ≫ Functor.whiskerRight (eqToHom ⋯) (Y.restrict ⋯).presheaf).app U =
    (Y.ofRestrict ⋯ ≫ g).c.app U

Tactic:
· induction U
    simp only [(NatTrans.comp_app), comp_c_app, unop_op, Functor.whiskerRight_app,
      pullbackConeOfLeftFst, app_invApp_assoc, eqToHom_app, Category.assoc,
      NatTrans.naturality_assoc, restrict_carrier, comp_base, ofRestrict_base, restrict_presheaf,
      Functor.comp_obj, Functor.op_obj, Opens.map_comp_obj, TopCat.Presheaf.pushforward_obj_obj,
      Opens.carrier_eq_coe, homOfLE_leOfHom, TopCat.Presheaf.pushforward_obj_map, Functor.comp_map,
      Functor.op_map, eqToHom_unop, ofRestrict_c_app, Functor.id_obj]
    rw [← Y.presheaf.map_comp, ← Y.presheaf.map_comp]
    congr 1

Goal state after:
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
⊢ HasLimit (cospan f g ⋙ forget)

Tactic:
by
  have : HasLimit (cospan ((cospan f g ⋙ forget).map Hom.inl)
      ((cospan f g ⋙ forget).map Hom.inr)) := by
    change HasLimit (cospan ((forget).map f) ((forget).map g))
    infer_instance
  apply hasLimit_of_iso (diagramIsoCospan _).symm

Goal state after:
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: X✝ Y✝ Z✝ : TopCommRingCat
f : { f // Continuous ⇑f }
g : { f // Continuous ⇑f }
⊢ Continuous ⇑((↑g).comp ↑f)

Tactic:
cases f

Goal state after:
case mk
X✝ Y✝ Z✝ : TopCommRingCat
g : { f // Continuous ⇑f }
val✝ : X✝.α →+* Y✝.α
property✝ : Continuous ⇑val✝
⊢ Continuous ⇑((↑g).comp ↑⟨val✝, property✝⟩)
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 : ℕ
hn : f ^ (n + 1) ∈ Ideal.span (Set.range b)
⊢ ∃ a, (toBasicOpenₗ R M f) a = s

Tactic:
Ideal.span,

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 : ℕ
hn : f ^ (n + 1) ∈ Submodule.span R (Set.range b)
⊢ ∃ a, (toBasicOpenₗ R M f) a = s
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
⊢ Scheme.Hom.app hU.fromSpec V =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op

Tactic:
by
  have : U.ι ⁻¹ᵁ V = ⊤ := eq_top_iff.mpr fun x _ ↦ h x.2
  rw [IsAffineOpen.fromSpec, Scheme.Hom.comp_app, Scheme.Opens.ι_app, Scheme.Hom.app_eq _ this,
    ← Scheme.Hom.appTop, IsAffineOpen.isoSpec_inv_appTop]
  simp only [Scheme.Opens.toScheme_presheaf_map, Scheme.Opens.topIso_hom,
    Category.assoc, ← X.presheaf.map_comp_assoc]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R : CommRingCat
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ

Tactic:
have := ΓSpec.adjunction.right_triangle_components (op R)

Goal state after:
R : CommRingCat
this :
  ΓSpec.adjunction.unit.app (Scheme.Spec.obj (op R)) ≫ Scheme.Spec.map (ΓSpec.adjunction.counit.app (op R)) =
    𝟙 (Scheme.Spec.obj (op R))
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R : CommRingCat
⊢ (Spec R).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)

Tactic:
by
  rw [← SpecMap_ΓSpecIso_hom, ← Spec.map_comp, Iso.inv_hom_id, Spec.map_id]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
⊢ Scheme.Hom.app f (Y.basicOpen r) =
    CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
          (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
          (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
      X.presheaf.map (eqToHom ⋯).op

Tactic:
have := hU.isLocalization_basicOpen r
  have := h.isLocalization_basicOpen (f.app U r)
  ext : 1
  apply IsLocalization.ringHom_ext (.powers r)
  rw [IsLocalization.Away.map, CommRingCat.hom_comp, RingHom.comp_assoc, CommRingCat.hom_ofHom,
    IsLocalization.map_comp, RingHom.algebraMap_toAlgebra,
    RingHom.algebraMap_toAlgebra, ← RingHom.comp_assoc, ← CommRingCat.hom_comp,
    ← CommRingCat.hom_comp, ← X.presheaf.map_comp]
  simp

Goal state after: