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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this : ∫ (y : AddCircle T), f y ∂Measure.map (fun x ↦ ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
⊢ ∫ (a : ℝ) in Ioc t (t + T), f ↑a = ∫ (b : AddCircle T), f b

Tactic:
rw [← (AddCircle.measurePreserving_mk T t).map_eq, ← integral_subtype m, ← this]

Goal state after:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this : ∫ (y : AddCircle T), f y ∂Measure.map (fun x ↦ ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
⊢ ∫ (y : AddCircle T), f y ∂Measure.map (fun x ↦ ↑↑x) volume =
    ∫ (b : AddCircle T), f b ∂Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T)))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
h₁f : Periodic f T
hT : T ≠ 0
h₂f : IntervalIntegrable f volume 0 T
a₁ a₂ : ℝ
⊢ IntervalIntegrable f volume 0 (0 + T)

Tactic:
simpa

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a ∈ Ici a₀
x : ℝ
⊢ ‖(Ioi a).indicator f x‖ ≤ (Ioi a₀).indicator (norm ∘ f) x

Tactic:
norm_indicator_eq_indicator_norm

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a ∈ Ici a₀
x : ℝ
⊢ (Ioi a).indicator (fun a ↦ ‖f a‖) x ≤ (Ioi a₀).indicator (norm ∘ f) x
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 (Ioi a₀) μ
⊢ ContinuousOn (fun b ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀)

Tactic:
intro a (ha : a₀ ≤ a)
  rw [continuousWithinAt_iff_continuous_left_right]
  constructor
  · rw [Ici_inter_Iic]
    have h_int : IntervalIntegrable f μ a₀ a :=
      (intervalIntegrable_iff_integrableOn_Ioc_of_le ha).2 <| hf.mono_set Ioc_subset_Ioi_self
    have h_split : ∀ b ∈ Icc a₀ a, ∫ x in Ioi b, f x ∂μ =
        (∫ x in Ioi a₀, f x ∂μ) - ∫ x in a₀..b, f x ∂μ := by
      intro b hb
      simp [← integral_Ioi_sub_Ioi hf hb.1]
    have h_cwa : ContinuousWithinAt (fun b ↦ ∫ x in a₀..b, f x ∂μ) (Icc a₀ a) a :=
      continuousWithinAt_primitive (measure_singleton a) (by simpa [ha])
    exact (continuousWithinAt_const.sub h_cwa).congr h_split (h_split a (right_mem_Icc.2 ha))
  · simpa [ha] using (hf.mono_set (Ioi_subset_Ioi ha)).continuousWithinAt_Ici_primitive_Ioi

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
x : ℝ
⊢ ‖(Iio a).indicator f x‖ ≤ (Iio a₀).indicator (norm ∘ f) x

Tactic:
norm_indicator_eq_indicator_norm

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
x : ℝ
⊢ (Iio a).indicator (fun a ↦ ‖f a‖) x ≤ (Iio a₀).indicator (norm ∘ f) x
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ ↥(Lp E 1 (μ.prod ν)) → ℝ≥0∞

Tactic:
exact fun i => ∫⁻ x, ∫⁻ y, ‖i (x, y) - g (x, y)‖ₑ ∂ν ∂μ

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

Goal state before:
pp: c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
n : ℕ
hn : n ≠ 0
⊢ -↑n - 1 ≠ -1

Tactic:
simpa

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
p q : F[X]
inst✝ : Decidable (q = 0)
hpq : p ∣ q
⊢ restrictDvd hpq = if hq : q = 0 then 1 else restrict p q.SplittingField

Tactic:
by
  unfold restrictDvd
  congr

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 (algebraMap F (q₁ * q₂).SplittingField) p₂).Splits

Tactic:
←
      (SplittingField.lift q₂
          ((SplittingField.splits _).of_dvd (map_ne_zero (mul_ne_zero hq₁ hq₂))
             ((map_dvd_map' _).mpr (dvd_mul_left q₂ q₁)))).comp_algebraMap,

Goal state after:
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₂ ⋯)).comp (algebraMap F q₂.SplittingField)) p₂).Splits
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this✝ : (⇑Finsupp.toMultiset ∘ fun t ↦ ∑ i ∈ t, Finsupp.single i 1) = val
this : ((powersetCard n univ).sup fun x ↦ x).val = (powersetCard n univ).sup val
⊢ (powersetCard n univ).sup val = univ.val

Tactic:
← this

Goal state after:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this✝ : (⇑Finsupp.toMultiset ∘ fun t ↦ ∑ i ∈ t, Finsupp.single i 1) = val
this : ((powersetCard n univ).sup fun x ↦ x).val = (powersetCard n univ).sup val
⊢ ((powersetCard n univ).sup fun x ↦ x).val = univ.val
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = f w

Tactic:
refine two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
    countable_empty hw ?_ ?_

Goal state after:
case refine_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ ContinuousOn f (closedBall c R)

case refine_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ ∀ x ∈ ball c R \ ∅, DifferentiableAt ℂ f x
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ ∑ j ∈ Finset.range (s.card + 1), (-1) ^ j * (C (s.esymm j) * X ^ (s.card - j)) =
    ∑ j ∈ Finset.range ((map (fun t ↦ -t) s).card + 1),
      C ((map (fun t ↦ -t) s).esymm j) * X ^ ((map (fun t ↦ -t) s).card - j)

Tactic:
simp only [esymm_neg, card_map, mul_assoc, map_mul, map_pow, map_neg, map_one]

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

Goal state before:
pp: case refine_5
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f (Set.Icc a b)
Hcg : ContinuousOn g (Set.Icc a b)
Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm
⊢ ∀ (x : ℝ × ℝ), (f' x) (1, 0) + (g' x) (0, 1) = ∑ i, (![f', g'] i x) (e.symm (Pi.single i 1))

Tactic:
intro x; rw [Fin.sum_univ_two]; rfl

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
num : ℤ
den : ℕ
x : M
h : num • 1 ≤ den • x
n : ℤ
hn : x ≤ n • 1
⊢ den • x ≤ ↑den • n • 1

Tactic:
simpa using nsmul_le_nsmul_right hn den

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
z : ℂ
⊢ z ∈ b → z ∉ c

Tactic:
rw [hb, hc]

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
z : ℂ
⊢ (aeval z) p = 0 ∧ z.im = 0 → ¬((aeval z) p = 0 ∧ z.im ≠ 0)
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 ℂ).toFinset.card = p.natDegree

Tactic:
Multiset.toFinset_card_of_nodup,

Goal state after:
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 ℂ).card = p.natDegree

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
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : R
hx0 : v x ≠ 0
hx1 : v x ≠ 1
⊢ v.restrict x ≠ 1

Tactic:
simpa

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 : L
⊢ 0 < v.norm x ↔ 0 < v x

Tactic:
rw [norm_def, ← NNReal.coe_zero, NNReal.coe_lt_coe, ← map_zero (RankOne.hom v),
    StrictMono.lt_iff_lt (RankOne.strictMono v)]
  rw [v.restrict_pos_iff]

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
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
⊢ ↑(toLex u) < φ.lexOrder ∨ ↑(toLex v) < ψ.lexOrder

Tactic:
or_iff_not_imp_left,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
⊢ ¬↑(toLex u) < φ.lexOrder → ↑(toLex v) < ψ.lexOrder
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x y : L
⊢ ↑((RankOne.hom v) (v.restrict (y + -x))) = ↑((RankOne.hom v) (v.restrict (-x + y)))

Tactic:
add_comm

Goal state after:
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)))
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
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w p) f = 0
⊢ weightedOrder w f < ?m.147

Tactic:
simpa

Goal state after:
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
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w q) g = 0
⊢ weightedOrder w g < ?m.171

Tactic:
simpa

Goal state after:
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)
⊢ IsPrincipalIdealRing ↥Valued.v.valuationSubring

Tactic:
rw [(Valuation.valuationSubring.integers (Valued.v)).isPrincipalIdealRing_iff_not_denselyOrdered,
    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.RingTheory.PowerSeries.Inverse

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

Tactic:
have : f.order = 0 := by
      simp [order_zero_of_unit h]
    conv_lhs => rw [← X_pow_order_mul_divXPowOrder (f := f), this, ENat.toNat_zero,
      pow_zero, one_mul]

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

Goal state before:
pp: k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ ∀ (c : ℕ), ↑c ≤ ↑(Multiset.count (normalize X) (normalizedFactors ↑P)) ↔ ↑c ≤ emultiplicity Polynomial.X P

Tactic:
← emultiplicity_eq_count_normalizedFactors X_irreducible

Goal state after:
k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ ∀ (c : ℕ), ↑c ≤ emultiplicity X ↑P ↔ ↑c ≤ emultiplicity Polynomial.X P

k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ ↑P ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (IsUnit 2)
⊢ (-48) ^ 3 = ↑(ofJ1728 R).Δ' * 1728

Tactic:
coe_Δ',

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (IsUnit 2)
⊢ (-48) ^ 3 = (ofJ1728 R).Δ * 1728
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝ : W.IsElliptic
j : R
h1 : Fact (IsUnit j)
h2 : Fact (IsUnit (j - 1728))
⊢ IsUnit (ofJNe0Or1728 j).Δ

Tactic:
ofJNe0Or1728_Δ

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝ : W.IsElliptic
j : R
h1 : Fact (IsUnit j)
h2 : Fact (IsUnit (j - 1728))
⊢ IsUnit (j ^ 2 * (j - 1728) ^ 9)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
j : R
inst✝¹ : Fact (IsUnit j)
inst✝ : Fact (IsUnit (j - 1728))
⊢ (j * (j - 1728) ^ 3) ^ 3 = ↑(ofJNe0Or1728 j).Δ' * j

Tactic:
coe_Δ',

Goal state after:
R : Type u_1
inst✝² : CommRing R
j : R
inst✝¹ : Fact (IsUnit j)
inst✝ : Fact (IsUnit (j - 1728))
⊢ (j * (j - 1728) ^ 3) ^ 3 = (ofJNe0Or1728 j).Δ * j
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
j : R
inst✝¹ : Fact (IsUnit j)
inst✝ : Fact (IsUnit (j - 1728))
⊢ (j * (j - 1728) ^ 3) ^ 3 = (ofJNe0Or1728 j).Δ * j

Tactic:
ofJNe0Or1728_Δ

Goal state after:
R : Type u_1
inst✝² : CommRing R
j : R
inst✝¹ : Fact (IsUnit j)
inst✝ : Fact (IsUnit (j - 1728))
⊢ (j * (j - 1728) ^ 3) ^ 3 = j ^ 2 * (j - 1728) ^ 9 * j
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
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
S : Sieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible
s : (i : E.I₀) → F.obj (op (E.X i))
hs : ∀ (i : E.I₀), (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) y → y = s i
i j : E.I₀
Z : C
gi : Z ⟶ E.X i
gj : Z ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
Y : C
f : Y ⟶ Z
x✝ : (E.sieve₁ gi gj).arrows f
k : E.I₁ i j
h : Y ⟶ E.Y k
hf₁ : f ≫ gi = h ≫ E.p₁ k
hf₂ : f ≫ gj = h ≫ E.p₂ k
W : C
p : W ⟶ E.Y k
hp : (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows p
⊢ (Sieve.pullback (E.f i) S).arrows (p ≫ E.p₁ k)

Tactic:
simpa

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP : W'.Nonsingular (u • P)
⊢ W'.Nonsingular P

Tactic:
rcases (nonsingular_iff _).mp hP with ⟨hP, hP'⟩

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * (u • P) y * (u • P) z - (3 * (u • P) x ^ 2 + 2 * W'.a₂ * (u • P) x * (u • P) z + W'.a₄ * (u • P) z ^ 2) ≠ 0 ∨
    2 * (u • P) y * (u • P) z + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * (u • P) z ^ 2 ≠ 0 ∨
      (u • P) y ^ 2 + W'.a₁ * (u • P) x * (u • P) y + 2 * W'.a₃ * (u • P) y * (u • P) z -
          (W'.a₂ * (u • P) x ^ 2 + 2 * W'.a₄ * (u • P) x * (u • P) z + 3 * W'.a₆ * (u • P) z ^ 2) ≠
        0
⊢ W'.Nonsingular P
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: ⊢ forgetToTop.IsContinuous zariskiTopology TopCat.grothendieckTopology

Tactic:
zariskiTopology,

Goal state after:
⊢ forgetToTop.IsContinuous (grothendieckTopology IsOpenImmersion) TopCat.grothendieckTopology
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: case h₂
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ IsOpenImmersion.precoverage ≤ (TopCat.isOpenEmbedding.inverseImage forgetToTop).precoverage

Tactic:
exact MorphismProperty.precoverage_monotone fun X Y f hf ↦ f.isOpenEmbedding

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

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Projective R
W : Projective F
inst✝ : DecidableEq F
⊢ Function.LeftInverse fromAffine toAffineLift

Tactic:
by
    rintro @⟨⟨P⟩, hP⟩
    by_cases hPz : P z = 0
    · rw [Point.ext_iff, toAffineLift_eq, toAffine_of_Z_eq_zero hPz]
      exact Quotient.eq.mpr <| Setoid.symm <| equiv_zero_of_Z_eq_zero hP hPz
    · rw [Point.ext_iff, toAffineLift_eq, toAffine_of_Z_ne_zero hP hPz]
      exact Quotient.eq.mpr <| Setoid.symm <| equiv_some_of_Z_ne_zero hPz

Goal state after:
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.FormallyUnramified
h : (g.comp f).FormallyEtale
⊢ g.FormallyEtale

Tactic:
algebraize [f, g, g.comp f]
  exact Algebra.FormallyEtale.of_restrictScalars (R := R)

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

Goal state before:
pp: case w
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite 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
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (1 + (aeval x) (derivative (minpoly K pb.gen)) * u) * (aeval x) (minpoly K pb.gen) ∈ I * I

pp: case w.hy
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite 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
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (u * (aeval x) (minpoly K pb.gen)) ^ 2 = 0

Tactic:
add_comm

Goal state after:
case w
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite 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
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ ((aeval x) (derivative (minpoly K pb.gen)) * u + 1) * (aeval x) (minpoly K pb.gen) ∈ I * I

case w.hy
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite 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
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (u * (aeval x) (minpoly K pb.gen)) ^ 2 = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
⊢ W.dblU P = (W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z + W.a₄ * P z ^ 2)) ^ 3 / P z ^ 2

Tactic:
rw [dblU, eval_polynomialX]

Goal state after: