mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case h₂
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this✝ : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst✝] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
⊢ ‖f a y - f a' y‖ ≤ ε

Tactic:
rw [← dist_eq_norm']
        change dist (f.uncurry (a', y)) (f.uncurry (a, y)) ≤ ε
        apply (hu _ _ _).le
        · exact ha'x'.1
        · simp [dyx]

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

Goal state before:
pp: 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 < min a₀ b₀
b : ℝ
lt_b : max a₀ b₀ < b
⊢ ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε

Tactic:
rw [lt_min_iff] at a_lt

Goal state after:
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 : max a₀ b₀ < b
⊢ ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), f x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) < ∞
F : ℝ → ℝ := NNReal.toReal ∘ ⇑f
hf : ENNReal.ofReal (g b - g a) < ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
intF : IntegrableOn F (Ioo a b) volume
A : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
⊢ ∫ (x : ℝ) in Ioo a b, F x ≤ g b - g a

Tactic:
← integral_Ioc_eq_integral_Ioo,

Goal state after:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), f x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) < ∞
F : ℝ → ℝ := NNReal.toReal ∘ ⇑f
hf : ENNReal.ofReal (g b - g a) < ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
intF : IntegrableOn F (Ioo a b) volume
A : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
⊢ ∫ (t : ℝ) in Ioc a b, F t ≤ g b - g a
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)
has_fund : HasFundamentalDomain (↥Γ.op) G ν
i : QuotientMeasureEqMeasurePreimage ν μ'
⊢ μ U = (map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s)) U

Tactic:
have : μ'.IsMulLeftInvariant :=
    MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient ν

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 ν
i : QuotientMeasureEqMeasurePreimage ν μ'
this : μ'.IsMulLeftInvariant
⊢ μ U = (map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s)) U
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)
has_fund : HasFundamentalDomain (↥Γ.op) G ν
i : QuotientMeasureEqMeasurePreimage ν μ'
this✝¹ : μ'.IsMulLeftInvariant
this✝ : SigmaFinite μ'
this : μ' V / ν (QuotientGroup.mk ⁻¹' V ∩ s) = 1
⊢ (μ' V / ν (QuotientGroup.mk ⁻¹' V ∩ s)) • μ = μ

Tactic:
rw [this, one_smul]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
⊢ volume (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))

Tactic:
have h₁ : ε < T / 2 → Metric.closedBall (0 : ℝ) ε ∩ I = Metric.closedBall (0 : ℝ) ε := by
    intro hε
    rw [inter_eq_left, Real.closedBall_eq_Icc, zero_sub, zero_add]
    rintro y ⟨hy₁, hy₂⟩; constructor <;> linarith

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
⊢ volume (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case hF.refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
i : ι
hi : ContinuousOn (f i) (sphere c R)
⊢ ContinuousOn (deriv (circleMap c R)) [[0, 2 * π]]

Tactic:
rw [funext (deriv_circleMap _ _)]

Goal state after:
case hF.refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
i : ι
hi : ContinuousOn (f i) (sphere c R)
⊢ ContinuousOn (fun x ↦ circleMap 0 R x * I) [[0, 2 * π]]
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 ν
f : α × β → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
⊢ ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
    ∫⁻ (a : α), ENNReal.ofReal (∫⁻ (a_1 : β), ‖f (a, a_1)‖ₑ ∂ν).toReal ∂μ < ∞

Tactic:
lintegral_congr_ae

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
⊢ ∫⁻ (a : α), ?m.107 a ∂μ < ∞ ↔ ∫⁻ (a : α), ENNReal.ofReal (∫⁻ (a_1 : β), ‖f (a, a_1)‖ₑ ∂ν).toReal ∂μ < ∞

α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
⊢ (fun x ↦ ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν) =ᵐ[μ] ?m.107

α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
⊢ α → ℝ≥0∞
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
⊢ HasSum (fun n ↦ (cauchyPowerSeries f c R n) fun x ↦ w) ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)

Tactic:
simp only [cauchyPowerSeries_apply]
  exact (hasSum_two_pi_I_cauchyPowerSeries_integral hf hw).const_smul _

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

Goal state before:
pp: case inl
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
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.univ.pi fun j ↦ Set.Ioc (a j) (b j)) = ∅
⊢ ∀ x ∈ Finset.univ,
    (∫ (x_1 : Fin n → ℝ) in Set.Icc (a ∘ x.succAbove) (b ∘ x.succAbove), f (x.insertNth (b x) x_1) x) -
        ∫ (x_1 : Fin n → ℝ) in Set.Icc (a ∘ x.succAbove) (b ∘ x.succAbove), f (x.insertNth (a x) x_1) x =
      0

Tactic:
rintro j -

Goal state after:
case inl
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
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.univ.pi fun j ↦ Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
⊢ (∫ (x : Fin n → ℝ) in Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove), f (j.insertNth (b j) x) j) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove), f (j.insertNth (a j) x) j =
    0
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
⊢ (map (algebraMap F p.SplittingField) p).degree ≠ 0

Tactic:
rwa [degree_map]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case e'_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ (map (fun x ↦ X + C (-x)) s).prod = (map (fun r ↦ X + C r) (map (fun t ↦ -t) s)).prod

Tactic:
rw [map_map]; rfl

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case e'_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ (map (fun x ↦ X + C (-x)) s).prod.coeff k = (map (fun r ↦ X + C r) (map (fun t ↦ -t) s)).prod.coeff ?convert_1

Tactic:
rw [map_map]; rfl

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

Goal state before:
pp: case a
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ⋯
b : Finset ℂ := ⋯
c : Finset ℂ := ⋯
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
z : ℂ
hz1 : (aeval z) p = 0
hz2 : z.im = 0
⊢ ((IsScalarTower.toAlgHom ℚ ℝ ℂ) z.re).re = z.re

pp: case a
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ⋯
b : Finset ℂ := ⋯
c : Finset ℂ := ⋯
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
z : ℂ
hz1 : (aeval z) p = 0
hz2 : z.im = 0
⊢ ((IsScalarTower.toAlgHom ℚ ℝ ℂ) z.re).im = z.im

Tactic:
· rfl

Goal state after:
case a
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ⋯
b : Finset ℂ := ⋯
c : Finset ℂ := ⋯
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
z : ℂ
hz1 : (aeval z) p = 0
hz2 : z.im = 0
⊢ ((IsScalarTower.toAlgHom ℚ ℝ ℂ) z.re).im = z.im
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (↑(hφ.embedding x)).re = (φ x).re

pp: case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (↑(hφ.embedding x)).im = (φ x).im

Tactic:
· rfl

Goal state after:
case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (↑(hφ.embedding x)).im = (φ x).im
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 : M
⊢ (ratLt x).Nonempty

Tactic:
obtain hneg | rfl | hxpos := lt_trichotomy x 0

Goal state after:
case inl
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 : M
hneg : x < 0
⊢ (ratLt x).Nonempty

case inr.inl
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
⊢ (ratLt 0).Nonempty

case inr.inr
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 : M
hxpos : 0 < x
⊢ (ratLt x).Nonempty
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
⊢ ∀ U ∈ nhds 1, ∃ V, ↑V ⊆ U

Tactic:
by simpa only [Metric.mem_nhds_iff]
    using fun U ⟨ε, hεp, hεU⟩ ↦ ⟨ball_openSubgroup M hεp, hεU⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
⊢ ‖∏ i ∈ s, f i‖₊ ≤ s.sup fun x ↦ ‖f x‖₊

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs
  · simp
  · simpa only [← Finset.sup'_eq_sup hs, Finset.le_sup'_iff, coe_le_coe, coe_nnnorm']
      using! hs.norm_prod_le_sup'_norm f

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R)
s : R
hrs : r * s = 0
⊢ (monomial n) r * C s = 0

Tactic:
rw [← monomial_zero_eq_C, monomial_mul_monomial]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R)
s : R
hrs : r * s = 0
⊢ (monomial (n + 0)) (r * s) = 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R)
s : R
hrs : r * s = 0
this : C s = 0
⊢ s = 0

Tactic:
simpa using congr(coeff 0 $(this))

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsRight (MvPowerSeries σ R)
s : R
hrs : s * r = 0
⊢ C s * (monomial n) r = 0

Tactic:
rw [← monomial_zero_eq_C, monomial_mul_monomial]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsRight (MvPowerSeries σ R)
s : R
hrs : s * r = 0
⊢ (monomial (0 + n)) (s * r) = 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsRight (MvPowerSeries σ R)
s : R
hrs : s * r = 0
this : C s = 0
⊢ s = 0

Tactic:
simpa using congr(coeff 0 $(this))

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

Goal state before:
pp: σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : constantCoeff φ = ↑u
⊢ φ.invOfUnit u = φ⁻¹

Tactic:
rw [← invOfUnit_eq φ (h.symm ▸ u.ne_zero)]

Goal state after:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : constantCoeff φ = ↑u
⊢ φ.invOfUnit u = φ.invOfUnit (Units.mk0 (constantCoeff φ) ⋯)
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g

Tactic:
by_cases hg : g.weightedOrder w < ⊤
    · let p := (f.weightedOrder w).toNat
      have hp : p = f.weightedOrder w := by
        simpa only [p, ENat.natCast_toNat_eq_self, ← lt_top_iff_ne_top]
      let q := (g.weightedOrder w).toNat
      have hq : q = g.weightedOrder w := by
        simpa only [q, ENat.natCast_toNat_eq_self, ← lt_top_iff_ne_top]
      have : f.weightedHomogeneousComponent w p * g.weightedHomogeneousComponent w q ≠ 0 := by
        simp only [ne_eq, mul_eq_zero]
        intro H
        rcases H with H | H <;>
        · refine weightedHomogeneousComponent_of_weightedOrder ?_ H
          simp only [ENat.natCast_toNat_eq_self, ne_eq, weightedOrder_eq_top_iff, p, q]
          rw [← ne_eq, ne_zero_iff_weightedOrder_finite w]
          exact ENat.natCast_toNat (ne_top_of_lt (by simpa))
      rw [← weightedHomogeneousComponent_mul_of_le_weightedOrder
          (le_of_eq hp) (le_of_eq hq)] at this
      rw [← hp, ← hq, ← Nat.cast_add, ← not_lt]
      intro H
      apply this
      apply weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero H
    · rw [not_lt_top_iff] at hg
      simp [hg]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : n = 0
⊢ a = a

pp: case neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ (-a *
      ∑ x ∈ antidiagonal (single () n),
        if x.2 < single () n then (MvPowerSeries.coeff x.1) φ * (MvPowerSeries.coeff x.2) (MvPowerSeries.inv.aux a φ)
        else 0) =
    -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) (MvPowerSeries.inv.aux a φ) else 0

Tactic:
· rfl

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ (-a *
      ∑ x ∈ antidiagonal (single () n),
        if x.2 < single () n then (MvPowerSeries.coeff x.1) φ * (MvPowerSeries.coeff x.2) (MvPowerSeries.inv.aux a φ)
        else 0) =
    -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) (MvPowerSeries.inv.aux a φ) else 0
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg.e_a.h.inr
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) (MvPowerSeries.inv.aux a φ) =
    (MvPowerSeries.coeff
          (match (i, j) with
            | (a, b) => (single () a, single () b)).1)
        φ *
      (MvPowerSeries.coeff
          (match (i, j) with
            | (a, b) => (single () a, single () b)).2)
        (MvPowerSeries.inv.aux a φ)

pp: case neg.e_a.h.inr.hc
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ (match (i, j) with
      | (a, b) => (single () a, single () b)).2 <
    single () n

Tactic:
· rfl

Goal state after:
case neg.e_a.h.inr.hc
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ (match (i, j) with
      | (a, b) => (single () a, single () b)).2 <
    single () n
Module: Mathlib.RingTheory.PowerSeries.Inverse

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

Tactic:
exact isUnit_divided_by_X_pow_order hf

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
h : (valuation K v).IsRankOneDiscrete
⊢ ∃ γ, Subgroup.zpowers γ = (MonoidWithZeroHom.ofClass Valued.v).valueGroup ∧ γ < 1

Tactic:
exact ⟨h.generator, by rw [h.generator_zpowers_eq_valueGroup, adicCompletion_valueGroup_eq],
      h.generator_lt_one⟩

Goal state after: