mathlib-initiative/mathlib-tactics huggingface dataset:
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
hPn0 : P ≠ 0
⊢ (X - C η).natDegree + P.natDegree = P.natDegree + 1

Tactic:
natDegree_X_sub_C,

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
hPn0 : P ≠ 0
⊢ 1 + P.natDegree = P.natDegree + 1
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
⊢ ((X - C η) * P).eraseLead.signVariations = ((X - C η) * P.eraseLead).signVariations

Tactic:
have hndxP : natDegree ((X - C η) * P) = P.natDegree + 1 := by
    have hPn0 : P ≠ 0 :=
      leadingCoeff_ne_zero.mp hP₀.ne'
    rw [natDegree_mul (X_sub_C_ne_zero η) hPn0, natDegree_X_sub_C, add_comm]

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
⊢ ((X - C η) * P).eraseLead.signVariations = ((X - C η) * P.eraseLead).signVariations
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
hePn0 : P.eraseLead ≠ 0
⊢ (X - C η).natDegree + P.eraseLead.natDegree = P.natDegree

Tactic:
natDegree_X_sub_C,

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
hePn0 : P.eraseLead ≠ 0
⊢ 1 + P.eraseLead.natDegree = P.natDegree
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 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
⊢ (X - C η).natDegree + P.natDegree = P.natDegree + 1

Tactic:
natDegree_X_sub_C,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
⊢ 1 + P.natDegree = P.natDegree + 1
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 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
⊢ ((X - C η) * P.eraseLead).signVariations ≤ ((X - C η) * P).signVariations

Tactic:
simp +decide only [hcs, hecs, h, h₂, signVariations, List.destutter, List.map_cons, sign_pos,
    List.filter_cons_of_pos, tsub_le_iff_right,
    Nat.sub_add_cancel (List.length_pos_of_ne_nil (List.destutter'_ne_nil _ _))]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (SignType.sign c₀ :: List.map (⇑SignType.sign) cs))).length
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
d : ℕ
ih : ∀ m < d, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
⊢ (X - C η).natDegree + P.natDegree = P.natDegree + 1

Tactic:
natDegree_X_sub_C,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
d : ℕ
ih : ∀ m < d, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
⊢ 1 + P.natDegree = P.natDegree + 1
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F (q.j * q.i) = c₂ • F q.j - F q.k

Tactic:
q.j_mul_i,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F (c₂ • q.j - q.k) = c₂ • F q.j - F q.k
Module: Mathlib.Algebra.Ring.Semireal.Defs

Goal state before:
pp: R : Type u_1
inst✝² : AddGroup R
inst✝¹ : One R
inst✝ : Mul R
h : ¬IsSumSq (-1)
⊢ ∀ {s : R}, IsSumSq s → 1 + s ≠ 0

Tactic:
aesop (add simp add_eq_zero_iff_neg_eq)

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

Goal state before:
pp: case mk.mk
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
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
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)
      { toAddMonoidHom := toAddMonoidHom✝, map_mul_left' := map_mul_left'✝, map_mul_right' := map_mul_right'✝ }
x : α
⊢ toAddMonoidHom✝¹ x = toAddMonoidHom✝ x

Tactic:
exact congrFun h x

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

Goal state before:
pp: case mk.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» α α
val✝¹ : CentroidHom α
property✝¹ : val✝¹ ∈ Subsemiring.center (CentroidHom α)
val✝ : CentroidHom α
property✝ : val✝ ∈ Subsemiring.center (CentroidHom α)
h :
  (fun f ↦ (↑(↑f).toAddMonoidHom).toFun) ⟨val✝¹, property✝¹⟩ = (fun f ↦ (↑(↑f).toAddMonoidHom).toFun) ⟨val✝, property✝⟩
x : α
⊢ val✝¹ x = val✝ x

Tactic:
exact congrFun h x

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

Goal state before:
pp: case mpr.comm
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ ∀ (a_1 : α), Commute a a_1

pp: case left_assoc
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ ∀ (b c : α), a * (b * c) = a * b * c

pp: case mpr.right_assoc
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ ∀ (a_1 b : α), a_1 * b * a = a_1 * (b * a)

Tactic:
case comm => exact (congr($hc.symm ·))

Goal state after:
case left_assoc
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ ∀ (b c : α), a * (b * c) = a * b * c

case mpr.right_assoc
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ ∀ (a_1 b : α), a_1 * b * a = a_1 * (b * a)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
f : SkewMonoidAlgebra k G
| ((lift k G A) ((↑F).comp (of k G))) f

Tactic:
simp [lift_apply]

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
f : SkewMonoidAlgebra k G
| f.sum fun a b ↦ b • F (single a 1)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Support

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : DecidableEq G
r : k
x : G
lx : IsLeftRegular x
hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0
⊢ (single x r * f).support = image (fun x_1 ↦ x * x_1) f.support

Tactic:
refine subset_antisymm (support_single_mul_subset f _ _) fun y hy ↦ ?_
  obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ x * a = y := by
    simpa only [Finset.mem_image, exists_prop] using hy
  simp [coeff_mul, mem_support_iff.mp yf, hrx, mem_support_iff, sum_single_index, Ne,
    zero_mul, ite_self, sum_zero, lx.eq_iff]

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

Goal state before:
pp: case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ ¬(a ≠ a ∧ a ∈ f.support)

Tactic:
exact fun H ↦ H.1 rfl

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁸ : Semiring R
S : Type uS
inst✝⁷ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁶ : Semiring A
inst✝⁵ : Algebra S A
r : R → R → Prop
inst✝⁴ : CommSemiring T
inst✝³ : SMul S T
inst✝² : Algebra S R
inst✝¹ : Algebra T R
inst✝ : IsScalarTower S T R
s : S
t : T
x✝ : RingQuot r
a : Quot (Rel r)
a' : R
⊢ (s • t) • { toQuot := Quot.mk (Rel r) a' } = s • t • { toQuot := Quot.mk (Rel r) a' }

Tactic:
simp only [RingQuot.smul_quot, smul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
a : R
⊢ (⇑φ)^[n] a = ofAdd n • a

Tactic:
by
  induction n with
  | zero => simp
  | succ n hn =>
    simp_all [MulSemiringAction.toRingHom_apply, Function.iterate_succ', -Function.iterate_succ,
      ← mul_smul, mul_comm]

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

Goal state before:
pp: R : Type u_1
m n : ℕ
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (↑m).coeff n = ↑(if n = 0 then m else 0)

Tactic:
simp [← C_eq_natCast, coeff_C]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : Mul S
inst✝ : StarMul S
this : Star R := e.star
⊢ StarMul R

Tactic:
let := e.mul

Goal state after:
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : Mul S
inst✝ : StarMul S
this✝ : Star R := e.star
this : Mul R := e.mul
⊢ StarMul R
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 α
g g' : G
f : SkewMonoidAlgebra M α
⊢ (g * g') • f = g • g' • f

Tactic:
comapSMul_def,

Goal state after:
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 α
g g' : G
f : SkewMonoidAlgebra M α
⊢ (mapDomain fun x ↦ (g * g') • x) f = g • g' • f
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 α
g g' : G
f : SkewMonoidAlgebra M α
⊢ (mapDomain fun x ↦ (g * g') • x) f = g • g' • f

Tactic:
comapSMul_def,

Goal state after:
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 α
g g' : G
f : SkewMonoidAlgebra M α
⊢ (mapDomain fun x ↦ (g * g') • x) f = (mapDomain fun x ↦ g • x) (g' • f)
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 α
g g' : G
f : SkewMonoidAlgebra M α
⊢ (mapDomain fun x ↦ (g * g') • x) f = (mapDomain fun x ↦ g • x) (g' • f)

Tactic:
comapSMul_def,

Goal state after:
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 α
g g' : G
f : SkewMonoidAlgebra M α
⊢ (mapDomain fun x ↦ (g * g') • x) f = (mapDomain fun x ↦ g • x) ((mapDomain fun x ↦ g' • x) f)
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 α
f : SkewMonoidAlgebra M α
⊢ 1 • f = f

Tactic:
comapSMul_def,

Goal state after:
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 α
f : SkewMonoidAlgebra M α
⊢ (mapDomain fun x ↦ 1 • x) f = f
Module: Mathlib.Algebra.TrivSqZeroExt.Ideal

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
x : TrivSqZeroExt R M
hx : x = inr x.snd
y : TrivSqZeroExt R M
hy : y = inr y.snd
⊢ inr x.snd * y ∈ ⊥

Tactic:
hy,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
x : TrivSqZeroExt R M
hx : x = inr x.snd
y : TrivSqZeroExt R M
hy : y = inr y.snd
⊢ inr x.snd * inr y.snd ∈ ⊥
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ x ∈ iSup V

Tactic:
simp only [Opens.mem_iSup]

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ ∃ i, x ∈ V i
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T✝ : ↑X → Type u_1
T : ↑X → Type u_2
P : PrelocalPredicate T
U : Opens ↑X
f : (x : ↥U) → T ↑x
x : ↥U
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
p : ∃ V_1, ∃ (_ : ↑⟨↑x, m⟩ ∈ V_1), ∃ i_1, P.pred fun x ↦ (fun x ↦ f (i x)) (i_1 x)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)

Tactic:
rcases p with ⟨V', m', i', p'⟩

Goal state after:
X : TopCat
T✝ : ↑X → Type u_1
T : ↑X → Type u_2
P : PrelocalPredicate T
U : Opens ↑X
f : (x : ↥U) → T ↑x
x : ↥U
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
V' : Opens ↑X
m' : ↑⟨↑x, m⟩ ∈ V'
i' : V' ⟶ V
p' : P.pred fun x ↦ (fun x ↦ f (i x)) (i' x)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ toStalk (↑R) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p) ≫
      PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p =
    f ≫
      CommRingCat.ofHom (algebraMap (↑S) ((structureSheafInType ↑S ↑S).obj.obj (op ⊤))) ≫
        (structurePresheafInCommRingCat ↑S).germ ⊤ p trivial

Tactic:
← algebraMap_germ ⊤ (PrimeSpectrum.comap f.hom p) trivial,

Goal state after:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op ⊤))) ≫
        (structurePresheafInCommRingCat ↑R).germ ⊤ (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p) trivial) ≫
      PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p =
    f ≫
      CommRingCat.ofHom (algebraMap (↑S) ((structureSheafInType ↑S ↑S).obj.obj (op ⊤))) ≫
        (structurePresheafInCommRingCat ↑S).germ ⊤ p trivial
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
x✝ : ↑R
x' : ↥(unop (op ⊤))
⊢ ↑((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op)) x✝) x' =
    ↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S)) x✝) x'

Tactic:
comap_apply

Goal state after:
R S : CommRingCat
f : R ⟶ S
x✝ : ↑R
x' : ↥(unop (op ⊤))
⊢ (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop) ↑x').asIdeal (↑x').asIdeal
        (CommRingCat.Hom.hom f.op.unop) ⋯)
      (↑((toSpecΓ R).hom' x✝) ⟨PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop) ↑x', ⋯⟩) =
    ↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S)) x✝) x'
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
h' : Epi f.base
⊢ IsIso f

Tactic:
have : ∀ (U : (Opens Y)ᵒᵖ), IsIso (f.c.app U) := by
    intro U
    have : U = op (opensFunctor f |>.obj ((Opens.map f.base).obj (unop U))) := by
      induction U with | op U => ?_
      cases U
      dsimp only [Functor.op, Opens.map]
      congr
      exact (Set.image_preimage_eq _ ((TopCat.epi_iff_surjective _).mp h')).symm
    convert! H.c_iso (Opens.map f.base |>.obj <| unop U)
  have : IsIso f.c := NatIso.isIso_of_isIso_app _
  apply +allowSynthFailures isIso_of_components
  let t : X ≃ₜ Y := H.base_open.isEmbedding.toHomeomorph.trans
    { toFun := Subtype.val
      invFun := fun x =>
        ⟨x, by rw [Set.range_eq_univ.mpr ((TopCat.epi_iff_surjective _).mp h')]; trivial⟩ }
  exact (TopCat.isoOfHomeo t).isIso_hom

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

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

Tactic:
rw [Scheme.mem_basicOpen X s x x.2] at hx
  have hu : IsUnit (X.presheaf.germ _ x x.2 (s ^ n)) := by
    rw [map_pow]
    exact IsUnit.pow n hx
  rw [← hu.mul_right_eq_zero, ← map_mul, hf, map_zero]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : MorphismProperty C
S✝ : C
E : P.precoverage.ZeroHypercover S✝
⊢ ∃ ι f, (E.restrictIndex f).presieve₀ ∈ P.precoverage.coverings S✝

Tactic:
use PEmpty, PEmpty.elim

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : MorphismProperty C
S✝ : C
E : P.precoverage.ZeroHypercover S✝
⊢ (E.restrictIndex PEmpty.elim).presieve₀ ∈ P.precoverage.coverings S✝
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Y.restrict ⋯ ⟶ X

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ?refine_1 ≫ f = Y.ofRestrict ⋯ ≫ g

Tactic:
· use PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.1 g.1
    intro x
    have := PresheafedSpace.stalkMap.congr_hom _ _
        (PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition f.1 g.1) x
    rw [PresheafedSpace.stalkMap.comp, PresheafedSpace.stalkMap.comp] at this
    rw [← IsIso.eq_inv_comp] at this
    rw [this]
    dsimp
    apply RingHom.isLocalHom_comp

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ { toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := ⋯ } ≫ f = Y.ofRestrict ⋯ ≫ g
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan f g)
    ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) ⋙ PresheafedSpace.forget CommRingCat)

Tactic:
apply +allowSynthFailures Limits.comp_preservesLimit

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace)
    (PresheafedSpace.forget CommRingCat)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(X, U)
⊢ U.ι ''ᵁ (↑U).basicOpen ((ConcreteCategory.hom U.topIso.inv) r) = X.basicOpen r

Tactic:
by
  simp only [Scheme.Opens.toScheme_presheaf_obj]
  rw [ι_image_basicOpen', basicOpen_res_eq, topIso_inv, basicOpen_res_eq X]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ U.topIso.hom ≫ (Arrow.mk (Scheme.Hom.appLE f U V e)).hom =
    (Arrow.mk (Scheme.Hom.appTop (Scheme.Hom.resLE f U V e))).hom ≫ V.topIso.hom

Tactic:
by
  simp only [Scheme.Opens.topIso_hom, eqToHom_op, Arrow.mk_hom, Scheme.Hom.map_appLE]
  rw [Scheme.Hom.appTop, ← Scheme.Hom.appLE_eq_app, Scheme.Hom.resLE_appLE, Scheme.Hom.appLE_map]

Goal state after: