mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (((∫ (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:
set e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
  have he : ∀ x y : ℝ, ↑x + ↑y * I = e (x, y) := fun x y => (mk_eq_add_mul_I x y).symm
  have he₁ : e (1, 0) = 1 := rfl; have he₂ : e (0, 1) = I := rfl
  simp only [he] at *
  set F : ℝ × ℝ → E := f ∘ e
  set F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp (e : ℝ × ℝ →L[ℝ] ℂ)
  have hF' : ∀ p : ℝ × ℝ, (-(I • F' p)) (1, 0) + F' p (0, 1) = -(I • f' (e p) 1 - f' (e p) I) := by
    rintro ⟨x, y⟩
    simp only [F', neg_apply, smul_apply, ContinuousLinearMap.comp_apply,
      ContinuousLinearEquiv.coe_coe, he₁, he₂, neg_add_eq_sub, neg_sub]
  set R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]
  set t : Set (ℝ × ℝ) := e ⁻¹' s
  rw [uIcc_comm z.im] at Hc Hi; rw [min_comm z.im, max_comm z.im] at Hd
  have hR : e ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R := rfl
  have htc : ContinuousOn F R := Hc.comp e.continuousOn hR.ge
  have htd :
    ∀ p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max w.im z.im) \ t,
      HasFDerivAt F (F' p) p :=
    fun p hp => (Hd (e p) hp).comp p e.hasFDerivAt
  simp_rw [← intervalIntegral.integral_smul, intervalIntegral.integral_symm w.im z.im, ←
    intervalIntegral.integral_neg, ← hF']
  refine (integral2_divergence_prod_of_hasFDerivAt_off_countable (fun p => -(I • F p)) F
    (fun p => -(I • F' p)) F' z.re w.im w.re z.im t (hs.preimage e.injective)
    (htc.const_smul _).neg htc (fun p hp => ((htd p hp).const_smul I).neg) htd ?_).symm
  rw [← (volume_preserving_equiv_real_prod.symm _).integrableOn_comp_preimage
    (MeasurableEquiv.measurableEmbedding _)] at Hi
  simpa only [hF'] using! Hi.neg

Goal state after:
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 := ⋯
this✝ : Fact (μ U < ∞)
V : Set Y := ⋯
this : Fact (ν V < ∞)
⊢ IntegrableOn (uncurry f) (tsupport (uncurry f)) ((μ.restrict U).prod (ν.restrict V))

Tactic:
refine ⟨(h'f.stronglyMeasurable_of_prod hf).aestronglyMeasurable, ?_⟩

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 < ∞)
⊢ HasFiniteIntegral (uncurry f) (((μ.restrict U).prod (ν.restrict V)).restrict (tsupport (uncurry f)))
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case inl
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i ↦ Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
⊢ ∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i, (f' x) (e i) i =
    ∑ i,
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)

pp: case inr
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i ↦ Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Set.Icc a b) volume
hne : ¬∃ i, a i = b i
⊢ ∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i, (f' x) (e i) i =
    ∑ i,
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)

Tactic:
· -- First we sort out the trivial case `∃ i, a i = b i`.
    rw [volume_pi, ← setIntegral_congr_set Measure.univ_pi_Ioc_ae_eq_Icc]
    have hi' : Ioc (a i) (b i) = ∅ := Ioc_eq_empty hi.not_lt
    have : (pi Set.univ fun j => Ioc (a j) (b j)) = ∅ := univ_pi_eq_empty hi'
    rw [this, setIntegral_empty, sum_eq_zero]
    rintro j -
    rcases eq_or_ne i j with (rfl | hne)
    · simp [hi]
    · rcases Fin.exists_succAbove_eq hne with ⟨i, rfl⟩
      have : Icc (a ∘ j.succAbove) (b ∘ j.succAbove) =ᵐ[volume] (∅ : Set ℝⁿ) := by
        rw [ae_eq_empty, Real.volume_Icc_pi, prod_eq_zero (Finset.mem_univ i)]
        simp [hi]
      rw [setIntegral_congr_set this, setIntegral_congr_set this, setIntegral_empty,
        setIntegral_empty, sub_self]

Goal state after:
case inr
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i ↦ Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Set.Icc a b) volume
hne : ¬∃ i, a i = b i
⊢ ∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i, (f' x) (e i) i =
    ∑ i,
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (map (algebraMap F E) p).Splits
ϕ : p.Gal
hϕ : (galActionHom p E) ϕ = 1
x : p.SplittingField
hx : x ∈ p.rootSet p.SplittingField
⊢ ϕ x = 1 x

Tactic:
have key := Equiv.Perm.ext_iff.mp hϕ (rootsEquivRoots p E ⟨x, hx⟩)

Goal state after:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (map (algebraMap F E) p).Splits
ϕ : p.Gal
hϕ : (galActionHom p E) ϕ = 1
x : p.SplittingField
hx : x ∈ p.rootSet p.SplittingField
key : ((galActionHom p E) ϕ) ((rootsEquivRoots p E) ⟨x, hx⟩) = 1 ((rootsEquivRoots p E) ⟨x, hx⟩)
⊢ ϕ x = 1 x
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : p * q = 0
⊢ Unique (Gal 0)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case hg
F : Type u_1
inst✝ : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : (map (algebraMap F q₁.SplittingField) p₁).Splits
h₂ : (map (algebraMap F q₂.SplittingField) p₂).Splits
⊢ (map (↑(SplittingField.lift q₂ ⋯)) (map (algebraMap F q₂.SplittingField) p₂)).Splits

Tactic:
exact h₂.map _

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 σ
n : ℕ
⊢ (esymm σ R n).IsSymmetric

Tactic:
intro

Goal state after:
σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
n : ℕ
e✝ : Perm σ
⊢ (rename ⇑e✝) (esymm σ R n) = esymm σ R n
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
⊢ ∀ (x : { x // Nat.Partition.ofSym x = μ }),
    (rename ⇑e) (Multiset.map X ↑↑x).prod = (Multiset.map X ↑↑((μ.ofSymShapeEquiv e) x)).prod

Tactic:
intro

Goal state after:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
x✝ : { x // Nat.Partition.ofSym x = μ }
⊢ (rename ⇑e) (Multiset.map X ↑↑x✝).prod = (Multiset.map X ↑↑((μ.ofSymShapeEquiv e) x✝)).prod
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℚ[X]
hp : p = 0
⊢ IsEmpty ↑∅

Tactic:
infer_instance

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
A : Type u_2
inst✝³ : Field A
inst✝² : CharZero A
inst✝¹ : NumberField K
inst✝ : IsAlgClosed A
⊢ 0 < Fintype.card (K →+* A)

Tactic:
NumberField.Embeddings.card K A

Goal state after:
K : Type u_1
inst✝⁴ : Field K
A : Type u_2
inst✝³ : Field A
inst✝² : CharZero A
inst✝¹ : NumberField K
inst✝ : IsAlgClosed A
⊢ 0 < finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: case refine_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))⌉₊
this :
  (⋃ f,
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C),
        ↑(map (algebraMap ℤ K) f).roots.toFinset).Finite
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
⊢ ↑|(minpoly ℤ x).coeff i| = ‖(minpoly ℚ x).coeff i‖

Tactic:
rw [h_map_ℚ_minpoly, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs]

Goal state after:
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: case refine_3
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : {x | x ≤ 1}.WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ Set.MapsTo (fun x ↦ if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1) (Set.range (⇑v ∘ ⇑(algebraMap O F)))
    {x | x ≤ 1}

Tactic:
intro

Goal state after:
case refine_3
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : {x | x ≤ 1}.WellFoundedOn fun x1 x2 ↦ x1 > x2
x✝ : Γ₀
⊢ x✝ ∈ Set.range (⇑v ∘ ⇑(algebraMap O F)) →
    (fun x ↦ if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1) x✝ ∈ {x | x ≤ 1}
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
hlt : b < a
⊢ x ^ (a - b) = 1

Tactic:
← Nat.sub_add_cancel hlt.le,

Goal state after:
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ (a - b + b) = x ^ b
hlt : b < a
⊢ x ^ (a - b) = 1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝ : Field K
⊢ Function.Involutive conjugate

Tactic:
intro

Goal state after:
K : Type u_1
inst✝ : Field K
x✝ : K →+* ℂ
⊢ conjugate (conjugate x✝) = x✝
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

Tactic:
rcases isEmpty_or_nonempty ι with hι | hι

Goal state after:
case inl
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : IsEmpty ι
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

case inr
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

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

Tactic:
intro H p hrp
    ext i
    have := congr(coeff (i + n) $hrp)
    rw [coeff_monomial_mul, if_pos le_add_self, add_tsub_cancel_right] at this
    simpa using H _ this

Goal state after:
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
x y : L
⊢ ↑((RankOne.hom v) (v.restrict (x - y))) = ↑((RankOne.hom v) (v.restrict (-x + y)))

Tactic:
rw [← v.restrict.map_neg, neg_sub, sub_eq_add_neg, add_comm]

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

Goal state before:
pp: k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ Inv_divided_by_X_pow_order hf * f.divXPowOrder = 1

Tactic:
mul_comm

Goal state after:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ f.divXPowOrder * Inv_divided_by_X_pow_order hf = 1
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
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ ‖(embedding v) ((algebraMap R K) x)‖ ≤ 1

Tactic:
rw [norm_embedding]

Goal state after:
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
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ (HeightOneSpectrum.adicAbv K v) ((algebraMap R K) x) ≤ 1
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
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ ‖(embedding v) ((algebraMap R K) x)‖ = 1 ↔ x ∉ v.asIdeal

Tactic:
rw [norm_embedding]

Goal state after:
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
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ (HeightOneSpectrum.adicAbv K v) ((algebraMap R K) x) = 1 ↔ x ∉ v.asIdeal
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
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ ‖(embedding v) ((algebraMap R K) x)‖ < 1 ↔ x ∈ v.asIdeal

Tactic:
rw [norm_embedding]

Goal state after:
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
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ (HeightOneSpectrum.adicAbv K v) ((algebraMap R K) x) < 1 ↔ x ∈ v.asIdeal
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 }.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

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 *
        (2 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₄ +
          { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₃) =
    0
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 }.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

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 *
        (2 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₄ +
          { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₁ * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₃) =
    -48
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
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
this : Fact (IsUnit 2)
⊢ (ofJ1728 F).IsElliptic

Tactic:
infer_instance

Goal state after:
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
h3 : ¬3 = 0
this : Fact (IsUnit 3)
⊢ (ofJ0 F).IsElliptic

Tactic:
infer_instance

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

Goal state before:
pp: case pos
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
h1728 : j = 1728
h2 : 2 ≠ 0
this : Fact (IsUnit 2)
⊢ (ofJ1728 F).IsElliptic

Tactic:
infer_instance

Goal state after:
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
h1728 : ¬j = 1728
this : Fact (IsUnit j)
⊢ (ofJ j).IsElliptic

Tactic:
have := Fact.mk (sub_ne_zero.2 h1728).isUnit

Goal state after:
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
h1728 : ¬j = 1728
this✝ : Fact (IsUnit j)
this : Fact (IsUnit (j - 1728))
⊢ (ofJ j).IsElliptic
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
h1728 : ¬j = 1728
this✝ : Fact (IsUnit j)
this : Fact (IsUnit (j - 1728))
⊢ (ofJNe0Or1728 j).IsElliptic

Tactic:
infer_instance

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

Goal state before:
pp: case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
this : Fact (IsUnit j)
⊢ (ofJ j).j = j

Tactic:
have := Fact.mk (sub_ne_zero.2 h1728).isUnit

Goal state after:
case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
this✝ : Fact (IsUnit j)
this : Fact (IsUnit (j - 1728))
⊢ (ofJ j).j = j
Module: Mathlib.AlgebraicGeometry.Geometrically.Connected

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : GeometricallyConnected f
inst✝² : GeometricallyConnected g
inst✝¹ : UniversallyOpen f
inst✝ : UniversallyOpen g
K : Type u_1
x✝ : Field K
x : Spec (CommRingCat.of K) ⟶ Z
⊢ ConnectedSpace ↥(pullback f (pullback.fst g x))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.Pretopology

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsMultiplicative
X : Scheme
S : Sieve X
x✝ : ∃ R ∈ (precoverage P).coverings X, R ≤ S.arrows
R : Presieve X
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
hle : R ≤ S.arrows
⊢ ∃ 𝒰, Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows

Tactic:
obtain ⟨(𝒰 : Scheme.Cover _ _), rfl⟩ := hR

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsMultiplicative
X : Scheme
S : Sieve X
x✝ : ∃ R ∈ (precoverage P).coverings X, R ≤ S.arrows
𝒰 : Cover (precoverage P) X
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
⊢ ∃ 𝒰, Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ W'.polynomialY = C 2 * Y * Z + C W'.a₁ * X * Z + C W'.a₃ * Z ^ 2

Tactic:
polynomialY,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ (pderiv y) W'.polynomial = C 2 * Y * Z + C W'.a₁ * X * Z + C W'.a₃ * Z ^ 2