mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝⁵ : ν.IsMulLeftInvariant
inst✝⁴ : Countable ↥Γ
inst✝³ : ν.IsMulRightInvariant
inst✝² : SigmaFinite ν
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : μ V ≠ 0
hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)
neTopV : μ V ≠ ∞
U : Set (G ⧸ Γ)
a✝ : MeasurableSet U
meas_π : Measurable QuotientGroup.mk
μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)
⊢ μ U = (map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s)) U

Tactic:
have has_fund : HasFundamentalDomain Γ.op G ν := ⟨⟨s, fund_dom_s⟩⟩

Goal state after:
G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝⁵ : ν.IsMulLeftInvariant
inst✝⁴ : Countable ↥Γ
inst✝³ : ν.IsMulRightInvariant
inst✝² : SigmaFinite ν
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : μ V ≠ 0
hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)
neTopV : μ V ≠ ∞
U : Set (G ⧸ Γ)
a✝ : MeasurableSet U
meas_π : Measurable QuotientGroup.mk
μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)
has_fund : HasFundamentalDomain (↥Γ.op) G ν
⊢ μ U = (map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s)) U
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
⊢ volume univ = ENNReal.ofReal T

Tactic:
dsimp [volume]

Goal state after:
T : ℝ
hT : Fact (0 < T)
⊢ ENNReal.ofReal T * (addHaarMeasure ⊤) univ = ENNReal.ofReal T
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case hf
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ IntegrableOn (fun t ↦ ‖f p t - f q t‖) (Icc a b) μ

Tactic:
exact ((hf.uncurry_left _).sub (hf.uncurry_left _)).norm.integrableOn_Icc

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ∞
⊢ HasFiniteIntegral (fun x ↦ ν.real (Prod.mk x ⁻¹' s)) μ

Tactic:
hasFiniteIntegral_iff_enorm,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ∞
⊢ ∫⁻ (a : α), ‖ν.real (Prod.mk a ⁻¹' s)‖ₑ ∂μ < ∞
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✝ : SFinite μ
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
⊢ Integrable f (μ.prod ν) ↔
    (∀ᵐ (y : β) ∂ν, Integrable (fun x ↦ f (x, y)) μ) ∧ Integrable (fun y ↦ ∫ (x : α), ‖f (x, y)‖ ∂μ) ν

Tactic:
convert! integrable_prod_iff h1f.prod_swap using 1
  rw [funext fun _ => Function.comp_apply.symm, integrable_swap_iff]

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 := Prod.fst '' tsupport (uncurry f)
this✝ : Fact (μ U < ∞)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (ν V < ∞)
⊢ ∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (x : X), ∫ (y : Y) in V, f x y ∂ν ∂μ

Tactic:
congr 1 with x

Goal state after:
case e_f
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 < ∞)
x : X
⊢ ∫ (y : Y), f x y ∂ν = ∫ (y : Y) in V, f x y ∂ν
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case right
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (map (algebraMap F E) p).Splits
y : ↑(p.rootSet E)
key :
  (map (algebraMap F E) p).roots =
    Multiset.map (⇑↑(IsScalarTower.toAlgHom F p.SplittingField E)) (map (algebraMap F p.SplittingField) p).roots
⊢ ∃ a, mapRoots p E a = y

Tactic:
have hy := Subtype.mem y

Goal state after:
case right
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (map (algebraMap F E) p).Splits
y : ↑(p.rootSet E)
key :
  (map (algebraMap F E) p).roots =
    Multiset.map (⇑↑(IsScalarTower.toAlgHom F p.SplittingField E)) (map (algebraMap F p.SplittingField) p).roots
hy : ↑y ∈ p.rootSet E
⊢ ∃ a, mapRoots p E a = y
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : p ∣ q
hq : q ≠ 0
⊢ Function.Surjective ⇑(restrictDvd hpq)

Tactic:
by
  classical
  have := Fact.mk <|
    (SplittingField.splits q).of_dvd (map_ne_zero hq) ((map_dvd_map' _).mpr hpq)
  simpa only [restrictDvd_def, dif_neg hq] using! restrict_surjective _ _

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
⊢ (map (algebraMap F (p.comp q).SplittingField) p).Splits

Tactic:
let P : F[X] → Prop := fun r => (r.map (algebraMap F (r.comp q).SplittingField)).Splits

Goal state after:
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
⊢ (map (algebraMap F (p.comp q).SplittingField) p).Splits
Module: Mathlib.RingTheory.Polynomial.Vieta

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

Tactic:
conv_lhs =>
    congr
    congr
    ext x
    rw [sub_eq_add_neg]
    rw [← map_neg C x]
  convert! prod_X_add_C_eq_sum_esymm (map (fun t => -t) s) using 1
  · rw [map_map]; rfl
  · simp only [esymm_neg, card_map, mul_assoc, map_mul, map_pow, map_neg, map_one]

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

Goal state before:
pp: 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
w : ℝ
hw : (aeval w) p = 0
⊢ (aeval ((IsScalarTower.toAlgHom ℚ ℝ ℂ) w)) p = 0

Tactic:
by rw [aeval_algHom_apply, hw, map_zero]

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

Goal state before:
pp: case mpr
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
z : ℂ
hz1 : (aeval z) p = 0
hz2 : z.im = 0
key : (IsScalarTower.toAlgHom ℚ ℝ ℂ) z.re = z
⊢ ∃ a, (aeval a) p = 0 ∧ (IsScalarTower.toAlgHom ℚ ℝ ℂ) a = z

Tactic:
exact ⟨z.re, inj (by rwa [← aeval_algHom_apply, key, map_zero]), key⟩

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

Tactic:
exact ⟨fun h ↦ lt_of_smul_lt_smul_left h (Int.natCast_nonneg n),
    fun h ↦ zsmul_lt_zsmul_right (Int.natCast_pos.mpr hn) h⟩

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

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
hu' : (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x
⊢ (↑(u + v).den * (u.num * ↑v.den + v.num * ↑u.den)) • 1 < ↑(u + v).den • (↑u.den * ↑v.den) • (x + y)

Tactic:
← smul_smul

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
hu' : (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x
⊢ ↑(u + v).den • (u.num * ↑v.den + v.num * ↑u.den) • 1 < ↑(u + v).den • (↑u.den * ↑v.den) • (x + y)
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:
← smul_smul

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
num : ℤ
den : ℕ
x : M
h : num • 1 ≤ den • x
n : ℤ
hn : x ≤ n • 1
⊢ den • x ≤ ↑den • n • 1
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
num : ℤ
den : ℕ
hden✝ : den ≠ 0
x : M
m : ℕ
hm0 : m ≠ 0
hnum :
  num =
    (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
          (fun h ↦
            (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 }) h)
          (instDecidableEqNat den 0)).num *
      ↑m
hden :
  den =
    (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
          (fun h ↦
            (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 }) h)
          (instDecidableEqNat den 0)).den *
      m
| (m *
      (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
          (fun h ↦
            (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 }) h)
          (instDecidableEqNat den 0)).den) •
    x

Tactic:
← smul_smul

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
num : ℤ
den : ℕ
hden✝ : den ≠ 0
x : M
m : ℕ
hm0 : m ≠ 0
hnum :
  num =
    (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
          (fun h ↦
            (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 }) h)
          (instDecidableEqNat den 0)).num *
      ↑m
hden :
  den =
    (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
          (fun h ↦
            (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 }) h)
          (instDecidableEqNat den 0)).den *
      m
| m •
    (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
          (fun h ↦
            (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 }) h)
          (instDecidableEqNat den 0)).den •
      x
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case mp.refine_1
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 ≤ k • (a.den • (x + y) - a.num • 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right✝ : ∀ (y : ℤ), (fun m ↦ 0 + m • 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + m • 1
hm2 : 0 + m • 1 < k • a.den • x - 1 + 1
⊢ m • 1 < (k * a.den) • x

Tactic:
← smul_smul

Goal state after:
case mp.refine_1
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 ≤ k • (a.den • (x + y) - a.num • 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right✝ : ∀ (y : ℤ), (fun m ↦ 0 + m • 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + m • 1
hm2 : 0 + m • 1 < k • a.den • x - 1 + 1
⊢ m • 1 < k • a.den • x
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : y ∈ closedBall x r
x✝ : X
⊢ x✝ ∈ closedBall x r ↔ x✝ ∈ closedBall y r

Tactic:
mem_closedBall

Goal state after:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
x✝ : X
h : dist y x ≤ r
⊢ dist x✝ x ≤ r ↔ dist x✝ y ≤ r
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
⊢ (RankOne.hom v) 0 < (RankOne.hom v) (v.restrict x) ↔ 0 < v x

Tactic:
StrictMono.lt_iff_lt (RankOne.strictMono v)

Goal state after:
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation L Γ₀
hv : v.RankOne
x : L
⊢ 0 < v.restrict x ↔ 0 < v x
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case inr
σ : Type u_1
k : Type u_3
inst✝ : Field k
r : k
hr : r ≠ 0
⊢ C (r⁻¹ * r) = 1

pp: case inr
σ : Type u_1
k : Type u_3
inst✝ : Field k
r : k
hr : r ≠ 0
⊢ constantCoeff (C r) ≠ 0

Tactic:
inv_mul_cancel₀ hr,

Goal state after:
case inr
σ : Type u_1
k : Type u_3
inst✝ : Field k
r : k
hr : r ≠ 0
⊢ C 1 = 1

case inr
σ : Type u_1
k : Type u_3
inst✝ : Field k
r : k
hr : r ≠ 0
⊢ constantCoeff (C r) ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
⊢ ofJ 1728 = ofJ1728 F

Tactic:
by_cases h3 : (3 : F) = 0

Goal state after:
case pos
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
h3 : 3 = 0
⊢ ofJ 1728 = ofJ1728 F

case neg
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
h3 : ¬3 = 0
⊢ ofJ 1728 = ofJ1728 F
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
⊢ (ofJ j).IsElliptic

Tactic:
by_cases h3 : (3 : F) = 0

Goal state after:
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
⊢ (ofJ j).IsElliptic

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
⊢ (ofJ j).IsElliptic
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
⊢ (ofJ j).j = j

Tactic:
by_cases h3 : (3 : F) = 0

Goal state after:
case pos
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : 3 = 0
⊢ (ofJ j).j = j

case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
⊢ (ofJ j).j = j
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)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) = 0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 = 0 ∧
      P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * 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

Tactic:
by linear_combination (norm := ring1) u ^ 2 * hP'.right.left

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type u_1
inst✝ : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
h : (Pi.lift fun i ↦ F.map (c.inj i).op) = F.map (Pi.lift fun i ↦ (c.inj i).op) ≫ piComparison F fun i ↦ op (X i)
⊢ (Pi.lift fun i ↦ (c.inj i).op) = (productIsProduct fun x ↦ op (X x)).lift c.op

Tactic:
simp [Pi.lift, productIsProduct]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type u_1
inst✝³ : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
inst✝² : (ofArrows X c.inj).HasPairwisePullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j ↦ IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct X
⊢ IsIso
    (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
      Equalizer.Presieve.Arrows.forkMap F X c.inj)

Tactic:
refine IsIso.comp_isIso' inferInstance ?_

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type u_1
inst✝³ : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
inst✝² : (ofArrows X c.inj).HasPairwisePullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j ↦ IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct X
⊢ IsIso (Equalizer.Presieve.Arrows.forkMap F X c.inj)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W'⁄B).polynomialZ = (MvPolynomial.map ↑f) (W'⁄A).polynomialZ

Tactic:
← map_polynomialZ,

Goal state after:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W'⁄B).polynomialZ = ((W'⁄A).map ↑f).polynomialZ
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
x✝² x✝¹ x✝ : W.Point
⊢ x✝² + x✝¹ + x✝ = x✝² + (x✝¹ + x✝)

Tactic:
apply (toAffineAddEquiv W).injective

Goal state after:
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
x✝² x✝¹ x✝ : W.Point
⊢ (toAffineAddEquiv W) (x✝² + x✝¹ + x✝) = (toAffineAddEquiv W) (x✝² + (x✝¹ + x✝))
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
x✝ : W.Point
⊢ 0 + x✝ = x✝

Tactic:
apply (toAffineAddEquiv W).injective

Goal state after:
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
x✝ : W.Point
⊢ (toAffineAddEquiv W) (0 + x✝) = (toAffineAddEquiv W) x✝
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
x✝ : W.Point
⊢ x✝ + 0 = x✝

Tactic:
apply (toAffineAddEquiv W).injective

Goal state after:
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
x✝ : W.Point
⊢ (toAffineAddEquiv W) (x✝ + 0) = (toAffineAddEquiv W) x✝
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
P : W.Point
⊢ -P + P = 0

Tactic:
apply (toAffineAddEquiv W).injective

Goal state after:
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
P : W.Point
⊢ (toAffineAddEquiv W) (-P + P) = (toAffineAddEquiv W) 0
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
x✝¹ x✝ : W.Point
⊢ x✝¹ + x✝ = x✝ + x✝¹

Tactic:
apply (toAffineAddEquiv W).injective

Goal state after:
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
x✝¹ x✝ : W.Point
⊢ (toAffineAddEquiv W) (x✝¹ + x✝) = (toAffineAddEquiv W) (x✝ + x✝¹)