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
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable g (map QuotientGroup.mk (μ.restrict 𝓕))
hπ : Measurable QuotientGroup.mk
γ : Gᵐᵒᵖ
hγ : γ ∈ Γ.op
x : G
⊢ ↑(x * MulOpposite.unop γ) = ↑x

Tactic:
exact QuotientGroup.mk_mul_of_mem x hγ

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : ‖w‖ / R ∈ Ico 0 1
n : ℕ
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      ‖deriv (circleMap c R) t • (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t)‖ ≤
        ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n

Tactic:
simp [norm_smul, abs_of_pos hR, mul_left_comm R, inv_mul_cancel_left₀ hR.ne', mul_comm ‖_‖]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: case refine_3
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ : ∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ Box.Icc J
x✝ : GP.bDistortion = true → J.distortion ≤ c
Hl : J.lower i ∈ Set.Icc (J.lower i) (J.upper i)
⊢ dist ((BoxAdditiveMap.volume J) ((f' x) (Pi.single i 1))) (F J) ≤ ε / 2 + ε / 2

Tactic:
have Hu : J.upper i ∈ Icc (J.lower i) (J.upper i) := Set.right_mem_Icc.2 (J.lower_le_upper i)

Goal state after:
case refine_3
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ : ∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ Box.Icc J
x✝ : GP.bDistortion = true → J.distortion ≤ c
Hl : J.lower i ∈ Set.Icc (J.lower i) (J.upper i)
Hu : J.upper i ∈ Set.Icc (J.lower i) (J.upper i)
⊢ dist ((BoxAdditiveMap.volume J) ((f' x) (Pi.single i 1))) (F J) ≤ ε / 2 + ε / 2
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z ↦ I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he₁ : e (1, 0) = 1
he₂ : e (0, 1) = I
he : ∀ (x y : ℝ), True
F : ℝ × ℝ → E := f ∘ ⇑e
⊢ (((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (e (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (e (z.re, y)) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (e (x, y))) 1 - (f' (e (x, y))) I

Tactic:
set F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp (e : ℝ × ℝ →L[ℝ] ℂ)

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z ↦ I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he₁ : e (1, 0) = 1
he₂ : e (0, 1) = I
he : ∀ (x y : ℝ), True
F : ℝ × ℝ → E := f ∘ ⇑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p ↦ f' (e p) ∘SL ↑e
⊢ (((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (e (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (e (z.re, y)) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (e (x, y))) 1 - (f' (e (x, y))) I
Module: Mathlib.Analysis.Complex.Liouville

Goal state before:
pp: E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
⊢ f = const E c

Tactic:
obtain ⟨c', hc'⟩ := hf.exists_eq_const_of_bounded h_bdd

Goal state after:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
c' : F
hc' : f = const E c'
⊢ f = const E c
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
⊢ esymm σ R 0 = 1

Tactic:
simp only [esymm, powersetCard_zero, sum_singleton, prod_empty]

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case pos
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
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : p₁.comp q = 0
⊢ P (p₁ * p₂)

Tactic:
rcases comp_eq_zero_iff.mp h₁ with h | h
      · rw [h, zero_mul]
        simp [P]
      · exact False.elim (hq (by rw [h.2, natDegree_C]))

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

Goal state before:
pp: case refine_3
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
⊢ IntegrableOn ((fun x ↦ ∑ i, (f' i (eL.symm x) ∘SL ↑eL.symm) (e i)) ∘ ⇑eL) (Set.Icc a b) volume

Tactic:
simp [← hDF, Function.comp_def, Hi]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ msymm σ R (Nat.Partition.indiscrete 1) = ∑ i, X i

Tactic:
have : (fun (x : Sym σ 1) ↦ x ∈ Set.univ) =
      (fun x ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1) := by
    simp_rw [Set.mem_univ, Nat.Partition.ofSym_one]

Goal state after:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x ↦ x ∈ Set.univ) = fun x ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
⊢ msymm σ R (Nat.Partition.indiscrete 1) = ∑ i, X i
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Finset σ
r : σ → R
k : ℕ
h : k ≤ #s
⊢ (∏ i ∈ s, (X + C (r i))).coeff k = ∑ t ∈ Finset.powersetCard (#s - k) s, ∏ i ∈ t, r i

Tactic:
rw [Finset.prod, prod_X_add_C_coeff' _ r h, Finset.esymm_map_val]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Finset σ
r : σ → R
k : ℕ
h : k ≤ #s
⊢ ∑ t ∈ Finset.powersetCard (s.val.card - k) s, t.prod r = ∑ t ∈ Finset.powersetCard (#s - k) s, ∏ i ∈ t, r i
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
B : ℝ≥0
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ ↑B
⊢ B ^ s.card = B ^ ((map f p).natDegree - i)

Tactic:
hs.2

Goal state after:
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
B : ℝ≥0
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ ↑B
⊢ B ^ ((map f p).natDegree - i) = B ^ ((map f p).natDegree - i)
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: 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
⊢ ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * ↑(p.natDegree.choose i)

Tactic:
obtain hB | hB := lt_or_ge B 0
  · rw [eq_one_of_roots_le hB h1 h2 h3, Polynomial.map_one, natDegree_one, zero_tsub, pow_zero,
      one_mul, coeff_one]
    split_ifs with h <;> simp [h]
  rw [← h1.natDegree_map f]
  obtain hi | hi := lt_or_ge (map f p).natDegree i
  · rw [coeff_eq_zero_of_natDegree_lt hi, norm_zero]
    positivity
  rw [coeff_eq_esymm_roots_of_splits h2 hi, (h1.map _).leadingCoeff,
    one_mul, norm_mul, norm_pow, norm_neg, norm_one, one_pow, one_mul]
  apply ((norm_multiset_sum_le _).trans <| sum_le_card_nsmul _ _ fun r hr => _).trans
  · rw [Multiset.map_map, card_map, card_powersetCard, ← Splits.natDegree_eq_card_roots h2,
      Nat.choose_symm hi, mul_comm, nsmul_eq_mul]
  intro r hr
  simp_rw [Multiset.mem_map] at hr
  obtain ⟨_, ⟨s, hs, rfl⟩, rfl⟩ := hr
  rw [mem_powersetCard] at hs
  lift B to ℝ≥0 using hB
  rw [← coe_nnnorm, ← NNReal.coe_pow, NNReal.coe_le_coe, ← nnnormHom_apply, ← MonoidHom.coe_coe,
    MonoidHom.map_multiset_prod]
  refine (prod_le_pow_card _ B fun x hx => ?_).trans_eq (by rw [card_map, hs.2])
  obtain ⟨z, hz, rfl⟩ := Multiset.mem_map.1 hx
  exact h3 z (mem_of_le hs.1 hz)

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

Goal state before:
pp: F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : CommRing O
inst✝ : Algebra O F
v✝ : Valuation F Γ₀
v : F →*₀ Γ₀
⊢ ∀ ⦃a : ↥(MonoidHom.mrange v)⦄, 0 < a → ∀ ⦃b c : ↥(MonoidHom.mrange v)⦄, b < c → a * b < a * c

Tactic:
by
    simp only [← Subtype.coe_lt_coe, val_mrange_zero, Submonoid.coe_mul, Subtype.forall,
      MonoidHom.mem_mrange, forall_exists_index, forall_apply_eq_imp_iff]
    rintro a ha b c hbc
    gcongr

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.num * ↑v.den) • 1 + (v.num * ↑u.den) • 1 < (↑u.den * ↑v.den) • (x + y)

Tactic:
smul_add

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.num * ↑v.den) • 1 + (v.num * ↑u.den) • 1 < (↑u.den * ↑v.den) • x + (↑u.den * ↑v.den) • y
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 ℂ).card = p.natDegree

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:
← Splits.natDegree_eq_card_roots,

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
⊢ (map (algebraMap ℚ ℂ) p).natDegree = 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
⊢ (map (algebraMap ℚ ℂ) p).Splits

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: case neg.inr.inl
R : Type u_3
inst✝¹ : Ring R
inst✝ : ValuativeRel R
h : MulArchimedean (ValueGroupWithZero R)
b : ValueGroupWithZero R
H : 1 < b
H' : 1 b ≤ 1 1
ha : 1 ≠ 0
⊢ IsNontrivial R

pp: case neg.inr.inr
R : Type u_3
inst✝¹ : Ring R
inst✝ : ValuativeRel R
h : MulArchimedean (ValueGroupWithZero R)
a b : ValueGroupWithZero R
H : a < b
H' : 1 b ≤ 1 a
ha : a ≠ 0
ha' : a ≠ 1
⊢ IsNontrivial R

Tactic:
· exact ⟨⟨b, (H.trans' zero_lt_one).ne', H.ne'⟩⟩

Goal state after:
case neg.inr.inr
R : Type u_3
inst✝¹ : Ring R
inst✝ : ValuativeRel R
h : MulArchimedean (ValueGroupWithZero R)
a b : ValueGroupWithZero R
H : a < b
H' : 1 b ≤ 1 a
ha : a ≠ 0
ha' : a ≠ 1
⊢ IsNontrivial R
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
⊢ (coeff (0, n).1) φ * (coeff (0, n).2) (φ.invOfUnit u) +
      ∑ x ∈ (antidiagonal n).erase (0, n), (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) =
    0

Tactic:
coeff_zero_eq_constantCoeff_apply,

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
⊢ constantCoeff φ * (coeff (0, n).2) (φ.invOfUnit u) +
      ∑ x ∈ (antidiagonal n).erase (0, n), (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) =
    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
⊢ ↑u *
        -(↑u⁻¹ *
            ∑ x ∈ antidiagonal (0, n).2, if x.2 < (0, n).2 then (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) else 0) +
      ∑ x ∈ (antidiagonal n).erase (0, n), (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) =
    0

Tactic:
mul_neg,

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
⊢ -(↑u *
          (↑u⁻¹ *
            ∑ x ∈ antidiagonal (0, n).2, if x.2 < (0, n).2 then (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) else 0)) +
      ∑ x ∈ (antidiagonal n).erase (0, n), (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) =
    0
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬constantCoeff φ = 0 ∧ ¬constantCoeff ψ = 0
⊢ ψ⁻¹ * 1 * ψ = 1

Tactic:
mul_one,

Goal state after:
case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬constantCoeff φ = 0 ∧ ¬constantCoeff ψ = 0
⊢ ψ⁻¹ * ψ = 1
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]

Goal state after:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
this : f.order = 0
⊢ f = f.divXPowOrder
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : 3 = 0
⊢ (ofJ j).IsElliptic

Tactic:
have : Fact <| IsUnit (2 : F) := ⟨.of_mul_eq_one 2 <| by linear_combination h3⟩

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
this : Fact (IsUnit 2)
⊢ (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
h3 : 3 = 0
⊢ (ofJ j).j = j

Tactic:
have : Fact <| IsUnit (2 : F) := ⟨.of_mul_eq_one 2 <| by linear_combination h3⟩

Goal state after:
case pos
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : 3 = 0
this : Fact (IsUnit 2)
⊢ (ofJ j).j = j
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomial / P z ^ 3 = Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomial

Tactic:
linear_combination (norm := (rw [eval_polynomial, Affine.evalEval_polynomial]; ring1))
    P y ^ 2 / P z ^ 2 * div_self hPz + W.a₁ * P x * P y / P z ^ 2 * div_self hPz
      + W.a₃ * P y / P z * div_self (pow_ne_zero 2 hPz) - W.a₂ * P x ^ 2 / P z ^ 2 * div_self hPz
      - W.a₄ * P x / P z * div_self (pow_ne_zero 2 hPz) - W.a₆ * div_self (pow_ne_zero 3 hPz)

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

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Projective F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : P z = 0
⊢ (MulAction.orbitRel Fˣ (Fin 3 → F)) ![0, 1, 0] P

Tactic:
exact Setoid.symm <| equiv_zero_of_Z_eq_zero hP hPz

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
        (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
      0 →
    (W'.a₁ * b * 1 - (3 * a ^ 2 + 2 * W'.a₂ * a * 1 + W'.a₄ * 1) = 0 ∧
        2 * b * 1 + W'.a₁ * a * 1 + W'.a₃ * 1 = 0 ∧
          b ^ 2 + W'.a₁ * a * b + 2 * W'.a₃ * b * 1 - (W'.a₂ * a ^ 2 + 2 * W'.a₄ * a * 1 + 3 * W'.a₆ * 1) = 0 ↔
      W'.toAffine.a₁ * b - (3 * a ^ 2 + 2 * W'.toAffine.a₂ * a + W'.toAffine.a₄) = 0 ∧
        2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0)

Tactic:
mul_one,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
        (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
      0 →
    (W'.a₁ * b - (3 * a ^ 2 + 2 * W'.a₂ * a + W'.a₄) = 0 ∧
        2 * b + W'.a₁ * a + W'.a₃ = 0 ∧
          b ^ 2 + W'.a₁ * a * b + 2 * W'.a₃ * b - (W'.a₂ * a ^ 2 + 2 * W'.a₄ * a + 3 * W'.a₆) = 0 ↔
      W'.toAffine.a₁ * b - (3 * a ^ 2 + 2 * W'.toAffine.a₂ * a + W'.toAffine.a₄) = 0 ∧
        2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 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✝ : W.Point
⊢ x✝ + 0 = x✝

Tactic:
classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, add_zero]

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).neg (⇑f ∘ P) = ⇑f ∘ W'.neg P

Tactic:
simp only [neg, map_negY, comp_fin3]

Goal state after:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
⊢ ![(⇑f ∘ P) x, f (W'.negY P), (⇑f ∘ P) z] = ![f (P x), f (W'.negY P), f (P z)]
Module: Mathlib.RingTheory.RingHom.Smooth

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.Smooth
hg : g.Smooth
⊢ (g.comp f).Smooth

Tactic:
by
  algebraize [f, g, g.comp f]
  exact Algebra.Smooth.comp R S T

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

Goal state before:
pp: ⊢ IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
by
  refine .mk respectsIso ?_
  introv H
  rw [formallyUnramified_algebraMap] at H ⊢
  infer_instance

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

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
⊢ f₁ e * 1 - f₁ e * f₂ e = f₁ e * f₁ e - f₁ e * f₂ e

Tactic:
mul_one,

Goal state after:
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
⊢ f₁ e - f₁ e * f₂ e = f₁ e * f₁ e - f₁ e * f₂ e