mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ∏ x ∈ Finset.range n, (s + 1 + ↑x) = ∏ k ∈ Finset.range n, (s + ↑(k + 1))

Tactic:
refine Finset.prod_congr rfl fun x _ => ?_

Goal state after:
case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
x : ℕ
x✝ : x ∈ Finset.range n
⊢ s + 1 + ↑x = s + ↑(x + 1)
Module: Mathlib.Analysis.Normed.Affine.Ceva

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
hp0 : ∀ (i : Fin 3), p i ≠ t.points (i + 2)
hp : ∀ (i : Fin 3), p i ∈ line[𝕜, t.points (i + 1), t.points (i + 2)]
hp' : ∀ (i : Fin 3), p' ∈ line[𝕜, t.points i, p i]
⊢ ∏ i, dist (t.points (i + 1)) (p i) / dist (p i) (t.points (i + 2)) = 1

Tactic:
have aux (i) : dist (p i) (t.points (i + 2)) ≠ 0 := by simpa using hp0 i

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
hp0 : ∀ (i : Fin 3), p i ≠ t.points (i + 2)
hp : ∀ (i : Fin 3), p i ∈ line[𝕜, t.points (i + 1), t.points (i + 2)]
hp' : ∀ (i : Fin 3), p' ∈ line[𝕜, t.points i, p i]
aux : ∀ (i : Fin 3), dist (p i) (t.points (i + 2)) ≠ 0
⊢ ∏ i, dist (t.points (i + 1)) (p i) / dist (p i) (t.points (i + 2)) = 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun n ↦ ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) atTop (𝓝 (Gamma s))

Tactic:
Gamma_eq_integral hs

Goal state after:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun n ↦ ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) atTop (𝓝 s.GammaIntegral)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
⊢ ↑n ^ z * ↑n ^ (1 - z) * ↑n ! ^ 2 /
      ((∏ j ∈ Finset.range (n + 1), (z + ↑j)) * ∏ j ∈ Finset.range (n + 1), (1 - z + ↑j)) =
    ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))

Tactic:
have : (n : ℂ) ^ z * (n : ℂ) ^ (1 - z) = n := by
    rw [← cpow_add _ _ (Nat.cast_ne_zero.mpr hn), add_sub_cancel, cpow_one]

Goal state after:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : ↑n ^ z * ↑n ^ (1 - z) = ↑n
⊢ ↑n ^ z * ↑n ^ (1 - z) * ↑n ! ^ 2 /
      ((∏ j ∈ Finset.range (n + 1), (z + ↑j)) * ∏ j ∈ Finset.range (n + 1), (1 - z + ↑j)) =
    ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
Module: Mathlib.Analysis.Normed.Affine.MazurUlam

Goal state before:

Tactic:
dist (e z) z ≤ dist (e z) x + dist x z := dist_triangle (e z) x z
      _ = dist (e x) (e z) + dist x z := by rw [hx, dist_comm]
      _ = dist x z + dist x z := by rw [e.dist_eq x z]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case pos
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : s.im = 0
this : s = ↑s.re
⊢ Gamma ↑s.re ≠ 0

Tactic:
Gamma_ofReal,

Goal state after:
case pos
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : s.im = 0
this : s = ↑s.re
⊢ ↑(Real.Gamma s.re) ≠ 0
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : CommRing k
inst✝³ : NoZeroDivisors k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
p' : P
hp' : ∀ (i : Fin 3), p' ∈ line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
h✝ : Nontrivial k
w : ↑Set.univ → Fin 3 → k := fun i ↦ Finset.affineCombinationLineMapWeights (↑i + 1) (↑i + 2) (r ↑i)
hw : ∀ (i : ↑Set.univ), ∑ j, w i j = 1
hp'w : ∀ (i : ↑Set.univ), p' ∈ line[k, t.points ↑i, (Finset.affineCombination k Finset.univ t.points) (w i)]
⊢ ∏ i, r i = ∏ i, (1 - r i)

Tactic:
obtain ⟨w', hw', rfl, h⟩ :=
    t.independent.exists_affineCombination_eq_smul_eq_of_fintype (by simp) hw hp'w

Goal state after:
case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : CommRing k
inst✝³ : NoZeroDivisors k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h✝ : Nontrivial k
w : ↑Set.univ → Fin 3 → k := fun i ↦ Finset.affineCombinationLineMapWeights (↑i + 1) (↑i + 2) (r ↑i)
hw : ∀ (i : ↑Set.univ), ∑ j, w i j = 1
w' : Fin (2 + 1) → k
hw' : ∑ j, w' j = 1
h : ∀ (i : ↑Set.univ), ∃ r, ∀ (j : Fin (2 + 1)), r * {↑i}ᶜ.indicator (w i) j = {↑i}ᶜ.indicator w' j
hp' :
  ∀ (i : Fin 3),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
hp'w :
  ∀ (i : ↑Set.univ),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points ↑i, (Finset.affineCombination k Finset.univ t.points) (w i)]
⊢ ∏ i, r i = ∏ i, (1 - r i)
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
h : Simplex.Scalene t
⊢ 0 ≠ 1

Tactic:
decide

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
h : Simplex.Scalene t
⊢ 0 ≠ 2

Tactic:
decide

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
h : Simplex.Scalene t
⊢ ¬(0 = 0 ∧ 1 = 2)

Tactic:
decide

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
h : Simplex.Scalene t
⊢ ¬(0 = 2 ∧ 1 = 0)

Tactic:
decide

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
h : Simplex.Scalene t
⊢ 1 ≠ 2

Tactic:
decide

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
h : Simplex.Scalene t
⊢ ¬(0 = 1 ∧ 1 = 2)

Tactic:
decide

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
h : Simplex.Scalene t
⊢ ¬(0 = 2 ∧ 1 = 1)

Tactic:
decide

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
h : Simplex.Scalene t
⊢ ¬(0 = 1 ∧ 2 = 2)

Tactic:
decide

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
h : Simplex.Scalene t
⊢ ¬(0 = 2 ∧ 2 = 1)

Tactic:
decide

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
h1 : AnalyticOnNhd ℂ (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ (Gamma ↑t * Gamma (↑t + 1 / 2))⁻¹ = (Gamma (2 * ↑t))⁻¹ * 2 ^ (2 * ↑t - 1) / ↑√π

Tactic:
Gamma_ofReal,

Goal state after:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ (↑(Real.Gamma t) * Gamma (↑t + 1 / 2))⁻¹ = (Gamma (2 * ↑t))⁻¹ * 2 ^ (2 * ↑t - 1) / ↑√π
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
h1 : AnalyticOnNhd ℂ (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ (↑(Real.Gamma t) * Gamma ↑(t + 1 / 2))⁻¹ = (Gamma (2 * ↑t))⁻¹ * 2 ^ (2 * ↑t - 1) / ↑√π

Tactic:
Gamma_ofReal,

Goal state after:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ (↑(Real.Gamma t) * ↑(Real.Gamma (t + 1 / 2)))⁻¹ = (Gamma (2 * ↑t))⁻¹ * 2 ^ (2 * ↑t - 1) / ↑√π
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
h1 : AnalyticOnNhd ℂ (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ (Gamma ↑(2 * t))⁻¹ * (↑(2 ^ (1 - 2 * t)))⁻¹ * (↑√π)⁻¹ = (Gamma ↑(2 * t))⁻¹ * 2 ^ (↑(2 * t) - 1) / ↑√π

Tactic:
Gamma_ofReal,

Goal state after:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ (↑(Real.Gamma (2 * t)))⁻¹ * (↑(2 ^ (1 - 2 * t)))⁻¹ * (↑√π)⁻¹ = (↑(Real.Gamma (2 * t)))⁻¹ * 2 ^ (↑(2 * t) - 1) / ↑√π
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : CommRing k
inst✝³ : NoZeroDivisors k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h✝ : Nontrivial k
w : ↑Set.univ → Fin 3 → k := fun i ↦ Finset.affineCombinationLineMapWeights (↑i + 1) (↑i + 2) (r ↑i)
hw : ∀ (i : ↑Set.univ), ∑ j, w i j = 1
w' : Fin (2 + 1) → k
hw' : ∑ j, w' j = 1
h : ∀ (i : ↑Set.univ), ∃ r, ∀ (j : Fin (2 + 1)), r * {↑i}ᶜ.indicator (w i) j = {↑i}ᶜ.indicator w' j
hp' :
  ∀ (i : Fin 3),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
hp'w :
  ∀ (i : ↑Set.univ),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points ↑i, (Finset.affineCombination k Finset.univ t.points) (w i)]
h' :
  ∀ (i : Fin 3), ∃ c, ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k := fun i ↦ ⋯.choose
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
hc2 : ∀ (i : Fin 3), c i * r i = w' (i + 2)
hcr : (∏ i, c i) * ∏ i, r i = (∏ i, c i) * ∏ i, (1 - r i)
i : Fin 3
hi : c i = 0
hw'i1 : w' (i + 1) = 0
hw'i2 : w' (i + 2) = 0
hw'i0 : w' i = 1
hi1 : c (i + 1) * r (i + 1) = 1
hi1' : c (i + 1) * (1 - r (i + 1)) = 0
hci1 : c (i + 1) = 1
hri1 : r (i + 1) = 1
hi2 : c (i + 2) * (1 - r (i + 2)) = 1
hi2' : c (i + 2) * r (i + 2) = 0
hci2 : c (i + 2) = 1
hri2 : r (i + 2) = 0
⊢ 1 - r (i + 1) = 0

Tactic:
simp [hri1]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: 𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst✝¹¹ : SeminormedCommRing S
inst✝¹⁰ : SeminormedRing R
inst✝⁹ : SeminormedAddCommGroup M
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsBoundedSMul S R
inst✝⁵ : IsBoundedSMul S M
inst✝⁴ : Module R M
inst✝³ : IsBoundedSMul R M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : IsBoundedSMul Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) + ‖m₁‖ * ‖m₂‖

Tactic:
apply le_add_of_nonneg_right
      positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: case calc_1
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : q ^ 2 = -↑(normSq q)
k : ℝ := ↑(2 * n)!
⊢ k⁻¹ • (-↑(normSq q)) ^ n = k⁻¹ • ↑((-1) ^ n * ‖q‖ ^ (2 * n))

pp: case calc_2
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : q ^ 2 = -↑(normSq q)
k : ℝ := ↑(2 * n)!
⊢ k⁻¹ • ↑((-1) ^ n * ‖q‖ ^ (2 * n)) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / k)

Tactic:
· congr 1
    rw [neg_pow, normSq_eq_norm_mul_self, pow_mul, sq]
    push_cast
    rfl

Goal state after:
case calc_2
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : q ^ 2 = -↑(normSq q)
k : ℝ := ↑(2 * n)!
⊢ k⁻¹ • ↑((-1) ^ n * ‖q‖ ^ (2 * n)) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / k)
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
H : ‖φ x z‖ ≠ 0
w : ℝ × ℝ
⊢ ‖φ x w‖ = ‖φ x z‖

Tactic:
set M : ℝ := ‖φ x z‖ with hM

Goal state after:
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
⊢ ‖φ x w‖ = M
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
⊢ 0 ≠ 1

Tactic:
decide

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
⊢ 0 ≠ 2

Tactic:
decide

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
⊢ 1 ≠ 2

Tactic:
decide

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case h.inl
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy0 : f y = 0 y
⊢ (fun y ↦ f (x * y) / f y) y ≤ c * f x

Tactic:
simpa [hy0] using seminormFromBounded_aux f_nonneg f_mul x

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy : 0 y < f y
⊢ f (x * y) ≤ c * f x * f y

Tactic:
apply f_mul

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
⊢ seminormFromBounded' f x = 0 ↔ f x = 0

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · have hf := seminormFromBounded_ge f_nonneg f_mul x
    rw [h, mul_zero] at hf
    exact hf.antisymm (f_nonneg _)
  · have hf : seminormFromBounded' f x ≤ c * f x :=
      seminormFromBounded_le f_nonneg f_mul x
    rw [h, mul_zero] at hf
    exact hf.antisymm (seminormFromBounded_nonneg f_nonneg f_mul x)

Goal state after:
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_4
inst✝⁷ : ConditionallyCompleteLinearOrder R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : OrderTopology R
F : Filter ι
inst✝⁴ : AddCommSemigroup R
inst✝³ : Sub R
inst✝² : ContinuousSub R
inst✝¹ : OrderedSub R
inst✝ : AddLeftMono R
f : ι → R
c : R
cobdd : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) F f
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) F f
h✝ : F.NeBot
⊢ limsup (fun i ↦ c - f i) F = c - liminf f F

Tactic:
· exact (Antitone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ c - x)
    (fun _ _ h ↦ tsub_le_tsub_left h c) (continuous_sub_left c).continuousAt cobdd bdd_below).symm

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
hx : μ x = 0
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

Tactic:
by
  have h0 (n : ℕ) (hn : 1 ≤ n) : μ (x ^ n) ^ (1 / (n : ℝ)) = 0 := by
    have hμn : μ (x ^ n) = 0 := by
      apply le_antisymm _ (apply_nonneg μ _)
      rw [← zero_pow (pos_iff_ne_zero.mp hn), ← hx]
      exact map_pow_le_pow _ x (one_le_iff_ne_zero.mp hn)
    rw [hμn, zero_rpow (one_div_cast_ne_zero (one_le_iff_ne_zero.mp hn))]
  have hL0 : (iInf fun n : PNat => μ (x ^ (n : ℕ)) ^ (1 / (n : ℝ))) = 0 :=
    le_antisymm
      (ciInf_le_of_le (smoothingSeminormSeq_bddBelow μ x) (1 : PNat) (le_of_eq (h0 1 (le_refl _))))
      (le_ciInf fun n ↦ by positivity)
  simpa only [hL0] using tendsto_atTop_of_eventually_const h0

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
m n : ℕ
hmn : m ≤ n
hc_pos : 0 < f c
heq : m = n
⊢ n - m = 0

Tactic:
rw [heq, Nat.sub_self n]

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : Field L
inst✝ : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean norm
h1 : LinearIndepOn K id {1}
ι : Type u_2 := { x // x ∈ h1.extend ⋯ }
B : Basis ι K L := Basis.extend h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex B
hem : Nonempty ι
h1L : 1 ∈ h1.extend ⋯
hB1 : B ⟨1, h1L⟩ = 1
g : L → ℝ := B.norm
hg0 : g 0 = 0
hg_nonneg : ∀ (x : L), 0 ≤ g x
hg_ext : ∀ (x : K), g ((algebraMap K L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
hg_neg : ∀ (a : L), g (-a) = g a
w✝¹ : ℝ
w✝ : 0 < w✝¹
hg_bdd : ∀ (x y : L), B.norm (x * y) ≤ w✝¹ * B.norm x * B.norm y
hg_mul : ∀ (k : K) (y : L), g ((algebraMap K L) k * y) = g ((algebraMap K L) k) * g y
f : RingSeminorm L := seminormFromBounded hg0 hg_nonneg hg_bdd hg_add hg_neg
hf_na : IsNonarchimedean ⇑f
hf_1 : f 1 ≤ 1
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
F' : RingSeminorm L := smoothingSeminorm f hf_1 hf_na
hF' : F' = smoothingSeminorm f hf_1 hf_na
hF'_ext : ∀ (k : K), F' ((algebraMap K L) k) = ‖k‖
hF'_1 : F' 1 = 1
⊢ F' 1 ≠ 0 1

Tactic:
by rw [hF'_1]; exact one_ne_zero

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ Antitone (seminormFromConst_seq c f x)

Tactic:
by
  intro m n hmn
  simp only [seminormFromConst_seq]
  nth_rw 1 [← Nat.add_sub_of_le hmn]
  rw [pow_add, ← mul_assoc]
  have hc_pos : 0 < f c := lt_of_le_of_ne (apply_nonneg f _) hc.symm
  apply le_trans ((div_le_div_iff_of_pos_right (pow_pos hc_pos _)).mpr (map_mul_le_mul f _ _))
  cases hmn.eq_or_lt with
  | inl heq =>
    have hnm : n - m = 0 := by rw [heq, Nat.sub_self n]
    rw [hnm, heq, div_le_div_iff_of_pos_right (pow_pos hc_pos _), pow_zero]
    conv_rhs => rw [← mul_one (f (x * c ^ n))]
    gcongr
  | inr hlt =>
    have h1 : 1 ≤ n - m := by
      rw [Nat.one_le_iff_ne_zero]
      exact Nat.sub_ne_zero_of_lt hlt
    rw [hpm c h1, mul_div_assoc, div_eq_mul_inv, pow_sub₀ _ hc hmn, mul_assoc, mul_comm (f c ^ m)⁻¹,
      ← mul_assoc (f c ^ n), mul_inv_cancel₀ (pow_ne_zero n hc), one_mul, div_eq_mul_inv]

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
hseq : seminormFromConst_seq c f x = fun _n ↦ f x
⊢ Tendsto (fun _n ↦ f x) atTop (𝓝 (f x))

Tactic:
exact tendsto_const_nhds

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hseq : seminormFromConst_seq c f c = fun _n ↦ f c
⊢ Tendsto (fun _n ↦ f c) atTop (𝓝 (f c))

Tactic:
exact tendsto_const_nhds

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
⊢ (map (algebraMap L f.SplittingField) f).degree ≠ 0

Tactic:
simpa using degree_ne_of_natDegree_ne fnatdeg0

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
⊢ (map (algebraMap L f.SplittingField) f).degree ≠ 0

Tactic:
simpa using degree_ne_of_natDegree_ne fnatdeg0

Goal state after: