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

Goal state before:
pp: case isTrue
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
h✝ : decide (SignType.sign c₀ ≠ 0) = true
⊢ (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
        (SignType.sign c₀ :: List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length

pp: case isFalse
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
h✝ : ¬decide (SignType.sign c₀ ≠ 0) = true
⊢ (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)) (List.map (⇑SignType.sign) cs))).length

Tactic:
swap

Goal state after:
case isFalse
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
h✝ : ¬decide (SignType.sign c₀ ≠ 0) = true
⊢ (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)) (List.map (⇑SignType.sign) cs))).length

case isTrue
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
h✝ : decide (SignType.sign c₀ ≠ 0) = true
⊢ (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
        (SignType.sign c₀ :: List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case isTrue.isTrue
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
h✝¹ : decide (SignType.sign c₀ ≠ 0) = true
h✝ : 1 ≠ SignType.sign c₀
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (1 ::
        List.destutter' (fun x1 x2 ↦ x1 ≠ x2) (SignType.sign c₀)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length

pp: case isTrue.isFalse
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
h✝¹ : decide (SignType.sign c₀ ≠ 0) = true
h✝ : ¬1 ≠ SignType.sign c₀
⊢ (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)) (List.map (⇑SignType.sign) cs))).length

Tactic:
swap

Goal state after:
case isTrue.isFalse
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
h✝¹ : decide (SignType.sign c₀ ≠ 0) = true
h✝ : ¬1 ≠ SignType.sign c₀
⊢ (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)) (List.map (⇑SignType.sign) cs))).length

case isTrue.isTrue
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
h✝¹ : decide (SignType.sign c₀ ≠ 0) = true
h✝ : 1 ≠ SignType.sign c₀
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (1 ::
        List.destutter' (fun x1 x2 ↦ x1 ≠ x2) (SignType.sign c₀)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length
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
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
hdp : (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k).degree < (∏ i ∈ s, g i).degree
hp0 : ∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k = 0
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
rw [hr0, hp0, mul_zero, zero_sub, neg_mul, eq_comm, neg_eq_zero,
      ← mul_rotate, (hpm.mul hg.1).mul_right_eq_zero_iff] 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
hgid : g i ∣ r₂ i - r₁ i
hf : q₁ - q₂ = 0
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
hdp : (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k).degree < (∏ i ∈ s, g i).degree
hp0 : ∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k = 0
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
⊢ (∀ (x : R), x * r = 0 → x = 0) →
    ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0

Tactic:
intro h z hz

Goal state after:
case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
z : QuadraticAlgebra R a b
hz : z * (algebraMap R (QuadraticAlgebra R a b)) r = 0
⊢ z = 0
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y → x = y

pp: case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x = y → x ◃ x = y ◃ y

Tactic:
swap

Goal state after:
case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x = y → x ◃ x = y ◃ y

case mp
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y → x = y
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
have h₁ : inst₁.toNonUnitalNonAssocRing = inst₂.toNonUnitalNonAssocRing := by
    ext : 1 <;> assumption

Goal state after:
R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : inst₁.toNonUnitalNonAssocRing = inst₂.toNonUnitalNonAssocRing
⊢ inst₁ = inst₂
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime : IsCoprime g₁ g₂
⊢ ∃ q r₁ r₂, r₁.degree < g₁.degree ∧ r₂.degree < g₂.degree ∧ ↑f / (↑g₁ * ↑g₂) = ↑q + ↑r₁ / ↑g₁ + ↑r₂ / ↑g₂

Tactic:
by
  let g : Bool → R[X] := Bool.rec g₂ g₁
  have hg (i : Bool) (_ : i ∈ Finset.univ) : (g i).Monic := Bool.rec hg₂ hg₁ i
  have hcoprime : Set.Pairwise (Finset.univ : Finset Bool) fun i j => IsCoprime (g i) (g j) := by
    simp [g, Set.pairwise_insert, hcoprime, hcoprime.symm]
  obtain ⟨q, r, hr, hf⟩ := div_prod_eq_quo_add_sum_rem_div K f hg hcoprime
  refine ⟨q, r true, r false, hr true (Finset.mem_univ true), hr false (Finset.mem_univ false), ?_⟩
  simpa [g, add_assoc] using hf

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

Goal state before:
pp: case refine_1.inr
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
b : α
⊢ R b * (toEndRingHom α) f = (toEndRingHom α) f * R b

Tactic:
· exact AddMonoidHom.ext fun a ↦ (map_mul_right f a b).symm

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:
by simp only [RingQuot.smul_quot, smul_assoc]

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

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
⊢ f.update a b = (erase a) f + single a b

Tactic:
classical ext x; by_cases hx : x = a <;> aesop (add norm coeff_single_apply)

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝ : Semiring R
r : R → R → Prop
⊢ Function.Surjective ⇑(mkRingHom r)

Tactic:
simp only [mkRingHom_def, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
  rintro ⟨⟨⟩⟩
  simp

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → f x = f y
g : RingQuot r →+* T
h : g.comp (mkRingHom r) = f
x✝ : R
⊢ (g.comp (mkRingHom r)) x✝ = ((lift ⟨f, w⟩).comp (mkRingHom r)) x✝

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → f x = f y
g : RingQuot s →ₐ[S] B
h : g.comp (mkAlgHom S s) = f
x✝ : A
⊢ (g.comp (mkAlgHom S s)) x✝ = (((liftAlgHom S) ⟨f, w⟩).comp (mkAlgHom S s)) x✝

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
mul_comm : IsMulCommutative (CentroidHom α)
x✝² x✝¹ : CentroidHom α
x✝ : α
⊢ (star (x✝² * x✝¹)) x✝ = (star x✝¹ * star x✝²) x✝

Tactic:
simp [mul_comm']

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
M : Type u_3
inst✝ : AddZeroClass M
f g : SkewMonoidAlgebra k G →+ M
h : ∀ (a : G) (b : k), f (single a b) = g (single a b)
⊢ f = g

Tactic:
by
  ext p; induction p using SkewMonoidAlgebra.induction_on <;> simp_all

Goal state after:
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 • x) ∘ fun x ↦ g' • x)) f = (mapDomain fun x ↦ g • x) ((mapDomain fun x ↦ g' • x) f)

Tactic:
mapDomain_comp

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 • x) ((mapDomain fun x ↦ g' • x) f) = (mapDomain fun x ↦ g • x) ((mapDomain fun x ↦ g' • x) f)
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a + b = 0 ↔ a = 0 ∧ b = 0

Tactic:
rw [add_eq_iff]

Goal state after:
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a ↔ a = 0 ∧ b = 0
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case pos
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    ((single x r).sum fun a₂ b₂ ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) = if a₁ * x = z then b₁ * a₁ • r else 0
h : ¬f.coeff y = 0
⊢ f.coeff y * y • r = f.coeff y * y • r

Tactic:
simp [h]

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

Goal state before:
pp: case neg
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    ((single x r).sum fun a₂ b₂ ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) = if a₁ * x = z then b₁ * a₁ • r else 0
h : f.coeff y = 0
⊢ 0 = f.coeff y * y • r

Tactic:
simp [h]

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

Goal state before:
pp: case pos
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : (f.sum fun a b ↦ if x * a = y then 0 * x • b else 0) = 0
h : ¬f.coeff z = 0
⊢ r * x • f.coeff z = r * x • f.coeff z

Tactic:
simp [h]

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

Goal state before:
pp: case neg
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : (f.sum fun a b ↦ if x * a = y then 0 * x • b else 0) = 0
h : f.coeff z = 0
⊢ 0 = r * x • f.coeff z

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (E →ₗ[R] F)
⊢ star f = f ↔ ∀ (x : E), f.ofConv (star x) = star (f.ofConv x)

Tactic:
WithConv.ext_iff,

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (E →ₗ[R] F)
⊢ (star f).ofConv = f.ofConv ↔ ∀ (x : E), f.ofConv (star x) = star (f.ofConv x)
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_4
V : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommGroup V
inst✝² : StarAddMonoid V
inst✝¹ : Module R V
inst✝ : StarModule R V
f : WithConv (End R V)
x : R
⊢ x ∈ spectrum R (star f).ofConv ↔ x ∈ star (spectrum R f.ofConv)

Tactic:
Set.mem_star,

Goal state after:
R : Type u_4
V : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommGroup V
inst✝² : StarAddMonoid V
inst✝¹ : Module R V
inst✝ : StarModule R V
f : WithConv (End R V)
x : R
⊢ x ∈ spectrum R (star f).ofConv ↔ star x ∈ spectrum R f.ofConv
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ X.basicOpen f ≤ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)

Tactic:
have := X.basicOpen_res (inv i) (X.presheaf.map i f)

Goal state after:
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this :
  X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (inv i))) ((ConcreteCategory.hom (X.presheaf.map i)) f)) =
    unop U ⊓ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)
⊢ X.basicOpen f ≤ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)
Module: Mathlib.AlgebraicGeometry.Scheme

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

Tactic:
simp only [Scheme.mem_basicOpen _ _ _ hxU, map_add] at hx ⊢

Goal state after:
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)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (opensFunctor f).IsCocontinuous (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Y)

Tactic:
rw [f.opensFunctorAdjunction.isCocontinuous_iff_coverPreserving]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
⊢ CoverPreserving (Opens.grothendieckTopology ↥Y) (Opens.grothendieckTopology ↥X) (Opens.map f.base)
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
U : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
⊢ (Opens.map s.snd.base).op.obj (⋯.functor.op.obj U) = (Opens.map (pullback.lift s.fst.base s.snd.base ⋯)).op.obj U

Tactic:
dsimp only [Opens.map_def, IsOpenMap.functor, Functor.op]
                congr 2
                let s' : PullbackCone f.base g.base :=
                  PullbackCone.mk s.fst.base s.snd.base (congr_arg Hom.base s.condition)
                have : _ = s.snd.base := limit.lift_π s' WalkingCospan.right
                conv_lhs =>
                  rw [← this]
                  dsimp [s']
                  rw [Function.comp_def, ← Set.preimage_preimage]
                rw [Set.preimage_image_eq _
                    (TopCat.snd_isOpenEmbedding_of_left hf.base_open g.base).injective]
                rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
⊢ ∃ R f, IsOpenImmersion f ∧ x ∈ Set.range ⇑f ∧ Set.range ⇑f ⊆ ↑U

Tactic:
have : e.hom.base ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U :=
    show ((e.hom ≫ e.inv).base ⟨x, hxV⟩).1 ∈ U from e.hom_inv_id ▸ hxU

Goal state after:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
⊢ ∃ R f, IsOpenImmersion f ∧ x ∈ Set.range ⇑f ∧ Set.range ⇑f ⊆ ↑U
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : ↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat
R : CommRingCat
i : Spec R ⟶ Y
left✝ : AlgebraicGeometry.IsOpenImmersion i
h₁ : (ConcreteCategory.hom f.base) x ∈ Set.range ⇑i
h₂ : Set.range ⇑i ⊆ ↑{ carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }
⊢ ∃ R f_1, x ∈ Set.range ⇑(ConcreteCategory.hom f_1.base) ∧ LocallyRingedSpace.IsOpenImmersion f_1

Tactic:
refine ⟨R, LocallyRingedSpace.IsOpenImmersion.lift (toLocallyRingedSpaceHom _ f) _ h₂, ?_, ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : ↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat
R : CommRingCat
i : Spec R ⟶ Y
left✝ : AlgebraicGeometry.IsOpenImmersion i
h₁ : (ConcreteCategory.hom f.base) x ∈ Set.range ⇑i
h₂ : Set.range ⇑i ⊆ ↑{ carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }
⊢ x ∈
    Set.range
      ⇑(ConcreteCategory.hom
          (LocallyRingedSpace.IsOpenImmersion.lift (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom'
              h₂).base)

case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : ↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat
R : CommRingCat
i : Spec R ⟶ Y
left✝ : AlgebraicGeometry.IsOpenImmersion i
h₁ : (ConcreteCategory.hom f.base) x ∈ Set.range ⇑i
h₂ : Set.range ⇑i ⊆ ↑{ carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }
⊢ LocallyRingedSpace.IsOpenImmersion
    (LocallyRingedSpace.IsOpenImmersion.lift (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom' h₂)
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : f x = g y
⊢ x ∈ {x | ∃ y, f x = g y}

Tactic:
use y

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 : IsOpenImmersion f
g : Y ⟶ Z
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this : IsIso (pullback.snd f.base g.base)
⊢ IsIso (pullback.snd f g)

Tactic:
have : IsIso (pullback.snd f g).base := by
    delta pullback.snd
    rw [← limit.isoLimitCone_hom_π ⟨_, pullbackConeOfLeftIsLimit f g⟩ WalkingCospan.right]
    change IsIso (_ ≫ pullback.snd _ _)
    infer_instance

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f.base g.base)
this : IsIso (pullback.snd f g).base
⊢ IsIso (pullback.snd f g)