mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: case e'_3
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
y : Fin n → ℝ
hy : y ∈ Box.Icc (I.face i)
g : (Fin (n + 1) → ℝ) → E
hε : ∀ y ∈ Box.Icc I, ‖g y‖ ≤ ε * ‖y - x‖
hfc : ContinuousOn (fun y ↦ a + f' (y - x) + g y) (Box.Icc I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable (I.face i) ⊥ ((fun y ↦ a + f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y ↦ (fun y ↦ a + f' (y - x) + g y) y - a - f' (y - x)
⊢ ‖f' (Pi.single i (I.upper i - I.lower i)) -
        ((fun y ↦ a + f' (y - x) + g y) (e (I.upper i) y) - (fun y ↦ a + f' (y - x) + g y) (e (I.lower i) y))‖ =
    ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖

pp: case convert_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
y : Fin n → ℝ
hy : y ∈ Box.Icc (I.face i)
g : (Fin (n + 1) → ℝ) → E
hε : ∀ y ∈ Box.Icc I, ‖g y‖ ≤ ε * ‖y - x‖
hfc : ContinuousOn (fun y ↦ a + f' (y - x) + g y) (Box.Icc I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable (I.face i) ⊥ ((fun y ↦ a + f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y ↦ (fun y ↦ a + f' (y - x) + g y) y - a - f' (y - x)
⊢ ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤ 2 * ε * diam (Box.Icc I)

Tactic:
· congr 1
      have := Fin.insertNth_sub_same (α := fun _ ↦ ℝ) i (I.upper i) (I.lower i) y
      simp only [← this, f'.map_sub]; abel

Goal state after:
case convert_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
y : Fin n → ℝ
hy : y ∈ Box.Icc (I.face i)
g : (Fin (n + 1) → ℝ) → E
hε : ∀ y ∈ Box.Icc I, ‖g y‖ ≤ ε * ‖y - x‖
hfc : ContinuousOn (fun y ↦ a + f' (y - x) + g y) (Box.Icc I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable (I.face i) ⊥ ((fun y ↦ a + f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y ↦ (fun y ↦ a + f' (y - x) + g y) y - a - f' (y - x)
⊢ ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤ 2 * ε * diam (Box.Icc I)
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ∞
⊢ ∫⁻ (a : α), ENNReal.ofReal (ν (Prod.mk a ⁻¹' s)).toReal ∂μ = (μ.prod ν) s

Tactic:
prod_apply hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ∞
⊢ ∫⁻ (a : α), ENNReal.ofReal (ν (Prod.mk a ⁻¹' s)).toReal ∂μ = ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hlt : ∃ z ∈ sphere c R, ‖f z‖ < C
⊢ ‖∮ (z : ℂ) in C(c, R), f z‖ < 2 * π * R * C

Tactic:
← _root_.abs_of_pos hR,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hlt : ∃ z ∈ sphere c |R|, ‖f z‖ < C
⊢ ‖∮ (z : ℂ) in C(c, R), f z‖ < 2 * π * R * C
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
⊢ ∮ (z : ℂ) in C(c, R), (z - w) ^ n = 0

Tactic:
by_cases! H : w ∈ sphere c |R| ∧ n < -1

Goal state after:
case pos
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| ∧ n < -1
⊢ ∮ (z : ℂ) in C(c, R), (z - w) ^ n = 0

case neg
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
⊢ ∮ (z : ℂ) in C(c, R), (z - w) ^ n = 0
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z ↦ I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he : ∀ (x y : ℝ), ↑x + ↑y * I = e (x, y)
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (↑x + ↑y * I)) 1 - (f' (↑x + ↑y * I)) I

Tactic:
have he₁ : e (1, 0) = 1 := rfl

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z ↦ I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he : ∀ (x y : ℝ), ↑x + ↑y * I = e (x, y)
he₁ : e (1, 0) = 1
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (↑x + ↑y * I)) 1 - (f' (↑x + ↑y * I)) I
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this✝ : Fact (μ U < ∞)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (ν V < ∞)
⊢ ∫ (x : X), ∫ (y : Y) in V, f x y ∂ν ∂μ = ∫ (x : X) in U, ∫ (y : Y) in V, f x y ∂ν ∂μ

Tactic:
apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm

Goal state after:
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this✝ : Fact (μ U < ∞)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (ν V < ∞)
x : X
hx : x ∉ U
⊢ ∫ (y : Y) in V, f x y ∂ν = 0
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case refine_4
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
F' : ℝ → ℝ →L[ℝ] E := fun x ↦ smulRight 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ IntegrableOn f' (Set.Icc a b) volume

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hle] at Hi
        exact Hi.congr_set_ae Ioc_ae_eq_Icc.symm

Goal state after:
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ z ∈ ball c ↑R \ s, DifferentiableAt ℂ f z
hR : 0 < R
w : ℂ
hw : w ∈ eball 0 ↑R
⊢ c + w ∈ ball c ↑R

Tactic:
simpa only [add_mem_ball_iff_norm, ← coe_nnnorm, mem_eball_zero_iff,
        NNReal.coe_lt_coe, enorm_lt_coe] using hw

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case e_a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
this : k ≤ p.roots.card
⊢ (map (fun a ↦ X - C a) p.roots).prod.coeff k = (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)

Tactic:
convert! p.roots.prod_X_sub_C_coeff this using 3 <;> rw [hroots]

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

Goal state before:
pp: case inr
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ ‖(map f p).coeff i‖ ≤ max B 1 ^ d * ↑(d.choose (d / 2))

Tactic:
eq_one_of_roots_le hB h1 h2 h4,

Goal state after:
case inr
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ ‖(map f 1).coeff i‖ ≤ max B 1 ^ d * ↑(d.choose (d / 2))
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case h3
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := ⋯
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ ((galActionHom p ℂ) conj').IsSwap

Tactic:
rw [← Equiv.Perm.card_support_eq_two]
    apply Nat.add_left_cancel
    rw [← p_roots, ← Set.toFinset_card (rootSet p ℝ), ← Set.toFinset_card (rootSet p ℂ)]
    exact (card_complex_roots_eq_card_real_add_card_not_gal_inv p).symm

Goal state after:
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case mp.refine_2
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 ≤ k • (a.den • (x + y) - a.num • 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right✝ : ∀ (y : ℤ), (fun m ↦ 0 + m • 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + m • 1
hm2 : 0 + m • 1 < k • a.den • x - 1 + 1
hk' : 1 + (k • a.num • 1 - k • a.den • y) ≤ k • a.den • x - 1
this : k • a.num • 1 - k • a.den • y < m • 1
⊢ mkRat (↑k * a.num - m) (k * a.den) ∈ ratLt y

Tactic:
rw [mkRat_mem_ratLt hka0, sub_smul, sub_lt_comm, ← smul_smul, ← smul_smul, natCast_zsmul]

Goal state after:
case mp.refine_2
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 ≤ k • (a.den • (x + y) - a.num • 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right✝ : ∀ (y : ℤ), (fun m ↦ 0 + m • 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + m • 1
hm2 : 0 + m • 1 < k • a.den • x - 1 + 1
hk' : 1 + (k • a.num • 1 - k • a.den • y) ≤ k • a.den • x - 1
this : k • a.num • 1 - k • a.den • y < m • 1
⊢ k • a.num • 1 - k • a.den • y < m • 1
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: case neg.inr.inl
R : Type u_3
inst✝¹ : Ring R
inst✝ : ValuativeRel R
h : MulArchimedean (ValueGroupWithZero R)
b : ValueGroupWithZero R
H : 1 < b
H' : 1 b ≤ 1 1
ha : 1 ≠ 0
⊢ IsNontrivial R

Tactic:
exact ⟨⟨b, (H.trans' zero_lt_one).ne', H.ne'⟩⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
⊢ IsOpen (sphere x r)

Tactic:
by
  rw [← closedBall_sdiff_ball, sdiff_eq]
  exact (isOpen_closedBall x hr).inter (isClosed_ball x r).isOpen_compl

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case refine_1
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
x✝ : ∃ i, {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U
ε : (ofClass v).ValueGroup₀ˣ
hε : {p | v.restrict (p.2 - p.1) < ↑ε} ⊆ U
δ : ℝ≥0 := (RankOne.hom v) ↑ε
hδ : δ = (RankOne.hom v) ↑ε
hδ_pos : 0 < δ
⊢ ∃ a, 0 < a ∧ {p | v.norm (p.1 - p.2) < a} ⊆ U

Tactic:
use δ, hδ_pos

Goal state after:
case right
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
x✝ : ∃ i, {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U
ε : (ofClass v).ValueGroup₀ˣ
hε : {p | v.restrict (p.2 - p.1) < ↑ε} ⊆ U
δ : ℝ≥0 := ⋯
hδ : δ = (RankOne.hom v) ↑ε
hδ_pos : 0 < δ
⊢ {p | v.norm (p.1 - p.2) < ↑δ} ⊆ U
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ ≠ 0
hψ : ψ ≠ 0
p : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
q : σ →₀ ℕ
hq : ψ.lexOrder = ↑(toLex q)
⊢ (φ * ψ).lexOrder ≤ φ.lexOrder + ψ.lexOrder

Tactic:
rw [hp, hq]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ ≠ 0
hψ : ψ ≠ 0
p : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
q : σ →₀ ℕ
hq : ψ.lexOrder = ↑(toLex q)
⊢ (φ * ψ).lexOrder ≤ ↑(toLex p) + ↑(toLex q)
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsLeft R
p : MvPowerSeries σ R
hrp : (monomial n) r * p = 0
⊢ p = 0

Tactic:
ext i

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsLeft R
p : MvPowerSeries σ R
hrp : (monomial n) r * p = 0
i : σ →₀ ℕ
⊢ (coeff i) p = (coeff i) 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsRight R
p : MvPowerSeries σ R
hrp : p * (monomial n) r = 0
⊢ p = 0

Tactic:
ext i

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsRight R
p : MvPowerSeries σ R
hrp : p * (monomial n) r = 0
i : σ →₀ ℕ
⊢ (coeff i) p = (coeff i) 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₂ ^ 2 - 24 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₄ = 0

Tactic:
b₂,

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ ({ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ ^ 2 + 4 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₂) ^
        2 -
      24 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₄ =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ -{ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₂ ^ 2 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₈ -
          8 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₄ ^ 3 -
        27 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₆ ^ 2 +
      9 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₂ * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₄ *
        { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₆ =
    -27

Tactic:
b₂,

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ -({ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ ^ 2 + 4 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₂) ^
                2 *
            { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₈ -
          8 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₄ ^ 3 -
        27 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₆ ^ 2 +
      9 *
            ({ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ ^ 2 +
              4 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₂) *
          { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₄ *
        { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₆ =
    -27
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.b₂ ^ 2 - 24 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.b₄ = -48

Tactic:
b₂,

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ ({ a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₁ ^ 2 + 4 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₂) ^
        2 -
      24 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.b₄ =
    -48
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ -{ a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.b₂ ^ 2 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.b₈ -
          8 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.b₄ ^ 3 -
        27 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.b₆ ^ 2 +
      9 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.b₂ * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.b₄ *
        { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.b₆ =
    -64

Tactic:
b₂,

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ -({ a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₁ ^ 2 + 4 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₂) ^
                2 *
            { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.b₈ -
          8 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.b₄ ^ 3 -
        27 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.b₆ ^ 2 +
      9 *
            ({ a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₁ ^ 2 +
              4 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₂) *
          { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.b₄ *
        { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.b₆ =
    -64
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j : R
inst✝ : W.IsElliptic
hu : Fact (IsUnit 2)
⊢ (ofJ1728 R).IsElliptic

Tactic:
rw [isElliptic_iff, ofJ1728_Δ]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j : R
inst✝ : W.IsElliptic
hu : Fact (IsUnit 2)
⊢ IsUnit (-64)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
⊢ (ofJ j).IsElliptic

Tactic:
by_cases h1728 : j = 1728
    · have h2 : (2 : F) ≠ 0 := fun h ↦ h0 (by linear_combination h1728 + 864 * h)
      have := Fact.mk h2.isUnit
      rw [h1728, ofJ_1728_of_two_ne_zero h2]
      infer_instance
    · have := Fact.mk (Ne.isUnit h0)
      have := Fact.mk (sub_ne_zero.2 h1728).isUnit
      rw [ofJ_ne_0_ne_1728 j h0 h1728]
      infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomial / P z ^ 3 +
        (P y ^ 2 / P z ^ 2 * 1 + W.a₁ * P x * P y / P z ^ 2 * 1 + W.a₃ * P y / P z * 1 +
              W.a₂ * P x ^ 2 / P z ^ 2 * (P z / P z) +
            W.a₄ * P x / P z * (P z ^ 2 / P z ^ 2) +
          W.a₆ * (P z ^ 3 / P z ^ 3)) -
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomial +
        (P y ^ 2 / P z ^ 2 * (P z / P z) + W.a₁ * P x * P y / P z ^ 2 * (P z / P z) +
                W.a₃ * P y / P z * (P z ^ 2 / P z ^ 2) +
              W.a₂ * P x ^ 2 / P z ^ 2 * 1 +
            W.a₄ * P x / P z * 1 +
          W.a₆ * 1)) =
    0

Tactic:
eval_polynomial,

Goal state after:
case a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (P y ^ 2 * P z + W.a₁ * P x * P y * P z + W.a₃ * P y * P z ^ 2 -
            (P x ^ 3 + W.a₂ * P x ^ 2 * P z + W.a₄ * P x * P z ^ 2 + W.a₆ * P z ^ 3)) /
          P z ^ 3 +
        (P y ^ 2 / P z ^ 2 * 1 + W.a₁ * P x * P y / P z ^ 2 * 1 + W.a₃ * P y / P z * 1 +
              W.a₂ * P x ^ 2 / P z ^ 2 * (P z / P z) +
            W.a₄ * P x / P z * (P z ^ 2 / P z ^ 2) +
          W.a₆ * (P z ^ 3 / P z ^ 3)) -
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomial +
        (P y ^ 2 / P z ^ 2 * (P z / P z) + W.a₁ * P x * P y / P z ^ 2 * (P z / P z) +
                W.a₃ * P y / P z * (P z ^ 2 / P z ^ 2) +
              W.a₂ * P x ^ 2 / P z ^ 2 * 1 +
            W.a₄ * P x / P z * 1 +
          W.a₆ * 1)) =
    0
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h₁ : E.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
S : Sieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible
s : (i : E.I₀) → F.obj (op (E.X i))
hs : ∀ (i : E.I₀), (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) y → y = s i
i j : E.I₀
Z : C
gi : Z ⟶ E.X i
gj : Z ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
Y : C
f : Y ⟶ Z
x✝ : (E.sieve₁ gi gj).arrows f
k : E.I₁ i j
h : Y ⟶ E.Y k
hf₁ : f ≫ gi = h ≫ E.p₁ k
hf₂ : f ≫ gj = h ≫ E.p₂ k
⊢ (ConcreteCategory.hom (F.map (E.p₁ k).op)) (s i) = (ConcreteCategory.hom (F.map (E.p₂ k).op)) (s j)

Tactic:
refine (H' k).ext fun W p hp ↦ ?_

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h₁ : E.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
S : Sieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible
s : (i : E.I₀) → F.obj (op (E.X i))
hs : ∀ (i : E.I₀), (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) y → y = s i
i j : E.I₀
Z : C
gi : Z ⟶ E.X i
gj : Z ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
Y : C
f : Y ⟶ Z
x✝ : (E.sieve₁ gi gj).arrows f
k : E.I₁ i j
h : Y ⟶ E.Y k
hf₁ : f ≫ gi = h ≫ E.p₁ k
hf₂ : f ≫ gj = h ≫ E.p₂ k
W : C
p : W ⟶ E.Y k
hp : (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows p
⊢ (ConcreteCategory.hom (F.map p.op)) ((ConcreteCategory.hom (F.map (E.p₁ k).op)) (s i)) =
    (ConcreteCategory.hom (F.map p.op)) ((ConcreteCategory.hom (F.map (E.p₂ k).op)) (s j))