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

Goal state before:
pp: case neg.convert_3
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
⊢ Tendsto (fun n ↦ ↑n / (↑n + 1 - z)) atTop (𝓝 1)

Tactic:
convert! tendsto_natCast_div_add_atTop (1 - z) using 1; ext1 n; rw [add_sub_assoc]

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

Goal state before:
pp: n : ℕ
ihn : ∀ (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun s ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < ↑(n + 1)
⊢ -(s.re + 1) < ↑n

Tactic:
neg_add',

Goal state after:
n : ℕ
ihn : ∀ (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun s ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < ↑(n + 1)
⊢ -s.re - 1 < ↑n
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case refine_2
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
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
    dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
i j : Fin (2 + 1)
hij : i ≠ j
hi : i = i₁ ∧ j = i₂ ∨ i = i₂ ∧ j = i₁ ∨ i = i₁ ∧ j = i₃ ∨ i = i₃ ∧ j = i₁ ∨ i = i₂ ∧ j = i₃ ∨ i = i₃ ∧ j = i₂
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i₂)

Tactic:
rcases h with ⟨h₁, h₂⟩

Goal state after:
case refine_2
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
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
i j : Fin (2 + 1)
hij : i ≠ j
hi : i = i₁ ∧ j = i₂ ∨ i = i₂ ∧ j = i₁ ∨ i = i₁ ∧ j = i₃ ∨ i = i₃ ∧ j = i₁ ∨ i = i₂ ∧ j = i₃ ∨ i = i₃ ∧ j = i₂
h₁ : dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃)
h₂ : dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i₂)
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: case e_a.inr
q : ℍ
hv : ‖q.im‖ ≠ 0
⊢ normSq ↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) ^ 2 * normSq q.im = Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2

Tactic:
div_pow,

Goal state after:
case e_a.inr
q : ℍ
hv : ‖q.im‖ ≠ 0
⊢ normSq ↑(Real.cos ‖q.im‖) + Real.sin ‖q.im‖ ^ 2 / ‖q.im‖ ^ 2 * normSq q.im = Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : ↑(m + 1) < (a / max 1 ‖x‖) ^ m
⊢ ‖x + 1‖ ≤ a

Tactic:
div_pow,

Goal state after:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : ↑(m + 1) < a ^ m / max 1 ‖x‖ ^ m
⊢ ‖x + 1‖ ≤ a
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
p : RingSeminorm R
⊢ p ≠ 0 ↔ ∃ x, p x ≠ 0

Tactic:
by simp [eq_zero_iff]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f✝ : AlgebraNorm R S
f f' : MulAlgebraNorm R S
h : f.toMulRingSeminorm = f'.toMulRingSeminorm
⊢ f = f'

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
f' : MulAlgebraNorm R S
toMulRingSeminorm✝ : MulRingSeminorm S
eq_zero_of_map_eq_zero'✝ : ∀ (x : S), toMulRingSeminorm✝.toFun x = 0 → x = 0
smul'✝ :
  ∀ (a : R) (x : S),
    { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }.toFun (a • x) =
      ‖a‖ * { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }.toFun x
h :
  { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝,
        smul' := smul'✝ }.toMulRingSeminorm =
    f'.toMulRingSeminorm
⊢ { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝, smul' := smul'✝ } = f'
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
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
x y : R
⊢ seminormFromBounded' f (x + y) ≤ seminormFromBounded' f x + seminormFromBounded' f y

Tactic:
refine ciSup_le (fun z ↦ ?_)

Goal state after:
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
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
x y z : R
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x + seminormFromBounded' f y
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n ↦ ↑(n % m1) / ↑n) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ (L + ε) ^ (-(↑(n % m1) / ↑n)) * (μ x ^ (n % m1)) ^ (1 * 1 / ↑n)) atTop (𝓝 (1 * 1))

Tactic:
apply Tendsto.mul

Goal state after:
case hf
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n ↦ ↑(n % m1) / ↑n) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ (L + ε) ^ (-(↑(x % m1) / ↑x))) atTop (𝓝 1)

case hg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n ↦ ↑(n % m1) / ↑n) atTop (𝓝 0)
⊢ Tendsto (fun x_1 ↦ (μ x ^ (x_1 % m1)) ^ (1 * 1 / ↑x_1)) atTop (𝓝 1)
Module: Mathlib.Analysis.Normed.Field.Krasner

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Normal K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this✝¹ : FiniteDimensional K ↥K⟮y⟯
this✝ : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : z ∈ K⟮y⟯
⊢ x ∈ K⟮y⟯

Tactic:
simpa [z, y'] using add_mem this y'.2

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this✝³ : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this✝² : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst✝ : Algebra L C := iL.toAlgebra
this✝¹ : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this✝ : IsKrasner K C := of_completeSpace_of_normal K C
norm_iL : ∀ (x : L), ‖iL x‖ = ‖x‖
this : iL x ∈ K⟮iL y⟯
⊢ x ∈ K⟮y⟯

Tactic:
by
      simpa [← Set.image_singleton, ← IntermediateField.adjoin_map] using! this

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
⊢ smoothingFun μ 1 ≤ 1

Tactic:
by
  apply le_of_tendsto (tendsto_smoothingFun_of_map_one_le_one μ hμ1 (1 : R))
  simp only [eventually_atTop]
  use 1
  rintro n hn
  simp only [smoothingSeminormSeq]
  rw [one_pow]
  conv_rhs => rw [← one_rpow (1 / n : ℝ)]
  have hn1 : 0 < (1 / n : ℝ) := by
    apply _root_.div_pos zero_lt_one
    rw [← cast_zero, cast_lt]
    exact succ_le_iff.mp hn
  exact (rpow_le_rpow_iff (apply_nonneg μ _) zero_le_one hn1).mpr hμ1

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

Goal state before:
pp: case pos
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
x✝ : L
h✝ : x✝ ∈ s
⊢ 0 ≤ f x✝

pp: case neg
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
x✝ : L
h✝ : x✝ ∉ s
⊢ 0 ≤ 0

Tactic:
exacts [apply_nonneg _ _, le_refl _]

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

Goal state before:
pp: case neg
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
⊢ ∃ g, f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖

Tactic:
set b : ℕ → ℝ := fun i => (1 / 2) ^ i * (ε * ‖h‖ / 2) / C

Goal state after:
case neg
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
⊢ ∃ g, f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
ha : a = 0
⊢ limsup (fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a

Tactic:
calc limsup (fun n : ℕ => μ (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ))) atTop ≤
          limsup (fun n : ℕ => μ x ^ ((s (ψ n) : ℝ) * (1 / (ψ n : ℝ)))) atTop := by
          apply csInf_le_csInf _ (μ_nonempty μ hs_le ψ)
          · intro b hb
            simp only [eventually_map, eventually_atTop, Set.mem_ofPred_eq] at hb ⊢
            obtain ⟨m, hm⟩ := hb
            use m
            intro k hkm
            apply le_trans _ (hm k hkm)
            rw [rpow_mul (apply_nonneg μ x), rpow_natCast]
            gcongr
            exact map_pow_le_pow' hμ1 x _
          · use 0
            simp only [mem_lowerBounds, eventually_map, eventually_atTop,
              Set.mem_ofPred_eq, forall_exists_index]
            exact fun _ m hm ↦ le_trans (by positivity) (hm m (le_refl _))
      _ ≤ 1 := (μ_limsup_le_one μ hs_le hψ_lim)
      _ = smoothingFun μ x ^ a := by rw [ha, rpow_zero]

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

Goal state before:

Tactic:
‖v‖ = ‖i.inv (i.hom v)‖ := by rw [← comp_apply, Iso.hom_inv_id, id_apply]
    _ ≤ ‖i.hom v‖ := h2 _

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
F : Type u_3
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
hf : ∀ (x : M), ‖x‖ = 0 → f x = 0
x y : M
h : Inseparable x y
⊢ f (x - y) = 0

Tactic:
Metric.inseparable_iff,

Goal state after:
M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
F : Type u_3
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
hf : ∀ (x : M), ‖x‖ = 0 → f x = 0
x y : M
h : dist x y = 0
⊢ f (x - y) = 0
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: case mp
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
⊢ ‖x‖ = 0

Tactic:
rw [SeparationQuotient.mk_eq_zero_iff.mp]

Goal state after:
case mp
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
⊢ mk x = 0
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
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun n ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : ↑m ≠ 0
⊢ (μ (x ^ (m * n)) ^ (1 / ↑(m * n))) ^ m = μ ((x ^ m) ^ n) ^ (1 / ↑n)

Tactic:
rw [pow_mul, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), cast_mul, ← one_div_mul_one_div,
      mul_comm (1 / (m : ℝ)), mul_assoc, one_div_mul_cancel hm', mul_one]

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

Goal state before:
pp: case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : ↥(lp E p)
h : 0 < p.toReal
⊢ ‖Equiv.lpPiLp f‖ = ‖f‖

Tactic:
PiLp.norm_eq_sum h,

Goal state after:
case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : ↥(lp E p)
h : 0 < p.toReal
⊢ (∑ i, ‖(Equiv.lpPiLp f).ofLp i‖ ^ p.toReal) ^ (1 / p.toReal) = ‖f‖
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
K : Type u
inst✝³ : NontriviallyNormedField K
L : Type v
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
h1 : (spectralAlgNorm K L).toRingSeminorm 1 ≤ 1
x : L
hx : x ≠ 0
hx' : (spectralAlgNorm K L) x ≠ 0
k : K
y✝ y : L
⊢ spectralNorm K L ((algebraMap K L) k * y) = ‖k‖ * spectralNorm K L y

Tactic:
← Algebra.smul_def,

Goal state after:
R : Type u_1
K : Type u
inst✝³ : NontriviallyNormedField K
L : Type v
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
h1 : (spectralAlgNorm K L).toRingSeminorm 1 ≤ 1
x : L
hx : x ≠ 0
hx' : (spectralAlgNorm K L) x ≠ 0
k : K
y✝ y : L
⊢ spectralNorm K L (k • y) = ‖k‖ * spectralNorm K L y
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ ↑Q = ↑Q * ↑P + (↑Q - ↑Q * ↑P)

Tactic:
add_sub_cancel

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ ↑Q = ↑Q
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x✝ : ⨂[𝕜] (i : ι), E i
G : Type (max (max uE u𝕜) uι) := (⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker
G' : Submodule 𝕜 F := (lift f.toMultilinearMap).range
e : ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) ≃ₗ[𝕜] ↥(lift f.toMultilinearMap).range :=
  (lift f.toMultilinearMap).quotKerEquivRange
this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e
f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) :=
  lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)
x : (i : ι) → E i
⊢ ‖f x‖ ≤ ‖f‖ * ∏ i, ‖x i‖

Tactic:
exact f.le_opNorm x

Goal state after:
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✝¹ : NormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
m : (i : ι) → E i
⊢ ‖⨂ₜ[𝕜] (i : ι), m i‖ ≤ ∏ i, ‖m i‖

Tactic:
have hle := ciInf_le (bddBelow_projectiveSemiNormAux (⨂ₜ[𝕜] i, m i))
    ⟨FreeAddMonoid.of (1, m), by simp [mem_lifts_iff]⟩

Goal state after:
ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
m : (i : ι) → E i
hle : ⨅ p, projectiveSeminormAux ↑p ≤ projectiveSeminormAux ↑⟨FreeAddMonoid.of (1, m), ⋯⟩
⊢ ‖⨂ₜ[𝕜] (i : ι), m i‖ ≤ ∏ i, ‖m i‖
Module: Mathlib.Topology.Maps.Strict.Group

Goal state before:
pp: G : Type u_1
H : Type u_2
G' : Type u_3
H' : Type u_4
inst✝⁹ : Group G'
inst✝⁸ : Group H'
inst✝⁷ : Group G
inst✝⁶ : Group H
f : G →* H
g : G' →* H'
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalGroup G
inst✝² : TopologicalSpace G'
inst✝¹ : IsTopologicalGroup G'
inst✝ : TopologicalSpace H'
⊢ IsStrictMap ⇑(f.prodMap g) ↔ IsStrictMap ⇑f ∧ IsStrictMap ⇑g

Tactic:
simp_rw [MonoidHom.isStrictMap_iff_isOpenQuotientMap_rangeRestrict]
  let Φ : (f.prodMap g).range ≃ₜ f.range × g.range :=
    (Homeomorph.setCongr (by simp [Subgroup.coe_prod])).trans (Homeomorph.Set.prod _ _)
  have eq : Φ ∘ (f.prodMap g).rangeRestrict = f.rangeRestrict.prodMap g.rangeRestrict := rfl
  rw [← Φ.comp_isOpenQuotientMap_iff, eq, MonoidHom.coe_prodMap, isOpenQuotientMap_prodMap_iff]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: case refine_1
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
⊢ 0 x =
    ((normSeminorm 𝕜
            (ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
              PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)})).comp
        (toDualContinuousMultilinearMap PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}))
      x

Tactic:
simp only [Seminorm.zero_apply, Seminorm.comp_apply, coe_normSeminorm]

Goal state after:
case refine_1
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
⊢ 0 = ‖(toDualContinuousMultilinearMap PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}) x‖
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →L[𝕜] W := (apply' W (RingHom.id 𝕜)) z ∘SL (↑f).toContinuousLinearMap ∘SL (smulRightL 𝕜 V V) v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
this : ∀ (A : V →L[𝕜] V) (x : V), T (A x) = (f A) (T x)
d : StrongDual 𝕜 W
hd : d ((f (smulRight v u)) z) = 1
surj : Function.Surjective ⇑T
x y : V
hxy : T x = T y
⊢ x = y

Tactic:
by
    have h_smul : smulRight v x = smulRight v y := by
      apply f.injective <| ContinuousLinearMap.ext fun z ↦ ?_
      obtain ⟨w, rfl⟩ := surj z
      simp [← this, hxy]
    simpa [huv.isUnit.smul_left_cancel] using congr((fun f ↦ f u) $h_smul)

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
⊢ IsStrictMap ⇑u ∧ IsClosed[inst✝⁴] ↑(↑u).range ↔
    IsStrictMap ⇑(A.mkQL ∘SL u) ∧ IsClosed[QuotientModule.Quotient.topologicalSpace A] ↑(↑(A.mkQL ∘SL u)).range

Tactic:
by
  obtain ⟨S, A_compl_S⟩ := A_compl.exists_isTopCompl
  let Φ : (F ⧸ A) ≃L[𝕜] S := A.quotientEquivOfIsTopCompl S A_compl_S
  let i : S →L[𝕜] F := S.subtypeL
  have i_clemb : IsClosedEmbedding i := S.isClosedEmbedding_subtypeL A_compl_S.symm.isClosed
  set p : F →L[𝕜] F := S.projectionL A A_compl_S.symm with p_def
  have eq : i ∘ Φ ∘ A.mkQ = p := rfl
  have : u.toLinearMap ≈ (p ∘L u).toLinearMap := by
    grw [toLinearMap_comp, p_def, toLinearMap_projectionL, projection_equiv_id, LinearMap.id_comp]
  calc  IsStrictMap u ∧ IsClosed (range u)
    _ ↔ (IsStrictMap (p ∘ u) ∧ IsClosed (range (p ∘ u))) :=
          ContinuousLinearMap.isStrictMap_isClosed_range_iff_of_finiteRangeSetoid _ _ this
    _ ↔ (IsStrictMap (i ∘ Φ ∘ A.mkQ ∘ u) ∧ IsClosed (range (i ∘ Φ ∘ A.mkQ ∘ u))) := by
          simp_rw [← eq, Function.comp_assoc]
    _ ↔ (IsStrictMap (Φ ∘ A.mkQ ∘ u) ∧ IsClosed (range (Φ ∘ A.mkQ ∘ u))) := by
          rw [i_clemb.isStrictMap_iff, i_clemb.isClosed_iff_image_isClosed, ← range_comp]
    _ ↔ (IsStrictMap (A.mkQ ∘ u) ∧ IsClosed (range (A.mkQ ∘ u))) := by
          rw [Φ.isHomeomorph.isEmbedding.isStrictMap_iff,
            Φ.isHomeomorph.isClosedEmbedding.isClosed_iff_image_isClosed,
            ← range_comp]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ dt : ℝ
⊢ IsIntegralCurveAt (γ ∘ fun x ↦ x + dt) (v ∘ fun x ↦ x + dt) (t₀ - dt) ↔ IsIntegralCurveAt γ v t₀

Tactic:
isIntegralCurveAt_iff_exists_pos

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ dt : ℝ
⊢ (∃ ε > 0, IsIntegralCurveOn (γ ∘ fun x ↦ x + dt) (v ∘ fun x ↦ x + dt) (Metric.ball (t₀ - dt) ε)) ↔
    ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
hγ : IsIntegralCurveAt γ v t₀
a : ℝ
ha : a ≠ 0
⊢ IsIntegralCurveAt (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (t₀ / a)

Tactic:
isIntegralCurveAt_iff_exists_pos

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
hγ : ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)
a : ℝ
ha : a ≠ 0
⊢ ∃ ε > 0, IsIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (Metric.ball (t₀ / a) ε)
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
hQ : ¬Q = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atTop] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

Tactic:
refine
    (P.isEquivalent_atTop_lead.symm.div Q.isEquivalent_atTop_lead.symm).symm.trans
      (EventuallyEq.isEquivalent ((eventually_gt_atTop 0).mono fun x hx => ?_))

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
hQ : ¬Q = 0
x : 𝕜
hx : 0 < x
⊢ ((fun x ↦ P.leadingCoeff * x ^ P.natDegree) / fun x ↦ Q.leadingCoeff * x ^ Q.natDegree) x =
    (fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)) x