mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case inr.inl
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₃₄lt : i₃ < i₄
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
rw [dist_comm]

Goal state after:
case inr.inl
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₃₄lt : i₃ < i₄
⊢ dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₃) (s.points i₄)
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case inr.inr
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₄₃lt : i₄ < i₃
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
rw [dist_comm]

Goal state after:
case inr.inr
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₄₃lt : i₄ < i₃
⊢ dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₃) (s.points i₄)
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case pos
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
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.swap 0 j) = ⇑x ∘ s.points
⊢ dist (s.points j) (s.points 1) = dist (s.points j) (s.points ((Equiv.swap 0 j) 1))

Tactic:
convert! rfl

Goal state after:
case e'_3
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
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.swap 0 j) = ⇑x ∘ s.points
⊢ (Equiv.swap 0 j) 1 = 1
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case neg
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
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : ¬i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) = ⇑x ∘ s.points
⊢ dist (s.points i) (s.points j) =
    dist (s.points ((Equiv.swap 1 j) i)) (s.points ((Equiv.swap 1 j) ((Equiv.swap 0 i) 1)))

Tactic:
convert! rfl

Goal state after:
case e'_3.e'_3
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
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : ¬i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) = ⇑x ∘ s.points
⊢ (Equiv.swap 1 j) i = i

case e'_3.e'_4
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
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : ¬i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) = ⇑x ∘ s.points
⊢ (Equiv.swap 1 j) ((Equiv.swap 0 i) 1) = j
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
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₁ x₂ : Fin (2 + 1)
hx : (x₁, x₂).1 < (x₁, x₂).2
y₁ y₂ : Fin (2 + 1)
hy : (y₁, y₂).1 < (y₁, y₂).2
hxy :
  (fun i ↦ dist (t.points (↑i).1) (t.points (↑i).2)) ⟨(x₁, x₂), hx⟩ =
    (fun i ↦ dist (t.points (↑i).1) (t.points (↑i).2)) ⟨(y₁, y₂), hy⟩
⊢ ⟨(x₁, x₂), hx⟩ = ⟨(y₁, y₂), hy⟩

Tactic:
simp only at hx hy hxy

Goal state after:
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
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₁ x₂ : Fin (2 + 1)
hx : x₁ < x₂
y₁ y₂ : Fin (2 + 1)
hy : y₁ < y₂
hxy : dist (t.points x₁) (t.points x₂) = dist (t.points y₁) (t.points y₂)
⊢ ⟨(x₁, x₂), hx⟩ = ⟨(y₁, y₂), hy⟩
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: F : Type u_2
α : Type u_3
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
a : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ f (a ^ (n + 1)) * f a ≤ f a ^ (n + 1) * f a

Tactic:
map_pow_le_pow _ _ n.succ_ne_zero

Goal state after:
F : Type u_2
α : Type u_3
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
a : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ f a ^ n.succ * f a ≤ f a ^ (n + 1) * f a
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R✝ : Type u_1
R : Type u_2
inst✝ : NormedRing R
x : R
hx : ‖x‖ = 0
⊢ x = 0

Tactic:
← norm_eq_zero

Goal state after:
R✝ : Type u_1
R : Type u_2
inst✝ : NormedRing R
x : R
hx : ‖x‖ = 0
⊢ ‖x‖ = 0
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R✝ : Type u_1
R : Type u_2
inst✝ : NormedField R
x : R
hx : ‖x‖ = 0
⊢ x = 0

Tactic:
← norm_eq_zero

Goal state after:
R✝ : Type u_1
R : Type u_2
inst✝ : NormedField R
x : R
hx : ‖x‖ = 0
⊢ ‖x‖ = 0
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: case inl.refine_1
ι : Type u_1
R : Type u_4
inst✝⁷ : ConditionallyCompleteLinearOrder R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : OrderTopology R
inst✝⁴ : AddCommSemigroup R
inst✝³ : Sub R
inst✝² : ContinuousSub R
inst✝¹ : OrderedSub R
inst✝ : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) ⊥ f
x : R
hx : ∀ (a : R), x ≥ a
y : R
⊢ y ∈ Set.univ → x - x ≤ y

Tactic:
simp only [Set.mem_univ, true_implies]

Goal state after:
case inl.refine_1
ι : Type u_1
R : Type u_4
inst✝⁷ : ConditionallyCompleteLinearOrder R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : OrderTopology R
inst✝⁴ : AddCommSemigroup R
inst✝³ : Sub R
inst✝² : ContinuousSub R
inst✝¹ : OrderedSub R
inst✝ : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) ⊥ f
x : R
hx : ∀ (a : R), x ≥ a
y : R
⊢ x - x ≤ y
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case neg
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
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f = 0
⊢ f x ≤ ⨆ y, f x * (f y / f y)

Tactic:
· simp_rw [f_ne_zero, Pi.zero_apply, zero_div, zero_mul, ciSup_const]; rfl

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

Goal state before:
pp: K : Type u_1
inst✝² : NormedField K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
x : L
⊢ ⨆ σ, (algNormOfAlgEquiv σ) x = 0 → x = 0

Tactic:
by
    contrapose!
    exact fun hx ↦ ne_of_gt (lt_of_lt_of_le (map_pos_of_ne_zero _ hx)
      (Finite.le_ciSup (fun σ ↦ (algNormOfAlgEquiv σ) x) AlgEquiv.refl))

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

Goal state before:
pp: case neg
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
n : ℕ
hn : ¬n = 0
⊢ seminormFromConst_seq c f x n = f x

Tactic:
· simp only [seminormFromConst_seq, hx (c ^ n), hpm _ (Nat.one_le_iff_ne_zero.mpr hn),
          mul_div_assoc, div_self (pow_ne_zero n hc), mul_one]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x ↦ ‖u x‖) → ∃ a, Tendsto (fun n ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
obtain ⟨f, hf₁, hf₂⟩ := Metric.exists_subseq_summable_dist_of_cauchySeq u hu

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x ↦ ‖u x‖) → ∃ a, Tendsto (fun n ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i ↦ dist (u (f (i + 1))) (u (f i))
⊢ ∃ a, Tendsto u atTop (𝓝 a)
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
⊢ 0 ≤ smoothingFun μ x

Tactic:
apply ge_of_tendsto (tendsto_smoothingFun_of_map_one_le_one μ hμ1 x)

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
⊢ ∀ᶠ (c : ℕ) in atTop, 0 ≤ smoothingSeminormSeq μ x c
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
⊢ ↑(mu μ hn n) / ↑n ∈ Set.Icc 0 1

Tactic:
by
  refine Set.mem_Icc.mpr ⟨div_nonneg (cast_nonneg (mu μ hn n)) (cast_nonneg n), ?_⟩
  by_cases hn0 : n = 0
  · rw [hn0, cast_zero, div_zero]; exact zero_le_one
  · rw [div_le_one (cast_pos.mpr (Nat.pos_of_ne_zero hn0)), cast_le]
    exact mu_le _ _ _

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ BddAbove (Set.range fun x_1 ↦ μ (x ^ s (ψ ↑x_1)) ^ (1 / ↑(ψ ↑x_1)))

Tactic:
convert! μ_bddAbove μ hμ1 hs x ψ

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ (Set.range fun x_1 ↦ μ (x ^ s (ψ ↑x_1)) ^ (1 / ↑(ψ ↑x_1))) = Set.range fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
y : L
hy : y ≠ 0
hy_alg : IsAlgebraic K y
h : minpoly K y = X ^ (minpoly K y).natDegree
⊢ (minpoly K y).coeff 0 = 0

Tactic:
rw [h, coeff_X_pow, if_neg (ne_of_lt (minpoly.natDegree_pos hy_alg.isIntegral))]

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

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
x : L
hf1 : f 1 = 1
p : K[X] := ⋯
hp_sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
s : Multiset L
hs : Polynomial.map (algebraMap K L) (minpoly K x) = (Multiset.map (fun x ↦ X - C x) s).prod
h_lc : (algebraMap K L) (minpoly K x).leadingCoeff = 1
⊢ ∀ (x_1 : L), (if x_1 ∈ s then f x_1 else 0) ≤ ⨆ σ, f (σ x)

Tactic:
intro y

Goal state after:
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
x : L
hf1 : f 1 = 1
p : K[X] := minpoly K x
hp_sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
s : Multiset L
hs : Polynomial.map (algebraMap K L) (minpoly K x) = (Multiset.map (fun x ↦ X - C x) s).prod
h_lc : (algebraMap K L) (minpoly K x).leadingCoeff = 1
y : L
⊢ (if y ∈ s then f y else 0) ≤ ⨆ σ, f (σ x)
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
cond2 : g ≫ h = 0
⊢ explicitCokernelDesc cond ≫ h = 0

Tactic:
by
  rw [← cancel_epi (explicitCokernelπ f), ← Category.assoc, explicitCokernelπ_desc]
  simp [cond2]

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

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hn : Normal K L
hu : IsUltrametricDist K
⊢ spectralNorm K L = ⇑(invariantExtension K L)

Tactic:
by
  ext x
  have hna := hu.isNonarchimedean_norm
  set f := Classical.choose (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional h_fin hna)
    with hf
  have hf_pow : IsPowMul f := (Classical.choose_spec
    (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional h_fin hna)).1
  have hf_ext : ∀ (x : K), f (algebraMap K L x) = ‖x‖ := (Classical.choose_spec
    (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional h_fin hna)).2.1
  have hf_na : IsNonarchimedean f := (Classical.choose_spec
    (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional h_fin hna)).2.2
  rw [spectralNorm_eq_iSup_of_finiteDimensional_normal K L hf_pow hf_na hf_ext]
  simp only [invariantExtension_apply, algNormOfAlgEquiv_apply, hf]

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

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ↑‖x‖₊
hf_iso : ∀ (σ : Gal(L/K)) (x : L), f x = f (σ x)
x : L
σ : Gal(L/K)
⊢ f (σ x) = f x

Tactic:
rw [hf_iso σ x]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.Finsupp

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : PseudoMetricSpace X
f g : WithLp (↑p) (ι →₀ X)
⊢ 0 ≤ ((zipWith dist ⋯ f.ofLp g.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹

Tactic:
dsimp [sum]

Goal state after:
ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : PseudoMetricSpace X
f g : WithLp (↑p) (ι →₀ X)
⊢ 0 ≤ (∑ a ∈ (zipWith dist ⋯ f.ofLp g.ofLp).support, dist (f.ofLp a) (g.ofLp a) ^ ↑p) ^ (↑p)⁻¹
Module: Mathlib.Analysis.Normed.Lp.Finsupp

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : PseudoMetricSpace X
f g : WithLp (↑p) (ι →₀ X)
⊢ 0 ≤ ((zipWith dist ⋯ f.ofLp g.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹

Tactic:
dsimp [sum]; positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.Finsupp

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : MetricSpace X
f g : WithLp (↑p) (ι →₀ X)
⊢ 0 ≤ ((zipWith dist ⋯ f.ofLp g.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹

Tactic:
dsimp [sum]

Goal state after:
ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : MetricSpace X
f g : WithLp (↑p) (ι →₀ X)
⊢ 0 ≤ (∑ a ∈ (zipWith dist ⋯ f.ofLp g.ofLp).support, dist (f.ofLp a) (g.ofLp a) ^ ↑p) ^ (↑p)⁻¹
Module: Mathlib.Analysis.Normed.Lp.Finsupp

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : MetricSpace X
f g : WithLp (↑p) (ι →₀ X)
⊢ 0 ≤ ((zipWith dist ⋯ f.ofLp g.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹

Tactic:
dsimp [sum]; positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
E : Type u_2
F : Type u_4
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommMonoid F
inst✝ : Module R F
f : E ≃L[R] F
⊢ ⋯.leftInverse = ↑f.symm

Tactic:
by
  ext y
  calc f.hasLeftInverse.leftInverse y
    _ = f.hasLeftInverse.leftInverse (f (f.symm y)) := by simp
    _ = f.symm y := f.hasLeftInverse.leftInverse_leftInverse (f.symm y)

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_7
E : Type u_8
F : Type u_10
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →L[R] F
hf : f.HasLeftInverse
⊢ ∀ (x : F), (f ∘SL hf.leftInverse) x ∈ (↑f).range

Tactic:
intro y

Goal state after:
R : Type u_7
E : Type u_8
F : Type u_10
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →L[R] F
hf : f.HasLeftInverse
y : F
⊢ (f ∘SL hf.leftInverse) y ∈ (↑f).range
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
hf : Summable fun i ↦ ‖f i‖
⊢ Multipliable fun i ↦ ‖1 + f i‖

Tactic:
conv => enter [1, i]; rw [← sub_add_cancel ‖1 + f i‖ 1, add_comm]

Goal state after:
ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
hf : Summable fun i ↦ ‖f i‖
⊢ Multipliable fun i ↦ 1 + (‖1 + f i‖ - 1)
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_5
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
⊢ ‖mapL f‖ ≤ ∏ i, ‖f i‖

Tactic:
refine (ContinuousLinearMap.opNorm_le_iff (by positivity)).mpr fun x ↦ ?_

Goal state after:
ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_5
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
x : ⨂[𝕜] (i : ι), E i
⊢ ‖(mapL f) x‖ ≤ (∏ i, ‖f i‖) * ‖x‖
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
y : ι → ℝ
⊢ AntitoneOn (fun x ↦ dist x y) (Iic y)

Tactic:
refine fun y₁ hy₁ y₂ hy₂ hy ↦ NNReal.coe_le_coe.2 (Finset.sup_mono_fun fun i _ ↦ ?_)
  rw [Real.nndist_eq', Real.nnabs_of_nonneg (sub_nonneg_of_le (‹_ ≤ y› i : y₂ i ≤ y i)),
    Real.nndist_eq', Real.nnabs_of_nonneg (sub_nonneg_of_le (‹_ ≤ y› i : y₁ i ≤ y i))]
  exact Real.toNNReal_mono (sub_le_sub_left (hy _) _)

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜 E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space F
u : E →L[𝕜] F
A : Submodule 𝕜 F
inst✝ : FiniteDimensional 𝕜 ↥A
A_compl : A.ClosedComplemented
S : Submodule 𝕜 F
A_compl_S : IsTopCompl A S
Φ : (F ⧸ A) ≃L[𝕜] ↥S := A.quotientEquivOfIsTopCompl S A_compl_S
i : ↥S →L[𝕜] F := S.subtypeL
i_clemb : IsClosedEmbedding ⇑i
p : F →L[𝕜] F := S.projectionL A ⋯
p_def : p = S.projectionL A ⋯
eq : ⇑i ∘ ⇑Φ ∘ ⇑A.mkQ = ⇑p
this : ↑u ≈ ↑(p ∘SL u)
⊢ IsStrictMap (⇑i ∘ ⇑Φ ∘ ⇑A.mkQ ∘ ⇑u) ∧ IsClosed[inst✝⁴] (range (⇑i ∘ ⇑Φ ∘ ⇑A.mkQ ∘ ⇑u)) ↔
    IsStrictMap (⇑i ∘ ⇑Φ ∘ ⇑A.mkQ ∘ ⇑u) ∧ IsClosed[instTopologicalSpaceSubtype] (range (⇑Φ ∘ ⇑A.mkQ ∘ ⇑u))

Tactic:
i_clemb.isClosed_iff_image_isClosed,

Goal state after:
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜 E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space F
u : E →L[𝕜] F
A : Submodule 𝕜 F
inst✝ : FiniteDimensional 𝕜 ↥A
A_compl : A.ClosedComplemented
S : Submodule 𝕜 F
A_compl_S : IsTopCompl A S
Φ : (F ⧸ A) ≃L[𝕜] ↥S := A.quotientEquivOfIsTopCompl S A_compl_S
i : ↥S →L[𝕜] F := S.subtypeL
i_clemb : IsClosedEmbedding ⇑i
p : F →L[𝕜] F := S.projectionL A ⋯
p_def : p = S.projectionL A ⋯
eq : ⇑i ∘ ⇑Φ ∘ ⇑A.mkQ = ⇑p
this : ↑u ≈ ↑(p ∘SL u)
⊢ IsStrictMap (⇑i ∘ ⇑Φ ∘ ⇑A.mkQ ∘ ⇑u) ∧ IsClosed[inst✝⁴] (range (⇑i ∘ ⇑Φ ∘ ⇑A.mkQ ∘ ⇑u)) ↔
    IsStrictMap (⇑i ∘ ⇑Φ ∘ ⇑A.mkQ ∘ ⇑u) ∧ IsClosed[inst✝⁴] (⇑i '' range (⇑Φ ∘ ⇑A.mkQ ∘ ⇑u))
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: δ K ε x : ℝ
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x

Tactic:
by
  by_cases hK : K = 0
  · subst K
    simp only [gronwallBound_K0, zero_mul, zero_add]
    convert! ((hasDerivAt_id x).const_mul ε).const_add δ
    rw [mul_one]
  · simp only [gronwallBound_of_K_ne_0 hK]
    convert!
      (((hasDerivAt_id x).const_mul K).exp.const_mul δ).add
        ((((hasDerivAt_id x).const_mul K).exp.sub_const 1).const_mul (ε / K)) using 1
    simp only [id]
    field

Goal state after:
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
⊢ IsFixedPt f (fixedPoint f^[n] hf)

Tactic:
by
  set x := hf.fixedPoint f^[n]
  have hx : f^[n] x = x := hf.fixedPoint_isFixedPt
  have := hf.toLipschitzWith.dist_le_mul x (f x)
  rw [← iterate_succ_apply, iterate_succ_apply', hx] at this
  contrapose! this
  simpa using mul_lt_mul_of_pos_right (NNReal.coe_lt_one.2 hf.left) <| dist_pos.2 (Ne.symm this)

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case mk
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
r L : ℝ≥0
β : FunSpace t₀ x₀ r L
toFun✝ : ↑(Icc tmin tmax) → E
lipschitzWith✝ : LipschitzWith L toFun✝
mem_closedBall₀✝ : toFun✝ t₀ ∈ closedBall x₀ ↑r
h :
  ∀ (t : ↑(Icc tmin tmax)),
    { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ }.toFun t = β.toFun t
⊢ { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ } = β

Tactic:
cases β

Goal state after:
case mk.mk
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
r L : ℝ≥0
toFun✝¹ : ↑(Icc tmin tmax) → E
lipschitzWith✝¹ : LipschitzWith L toFun✝¹
mem_closedBall₀✝¹ : toFun✝¹ t₀ ∈ closedBall x₀ ↑r
toFun✝ : ↑(Icc tmin tmax) → E
lipschitzWith✝ : LipschitzWith L toFun✝
mem_closedBall₀✝ : toFun✝ t₀ ∈ closedBall x₀ ↑r
h :
  ∀ (t : ↑(Icc tmin tmax)),
    { toFun := toFun✝¹, lipschitzWith := lipschitzWith✝¹, mem_closedBall₀ := mem_closedBall₀✝¹ }.toFun t =
      { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ }.toFun t
⊢ { toFun := toFun✝¹, lipschitzWith := lipschitzWith✝¹, mem_closedBall₀ := mem_closedBall₀✝¹ } =
    { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ }