mathlib-initiative/mathlib-tactics huggingface dataset:
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 < 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
x : ℝ
hx : x ∈ Icc (b₀ - δ) (b₀ + δ)
⊢ ‖f p x‖ = ‖f q x + (f p x - f q x)‖

Tactic:
congr

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 : 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
x : ℝ
hx : x ∈ Icc (b₀ - δ) (b₀ + δ)
⊢ f p x = f q x + (f p x - f q x)
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' ↦ circleMap c R θ' - circleMap c R θ
⊢ ∀ a ∈ {circleMap c R θ}ᶜ, a ∈ ball (circleMap c R θ) 1 → a - circleMap c R θ ∈ ball 0 1 \ {0}

Tactic:
simp_all [dist_eq, sub_eq_zero]

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

Goal state before:
pp: c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → ∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1) = 0
this : ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹ = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
z : ℂ
hz✝ : z ∈ sphere c R
⊢ (z - c)⁻¹ ^ ↑(n + 1) = (z - c) ^ (-↑n - 1)

Tactic:
inv_zpow,

Goal state after:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → ∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1) = 0
this : ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹ = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
z : ℂ
hz✝ : z ∈ sphere c R
⊢ ((z - c) ^ ↑(n + 1))⁻¹ = (z - c) ^ (-↑n - 1)
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
F : ℝ → ℝ → E
a b c d : ℝ
h : IntegrableOn (uncurry F) (uIoc a b ×ˢ uIoc c d) volume
⊢ ∫ (x : ℝ) in a..b, ∫ (y : ℝ) in c..d, F x y = ∫ (y : ℝ) in c..d, ∫ (x : ℝ) in a..b, F x y

Tactic:
intervalIntegral.intervalIntegral_eq_integral_uIoc,

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
F : ℝ → ℝ → E
a b c d : ℝ
h : IntegrableOn (uncurry F) (uIoc a b ×ˢ uIoc c d) volume
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in uIoc a b, ∫ (y : ℝ) in c..d, F x y ∂volume =
    ∫ (y : ℝ) in c..d, ∫ (x : ℝ) in a..b, F x y
Module: Mathlib.Analysis.Complex.CauchyIntegral

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

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

Tactic:
· exact circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable hr0
          hrR hs (hc.mono hsub) fun z hz => hd z ⟨hsub' hz.1, hz.2⟩

Goal state after:
case e_a
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ (2 * ↑π * I) • y = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y
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
⊢ (if hq : q = 0 then 1 else restrict p q.SplittingField) = if hq : q = 0 then 1 else restrict p q.SplittingField

Tactic:
congr

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
s : S
n : ℕ
m x : Multiset R
hx : x ∈ powersetCard n m
⊢ ((fun x ↦ s ^ n • x) ∘ prod) x = s ^ x.card • x.prod

Tactic:
Function.comp_apply,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
s : S
n : ℕ
m x : Multiset R
hx : x ∈ powersetCard n m
⊢ s ^ n • x.prod = s ^ x.card • x.prod
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

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

Tactic:
congr

Goal state after:
case e_t
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ (fun t ↦ (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support) = fun t ↦ {∑ i ∈ t, Finsupp.single i 1}
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
⊢ ((image (fun t ↦ ∑ i ∈ t, Finsupp.single i 1) (powersetCard n univ)).sup fun s ↦ Finsupp.toMultiset s) = univ.val

Tactic:
sup_image,

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
⊢ (powersetCard n univ).sup ((fun s ↦ Finsupp.toMultiset s) ∘ fun t ↦ ∑ i ∈ t, Finsupp.single i 1) = univ.val
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)) (Set.Icc (eL a) (eL b)) volume

Tactic:
← he_vol.integrableOn_comp_preimage he_emb,

Goal state after:
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) (⇑eL ⁻¹' Set.Icc (eL a) (eL b)) volume
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : 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
x : { x // x ∈ Set.univ }
⊢ (Multiset.map X ↑↑x).prod = (Multiset.map X ↑↑((Equiv.subtypeEquivProp this) x)).prod

Tactic:
congr

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 σ
this : (fun x ↦ x ∈ Set.univ) = fun x ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
x : σ
⊢ (Multiset.map X {x}).prod = (Multiset.map X ↑↑((Sym.oneEquiv.trans (Equiv.Set.univ (Sym σ 1)).symm) x)).prod

Tactic:
congr

Goal state after:
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

Tactic:
congr

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
s : Multiset R
| map (fun t ↦ X - C t) s
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
s : Multiset R
| map (fun t ↦ X - C t) s

Tactic:
congr

Goal state after:
case a.f
R : Type u_1
inst✝ : CommRing R
s : Multiset R
| fun t ↦ X - C t

case a.s
R : Type u_1
inst✝ : CommRing R
s : Multiset R
| s
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| (map (fun t ↦ X - C t) s).prod.coeff k

Tactic:
congr

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| (map (fun t ↦ X - C t) s).prod

case a
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| k
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| (map (fun t ↦ X - C t) s).prod

pp: case a
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| k

Tactic:
congr

Goal state after:
case a.a
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| map (fun t ↦ X - C t) s

case a
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| k
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case a.a
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| map (fun t ↦ X - C t) s

pp: case a
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| k

Tactic:
congr

Goal state after:
case a.a.f
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| fun t ↦ X - C t

case a.a.s
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| s

case a
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| k
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ p.leadingCoeff * (map (fun a ↦ X - C a) p.roots).prod.coeff k =
    p.leadingCoeff * ((-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k))

Tactic:
congr

Goal state after:
case e_a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ (map (fun a ↦ X - C a) p.roots).prod.coeff k = (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)
Module: Mathlib.Analysis.Complex.Polynomial.Basic

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

Tactic:
rintro ⟨hz1, hz2⟩
      have key : IsScalarTower.toAlgHom ℚ ℝ ℂ z.re = z := by
        ext
        · rfl
        · rw [hz2]; rfl
      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 : ℤ
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
⊢ (mkRat num den).num • 1 < (mkRat num den).den • x ↔ num • 1 < den • x

Tactic:
conv in num • 1 => rw [hnum, mul_comm, ← smul_smul, natCast_zsmul]

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
⊢ (mkRat num den).num • 1 < (mkRat num den).den • x ↔
    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)).num •
          1 <
      den • x
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

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

Tactic:
exact RingHom.congr_fun hφ x

Goal state after:
Module: Mathlib.RingTheory.Valuation.Discrete.RankOne

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst✝ : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
x : (ofClass v).ValueGroup₀
⊢ ∀ ⦃b : (ofClass v).ValueGroup₀⦄,
    x < b → (valueGroup₀_equiv_withZeroMulInt v) x < (valueGroup₀_equiv_withZeroMulInt v) b

Tactic:
y

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst✝ : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
x y : (ofClass v).ValueGroup₀
⊢ x < y → (valueGroup₀_equiv_withZeroMulInt v) x < (valueGroup₀_equiv_withZeroMulInt v) y
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: case pos
R : Type u_3
inst✝¹ : Ring R
inst✝ : ValuativeRel R
h : MulArchimedean (ValueGroupWithZero R)
H : IsNontrivial R
⊢ IsRankLeOne R

Tactic:
rw [isNontrivial_iff_isNontrivial (valuation R)] at H

Goal state after:
case pos
R : Type u_3
inst✝¹ : Ring R
inst✝ : ValuativeRel R
h : MulArchimedean (ValueGroupWithZero R)
H : (valuation R).IsNontrivial
⊢ IsRankLeOne R
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
⊢ ∀ ⦃b : M⦄, x < b → embedRealFun x < embedRealFun b

Tactic:
y

Goal state after:
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
⊢ x < y → embedRealFun x < embedRealFun y
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x : R
⊢ ∀ (b : R), (fun x ↦ ‖x‖) (x + b) ≤ max ((fun x ↦ ‖x‖) x) ((fun x ↦ ‖x‖) b)

Tactic:
y

Goal state after:
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x ↦ ‖x‖) (x + y) ≤ max ((fun x ↦ ‖x‖) x) ((fun x ↦ ‖x‖) y)
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case e'_4
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ max ((fun x ↦ ‖x‖) x) ((fun x ↦ ‖x‖) y) = max (dist 0 x) (dist x (x + y))

Tactic:
congr

Goal state after:
case e'_4.e_a
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x ↦ ‖x‖) x = dist 0 x

case e_a
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x ↦ ‖x‖) y = dist x (x + y)
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: M : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M
inst✝¹ : IsUltrametricDist M
s : Multiset ι
inst✝ : Nonempty ι
f : ι → M
inhabited_h : Inhabited ι
⊢ ∃ i, (s ≠ 0 → i ∈ s) ∧ ‖(Multiset.map f s).prod‖ ≤ ‖f i‖

Tactic:
induction s using Multiset.induction_on with
  | empty => simp
  | cons a t hM =>
      obtain ⟨M, hMs, hM⟩ := hM
      by_cases! hMa : ‖f M‖ ≤ ‖f a‖
      · refine ⟨a, by simp, ?_⟩
        · rw [Multiset.map_cons, Multiset.prod_cons]
          exact le_trans (norm_mul_le_max _ _) (max_le (le_refl _) (le_trans hM hMa))
      · rcases eq_or_ne t 0 with rfl | ht
        · exact ⟨a, by simp, by simp⟩
        · refine ⟨M, ?_, ?_⟩
          · simp [hMs ht]
          rw [Multiset.map_cons, Multiset.prod_cons]
          exact le_trans (norm_mul_le_max _ _) (max_le hMa.le hM)

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
⊢ (∃ ε > 0, Metric.ball 0 ε ⊆ U) ↔ ∃ γ, {x | valuation.restrict x < ↑γ} ⊆ U

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
⊢ (∃ ε > 0, Metric.ball 0 ε ⊆ U) → ∃ γ, {x | valuation.restrict x < ↑γ} ⊆ U

case refine_2
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
⊢ (∃ γ, {x | valuation.restrict x < ↑γ} ⊆ U) → ∃ ε > 0, Metric.ball 0 ε ⊆ U
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
C : ℝ
hC : 0 ≤ C
h : ∀ (i : ι), ‖f i‖ ≤ C
⊢ ‖∏' (i : ι), f i‖ ≤ C

Tactic:
rcases isEmpty_or_nonempty ι
  · simpa only [tprod_empty, norm_one'] using hC
  · exact norm_tprod_le_of_forall_le h

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 ∧ ↑(toLex d) < ψ.lexOrder
⊢ 0 + (coeff d) ψ = 0

Tactic:
coeff_eq_zero_of_lt_lexOrder hd.2,

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

Goal state before:
pp: case h
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
x : { ε // ε > 0 }
⊢ ∀ (y : { ε // ε > 0 }),
    ∃ z,
      𝓟 {p | v.norm (p.1 - p.2) < ↑x} ≥ 𝓟 {p | v.norm (p.1 - p.2) < ↑z} ∧
        𝓟 {p | v.norm (p.1 - p.2) < ↑y} ≥ 𝓟 {p | v.norm (p.1 - p.2) < ↑z}

Tactic:
y

Goal state after:
case h
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
x y : { ε // ε > 0 }
⊢ ∃ z,
    𝓟 {p | v.norm (p.1 - p.2) < ↑x} ≥ 𝓟 {p | v.norm (p.1 - p.2) < ↑z} ∧
      𝓟 {p | v.norm (p.1 - p.2) < ↑y} ≥ 𝓟 {p | v.norm (p.1 - p.2) < ↑z}
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : constantCoeff φ = 0
n : σ →₀ ℕ
⊢ (coeff n) φ⁻¹ = (coeff n) 0

Tactic:
coeff_inv

Goal state after:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : constantCoeff φ = 0
n : σ →₀ ℕ
⊢ (if n = 0 then (constantCoeff φ)⁻¹
    else -(constantCoeff φ)⁻¹ * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) φ⁻¹ else 0) =
    (coeff n) 0
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg.e_a.h.inr.hc.refine_1
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

pp: case neg.e_a.h.inr.hc.refine_2
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
hh :
  single () n ≤
    (match (i, j) with
      | (a, b) => (single () a, single () b)).2
⊢ n ≤ j

Tactic:
· rintro ⟨⟩
      simpa [Finsupp.single_eq_same] using le_of_lt H

Goal state after:
case neg.e_a.h.inr.hc.refine_2
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
hh :
  single () n ≤
    (match (i, j) with
      | (a, b) => (single () a, single () b)).2
⊢ n ≤ j