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) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ y ∈ Box.Icc I, ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖
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)
Hi : ∀ x ∈ Set.Icc (I.lower i) (I.upper i), Integrable (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ y ∈ Box.Icc (I.face i),
    ‖f' (Pi.single i (I.upper i - I.lower i)) - (f (e (I.upper i) y) - f (e (I.lower i) y))‖ ≤ 2 * ε * diam (Box.Icc I)
⊢ ‖(∏ j, (I.upper j - I.lower j)) • f' (Pi.single i 1) -
        (integral (I.face i) ⊥ (f ∘ e (I.upper i)) BoxAdditiveMap.volume -
          integral (I.face i) ⊥ (f ∘ e (I.lower i)) BoxAdditiveMap.volume)‖ ≤
    2 * ε * ↑c * ∏ j, (I.upper j - I.lower j)

Tactic:
calc
    ‖(∏ j, (I.upper j - I.lower j)) • f' (Pi.single i 1) -
            (integral (I.face i) ⊥ (f ∘ e (I.upper i)) BoxAdditiveMap.volume -
              integral (I.face i) ⊥ (f ∘ e (I.lower i)) BoxAdditiveMap.volume)‖ =
        ‖integral.{0, u, u} (I.face i) ⊥
            (fun x : Fin n → ℝ =>
              f' (Pi.single i (I.upper i - I.lower i)) -
                (f (e (I.upper i) x) - f (e (I.lower i) x)))
            BoxAdditiveMap.volume‖ := by
      rw [← integral_sub (Hi _ Hu) (Hi _ Hl), ← Box.volume_face_mul i, mul_smul, ← Box.volume_apply,
        ← BoxAdditiveMap.toSMul_apply, ← integral_const, ← BoxAdditiveMap.volume,
        ← integral_sub (integrable_const _) ((Hi _ Hu).sub (Hi _ Hl))]
      simp only [(· ∘ ·), Pi.sub_def, ← f'.map_smul, ← Pi.single_smul', smul_eq_mul, mul_one]
    _ ≤ (volume (I.face i : Set (Fin n → ℝ))).toReal * (2 * ε * c * (I.upper i - I.lower i)) := by
      -- The hard part of the estimate was done above, here we just replace `diam I.Icc`
      -- with `c * (I.upper i - I.lower i)`
      refine norm_integral_le_of_le_const (fun y hy => (this y hy).trans ?_) volume
      rw [mul_assoc (2 * ε)]
      gcongr
      exact I.diam_Icc_le_of_distortion_le i hc
    _ = 2 * ε * c * ∏ j, (I.upper j - I.lower j) := by
      rw [← measureReal_def, ← Measure.toBoxAdditive_apply, Box.volume_apply,
        ← I.volume_face_mul i]
      ac_rfl

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

Goal state before:
pp: case e'_2
α : 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 μ
hE : CompleteSpace E
f g : α × β → E
hfg : f =ᵐ[μ.prod ν] g
hf : ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ ∫ (z : α × β), g z ∂μ.prod ν = ∫ (z : α × β), f z ∂μ.prod ν

Tactic:
exact integral_congr_ae hfg.symm

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

Goal state before:
pp: case inr
α : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
a b : ℝ
f : ℝ → α → E
h_int : Integrable (uncurry f) ((volume.restrict (uIoc a b)).prod μ)
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, ∫ (y : α), f x y ∂μ = ∫ (y : α), ∫ (x : ℝ) in a..b, f x y ∂μ

Tactic:
intervalIntegral.integral_of_ge hab

Goal state after:
case inr
α : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
a b : ℝ
f : ℝ → α → E
h_int : Integrable (uncurry f) ((volume.restrict (uIoc a b)).prod μ)
hab : b ≤ a
⊢ -∫ (x : ℝ) in Ioc b a, ∫ (y : α), f x y ∂μ ∂volume = ∫ (y : α), -∫ (x : ℝ) in Ioc b a, f x y ∂volume ∂μ
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
⊢ ∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp a) θ)

Tactic:
set R := [[a, b]] ×ℂ [[0, 2 * π]]

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
⊢ ∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp a) θ)
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
ϕ : Gal(E/F)
x : ↑(p.rootSet E)
ψ : p.SplittingField ≃ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
⊢ ↑((restrict p E) ϕ • x) = ϕ ↑x

Tactic:
change ↑(ψ (ψ.symm _)) = ϕ x

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
ϕ : Gal(E/F)
x : ↑(p.rootSet E)
ψ : p.SplittingField ≃ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
⊢ ↑(ψ
        (ψ.symm
          (↑((↑ϕ).restrictNormalAux p.SplittingField)
            (↑↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E))
              ↑((rootsEquivRoots p E).symm x))))) =
    ϕ ↑x
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
⊢ ∀ (a : p.Gal), (galActionHom p E) a = 1 → a = 1

Tactic:
intro ϕ hϕ

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
⊢ ϕ = 1
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case refine_2
E : Type u
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : Preorder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y
he_vol : MeasurePreserving (⇑eL) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i, (f' i x) (eL.symm (e i))
Hi : IntegrableOn DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding ⇑eL
hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b
hIcc' : Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b
x : Fin (n + 1) → ℝ
hx : x ∈ (Set.univ.pi fun i ↦ Set.Ioo (eL a i) (eL b i)) \ ⇑eL.symm ⁻¹' s
i : Fin (n + 1)
⊢ eL.symm x ∈ interior (⇑eL ⁻¹' Set.Icc (eL a) (eL b))

Tactic:
refine preimage_interior_subset_interior_preimage eL.continuous ?_

Goal state after:
case refine_2
E : Type u
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : Preorder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y
he_vol : MeasurePreserving (⇑eL) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i, (f' i x) (eL.symm (e i))
Hi : IntegrableOn DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding ⇑eL
hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b
hIcc' : Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b
x : Fin (n + 1) → ℝ
hx : x ∈ (Set.univ.pi fun i ↦ Set.Ioo (eL a i) (eL b i)) \ ⇑eL.symm ⁻¹' s
i : Fin (n + 1)
⊢ eL.symm x ∈ ⇑eL ⁻¹' interior (Set.Icc (eL a) (eL b))
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
⊢ (map (prod ∘ map Neg.neg) (powersetCard k s)).sum = (map (fun i ↦ (-1) ^ k * i.prod) (powersetCard k s)).sum

Tactic:
map_congr rfl

Goal state after:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
⊢ (map ?m.56 (powersetCard k s)).sum = (map (fun i ↦ (-1) ^ k * i.prod) (powersetCard k s)).sum

R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
⊢ ∀ x ∈ powersetCard k s, (prod ∘ map Neg.neg) x = ?m.56 x

R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
⊢ Multiset R → R
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case inl
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : B < 0
⊢ ‖if i = 0 then 1 else 0‖ ≤ ↑(Nat.choose 0 i)

Tactic:
split_ifs with h

Goal state after:
case pos
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : B < 0
h : i = 0
⊢ ‖1‖ ≤ ↑(Nat.choose 0 i)

case neg
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : B < 0
h : ¬i = 0
⊢ ‖0‖ ≤ ↑(Nat.choose 0 i)
Module: Mathlib.Topology.Algebra.Polynomial

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

Tactic:
rw [coeff_eq_zero_of_natDegree_lt hi, norm_zero]
    positivity

Goal state after:
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 ∈ Icc (-↑C) ↑C

Tactic:
rw [mem_Icc, ← abs_le, ← @Int.cast_le ℝ]

Goal state after:
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| ≤ ↑↑C
Module: Mathlib.Analysis.Normed.Group.Ultra

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

Tactic:
rw [← inv_inv x, ← dist_eq_norm_inv_mul, dist_eq_max_of_dist_ne_dist _ 1 _ (by simp [h])]

Goal state after:
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y : S
h : ‖x‖ ≠ ‖y‖
⊢ max (dist x⁻¹ 1) (dist 1 y) = max ‖x⁻¹⁻¹‖ ‖y‖
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
⊢ (if h : φ = 0 then ⊤
      else
        have ne := ⋯;
        ↑(⋯.min (⇑toLex '' Function.support φ) ne)) =
      ⊤ ↔
    φ = 0

Tactic:
split_ifs with h

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

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : constantCoeff φ = ↑u
n : σ →₀ ℕ
this : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
⊢ (coeff n) (φ * φ.invOfUnit u) = (coeff n) 1

Tactic:
classical
      have : ((0 : σ →₀ ℕ), n) ∈ antidiagonal n := by rw [mem_antidiagonal, zero_add]
      rw [coeff_one, if_neg H, coeff_mul, ← Finset.insert_erase this,
        Finset.sum_insert (Finset.notMem_erase _ _), coeff_zero_eq_constantCoeff_apply, h,
        coeff_invOfUnit, if_neg H, neg_mul, mul_neg, Units.mul_inv_cancel_left, ←
        Finset.insert_erase this, Finset.sum_insert (Finset.notMem_erase _ _),
        Finset.insert_erase this, if_neg (not_lt_of_ge <| le_rfl), zero_add, add_comm, ←
        sub_eq_add_neg, sub_eq_zero, Finset.sum_congr rfl]
      rintro ⟨i, j⟩ hij
      rw [Finset.mem_erase, mem_antidiagonal] at hij
      obtain ⟨h₁, rfl⟩ := hij
      rw [if_pos]
      refine lt_add_of_pos_left _ <| pos_iff_ne_zero.2 ?_
      rintro rfl
      simp at h₁

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

Goal state before:
pp: k : Type u_2
inst✝ : Field k
n : ℕ
φ : k⟦X⟧
⊢ (coeff n) φ⁻¹ =
    if n = 0 then (constantCoeff φ)⁻¹
    else -(constantCoeff φ)⁻¹ * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) φ⁻¹ else 0

Tactic:
inv_eq_inv_aux,

Goal state after:
k : Type u_2
inst✝ : Field k
n : ℕ
φ : k⟦X⟧
⊢ (coeff n) (inv.aux (constantCoeff φ)⁻¹ φ) =
    if n = 0 then (constantCoeff φ)⁻¹
    else
      -(constantCoeff φ)⁻¹ *
        ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) (inv.aux (constantCoeff φ)⁻¹ φ) else 0
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case right
k : Type u_2
inst✝ : Field k
⊢ ∀ (J : Ideal k⟦X⟧) (x : k⟦X⟧), Ideal.span {X} ≤ J → x ∉ Ideal.span {X} → x ∈ J → 1 ∈ J

Tactic:
intro I f hI hfX hfI
      rw [Ideal.mem_span_singleton, X_dvd_iff] at hfX
      have hfI0 : C (f 0) ∈ I := by
        have : C (f 0) = f - (f - C (f 0)) := by rw [sub_sub_cancel]
        rw [this]
        apply Ideal.sub_mem I hfI
        apply hI
        rw [Ideal.mem_span_singleton, X_dvd_iff, map_sub, constantCoeff_C, ←
          coeff_zero_eq_constantCoeff_apply, sub_eq_zero, coeff_zero_eq_constantCoeff]
        rfl
      rw [← Ideal.eq_top_iff_one]
      apply Ideal.eq_top_of_isUnit_mem I hfI0 (IsUnit.map C (Ne.isUnit hfX))

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
a : v₁ = v₂
⊢ mk v₁ = mk v₂

Tactic:
rw [a]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
⊢ ∃ x ∈ v₁.asIdeal, x ∉ v₂.asIdeal

Tactic:
by
    by_contra! H
    exact h <| HeightOneSpectrum.ext_iff.mpr <| IsMaximal.eq_of_le (isMaximal v₁) IsPrime.ne_top' H

Goal state after:
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
⊢ Function.Bijective (E.multifork F).toSections

Tactic:
refine ⟨fun s t hst ↦ ?_, fun s ↦ ?_⟩

Goal state after:
case refine_1
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
s t : (E.multifork F).pt
hst : (E.multifork F).toSections s = (E.multifork F).toSections t
⊢ s = t

case refine_2
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
s : (E.multicospanIndex F).sections
⊢ ∃ a, (E.multifork F).toSections a = s
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.polynomialX / P z ^ 2 +
        (W.a₁ * P y / P z * 1 + 2 * W.a₂ * P x / P z * (P z / P z) + W.a₄ * (P z ^ 2 / P z ^ 2)) -
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialX +
        (W.a₁ * P y / P z * (P z / P z) + 2 * W.a₂ * P x / P z * 1 + W.a₄ * 1)) =
    0

Tactic:
(rw [eval_polynomialX, Affine.evalEval_polynomialX]; ring1)

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

Goal state before:
pp: case refine_1
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'
⊢ ∀ ⦃i j : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀⦄ (k : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ i j),
    (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y k)).hom ≫
        (E.toPreOneHypercover.sigmaOfIsColimit hc hc').p₁
          ((Equiv.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ i j)) k) =
      (E.sigmaOfIsColimit hc).toPreOneHypercover.p₁ k ≫ (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.X i)).hom

Tactic:
intro ⟨⟩

Goal state after:
case refine_1
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'
⊢ ∀ ⦃j : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀⦄
    (k : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit j),
    (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y k)).hom ≫
        (E.toPreOneHypercover.sigmaOfIsColimit hc hc').p₁
          ((Equiv.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit j)) k) =
      (E.sigmaOfIsColimit hc).toPreOneHypercover.p₁ k ≫
        (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.X PUnit.unit)).hom
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ 3 * (eval P) W'.polynomial =
    P x * (eval P) W'.polynomialX + P y * (eval P) W'.polynomialY + P z * (eval P) W'.polynomialZ

Tactic:
by
  rw [eval_polynomial, eval_polynomialX, eval_polynomialY, eval_polynomialZ]
  ring1

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

Goal state before:
pp: case refine_2
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'
⊢ ∀ ⦃i j : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀⦄ (k : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ i j),
    (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y k)).hom ≫
        (E.toPreOneHypercover.sigmaOfIsColimit hc hc').p₂
          ((Equiv.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ i j)) k) =
      (E.sigmaOfIsColimit hc).toPreOneHypercover.p₂ k ≫ (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.X j)).hom

Tactic:
intro ⟨⟩

Goal state after:
case refine_2
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'
⊢ ∀ ⦃j : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₀⦄
    (k : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit j),
    (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y k)).hom ≫
        (E.toPreOneHypercover.sigmaOfIsColimit hc hc').p₂
          ((Equiv.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit j)) k) =
      (E.sigmaOfIsColimit hc).toPreOneHypercover.p₂ k ≫ (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.X j)).hom