mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ≤ a₀
h_int : IntervalIntegrable f μ a a₀
⊢ ∀ b ∈ Icc a a₀, ∫ (x : ℝ) in Iio b, f x ∂μ = ∫ (x : ℝ) in Iio a₀, f x ∂μ + ∫ (x : ℝ) in a₀..b, f x ∂μ

Tactic:
intro b

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ≤ a₀
h_int : IntervalIntegrable f μ a a₀
b : ℝ
⊢ b ∈ Icc a a₀ → ∫ (x : ℝ) in Iio b, f x ∂μ = ∫ (x : ℝ) in Iio a₀, f x ∂μ + ∫ (x : ℝ) in a₀..b, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case h_lim
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ sphere c R, dist (g x) (f n x) < ε
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (n : ι) in l, ∀ x ∈ [[0, 2 * π]], R * dist (g (circleMap c R x)) (f n (circleMap c R x)) < ε

Tactic:
rcases exists_pos_mul_lt hε R with ⟨δ, hδ₀, hRδ⟩

Goal state after:
case h_lim
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ sphere c R, dist (g x) (f n x) < ε
ε : ℝ
hε : ε > 0
δ : ℝ
hδ₀ : 0 < δ
hRδ : R * δ < ε
⊢ ∀ᶠ (n : ι) in l, ∀ x ∈ [[0, 2 * π]], R * dist (g (circleMap c R x)) (f n (circleMap c R x)) < ε
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
w : ℂ
⊢ w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z =
    (2 * ↑π * I)⁻¹ • w ^ n • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z

Tactic:
← smul_comm (w ^ n)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
w : ℂ
⊢ w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z =
    w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case inl.zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
⊢ (2 * π)⁻¹ * (|0|⁻¹ ^ 0 * (|0| * (|0|⁻¹ * ∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c 0 x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c 0 θ)‖) * |0|⁻¹ ^ 0

Tactic:
simp [-mul_inv_rev]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case inl.succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
n✝ : ℕ
⊢ (2 * π)⁻¹ * (|0|⁻¹ ^ (n✝ + 1) * (|0| * (|0|⁻¹ * ∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c 0 x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c 0 θ)‖) * |0|⁻¹ ^ (n✝ + 1)

Tactic:
simp [-mul_inv_rev]

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: 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
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : p₁.comp q = 0
h : eval (q.coeff 0) p₁ = 0 ∧ q = C (q.coeff 0)
⊢ q.natDegree = 0

Tactic:
rw [h.2, natDegree_C]

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: 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
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬p₁.comp q = 0
h₂ : p₂.comp q = 0
h : eval (q.coeff 0) p₂ = 0 ∧ q = C (q.coeff 0)
⊢ q.natDegree = 0

Tactic:
rw [h.2, natDegree_C]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ msymm σ R (Nat.Partition.indiscrete 0) = 1

Tactic:
rw [msymm, Fintype.sum_subsingleton _ ⟨(Sym.nil : Sym σ 0), rfl⟩]
  simp

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

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
o : IsOpen s
⊢ AnalyticOn ℂ f s ↔ DifferentiableOn ℂ f s

Tactic:
by
  rw [o.analyticOn_iff_analyticOnNhd]
  exact analyticOnNhd_iff_differentiableOn o

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case neg.refine_2.refine_2.refine_2
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
hc0 :
  ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ (aeval z) p = 0 ∧ z.im ≠ 0
⊢ Disjoint b c

Tactic:
Finset.disjoint_left

Goal state after:
case neg.refine_2.refine_2.refine_2
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
hc0 :
  ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ (aeval z) p = 0 ∧ z.im ≠ 0
⊢ ∀ ⦃a : ℂ⦄, a ∈ b → a ∉ c
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: 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
⊢ 1 + (k • a.num • 1 - k • a.den • y) ≤ k • a.den • x - 1

Tactic:
rw [smul_add, smul_sub, smul_add, le_sub_iff_add_le, ← sub_le_iff_le_add] at hk

Goal state after:
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.num • 1 - k • a.den • y ≤ k • a.den • x
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
⊢ 1 + (k • a.num • 1 - k • a.den • y) ≤ k • a.den • x - 1
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case h1
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 := (restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ p.natDegree ∣ Fintype.card ↥(galActionHom p ℂ).range

Tactic:
simpa only [Fintype.card_eq_nat_card,
      Nat.card_congr (MonoidHom.ofInjective (galActionHom_injective p ℂ)).toEquiv.symm]
      using prime_degree_dvd_card p_irr p_deg

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

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x✝ y✝ : X
r✝ s✝ : ℝ
x y : X
r s : ℝ
hrs : r ≤ s
h : (ball x r ∩ ball y s).Nonempty
⊢ ball x r ⊆ ball y s

Tactic:
obtain ⟨hxz, hyz⟩ := (Set.mem_inter_iff _ _ _).mp h.some_mem

Goal state after:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x✝ y✝ : X
r✝ s✝ : ℝ
x y : X
r s : ℝ
hrs : r ≤ s
h : (ball x r ∩ ball y s).Nonempty
hxz : h.some ∈ ball x r
hyz : h.some ∈ ball y s
⊢ ball x r ⊆ ball y s
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
x✝ : X
h : dist y x ≤ r
h' : dist x✝ x ≤ r
⊢ dist x✝ y ≤ r

Tactic:
exact (dist_triangle_max _ _ _).trans (max_le h' (dist_comm x _ ▸ h))

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

Goal state before:
pp: case mpr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
x✝ : X
h : dist y x ≤ r
h' : dist x✝ y ≤ r
⊢ dist x✝ x ≤ r

Tactic:
exact (dist_triangle_max _ _ _).trans (max_le h' (dist_comm x _ ▸ h))

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

Goal state before:
pp: 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
this : ∀ (x : ℝ), (∀ (y : ℚ), y.num • 1 < ↑y.den • 1 → ↑y ≤ x) → 1 ≤ x
⊢ ∀ (b : ℝ), (∀ x ∈ ratLt' 1, x ≤ b) → 1 ≤ b

Tactic:
by
      simpa using this

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

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x✝ y✝ : X
r✝ s✝ : ℝ
x y : X
r s : ℝ
hrs : r ≤ s
h : (closedBall x r ∩ closedBall y s).Nonempty
⊢ closedBall x r ⊆ closedBall y s

Tactic:
obtain ⟨hxz, hyz⟩ := (Set.mem_inter_iff _ _ _).mp h.some_mem

Goal state after:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x✝ y✝ : X
r✝ s✝ : ℝ
x y : X
r s : ℝ
hrs : r ≤ s
h : (closedBall x r ∩ closedBall y s).Nonempty
hxz : h.some ∈ closedBall x r
hyz : h.some ∈ closedBall y s
⊢ closedBall x r ⊆ closedBall y s
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: M : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M
inst✝¹ : IsUltrametricDist M
s : Multiset ι
inst✝ : Nonempty ι
f : ι → M
⊢ ∃ i, (s ≠ 0 → i ∈ s) ∧ ‖(Multiset.map f s).prod‖ ≤ ‖f i‖

Tactic:
by
  inhabit ι
  induction s using Multiset.induction_on with
  | empty => simp
  | cons a t hM =>
      obtain ⟨M, hMs, hM⟩ := hM
      by_cases! hMa : ‖f M‖ ≤ ‖f a‖
      · refine ⟨a, by simp, ?_⟩
        · rw [Multiset.map_cons, Multiset.prod_cons]
          exact le_trans (norm_mul_le_max _ _) (max_le (le_refl _) (le_trans hM hMa))
      · rcases eq_or_ne t 0 with rfl | ht
        · exact ⟨a, by simp, by simp⟩
        · refine ⟨M, ?_, ?_⟩
          · simp [hMs ht]
          rw [Multiset.map_cons, Multiset.prod_cons]
          exact le_trans (norm_mul_le_max _ _) (max_le hMa.le hM)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
h : ¬φ = 0
ne : (⇑toLex '' Function.support φ).Nonempty
⊢ WithTop (Lex (σ →₀ ℕ))

Tactic:
apply WithTop.some

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
h : ¬φ = 0
ne : (⇑toLex '' Function.support φ).Nonempty
⊢ Lex (σ →₀ ℕ)
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
h : φ = 0
⊢ ⊤ = ⊤ ↔ φ = 0

pp: case neg
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
h : ¬φ = 0
⊢ (have ne := ⋯;
      ↑(⋯.min (⇑toLex '' Function.support φ) ne)) =
      ⊤ ↔
    φ = 0

Tactic:
· simp only [h]

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
h : ¬φ = 0
⊢ (have ne := ⋯;
      ↑(⋯.min (⇑toLex '' Function.support φ) ne)) =
      ⊤ ↔
    φ = 0
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hφ : ¬φ = 0
ne : (⇑toLex '' Function.support φ).Nonempty
h : toLex d < ⋯.min (⇑toLex '' Function.support φ) ne
hφ' : φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)
⊢ (coeff d) φ = 0

Tactic:
by_contra h'

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hφ : ¬φ = 0
ne : (⇑toLex '' Function.support φ).Nonempty
h : toLex d < ⋯.min (⇑toLex '' Function.support φ) ne
hφ' : φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)
h' : ¬(coeff d) φ = 0
⊢ False
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff d) φ = 0
h' : φ.lexOrder < w
hφ : φ ≠ 0
⊢ False

Tactic:
obtain ⟨d, hd⟩ := exists_finsupp_eq_lexOrder_of_ne_zero hφ

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff d) φ = 0
h' : φ.lexOrder < w
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : φ.lexOrder = ↑(toLex d)
⊢ False
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation L Γ₀
hv : v.RankOne
x : L
⊢ 0 ≤ v.norm x

Tactic:
by simp only [norm, NNReal.zero_le_coe]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
⊢ Function.Injective ⇑(rescale a)

Tactic:
intro p q h

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
h : (rescale a) p = (rescale a) q
⊢ p = q
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite (A ⧸ v.asIdeal)
⊢ ¬DenselyOrdered ↑(Set.range ⇑(valuation K v))

Tactic:
WithZero.denselyOrdered_set_iff_subsingleton

Goal state after:
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite (A ⧸ v.asIdeal)
⊢ ¬(Set.range ⇑(valuation K v)).Subsingleton
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite (A ⧸ v.asIdeal)
⊢ ¬DenselyOrdered ↑(Set.range ⇑Valued.v)

Tactic:
WithZero.denselyOrdered_set_iff_subsingleton

Goal state after:
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite (A ⧸ v.asIdeal)
⊢ ¬(Set.range ⇑Valued.v).Subsingleton
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * P x * W'.neg P z + 3 * P x * P x ^ 2 * P z + P y ^ 2 * W'.neg P z ^ 2 - W'.neg P y ^ 2 * P z ^ 2 +
                    W'.a₁ * P x * P y * W'.neg P z ^ 2 -
                  W'.a₁ * P x * W'.neg P y * P z ^ 2 -
                W'.a₂ * P x ^ 2 * W'.neg P z ^ 2 +
              W'.a₂ * P x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * W'.neg P z ^ 2 -
          W'.a₃ * W'.neg P y * P z ^ 2 * W'.neg P z -
        W'.a₄ * P x * P z * W'.neg P z ^ 2 +
      W'.a₄ * P x * P z ^ 2 * W'.neg P z =
    0

Tactic:
neg_Y,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * P x * W'.neg P z + 3 * P x * P x ^ 2 * P z + P y ^ 2 * W'.neg P z ^ 2 - W'.negY P ^ 2 * P z ^ 2 +
                    W'.a₁ * P x * P y * W'.neg P z ^ 2 -
                  W'.a₁ * P x * W'.negY P * P z ^ 2 -
                W'.a₂ * P x ^ 2 * W'.neg P z ^ 2 +
              W'.a₂ * P x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * W'.neg P z ^ 2 -
          W'.a₃ * W'.negY P * P z ^ 2 * W'.neg P z -
        W'.a₄ * P x * P z * W'.neg P z ^ 2 +
      W'.a₄ * P x * P z ^ 2 * W'.neg P z =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -P x * W'.neg P y ^ 2 * P z + P x * P y ^ 2 * W'.neg P z - 2 * P x * P y * W'.neg P y * W'.neg P z +
                              2 * P x * P y * W'.neg P y * P z -
                            W'.a₁ * P x ^ 2 * W'.neg P y * W'.neg P z +
                          W'.a₁ * P x ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * P x * W'.neg P z -
                      W'.a₂ * P x * P x ^ 2 * P z -
                    W'.a₃ * P x * P y * W'.neg P z ^ 2 +
                  W'.a₃ * P x * W'.neg P y * P z ^ 2 -
                2 * W'.a₃ * P x * W'.neg P y * P z * W'.neg P z +
              2 * W'.a₃ * P x * P y * P z * W'.neg P z +
            W'.a₄ * P x ^ 2 * W'.neg P z ^ 2 -
          W'.a₄ * P x ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * W'.neg P z ^ 2 -
      3 * W'.a₆ * P x * P z ^ 2 * W'.neg P z =
    0

Tactic:
neg_Y,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -P x * W'.negY P ^ 2 * P z + P x * P y ^ 2 * W'.neg P z - 2 * P x * P y * W'.negY P * W'.neg P z +
                              2 * P x * P y * W'.negY P * P z -
                            W'.a₁ * P x ^ 2 * W'.negY P * W'.neg P z +
                          W'.a₁ * P x ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * P x * W'.neg P z -
                      W'.a₂ * P x * P x ^ 2 * P z -
                    W'.a₃ * P x * P y * W'.neg P z ^ 2 +
                  W'.a₃ * P x * W'.negY P * P z ^ 2 -
                2 * W'.a₃ * P x * W'.negY P * P z * W'.neg P z +
              2 * W'.a₃ * P x * P y * P z * W'.neg P z +
            W'.a₄ * P x ^ 2 * W'.neg P z ^ 2 -
          W'.a₄ * P x ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * W'.neg P z ^ 2 -
      3 * W'.a₆ * P x * P z ^ 2 * W'.neg P z =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
⊢ -3 * P x ^ 2 * P x * W'.neg P y + 3 * P x * P x ^ 2 * P y - P y ^ 2 * W'.neg P y * W'.neg P z +
                                      P y * W'.neg P y ^ 2 * P z +
                                    W'.a₁ * P x * W'.neg P y ^ 2 * P z -
                                  W'.a₁ * P x * P y ^ 2 * W'.neg P z -
                                W'.a₂ * P x ^ 2 * W'.neg P y * W'.neg P z +
                              W'.a₂ * P x ^ 2 * P y * P z +
                            2 * W'.a₂ * P x * P x * P y * W'.neg P z -
                          2 * W'.a₂ * P x * P x * W'.neg P y * P z -
                        W'.a₃ * P y ^ 2 * W'.neg P z ^ 2 +
                      W'.a₃ * W'.neg P y ^ 2 * P z ^ 2 +
                    W'.a₄ * P x * P y * W'.neg P z ^ 2 -
                  2 * W'.a₄ * P x * W'.neg P y * P z * W'.neg P z +
                2 * W'.a₄ * P x * P y * P z * W'.neg P z -
              W'.a₄ * P x * W'.neg P y * P z ^ 2 +
            3 * W'.a₆ * P y * P z * W'.neg P z ^ 2 -
          3 * W'.a₆ * W'.neg P y * P z ^ 2 * W'.neg P z +
        -3 * (P y - W'.negY P) * 0 -
      (W'.dblZ P +
        -3 * (P y - W'.negY P) *
          (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))) =
    0

Tactic:
neg_Y,

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
⊢ -3 * P x ^ 2 * P x * W'.negY P + 3 * P x * P x ^ 2 * P y - P y ^ 2 * W'.negY P * W'.neg P z +
                                      P y * W'.negY P ^ 2 * P z +
                                    W'.a₁ * P x * W'.negY P ^ 2 * P z -
                                  W'.a₁ * P x * P y ^ 2 * W'.neg P z -
                                W'.a₂ * P x ^ 2 * W'.negY P * W'.neg P z +
                              W'.a₂ * P x ^ 2 * P y * P z +
                            2 * W'.a₂ * P x * P x * P y * W'.neg P z -
                          2 * W'.a₂ * P x * P x * W'.negY P * P z -
                        W'.a₃ * P y ^ 2 * W'.neg P z ^ 2 +
                      W'.a₃ * W'.negY P ^ 2 * P z ^ 2 +
                    W'.a₄ * P x * P y * W'.neg P z ^ 2 -
                  2 * W'.a₄ * P x * W'.negY P * P z * W'.neg P z +
                2 * W'.a₄ * P x * P y * P z * W'.neg P z -
              W'.a₄ * P x * W'.negY P * P z ^ 2 +
            3 * W'.a₆ * P y * P z * W'.neg P z ^ 2 -
          3 * W'.a₆ * W'.negY P * P z ^ 2 * W'.neg P z +
        -3 * (P y - W'.negY P) * 0 -
      (W'.dblZ P +
        -3 * (P y - W'.negY P) *
          (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))) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case pos
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

Tactic:
exact ⟨hu.unit ^ 4, by convert! (add_smul_of_equiv h hu hv).symm⟩

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

Goal state before:
pp: case e_a
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
hc' : IsColimit c'
k✝ : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit
k : E.toPreOneHypercover.I₁'
⊢ (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y k✝)).hom ≫
      (E.toPreOneHypercover.sigmaOfIsColimit hc hc').p₁
        ((Equiv.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit)) k✝) =
    (E.sigmaOfIsColimit hc).toPreOneHypercover.p₁ k✝ ≫
      (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.X PUnit.unit)).hom

Tactic:
exact Cofan.IsColimit.hom_ext hc' _ _ fun a ↦ by simp; simp [c']

Goal state after: