mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ rexp y * (z - y) < rexp y * (rexp (z - y) - 1)

Tactic:
by
        gcongr _ * ?_
        linarith [add_one_lt_exp h1.ne']

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
hxy' : 0 < x / y
hxy'' : x / y ≠ 1
⊢ 1 - x / y < -log (x / y)

Tactic:
linarith [log_lt_sub_one_of_pos hxy' hxy'']

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg.e_a
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ (Function.support fun x ↦ ‖f x‖ₑ ^ p.toReal) ⊆ s

Tactic:
have : ¬(p.toReal ≤ 0) := by simpa only [not_le] using ENNReal.toReal_pos hp0 hp_top

Goal state after:
case neg.e_a
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
this : ¬p.toReal ≤ 0
⊢ (Function.support fun x ↦ ‖f x‖ₑ ^ p.toReal) ⊆ s
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hy : y ∈ s
hxy : x < y
hxy' : f y < f x
this : StrictMonoOn (f ∘ ⇑(-AffineMap.id 𝕜 𝕜)) (⇑(-AffineMap.id 𝕜 𝕜) ⁻¹' s ∩ Set.Ici (-x))
⊢ StrictAntiOn f (s ∩ Set.Iic x)

Tactic:
simpa [Function.comp_def] using this.comp_strictAntiOn strictMonoOn_id.neg fun _ _ ↦ by simpa

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
⊢ ∏ i ∈ s, z i ^ w i = ∏ i ∈ s, x ^ w i

Tactic:
refine prod_congr rfl fun i hi => ?_

Goal state after:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
⊢ z i ^ w i = x ^ w i
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case neg
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
h_mul : (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
rwa [div_eq_mul_inv, div_eq_mul_inv, mul_add, mul_comm (a ^ p), mul_comm (b ^ p), ← mul_assoc, ←
    mul_assoc, mul_inv_cancel₀ hab_0, one_mul, one_mul] at h_mul

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case inr
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
⊢ eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)

Tactic:
obtain rfl | hq_top := eq_or_ne q ∞

Goal state after:
case inr.inl
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hpq : p ≤ ∞
hq0_lt : 0 < ∞
⊢ eLpNorm f p μ ≤ eLpNorm f ∞ μ * μ Set.univ ^ (1 / p.toReal - 1 / ∞.toReal)

case inr.inr
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
hq_top : q ≠ ∞
⊢ eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ q
⊢ ∀ (s : Finset ι), ∑ i ∈ s, (f i * g i) ^ r ≤ (∑' (i : ι), f i ^ p) ^ (r / p) * (∑' (i : ι), g i ^ q) ^ (r / q)

Tactic:
intro s

Goal state after:
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ q
s : Finset ι
⊢ ∑ i ∈ s, (f i * g i) ^ r ≤ (∑' (i : ι), f i ^ p) ^ (r / p) * (∑' (i : ι), g i ^ q) ^ (r / q)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ p
pos : 0 < p
⊢ ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p

Tactic:
intro s

Goal state after:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ p
pos : 0 < p
s : Finset ι
⊢ ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i ↦ (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
⊢ A = (∑' (i : ι), f i ^ p) ^ (1 / p)

Tactic:
rw [hf.tsum_eq, rpow_inv_rpow_self hp']

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i ↦ (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ p) ^ (1 / p)
⊢ ∃ C ≤ A + B, HasSum (fun i ↦ (f i + g i) ^ p) (C ^ p)

Tactic:
refine ⟨(∑' i, (f i + g i) ^ p) ^ (1 / p), ?_, ?_⟩

Goal state after:
case refine_1
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i ↦ (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ p) ^ (1 / p)
⊢ (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ A + B

case refine_2
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i ↦ (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ p) ^ (1 / p)
⊢ HasSum (fun i ↦ (f i + g i) ^ p) (((∑' (i : ι), (f i + g i) ^ p) ^ (1 / p)) ^ p)
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
ι : Type u_6
s : Finset ι
f : ι → ↥(Lp E p μ)
⊢ ↑↑(∑ i ∈ s, f i) =ᵐ[μ] ∑ i ∈ s, ↑↑(f i)

Tactic:
simp [AEEqFun.coeFn_finsetSum]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
hf_sum : Summable fun i ↦ f i ^ p
hg_sum : Summable fun i ↦ g i ^ q
⊢ (∑' (i : ι), (f i * g i) ^ r) ^ (1 / r) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)

Tactic:
by
  -- It's really inconvenient that `positivity` can't use `∀` hypotheses.
  have hf' : 0 ≤ ∑' i, f i ^ p := tsum_nonneg fun i ↦ rpow_nonneg (hf i) p
  have hg' : 0 ≤ ∑' i, g i ^ q := tsum_nonneg fun i ↦ rpow_nonneg (hg i) q
  have hr := hpqr.pos'
  convert
    rpow_le_rpow_iff (tsum_nonneg fun i ↦ by positivity [hf i, hg i]) (by positivity)
          (inv_eq_one_div r ▸ inv_pos.mpr hr) |>.mpr <|
      Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg hpqr hf hg hf_sum hg_sum
  rw [mul_rpow (rpow_nonneg hf' _) (rpow_nonneg hg' _), ← Real.rpow_mul hg', ← Real.rpow_mul hf']
  field_simp

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : ¬((∑ i ∈ s, f i ^ p) ^ (1 / p) = ∞ ∨ (∑ i ∈ s, g i ^ q) ^ (1 / q) = ∞)
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
replace H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤ := by
    simpa [ENNReal.rpow_eq_top_iff, asymm hpq.pos, asymm hpq.symm.pos, hpq.pos, hpq.symm.pos,
      ENNReal.sum_eq_top, not_or] using H'

Goal state after:
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
g✝ : E → F
c✝ : ℝ≥0
inst✝ : NormedSpace ℝ E
ν : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ≤ c • ν
f g : ↥(Lp E p ν)
this : μ ≪ ν
⊢ ↑↑(f + g) =ᵐ[μ] ↑↑f + ↑↑g

Tactic:
apply this.ae_eq

Goal state after:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
g✝ : E → F
c✝ : ℝ≥0
inst✝ : NormedSpace ℝ E
ν : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ≤ c • ν
f g : ↥(Lp E p ν)
this : μ ≪ ν
⊢ ↑↑(f + g) =ᵐ[ν] ↑↑f + ↑↑g
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
g : E → F
c✝¹ : ℝ≥0
inst✝ : NormedSpace ℝ E
ν : Measure α
c✝ : ℝ≥0∞
hc : c✝ ≠ ∞
h : μ ≤ c✝ • ν
c : ℝ
f : ↥(Lp E p ν)
this : μ ≪ ν
⊢ ↑↑(c • f) =ᵐ[μ] (RingHom.id ℝ) c • ↑↑f

Tactic:
apply this.ae_eq

Goal state after:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
g : E → F
c✝¹ : ℝ≥0
inst✝ : NormedSpace ℝ E
ν : Measure α
c✝ : ℝ≥0∞
hc : c✝ ≠ ∞
h : μ ≤ c✝ • ν
c : ℝ
f : ↥(Lp E p ν)
this : μ ≪ ν
⊢ ↑↑(c • f) =ᵐ[ν] (RingHom.id ℝ) c • ↑↑f
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
property✝ : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
⊢ (fun f ↦ ⟨(inl.trans f, inr.trans f), ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨(f, g), disj⟩ =>
            {
              toFun := fun x ↦
                match x with
                | Sum.inl a => f a
                | Sum.inr b => g b,
              inj' := ⋯ })
        ⟨(f, g), property✝⟩) =
    ⟨(f, g), property✝⟩

Tactic:
simp only
    rfl

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
hfg : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
by
  refine tendstoInMeasure_of_ne_top fun ε hε hε_top ↦ ?_
  replace hfg := ENNReal.Tendsto.const_mul (a := 1 / ε ^ p.toReal)
    (Tendsto.ennrpow_const p.toReal hfg) (Or.inr <| by simp [hε.ne'])
  simp only [mul_zero,
    ENNReal.zero_rpow_of_pos (ENNReal.toReal_pos hp_ne_zero hp_ne_top)] at hfg
  rw [ENNReal.tendsto_nhds_zero] at hfg ⊢
  intro δ hδ
  refine (hfg δ hδ).mono fun n hn => ?_
  refine le_trans ?_ hn
  rw [one_div, ← ENNReal.inv_mul_le_iff, inv_inv]
  · convert!
      mul_meas_ge_le_pow_eLpNorm' μ hp_ne_zero hp_ne_top ((hf n).sub hg).aestronglyMeasurable ε
      using 6
    simp [edist_eq_enorm_sub]
  · simp [hε_top]
  · simp [hε.ne']

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
⊢ Tendsto (fun x ↦ ↑(‖c‖₊ * x ^ (1 / p.toReal))) (𝓝 0) (𝓝 ↑0)

Tactic:
rw [ENNReal.tendsto_coe]

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
⊢ Tendsto (fun x ↦ ‖c‖₊ * x ^ (1 / p.toReal)) (𝓝 0) (𝓝 0)
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : ¬finrank 𝕜 ↥l.range = 0
⊢ Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑l

Tactic:
· -- In the case where `l` is surjective, we factor it as `φ : (E ⧸ l.ker) ≃ₗ[𝕜] 𝕜`. Note that
    -- `E ⧸ l.ker` is T2 since `l.ker` is closed.
    have : finrank 𝕜 (LinearMap.range l) = 1 :=
      le_antisymm (finrank_self 𝕜 ▸ (LinearMap.range l).finrank_le) (zero_lt_iff.mpr H)
    have hi : Function.Injective ((LinearMap.ker l).liftQ l (le_refl _)) := by
      rw [← LinearMap.ker_eq_bot]
      exact Submodule.ker_liftQ_eq_bot _ _ _ (le_refl _)
    have hs : Function.Surjective ((LinearMap.ker l).liftQ l (le_refl _)) := by
      rw [← LinearMap.range_eq_top, Submodule.range_liftQ]
      exact Submodule.eq_top_of_finrank_eq ((finrank_self 𝕜).symm ▸ this)
    let φ : (E ⧸ LinearMap.ker l) ≃ₗ[𝕜] 𝕜 :=
      LinearEquiv.ofBijective ((LinearMap.ker l).liftQ l (le_refl _)) ⟨hi, hs⟩
    have hlφ : (l : E → 𝕜) = φ ∘ (LinearMap.ker l).mkQ := by ext; rfl
    -- Since the quotient map `E →ₗ[𝕜] (E ⧸ l.ker)` is continuous, the continuity of `l` will follow
    -- form the continuity of `φ`.
    suffices Continuous φ.toEquiv by
      rw [hlφ]
      exact this.comp continuous_quot_mk
    -- The pullback by `φ.symm` of the quotient topology is a T2 topology on `𝕜`, because `φ.symm`
    -- is injective. Since `φ.symm` is linear, it is also a vector space topology.
    -- Hence, we know that it is equal to the topology induced by the norm.
    have : induced φ.toEquiv.symm inferInstance = hnorm.toUniformSpace.toTopologicalSpace := by
      refine unique_topology_of_t2 (topologicalAddGroup_induced φ.symm.toLinearMap)
        (continuousSMul_induced φ.symm.toMulActionHom) ?_
      rw [t2Space_iff]
      exact fun x y hxy =>
        @separated_by_continuous _ _ (induced _ _) _ _ _ continuous_induced_dom _ _
          (φ.toEquiv.symm.injective.ne hxy)
    -- Finally, the pullback by `φ.symm` is exactly the pushforward by `φ`, so we have to prove
    -- that `φ` is continuous when `𝕜` is endowed with the pushforward by `φ` of the quotient
    -- topology, which is trivial by definition of the pushforward.
    simp_rw +instances [this.symm, Equiv.induced_symm]
    exact continuous_coinduced_rng

Goal state after:
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_6 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_1 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_2 := ⋯;
    Fintype.card ι = n → Continuous[_, Pi.topologicalSpace] ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝² : Fintype ι
this✝¹ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this✝ : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this : FiniteDimensional 𝕜 E
⊢ ∀ (s : Submodule 𝕜 E), finrank 𝕜 ↥s = n → IsClosed[inst✝⁴] ↑s

Tactic:
intro s

Goal state after:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_6 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_1 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_2 := ⋯;
    Fintype.card ι = n → Continuous[_, Pi.topologicalSpace] ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝² : Fintype ι
this✝¹ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this✝ : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
⊢ finrank 𝕜 ↥s = n → IsClosed[inst✝⁴] ↑s
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: case succ
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_6 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_1 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_2 := ⋯;
    Fintype.card ι = n → Continuous[_, Pi.topologicalSpace] ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝² : Fintype ι
this✝¹ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this✝ : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this : FiniteDimensional 𝕜 E
⊢ Continuous[inst✝⁴, Pi.topologicalSpace] ⇑ξ.equivFun

Tactic:
have H₁ : ∀ s : Submodule 𝕜 E, finrank 𝕜 s = n → IsClosed (s : Set E) := by
      intro s s_dim
      let : IsUniformAddGroup s := s.toAddSubgroup.isUniformAddGroup
      let b := Basis.ofVectorSpace 𝕜 s
      have U : IsUniformEmbedding b.equivFun.symm.toEquiv := by
        have : Fintype.card (Basis.ofVectorSpaceIndex 𝕜 s) = n := by
          rw [← s_dim]
          exact (finrank_eq_card_basis b).symm
        have : Continuous b.equivFun := IH b inferInstance this
        exact
          b.equivFun.symm.isUniformEmbedding b.equivFun.symm.toLinearMap.continuous_on_pi this
      have : IsComplete (s : Set E) :=
        completeSpace_coe_iff_isComplete.1 ((completeSpace_congr U).1 inferInstance)
      exact this.isClosed

Goal state after:
case succ
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_6 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_1 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_2 := ⋯;
    Fintype.card ι = n → Continuous[_, Pi.topologicalSpace] ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝² : Fintype ι
this✝¹ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this✝ : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 ↥s = n → IsClosed[inst✝⁴] ↑s
⊢ Continuous[inst✝⁴, Pi.topologicalSpace] ⇑ξ.equivFun
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ ↑‖f m‖₊ ≤ ↑(‖f‖₊ * ∏ i, ‖m i‖₊)

Tactic:
by
    push_cast
    exact f.le_opNorm m

Goal state after:
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : CompleteSpace 𝕜
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : ContinuousSMul 𝕜 F
E : Type u_4
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
f : E →ₗ[𝕜] F
s : Submodule 𝕜 E
inst✝ : s.CoFG
h : IsClosed[inst✝⁶] ↑(Submodule.map f s)
t : Submodule 𝕜 E
s_compl_t : IsCompl s t
this : FiniteDimensional 𝕜 ↥t
⊢ IsClosed[inst✝⁶] ↑(Submodule.map f s ⊔ Submodule.map f t)

Tactic:
exact Submodule.isClosed_sup_finiteDimensional _ _ h

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: case inl
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace E
inst✝² : Countable ι
f : ι → X → E
hE : Nonempty E
inst✝¹ : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
inst✝ : ⊥.IsCountablyGenerated
⊢ StronglyMeasurable fun x ↦ ⊥.limUnder fun x_1 ↦ f x_1 x

Tactic:
simpa [limUnder, Filter.map_bot] using stronglyMeasurable_const

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ edist f g = ∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ

Tactic:
simp only [Lp.edist_def, eLpNorm, one_ne_zero, eLpNorm'_eq_lintegral_enorm, Pi.sub_apply,
    toReal_one, ENNReal.rpow_one, ne_eq, not_false_eq_true, div_self, ite_false]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ (if 1 = ∞ then eLpNormEssSup (↑↑f - ↑↑g) μ else ∫⁻ (a : α), ‖↑↑f a - ↑↑g a‖ₑ ∂μ) =
    ∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
hs : MeasurableSet s
⊢ LocallyIntegrable (fun x ↦ f ↑x) (Measure.comap Subtype.val μ) ↔ LocallyIntegrableOn f s μ

Tactic:
simp_rw [LocallyIntegrableOn, Subtype.forall', ← map_nhds_subtype_val]
  exact forall_congr' fun _ ↦ (MeasurableEmbedding.subtype_coe hs).integrableAtFilter_iff_comap.symm

Goal state after:
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
E : Type u_6
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
μ : Measure X
inst✝⁶ : OpensMeasurableSpace X
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : T2Space X
𝕜 : Type u_9
inst✝³ : NormedRing 𝕜
inst✝² : SecondCountableTopologyEither X 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : X → E
g : X → 𝕜
s : Set X
hs : IsLocallyClosed s
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn (fun x ↦ g x • f x) k μ

Tactic:
exact fun k hk_sub hk_c => (hf k hk_sub hk_c).continuousOn_smul (hg.mono hk_sub) hk_c

Goal state after: