mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
r R : ℝ
h0 : 0 < r
hle : r ≤ R
f : ℂ → E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ ball c r)
hd : ∀ z ∈ (ball c R \ closedBall c r) \ s, DifferentiableAt ℂ f z
⊢ ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z

Tactic:
set A := closedBall c R \ ball c r
  obtain ⟨a, rfl⟩ : ∃ a, Real.exp a = r := ⟨Real.log r, Real.exp_log h0⟩
  obtain ⟨b, rfl⟩ : ∃ b, Real.exp b = R := ⟨Real.log R, Real.exp_log (h0.trans_le hle)⟩
  rw [Real.exp_le_exp] at hle
  -- Unfold definition of `circleIntegral` and cancel some terms.
  suffices
    (∫ θ in 0..2 * π, I • f (circleMap c (Real.exp b) θ)) =
      ∫ θ in 0..2 * π, I • f (circleMap c (Real.exp a) θ) by
    simpa only [circleIntegral, add_sub_cancel_left, ofReal_exp, ← exp_add, smul_smul, ←
      div_eq_mul_inv, mul_div_cancel_left₀ _ (circleMap_ne_center (Real.exp_pos _).ne'),
      circleMap_sub_center, deriv_circleMap]
  set R := [[a, b]] ×ℂ [[0, 2 * π]]
  set g : ℂ → ℂ := (c + exp ·)
  have hdg : Differentiable ℂ g := differentiable_exp.const_add _
  replace hs : (g ⁻¹' s).Countable := (hs.preimage (add_right_injective c)).preimage_cexp
  have h_maps : MapsTo g R A := by
    rintro z ⟨h, -⟩; simpa [g, A, dist_eq, norm_exp, hle] using h.symm
  replace hc : ContinuousOn (f ∘ g) R := hc.comp hdg.continuous.continuousOn h_maps
  replace hd : ∀ z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s,
      DifferentiableAt ℂ (f ∘ g) z := by
    refine fun z hz => (hd (g z) ⟨?_, hz.2⟩).comp z (hdg _)
    simpa [g, dist_eq, norm_exp, hle, and_comm] using hz.1.1
  simpa [g, circleMap, exp_periodic _, sub_eq_zero, ← exp_add] using
    integral_boundary_rect_eq_zero_of_differentiable_on_off_countable _ ⟨a, 0⟩ ⟨b, 2 * π⟩ _ hs hc hd

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

Goal state before:
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
hlt : ∀ (i : Fin (n + 1)), 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:
exact integral_divergence_of_hasFDerivAt_off_countable_aux₂ ⟨a, b, hlt⟩ f f' s hs Hc Hd Hi

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

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hzne : z ≠ c
hz : ‖z - c‖ = r
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))

Tactic:
norm_smul,

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hzne : z ≠ c
hz : ‖z - c‖ = r
⊢ ‖(z - c)⁻¹‖ * ‖f z - y‖ ≤ r⁻¹ * (ε / (2 * π))
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ (∑ t ∈ powersetCard n univ, AddMonoidAlgebra.single (∑ i ∈ t, Finsupp.single i 1) 1).support =
    (powersetCard n univ).biUnion fun t ↦ (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support

Tactic:
simp only [support, MvPolynomial, AddMonoidAlgebra.coeff_sum, AddMonoidAlgebra.coeff_single]

Goal state after:
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ (∑ i ∈ powersetCard n univ, Finsupp.single (∑ i ∈ i, Finsupp.single i 1) 1).support =
    (powersetCard n univ).biUnion fun t ↦ (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support
Module: Mathlib.Analysis.Complex.CauchyIntegral

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

Tactic:
by
    have hw' : c + w ∈ ball c R := by
      simpa only [add_mem_ball_iff_norm, ← coe_nnnorm, mem_eball_zero_iff,
        NNReal.coe_lt_coe, enorm_lt_coe] using hw
    rw [← two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
      hs hw' hc hd]
    exact (hasFPowerSeriesOn_cauchy_integral
      ((hc.mono sphere_subset_closedBall).circleIntegrable R.2) hR).hasSum hw

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 : ℕ
⊢ -↑C ≤ (minpoly ℤ x).coeff i ∧ (minpoly ℤ x).coeff i ≤ ↑C

Tactic:
← abs_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.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝² : Field K
k : Type u_2
inst✝¹ : Field k
inst✝ : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
ν : Gal(K/k)
⊢ IsConj (φ.comp ↑ν) (ν⁻¹ * σ * ν)

Tactic:
by
  ext
  simpa [← AlgEquiv.mul_apply, ← mul_assoc] using! RingHom.congr_fun hσ _

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

Goal state before:
pp: p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
⊢ (p.aroots ℂ).Nodup

Tactic:
exact nodup_roots ((separable_map (algebraMap ℚ ℂ)).mpr p_irr.separable)

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
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
⊢ 0 < embedRealFun y - embedRealFun x

Tactic:
hy,

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
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
⊢ 0 < embedRealFun (y - x + x) - embedRealFun x
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist x y < dist y z
⊢ max (dist x y) (dist y z) ≤ dist x z

Tactic:
rw [max_eq_right h.le]
    apply (le_max_iff.mp <| dist_triangle_max y x z).resolve_left
    simpa only [not_le, dist_comm x y] using h

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

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist y z < dist x y
⊢ dist y x ≤ dist z x

Tactic:
apply (le_max_iff.mp <| dist_triangle_max y z x).resolve_left

Goal state after:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist y z < dist x y
⊢ ¬dist y x ≤ dist y z
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
⊢ ball x r = ball y r ∨ Disjoint (ball x r) (ball y r)

Tactic:
refine Set.disjoint_or_nonempty_inter (ball x r) (ball y r) |>.symm.imp (fun h ↦ ?_) id
  have h₁ := ball_eq_of_mem <| Set.inter_subset_left h.some_mem
  have h₂ := ball_eq_of_mem <| Set.inter_subset_right h.some_mem
  exact h₁.trans h₂.symm

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 : 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])]
  simp only [dist_one_right, dist_one_left, norm_inv']

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 Γ₀
v : Valuation L Γ₀
hv : v.RankOne
x y : L
⊢ v.norm (x + y) ≤ max (v.norm x) (v.norm y)

Tactic:
simp only [norm, NNReal.coe_le_coe, le_max_iff, StrictMono.le_iff_le hv.strictMono]
  exact le_max_iff.mp (Valuation.map_add_le_max' v.restrict _ _)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsRight R
x : MvPowerSeries σ R
hx : x * φ = 0
⊢ x = 0

Tactic:
ext d

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsRight R
x : MvPowerSeries σ R
hx : x * φ = 0
d : σ →₀ ℕ
⊢ (coeff d) x = (coeff d) 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsLeft R
x : MvPowerSeries σ R
hx : φ * x = 0
⊢ x = 0

Tactic:
ext d

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsLeft R
x : MvPowerSeries σ R
hx : φ * x = 0
d : σ →₀ ℕ
⊢ (coeff d) x = (coeff d) 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
this : (0, n) ∈ antidiagonal n
⊢ ∑ x ∈ (antidiagonal n).erase (0, n), (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) =
    ∑ x ∈ (antidiagonal n).erase (0, n), if x.2 < (0, n).2 then (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) else 0

Tactic:
Finset.sum_congr rfl

Goal state after:
σ : 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
this : (0, n) ∈ antidiagonal n
⊢ ((antidiagonal n).erase (0, n)).sum ?m.201 =
    ∑ x ∈ (antidiagonal n).erase (0, n), if x.2 < (0, n).2 then (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) else 0

σ : 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
this : (0, n) ∈ antidiagonal n
⊢ ∀ x ∈ (antidiagonal n).erase (0, n), (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) = ?m.201 x

σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : constantCoeff φ = ↑u
n : σ →₀ ℕ
this✝ : DecidableEq (σ →₀ ℕ) := ⋯
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
⊢ (σ →₀ ℕ) × (σ →₀ ℕ) → R
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
⊢ weightedOrder w (f * g) = weightedOrder w f + weightedOrder w g

Tactic:
apply le_antisymm _ (le_weightedOrder_mul w)

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
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:
rw [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.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 *
            { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₈ -
          8 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₄ ^ 3 -
        27 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₆ ^ 2 +
      9 *
            ({ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ ^ 2 +
              4 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₂) *
          { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₄ *
        { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.b₆ =
    -27

Tactic:
b₄,

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

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

Tactic:
b₄,

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

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P

Tactic:
· rw [neg_of_Z_ne_zero hPz, toAffine_smul _ <| Ne.isUnit hPz, toAffine_some <|
        (nonsingular_smul _ <| Ne.isUnit hPz).mp <| neg_of_Z_ne_zero hPz ▸ nonsingular_neg hP,
      toAffine_of_Z_ne_zero hP hPz, Affine.Point.neg_some]

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

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : f (P z) = 0
⊢ P ≈ Q

Tactic:
exact equiv_of_Z_eq_zero hP hQ ((map_eq_zero_iff f f.injective).mp hz) <|
        (map_eq_zero_iff f f.injective).mp <| (Z_eq_zero_of_equiv h).mp hz

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

Goal state before:
pp: X : TopCat
⊢ ∀ ⦃X_1 : TopCat⦄ (E : precoverage.ZeroHypercover X_1), Presieve.IsSheafFor (yoneda.obj X) E.presieve₀

Tactic:
intro Y 𝒰

Goal state after:
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
⊢ Presieve.IsSheafFor (yoneda.obj X) 𝒰.presieve₀
Module: Mathlib.RingTheory.Smooth.Locus

Goal state before:
pp: case e'_2
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
this✝ : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[A] Ω[Localization.Away f⁄R]
this : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[Localization.Away f] Ω[Localization.Away f⁄R]
⊢ Module.Projective (Localization.Away f) Ω[Localization.Away f⁄R] ↔
    Module.Projective (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])

Tactic:
exact ⟨fun _ ↦ .of_equiv this.symm, fun _ ↦ .of_equiv this⟩

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
hy' : (eval P) W.polynomialY = (P y - W.negY P) * P z
⊢ W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (P y - W.negY P) * P z ≠ 0) ↔ W.Equation P ∧ (eval P) W.polynomialX ≠ 0

Tactic:
hy,

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
hy' : (eval P) W.polynomialY = (P y - W.negY P) * P z
⊢ W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (W.negY P - W.negY P) * P z ≠ 0) ↔
    W.Equation P ∧ (eval P) W.polynomialX ≠ 0
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
this : ∀ (k : L), ∃! g, (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)
⊢ ∃ a, (Ideal.Quotient.mkₐ K I).comp a = f

Tactic:
choose g hg₁ hg₂ using this

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
⊢ ∃ a, (Ideal.Quotient.mkₐ K I).comp a = f
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case refine_5
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
H : ∀ (x y : L), ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
r : K
⊢ (g ((algebraMap K L) r)) ((algebraMap K ↥K⟮(algebraMap K L) r⟯) r) = (algebraMap K B) r

Tactic:
rw [AlgHom.commutes]

Goal state after:
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case mpr
K : Type u_1
A : Type u
inst✝² : Field K
inst✝¹ : CommRing A
inst✝ : Algebra K A
I : Type u
w✝² : Finite I
Ai : I → Type u
w✝¹ : (i : I) → Field (Ai i)
w✝ : (i : I) → Algebra K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
H : ∀ (i : I), Module.Finite K (Ai i) ∧ Algebra.IsSeparable K (Ai i)
⊢ Etale K A

Tactic:
choose h₁ h₂ using H

Goal state after:
case mpr
K : Type u_1
A : Type u
inst✝² : Field K
inst✝¹ : CommRing A
inst✝ : Algebra K A
I : Type u
w✝² : Finite I
Ai : I → Type u
w✝¹ : (i : I) → Field (Ai i)
w✝ : (i : I) → Algebra K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
h₁ : ∀ (i : I), Module.Finite K (Ai i)
h₂ : ∀ (i : I), Algebra.IsSeparable K (Ai i)
⊢ Etale K A
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
x : AdicCauchySequence I N
n : ℕ
y yₙ : M
hy : f y = ↑x (n + 1)
hyₙ : f yₙ = ↑x n
⊢ ↑x n - f y ∈ I ^ n • ⊤

Tactic:
hy,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
x : AdicCauchySequence I N
n : ℕ
y yₙ : M
hy : f y = ↑x (n + 1)
hyₙ : f yₙ = ↑x n
⊢ ↑x n - ↑x (n + 1) ∈ I ^ n • ⊤
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R✝¹ : Type u_1
S✝ : Type u_2
inst✝⁹ : CommRing R✝¹
inst✝⁸ : CommRing S✝
I✝ : Ideal R✝¹
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R✝¹ M
R✝ : Type u_4
S : Type u_5
inst✝⁵ : NonAssocSemiring R✝
inst✝⁴ : CommRing S
I : Ideal S
f✝ : (n : ℕ) → R✝ →+* S ⧸ I ^ n
hf✝ : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f✝ n) = f✝ m
R : Type u_6
A : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m
m✝ n✝ : ℕ
hle : m✝ ≤ n✝
x : A
⊢ ((Ideal.Quotient.factorPow I hle).comp (f n✝).toRingHom) x = (f m✝).toRingHom x

Tactic:
exact congr($(hf hle) x)

Goal state after: