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

Goal state before:
pp: 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))‖ ≤
    2 * ε * diam (Box.Icc I)

Tactic:
convert_to ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤ _

Goal state after:
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)‖

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.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hf₁ : CircleIntegrable f₁ c R
⊢ CircleIntegrable f₂ c R

Tactic:
by_cases hR : R = 0

Goal state after:
case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hf₁ : CircleIntegrable f₁ c R
hR : R = 0
⊢ CircleIntegrable f₂ c R

case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hf₁ : CircleIntegrable f₁ c R
hR : ¬R = 0
⊢ CircleIntegrable f₂ c R
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: case negSucc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = m • ∫ (x : ℝ) in 0..T, f x
n : ℕ
⊢ ∫ (x : ℝ) in 0..Int.negSucc n • T, f x = Int.negSucc n • ∫ (x : ℝ) in 0..T, f x

Tactic:
· conv_rhs => rw [negSucc_zsmul]
    have h₀ : Int.negSucc n • T + (n + 1) • T = 0 := by simp; linarith
    rw [integral_symm, ← (hf.nsmul (n + 1)).funext, neg_inj]
    simp_rw [integral_comp_add_right, h₀, zero_add, this (n + 1), add_comm T,
      hf.intervalIntegral_add_eq ((n + 1) • T) 0, zero_add]

Goal state after:
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
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ ∫ (θ : ℝ) in 0..2 * π, R * ‖f (circleMap c R θ)‖ < ∫ (x : ℝ) in 0..2 * π, R * C

Tactic:
refine intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt
          Real.two_pi_pos ?_ continuousOn_const (fun θ _ => ?_) ⟨θ₀, Ioc_subset_Icc_self hmem, ?_⟩

Goal state after:
case refine_1
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
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ ContinuousOn (fun θ ↦ R * ‖f (circleMap c R θ)‖) (Icc 0 (2 * π))

case refine_2
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
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
θ : ℝ
x✝ : θ ∈ Ioc 0 (2 * π)
⊢ R * ‖f (circleMap c R θ)‖ ≤ R * C

case refine_3
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
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ R * ‖f (circleMap c R θ₀)‖ < R * C
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
⊢ ∀ (x : ↥(Lp E 1 (μ.prod ν))), ContinuousAt (fun f ↦ ∫ (x : α), ∫ (y : β), ↑↑f (x, y) ∂ν ∂μ) x

Tactic:
intro g

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ ContinuousAt (fun f ↦ ∫ (x : α), ∫ (y : β), ↑↑f (x, y) ∂ν ∂μ) g
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α × β → E
hf : Integrable f (μ.prod ν)
⊢ ∫ (z : α × β), f z ∂μ.prod ν = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν

Tactic:
rw [← integral_prod_swap f]

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α × β → E
hf : Integrable f (μ.prod ν)
⊢ ∫ (z : β × α), f z.swap ∂ν.prod μ = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν
Module: Mathlib.Analysis.Complex.Liouville

Goal state before:
pp: F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ z ∈ sphere c R, ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
this : 2 * ↑π * I / ↑n.factorial ≠ 0
⊢ iteratedDeriv n f c = n.factorial • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z

Tactic:
← inv_smul_smul₀ this (iteratedDeriv n f c),

Goal state after:
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ z ∈ sphere c R, ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
this : 2 * ↑π * I / ↑n.factorial ≠ 0
⊢ (2 * ↑π * I / ↑n.factorial)⁻¹ • (2 * ↑π * I / ↑n.factorial) • iteratedDeriv n f c =
    n.factorial • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
r : F[X]
hr : Irreducible r
hr' : ¬r.natDegree = 0
x : (r.comp q).SplittingField
hx : (aeval ((aeval x) q)) r = 0
⊢ P r

Tactic:
have h_normal : Normal F (r.comp q).SplittingField := SplittingField.instNormal (r.comp q)

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
r : F[X]
hr : Irreducible r
hr' : ¬r.natDegree = 0
x : (r.comp q).SplittingField
hx : (aeval ((aeval x) q)) r = 0
h_normal : Normal F (r.comp q).SplittingField
⊢ P r
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
Hc : ContinuousOn f (Set.Icc b a)
Hd : ∀ x ∈ Set.Ioo b a \ s, HasDerivAt f (f' x) x
⊢ ∫ (x : ℝ) in a..b, f' x = f b - f a

Tactic:
intervalIntegral.integral_symm,

Goal state after:
case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
Hc : ContinuousOn f (Set.Icc b a)
Hd : ∀ x ∈ Set.Ioo b a \ s, HasDerivAt f (f' x) x
⊢ -∫ (x : ℝ) in b..a, f' x = f b - f a
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case a
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ⋯
b : Finset ℂ := ⋯
c : Finset ℂ := ⋯
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
z : ℂ
hz1 : (aeval z) p = 0
hz2 : z.im = 0
⊢ ((IsScalarTower.toAlgHom ℚ ℝ ℂ) z.re).im = z.im

Tactic:
hz2

Goal state after:
case a
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
z : ℂ
hz1 : (aeval z) p = 0
hz2 : z.im = 0
⊢ ((IsScalarTower.toAlgHom ℚ ℝ ℂ) z.re).im = 0
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
⊢ ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0

Tactic:
intro w

Goal state after:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
w : ↑(p.rootSet ℂ)
⊢ ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ (X - C ((starRingEnd ℂ) z)) * (X - C z) ∣ map (algebraMap ℝ ℂ) p

Tactic:
apply IsCoprime.mul_dvd
  · exact isCoprime_X_sub_C_of_isUnit_sub <| .mk0 _ <| sub_ne_zero.2 <| mt conj_eq_iff_im.1 hz
  · simpa [dvd_iff_isRoot, aeval_conj]
  · simpa [dvd_iff_isRoot]

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

Goal state before:
pp: case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : r < 0
⊢ IsOpen (closedBall x r)

Tactic:
| inl h =>

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y z : S
h : ‖x / y‖₊ ≠ ‖y / z‖₊
⊢ ‖x / z‖₊ = max ‖x / y‖₊ ‖y / z‖₊

Tactic:
by
  simpa only [← NNReal.coe_inj, NNReal.coe_max] using!
    norm_div_eq_max_of_norm_div_ne_norm_div _ _ _ (NNReal.coe_injective.ne h)

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: case inr.inr
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ ≠ 0
hψ : ψ ≠ 0
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

Tactic:
rcases exists_finsupp_eq_lexOrder_of_ne_zero hφ with ⟨p, hp⟩

Goal state after:
case inr.inr
σ : 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)
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: 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✝ : ∃ a, 0 < a ∧ {p | v.norm (p.1 - p.2) < a} ⊆ U
r : ℝ
hr_pos : 0 < r
hr : {p | v.norm (p.1 - p.2) < r} ⊆ U
this : Nontrivial Γ₀ˣ
u : (ofClass v).ValueGroup₀ˣ
hu : ↑((RankOne.hom v) ↑u) < r
x : L × L
hx : x ∈ {p | v.restrict (p.2 - p.1) < ↑u}
⊢ ↑((RankOne.hom v) (v.restrict (x.1 - x.2))) < ↑((RankOne.hom v) ↑u)

Tactic:
rw [NNReal.coe_lt_coe, ← neg_sub, Valuation.map_neg]

Goal state after:
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✝ : ∃ a, 0 < a ∧ {p | v.norm (p.1 - p.2) < a} ⊆ U
r : ℝ
hr_pos : 0 < r
hr : {p | v.norm (p.1 - p.2) < r} ⊆ U
this : Nontrivial Γ₀ˣ
u : (ofClass v).ValueGroup₀ˣ
hu : ↑((RankOne.hom v) ↑u) < r
x : L × L
hx : x ∈ {p | v.restrict (p.2 - p.1) < ↑u}
⊢ (RankOne.hom v) (v.restrict (x.2 - x.1)) < (RankOne.hom v) ↑u
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
⊢ ∀ (a : MvPowerSeries σ R), IsUnit a ∨ IsUnit (1 - a)

Tactic:
by
    intro φ
    obtain ⟨u, h⟩ | ⟨u, h⟩ := IsLocalRing.isUnit_or_isUnit_one_sub_self (constantCoeff φ) <;>
        [left; right] <;>
      · refine .of_mul_eq_one _ (mul_invOfUnit _ u ?_)
        simpa using h.symm

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: R : Type u_1
k : Type u_2
inst✝ : Field k
⊢ (Unit_of_divided_by_X_pow_order 0)⁻¹ = 1

Tactic:
simp only [Unit_of_divided_by_X_pow_order_zero, inv_one]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : FinitePlace K
x : 𝓞 K
hx : x ≠ 0
hnz : span {x} ≠ ⊥
⊢ v ↑x * ↑(absNorm v.maximalIdeal.asIdeal) ^ multiplicity v.maximalIdeal.asIdeal (span {x}) = 1

Tactic:
rw [← norm_embedding_eq v x, ← Nat.cast_pow, ← map_pow, ← maxPowDividing_eq_pow_multiplicity hnz]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : FinitePlace K
x : 𝓞 K
hx : x ≠ 0
hnz : span {x} ≠ ⊥
⊢ ‖(embedding v.maximalIdeal) ↑x‖ * ↑(absNorm (v.maximalIdeal.maxPowDividing (span {x}))) = 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: 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
h3 : 3 = 0
⊢ 2 * 2 = 1

Tactic:
linear_combination h3

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹¹ : Field K
R : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : Algebra R K
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : IsFractionRing R K
v✝ : HeightOneSpectrum R
L : Type u_3
inst✝⁶ : NumberField K
inst✝⁵ : Field L
inst✝⁴ : NumberField L
inst✝³ : Algebra K L
v : HeightOneSpectrum (𝓞 K)
w : HeightOneSpectrum (𝓞 L)
inst✝² : Algebra (adicCompletion K v) (adicCompletion L w)
inst✝¹ : ContinuousSMul (adicCompletion K v) (adicCompletion L w)
inst✝ : IsScalarTower K (adicCompletion K v) (adicCompletion L w)
Φ : adicCompletion K v ⊗[K] L →ₗ[adicCompletion K v] adicCompletion L w :=
  (Algebra.TensorProduct.lift (Algebra.algHom (adicCompletion K v) (adicCompletion K v) (adicCompletion L w))
      (Algebra.algHom K L (adicCompletion L w)) ⋯).toLinearMap
⊢ DenseRange ⇑Φ

Tactic:
apply (w.denseRange_algebraMap L).mono
    rintro _ ⟨l, rfl⟩
    exact ⟨1 ⊗ₜ l, by simp [Φ, Algebra.algHom]⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : 3 = 0
⊢ 2 * 2 = 1

Tactic:
linear_combination h3

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: case h
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows ≤ (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows

pp: case hS
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows

pp: case trans
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ S⦄,
    (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows f →
      Presieve.IsSeparatedFor F (Sieve.pullback f (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f))).arrows

Tactic:
· rw [← Sieve.generate_le_iff, Sieve.generate_sieve, Sieve.generate_le_iff,
      Presieve.ofArrows_le_iff]
    intro i
    rw [← f.w₀]
    exact ⟨_, f.h₀ i, 𝒱.f _, ⟨_⟩, rfl⟩

Goal state after:
case hS
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows

case trans
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ S⦄,
    (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows f →
      Presieve.IsSeparatedFor F (Sieve.pullback f (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f))).arrows
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : Nontrivial R
⊢ W'.Nonsingular ![0, 1, 0]

Tactic:
by
  simp only [nonsingular_of_Z_eq_zero, equation_zero, true_and, fin3_def_ext, ← not_and_or]
  exact fun h => one_ne_zero <| by linear_combination (norm := ring1) h.right

Goal state after:
Module: Mathlib.Topology.Category.TopCat.ULift

Goal state before:
pp: J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cocone K
hc : IsColimit c
⊢ (uliftFunctor.mapCocone c).pt.str =
    ⨆ j,
      TopologicalSpace.coinduced (⇑(ConcreteCategory.hom ((uliftFunctor.mapCocone c).ι.app j)))
        ((K ⋙ uliftFunctor).obj j).str

Tactic:
ext s

Goal state after:
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cocone K
hc : IsColimit c
s : Set ↑(uliftFunctor.mapCocone c).pt
⊢ IsOpen s ↔ IsOpen s
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case pos
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Projective R
W : Projective F
inst✝ : DecidableEq F
point✝ : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P)
hPz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ fromAffine { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }

Tactic:
Point.ext_iff,

Goal state after:
case pos
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Projective R
W : Projective F
inst✝ : DecidableEq F
point✝ : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P)
hPz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (fromAffine { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }.toAffineLift).point =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }.point
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case neg
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Projective R
W : Projective F
inst✝ : DecidableEq F
point✝ : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P)
hPz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ fromAffine { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }

Tactic:
Point.ext_iff,

Goal state after:
case neg
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Projective R
W : Projective F
inst✝ : DecidableEq F
point✝ : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P)
hPz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (fromAffine { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }.toAffineLift).point =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }.point