mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ A.unitGroup ≤ B.unitGroup → A ≤ B

pp: case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ A ≤ B → A.unitGroup ≤ B.unitGroup

Tactic:
· intro h x hx
    rw [← A.valuation_le_one_iff x, le_iff_lt_or_eq] at hx
    by_cases h_1 : x = 0; · simp only [h_1, zero_mem]
    by_cases h_2 : 1 + x = 0
    · simp only [← add_eq_zero_iff_neg_eq.1 h_2, neg_mem _ _ (one_mem _)]
    rcases hx with hx | hx
    · have := h (show Units.mk0 _ h_2 ∈ A.unitGroup from A.valuation.map_one_add_of_lt hx)
      simpa using
        B.add_mem _ _ (show 1 + x ∈ B from SetLike.coe_mem (B.unitGroupMulEquiv ⟨_, this⟩ : B))
          (B.neg_mem _ B.one_mem)
    · have := h (show Units.mk0 x h_1 ∈ A.unitGroup from hx)
      exact SetLike.coe_mem (B.unitGroupMulEquiv ⟨_, this⟩ : B)

Goal state after:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ A ≤ B → A.unitGroup ≤ B.unitGroup
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x : K
⊢ x⁻¹ = 0 ∨ x ∉ A ↔ x = 0 ∨ x ∉ A

Tactic:
inv_eq_zero

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : K
⊢ x = 0 ∨ x ∉ A ↔ x = 0 ∨ x ∉ A
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Subgroup G
a : G
h : ∀ (b : G), a • b ∈ ↑s ↔ b ∈ ↑s
⊢ a ∈ s

Tactic:
simpa only [smul_eq_mul, SetLike.mem_coe, mul_one] using (h 1).2 s.one_mem

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
⊢ seed.baseEmbedding ≤ f.extendFun hx

Tactic:
rw [extendFun]
  exact le_trans f.prop.baseEmbedding_le <| LinearPMap.left_le_sup _ _ _

Goal state after:
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb : x < ↑b
hn : {r | x < f r}.Nonempty
⊢ stdPart x = sInf {r | x < f r}

Tactic:
have hb : BddBelow {r | x < f r} := by
      refine ⟨a, fun r hr ↦ ?_⟩
      by_contra! hra
      exact (f.monotone' hra.le).not_gt (by simpa using ha.trans hr)

Goal state after:
case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb✝ : x < ↑b
hn : {r | x < f r}.Nonempty
hb : BddBelow {r | x < f r}
⊢ stdPart x = sInf {r | x < f r}
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P.nextCoeff ≠ 0
h₂ : P ≠ 0
h₃ : ¬P.eraseLead = 0
⊢ P.leadingCoeff :: P.eraseLead.coeffList = P.coeffList

Tactic:
simpa [natDegree_eraseLead_add_one h, coeffList, withBotSucc_degree_eq_natDegree_add_one h₂,
    withBotSucc_degree_eq_natDegree_add_one h₃, List.range_succ] using
    (Polynomial.eraseLead_coeff_of_ne · ·.ne)

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : q = 0
⊢ ↑(Fintype.card Fq) ^ p.natDegree < 0 ↔ p.degree < q.degree

pp: case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ ↑(Fintype.card Fq) ^ p.natDegree < ↑(Fintype.card Fq) ^ q.natDegree ↔ p.degree < q.degree

Tactic:
· simp only [hq, degree_zero, not_lt_bot, (pow_pos _).not_gt]

Goal state after:
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ ↑(Fintype.card Fq) ^ p.natDegree < ↑(Fintype.card Fq) ^ q.natDegree ↔ p.degree < q.degree
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
f : Partial seed
x : M
hx : x ∉ (↑f).domain
⊢ ∃ b, f < b

Tactic:
exact ⟨f.extend hx, f.lt_extend hx⟩

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
H : i ≤ p.natDegree
⊢ p.coeff i = 0

pp: case inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
H : p.natDegree < i
⊢ p.coeff i = 0

Tactic:
· have : p.coeff i = (p.homogenize n).coeff fun₀ | 0 => i | 1 => n - i := by
      simp [coeff_homogenize, Nat.add_sub_of_le (H.trans hn)]
    simp [this, h]

Goal state after:
case inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
H : p.natDegree < i
⊢ p.coeff i = 0
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
i : Fin 2
⊢ (p.toTupleMvPolynomial i).IsHomogeneous p.natDegree

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

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain R (a :: l₁)
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

Tactic:
by
    by_cases hab : R a b
    · simpa [destutter_cons_cons, hab] using! hl₁.tail.length_le_length_destutter (hl.cons _)
    · simpa [destutter_cons_cons, hab] using! hl₁.length_le_length_destutter (hl.cons_cons _)

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
r : R
p : R[X]
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Module R S
inst✝ : Pow S ℕ
x : S
⊢ (C r * p).smeval x = r • p.smeval x

Tactic:
induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [mul_add, smeval_add, ph, qh, smul_add]
  | monomial n b => simp only [C_mul_monomial, smeval_monomial, mul_smul]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : p.natDegree ∈ Finset.Icc 1 3
hnot : ∀ (x : K), ¬p.IsRoot x
⊢ Irreducible p

Tactic:
Finset.mem_Icc

Goal state after:
K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
⊢ Irreducible p
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
k : ℕ
hk : k + 1 ≤ q
x : ℕ
⊢ 1 ≤ q - (k - x)

Tactic:
exact (le_tsub_of_add_le_left hk).trans (tsub_le_tsub_left (tsub_le_self : _ ≤ k) _)

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

Goal state before:
pp: case inr.refine_1
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)
⊢ (∑ x ∈ Ico q (p.natDegree + 1), c x).natDegree ≤ p.natDegree - q

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]},
    map (algebraMap R A) p = (X - C r) ^ (q - 1) * p' →
      (aeval r) (sumIDeriv p) = (q - 1)! • eval r p' + q ! • (aeval r) (∑ x ∈ Ico q (p.natDegree + 1), c x)

Tactic:
· refine (natDegree_sum_le _ _).trans ?_
    rw [fold_max_le]
    exact ⟨Nat.zero_le _, fun i hi => (c_le i).trans (tsub_le_tsub_left (mem_Ico.mp hi).1 _)⟩

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]},
    map (algebraMap R A) p = (X - C r) ^ (q - 1) * p' →
      (aeval r) (sumIDeriv p) = (q - 1)! • eval r p' + q ! • (aeval r) (∑ x ∈ Ico q (p.natDegree + 1), c x)
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case succ.inr.inr.refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : P.eraseLead.signVariations + 1 ≤ ((X - C η) * P.eraseLead).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = 1
h₁ : P.nextCoeff ≠ 0
this : P.signVariations = P.eraseLead.signVariations + 0
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
grind [sign_eq_one_iff, signVariations_X_sub_C_mul_eraseLead_le]

Goal state after:
Module: Mathlib.Algebra.Quandle

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

Tactic:
by
  have h := @self_act_eq_iff_eq _ _ (op x) (op y)
  simpa using h

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: n : ℕ
a : ZMod n
⊢ Function.Involutive (dihedralAct n a)

Tactic:
intro b

Goal state after:
n : ℕ
a b : ZMod n
⊢ dihedralAct n a (dihedralAct n a b) = b
Module: Mathlib.Algebra.Ring.Action.Pointwise.Finset

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommMonoid M
inst✝² : DecidableEq M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
t : Finset M
r : R
hr : r ≠ 0
⊢ 0 ∈ ↑t ↔ 0 ∈ t

Tactic:
mem_coe

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommMonoid M
inst✝² : DecidableEq M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
t : Finset M
r : R
hr : r ≠ 0
⊢ 0 ∈ t ↔ 0 ∈ t
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
⊢ p.support = Finset.map toAdd.toEmbedding (SkewMonoidAlgebra.support p)

Tactic:
simp only [support]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p q : SkewPolynomial R
n : ℕ
⊢ (p - q).coeff n = p.coeff n - q.coeff n

Tactic:
simp_rw [sub_eq_add_neg, ← coeff_neg, SkewPolynomial.coeff_add]

Goal state after:
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)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
this : star y * y = 1
⊢ y ∈ unitary S

Tactic:
by simp [mem_iff, this, mul_comm y]

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

Goal state before:
pp: R : Type u_5
A : Type u_6
C : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalNonAssocSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
inst✝⁶ : StarRing A
inst✝⁵ : StarModule R A
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : StarAddMonoid C
inst✝¹ : StarModule R C
inst✝ : CoalgebraStruct R C
h : star (toConv comul) = toConv (↑(TensorProduct.comm R C C) ∘ₗ comul)
f g : WithConv (C →ₗ[R] A)
⊢ toConv
      ((star (toConv (mul' R A))).ofConv ∘ₗ
        (star (toConv (TensorProduct.map f.ofConv g.ofConv))).ofConv ∘ₗ (star (toConv comul)).ofConv) =
    toConv (mul' R A ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv ∘ₗ comul)

Tactic:
intrinsicStar_mul',

Goal state after:
R : Type u_5
A : Type u_6
C : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalNonAssocSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
inst✝⁶ : StarRing A
inst✝⁵ : StarModule R A
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : StarAddMonoid C
inst✝¹ : StarModule R C
inst✝ : CoalgebraStruct R C
h : star (toConv comul) = toConv (↑(TensorProduct.comm R C C) ∘ₗ comul)
f g : WithConv (C →ₗ[R] A)
⊢ toConv
      ((mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) ∘ₗ
        (star (toConv (TensorProduct.map f.ofConv g.ofConv))).ofConv ∘ₗ (star (toConv comul)).ofConv) =
    toConv (mul' R A ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv ∘ₗ comul)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ homOfSheafedSpaceHomOfIsIso f.hom ≫ homOfSheafedSpaceHomOfIsIso f.inv = 𝟙 X

Tactic:
ext : 1
    dsimp
    rw [← InducedCategory.comp_hom, f.hom_inv_id, SheafedSpace.id_hom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (((sheafedSpaceMap (f ≫ g)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj T).presheaf).app (op U✝)))
      x✝ =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c.app (op U✝))) x✝

Tactic:
NatTrans.comp_app,

Goal state after:
case h
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        ((sheafedSpaceMap (f ≫ g)).hom.c.app (op U✝) ≫
          (Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj T).presheaf).app (op U✝)))
      x✝ =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c.app (op U✝))) x✝
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
x : ↥X
hx : IsClosed {x}
⊢ IsMin x

Tactic:
intro b

Goal state after:
X : Scheme
x : ↥X
hx : IsClosed {x}
b : ↥X
⊢ b ≤ x → x ≤ b
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
x : ↥X
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f + (ConcreteCategory.hom (X.presheaf.germ U x hxU)) g)
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f) ∨
    IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) g)

Tactic:
exact IsLocalRing.isUnit_or_isUnit_of_isUnit_add hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case refine_1
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ x ∉ X.basicOpen 0

pp: case refine_2
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ ∀ (x_1 y : ↑Γ(X, U)),
    x_1 ∈ Submodule.span (↑Γ(X, U)) s →
      y ∈ Submodule.span (↑Γ(X, U)) s → x ∉ X.basicOpen x_1 → x ∉ X.basicOpen y → x ∉ X.basicOpen (x_1 + y)

pp: case refine_3
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ ∀ (a x_1 : ↑Γ(X, U)), x_1 ∈ Submodule.span (↑Γ(X, U)) s → x ∉ X.basicOpen x_1 → x ∉ X.basicOpen (a • x_1)

Tactic:
· simp only [Scheme.basicOpen_zero]; exact not_false

Goal state after:
case refine_2
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ ∀ (x_1 y : ↑Γ(X, U)),
    x_1 ∈ Submodule.span (↑Γ(X, U)) s →
      y ∈ Submodule.span (↑Γ(X, U)) s → x ∉ X.basicOpen x_1 → x ∉ X.basicOpen y → x ∉ X.basicOpen (x_1 + y)

case refine_3
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ ∀ (a x_1 : ↑Γ(X, U)), x_1 ∈ Submodule.span (↑Γ(X, U)) s → x ∉ X.basicOpen x_1 → x ∉ X.basicOpen (a • x_1)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : AlgebraicGeometry.IsOpenImmersion f
⊢ toScheme Y f.toPshHom = X

Tactic:
by
  apply scheme_eq_of_locallyRingedSpace_eq
  exact locallyRingedSpace_toLocallyRingedSpace f.toLRSHom

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✝ 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:
use pullbackConeOfLeftLift f g s

Goal state after:
case property
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
⊢ pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst = s.fst ∧
    pullbackConeOfLeftLift f g s ≫ (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 = pullbackConeOfLeftLift f g s
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) g
⊢ ∀ (i : ↥X),
    (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op)) f =
      (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op)) g

Tactic:
· intro x
    replace h := h (𝒰.idx x)
    rw [← IsOpenImmersion.map_ΓIso_inv] at h
    exact (IsOpenImmersion.ΓIso (𝒰.f (𝒰.idx x)) U).commRingCatIsoToRingEquiv.symm.injective h

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
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
⊢ basicOpen (g i * g j) ≤ U

Tactic:
· exact ((PrimeSpectrum.basicOpen_mul (g i) (g j)).trans_le inf_le_right).trans (igU _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ IsOpen (X.toΓSpecFun ⁻¹' (fun r ↦ ↑(basicOpen r)) r)

Tactic:
X.toΓSpec_preimage_basicOpen_eq r

Goal state after:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ IsOpen ↑(X.toRingedSpace.basicOpen r)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ toStalk (↑(unop (op (Γ.obj (op X))))) ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x) ≫
      PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x =
    X.presheaf.Γgerm x

Tactic:
PresheafedSpace.Hom.stalkMap,

Goal state after:
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ toStalk (↑(unop (op (Γ.obj (op X))))) ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x) ≫
      (stalkFunctor CommRingCat ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x)).map
          X.toΓSpecSheafedSpace.hom.c ≫
        stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x =
    X.presheaf.Γgerm x
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
⊢ Opens.IsBasis X.affineOpens

Tactic:
rw [Opens.isBasis_iff_nbhd]

Goal state after:
X : Scheme
⊢ ∀ {U : TopologicalSpace.Opens ↥X} {x : ↥X}, x ∈ U → ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_2.refine_1
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ IsPullback (g ∣_ UX) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯ ≫ (f ⁻¹ᵁ US).ι) (resLE iX US UX hUSX ≫ US.ι) f

Tactic:
simpa using (isPullback_morphismRestrict g UX).paste_vert H

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ (equalizer.ι lhs rhs ≫ pullback.fst s v) ≫ f = (equalizer.ι lhs rhs ≫ pullback.fst s v) ≫ g

Tactic:
by
          simp [hl, hr, equalizer.condition_assoc lhs rhs]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
⊢ Γ.rightOp.map (identityToΓSpec.app X) ≫ (NatIso.op SpecΓIdentity).inv.app (Γ.rightOp.obj X) = 𝟙 (Γ.rightOp.obj X)

Tactic:
simp only [Functor.id_obj, Γ_obj, Functor.rightOp_map, Γ_map,
      Quiver.Hom.unop_op, NatIso.op_inv, NatTrans.op_app, SpecΓIdentity_inv_app]
    exact congr_arg Quiver.Hom.op (left_triangle X)

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasEqualizers C
inst✝² : HasPullbacks C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage C
𝒰 : J.ZeroHypercover S
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : (MorphismProperty.isomorphisms C).IsLocalAtTarget J
H :
  ∀ (i : 𝒰.I₀),
    pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯ = pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯
⊢ f = g

Tactic:
by
  suffices IsIso (equalizer.ι f g) from Limits.eq_of_epi_equalizer
  change MorphismProperty.isomorphisms C _
  rw [(MorphismProperty.isomorphisms C).iff_of_zeroHypercover_target (𝒰.pullback₁ s)]
  intro i
  have : pullback.snd (equalizer.ι f g) (pullback.fst s (𝒰.f i)) =
      (equalizerPullbackMapIso hf hg _).inv ≫ equalizer.ι _ _ := by
    ext <;> simp [pullback.condition]
  simpa [this] using equalizer.ι_of_eq (H i)

Goal state after: