harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_affineSubspace {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [IsAddHaarMeasure μ]
    (s : AffineSubspace ℝ E) (hs : s ≠ ⊤) : μ s = 0

Proof state:
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : AffineSubspace ℝ E
hs : ¬s.direction = ⊤
hne : (↑s).Nonempty
⊢ μ ↑s = 0

Tactic:
rcases hne with ⟨x, hx : x ∈ s⟩

Result:
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : AffineSubspace ℝ E
hs : ¬s.direction = ⊤
x : E
hx : x ∈ s
⊢ μ ↑s = 0

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : AffineSubspace ℝ E
hs : s ≠ ⊤
⊢ μ ↑s = 0

Tactic:
rcases s.eq_bot_or_nonempty with (rfl | hne)

Result:
case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : ⊥ ≠ ⊤
⊢ μ ↑⊥ = 0

case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : AffineSubspace ℝ E
hs : s ≠ ⊤
hne : (↑s).Nonempty
⊢ μ ↑s = 0

Proof state:
case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : ⊥ ≠ ⊤
⊢ μ ↑⊥ = 0

Tactic:
rw [AffineSubspace.bot_coe, measure_empty]

Result:
no goals

Proof state:
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : AffineSubspace ℝ E
hs : ¬s.direction = ⊤
x : E
hx : x ∈ s
⊢ μ ↑s = 0

Tactic:
simpa only [AffineSubspace.coe_direction_eq_vsub_set_right hx, vsub_eq_sub, sub_eq_add_neg,
  image_add_right, neg_neg, measure_preimage_add_right] using addHaar_submodule μ s.direction hs

Result:
no goals

Proof state:
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : AffineSubspace ℝ E
hs : s ≠ ⊤
hne : (↑s).Nonempty
⊢ μ ↑s = 0

Tactic:
rw [Ne, ← AffineSubspace.direction_eq_top_iff_of_nonempty hne] at hs

Result:
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : AffineSubspace ℝ E
hs : ¬s.direction = ⊤
hne : (↑s).Nonempty
⊢ μ ↑s = 0
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma abs_lt_iff_mul_self_lt : |a| < |b| ↔ a * a < b * b

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ |a| < |b| ↔ |a| * |a| < |b| * |b|

Tactic:
exact mul_self_lt_mul_self_iff (abs_nonneg a) (abs_nonneg b)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ |a| < |b| ↔ a * a < b * b

Tactic:
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]

Result:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ |a| < |b| ↔ |a| * |a| < |b| * |b|
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthSup_le_iff {u : ℕ → ℝ≥0∞} {a : EReal} :
    expGrowthSup u ≤ a ↔ ∀ b > a, ∀ᶠ n : ℕ in atTop, u n < exp (b * n)

Proof state:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : n ≥ 1
⊢ (u n).log < b * ↑n ↔ u n < (b * ↑n).exp

Tactic:
nth_rw 1 [← EReal.log_exp (b * n)]

Result:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : n ≥ 1
⊢ (u n).log < (b * ↑n).exp.log ↔ u n < (b * ↑n).exp

Proof state:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : n ≥ 1
⊢ (u n).log / ↑n < b ↔ u n < (b * ↑n).exp

Tactic:
rw [EReal.div_lt_iff (by norm_cast) (natCast_ne_top n)]

Result:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : n ≥ 1
⊢ (u n).log < b * ↑n ↔ u n < (b * ↑n).exp

Proof state:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y > a, ∀ᶠ (a : ℕ) in atTop, (u a).log / ↑a < y) ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n < (b * ↑n).exp

Tactic:
refine forall₂_congr fun b _ ↦ eventually_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Result:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : n ≥ 1
⊢ (u n).log / ↑n < b ↔ u n < (b * ↑n).exp

Proof state:
u : ℕ → ℝ≥0∞
a : EReal
⊢ expGrowthSup u ≤ a ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n < (b * ↑n).exp

Tactic:
rw [expGrowthSup, Filter.limsup_le_iff]

Result:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y > a, ∀ᶠ (a : ℕ) in atTop, (u a).log / ↑a < y) ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n < (b * ↑n).exp

Proof state:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : n ≥ 1
⊢ 0 < ↑n

Tactic:
norm_cast

Result:
no goals

Proof state:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : n ≥ 1
⊢ (u n).log < (b * ↑n).exp.log ↔ u n < (b * ↑n).exp

Tactic:
exact logOrderIso.lt_iff_lt

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem exists_degree_lt [Fintype σ] (f : MvPolynomial σ R) (n : ℕ)
    (h : f.totalDegree < n * Fintype.card σ) {d : σ →₀ ℕ} (hd : d ∈ f.support) : ∃ i, d i < n

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ d i
⊢ ∑ s : σ, d s ≤ d.sum fun x e => e

Tactic:
rw [Finsupp.sum_fintype]

Result:
case h
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ d i
⊢ σ → 0 = 0

Proof state:
case h
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ d i
i✝ : σ
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
h : f.totalDegree < n * Fintype.card σ
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ ∃ i, d i < n

Tactic:
contrapose! h

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ d i
⊢ n * Fintype.card σ ≤ f.totalDegree

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ d i
⊢ n * Fintype.card σ ≤ f.totalDegree

Tactic:
calc
  n * Fintype.card σ = ∑ _s : σ, n := by
    rw [Finset.sum_const, Nat.nsmul_eq_mul, mul_comm, Finset.card_univ]
  _ ≤ ∑ s, d s := Finset.sum_le_sum fun s _ => h s
  _ ≤ d.sum fun _ e => e := by
    rw [Finsupp.sum_fintype]
    intros
    rfl
  _ ≤ f.totalDegree := le_totalDegree hd

Result:
no goals

Proof state:
case h
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ d i
⊢ σ → 0 = 0

Tactic:
intros

Result:
case h
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ d i
i✝ : σ
⊢ 0 = 0

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ d i
⊢ n * Fintype.card σ = ∑ _s : σ, n

Tactic:
rw [Finset.sum_const, Nat.nsmul_eq_mul, mul_comm, Finset.card_univ]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
theorem sup_mul : (M ⊔ N) * P = M * P ⊔ N * P :=
  le_antisymm (mul_le.mpr fun mn hmn p hp ↦ by
    obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn
    rw [right_distrib]; exact add_mem_sup (mul_mem_mul hm hp) <| mul_mem_mul hn hp)
    (sup_le (mul_le_mul_left le_sup_left) <| mul_le_mul_left le_sup_right)

Proof state:
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
mn : R
hmn : mn ∈ M ⊔ N
p : R
hp : p ∈ P
⊢ mn * p ∈ M * P ⊔ N * P

Tactic:
obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn

Result:
case intro.intro.intro.intro
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
p : R
hp : p ∈ P
m : R
hm : m ∈ M
n : R
hn : n ∈ N
hmn : m + n ∈ M ⊔ N
⊢ (m + n) * p ∈ M * P ⊔ N * P

Proof state:
case intro.intro.intro.intro
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
p : R
hp : p ∈ P
m : R
hm : m ∈ M
n : R
hn : n ∈ N
hmn : m + n ∈ M ⊔ N
⊢ (m + n) * p ∈ M * P ⊔ N * P

Tactic:
rw [right_distrib]

Result:
case intro.intro.intro.intro
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
p : R
hp : p ∈ P
m : R
hm : m ∈ M
n : R
hn : n ∈ N
hmn : m + n ∈ M ⊔ N
⊢ m * p + n * p ∈ M * P ⊔ N * P

Proof state:
case intro.intro.intro.intro
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
p : R
hp : p ∈ P
m : R
hm : m ∈ M
n : R
hn : n ∈ N
hmn : m + n ∈ M ⊔ N
⊢ m * p + n * p ∈ M * P ⊔ N * P

Tactic:
exact add_mem_sup (mul_mem_mul hm hp) <| mul_mem_mul hn hp

Result:
no goals
-- Mathlib/ModelTheory/Fraisse.lean
theorem age_directLimit {ι : Type w} [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι]
    (G : ι → Type max w w') [∀ i, L.Structure (G i)] (f : ∀ i j, i ≤ j → G i ↪[L] G j)
    [DirectedSystem G fun i j h => f i j h] : L.age (DirectLimit G f) = ⋃ i : ι, L.age (G i)

Proof state:
case h.mp.intro.intro.intro.intro
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
⊢ ∃ i, M ∈ L.age (G i)

Tactic:
refine ⟨i, Mfg, ⟨e'.comp ((Substructure.inclusion ?_).comp e.equivRange.toEmbedding)⟩⟩

Result:
case h.mp.intro.intro.intro.intro
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
⊢ e.toHom.range ≤ (DirectLimit.of L ι G f i).toHom.range
-- Mathlib/CategoryTheory/Functor/EpiMono.lean
theorem isSplitMono_iff [Full F] [Faithful F] : IsSplitMono (F.map f) ↔ IsSplitMono f

Proof state:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
h : IsSplitMono (F.map f)
⊢ IsSplitMono f

Tactic:
exact IsSplitMono.mk' ((splitMonoEquiv F f).invFun h.exists_splitMono.some)

Result:
no goals

Proof state:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ IsSplitMono f → IsSplitMono (F.map f)

Tactic:
intro h

Result:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
h : IsSplitMono f
⊢ IsSplitMono (F.map f)

Proof state:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
h : IsSplitMono f
⊢ IsSplitMono (F.map f)

Tactic:
exact IsSplitMono.mk' ((splitMonoEquiv F f).toFun h.exists_splitMono.some)

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ IsSplitMono (F.map f) ↔ IsSplitMono f

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ IsSplitMono (F.map f) → IsSplitMono f

case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ IsSplitMono f → IsSplitMono (F.map f)

Proof state:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ IsSplitMono (F.map f) → IsSplitMono f

Tactic:
intro h

Result:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
h : IsSplitMono (F.map f)
⊢ IsSplitMono f
-- Mathlib/Topology/UniformSpace/CompactConvergence.lean
theorem tendsto_iff_forall_isCompact_tendstoUniformlyOn
    {ι : Type u₃} {p : Filter ι} {F : ι → C(α, β)} {f} :
    Tendsto F p (𝓝 f) ↔ ∀ K, IsCompact K → TendstoUniformlyOn (fun i a => F i a) f p K

Proof state:
case mpr
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
⊢ (∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K) →
    ∀ (K : Set α), IsCompact K → ∀ (U : Set β), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U

Tactic:
intro h K hK U hU hf

Result:
case mpr
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen U
hf : MapsTo (⇑f) K U
⊢ ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U

Proof state:
case right
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → ∀ (U : Set β), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen V
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed W
hWU : W ⊆ V
s : Set α := K ∩ ⇑f ⁻¹' ball (f x) W
hnhds : s ∈ 𝓝[K] x
hcomp : IsCompact s
hmaps : MapsTo (⇑f) s (ball (f x) V)
g : ι
hg : MapsTo (⇑(F g)) s (ball (f x) V)
y : α
hy : y ∈ s
⊢ (f y, (fun i a => (F i) a) g y) ∈ U

Tactic:
exact hVU ⟨f x, hVsymm.mk_mem_comm.2 <| hmaps hy, hg hy⟩

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → ∀ (U : Set β), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen V
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a => (F i) a) n y) ∈ U

Tactic:
rcases mem_uniformity_isClosed hV with ⟨W, hW, hWc, hWU⟩

Result:
case mp.intro.intro.intro.intro.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → ∀ (U : Set β), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen V
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed W
hWU : W ⊆ V
⊢ ∃ t ∈ 𝓝[K] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a => (F i) a) n y) ∈ U
-- Mathlib/Data/Nat/ModEq.lean
theorem pow (m : ℕ) (h : a ≡ b [MOD n]) : a ^ m ≡ b ^ m [MOD n]

Proof state:
case zero
n a b : ℕ
h : a ≡ b [MOD n]
⊢ a ^ 0 ≡ b ^ 0 [MOD n]

Tactic:
rfl

Result:
no goals

Proof state:
case succ
n a b : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ d * a ≡ b ^ d * b [MOD n]

Tactic:
exact hd.mul h

Result:
no goals

Proof state:
n a b m : ℕ
h : a ≡ b [MOD n]
⊢ a ^ m ≡ b ^ m [MOD n]

Tactic:
induction m with
| zero => rfl
| succ d hd =>
  rw [Nat.pow_succ, Nat.pow_succ]
  exact hd.mul h

Result:
no goals

Proof state:
case succ
n a b : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ (d + 1) ≡ b ^ (d + 1) [MOD n]

Tactic:
rw [Nat.pow_succ, Nat.pow_succ]

Result:
case succ
n a b : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ d * a ≡ b ^ d * b [MOD n]
-- Mathlib/CategoryTheory/EqToHom.lean
theorem conj_eqToHom_iff_heq {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : X = Z) :
    f = eqToHom h ≫ g ≫ eqToHom h'.symm ↔ HEq f g

Proof state:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X Z : C
f : W ⟶ X
h' : X = Z
g : W ⟶ Z
⊢ f = eqToHom ⋯ ≫ g ≫ eqToHom ⋯ ↔ HEq f g

Tactic:
cases h'

Result:
case refl.refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X : C
f g : W ⟶ X
⊢ f = eqToHom ⋯ ≫ g ≫ eqToHom ⋯ ↔ HEq f g

Proof state:
case refl.refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X : C
f g : W ⟶ X
⊢ f = eqToHom ⋯ ≫ g ≫ eqToHom ⋯ ↔ HEq f g

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
h : W = Y
h' : X = Z
⊢ f = eqToHom h ≫ g ≫ eqToHom ⋯ ↔ HEq f g

Tactic:
cases h

Result:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X Z : C
f : W ⟶ X
h' : X = Z
g : W ⟶ Z
⊢ f = eqToHom ⋯ ≫ g ≫ eqToHom ⋯ ↔ HEq f g
-- Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean
theorem exists_eq_polynomial [Semiring Fq] {d : ℕ} {m : ℕ} (hm : Fintype.card Fq ^ d ≤ m)
    (b : Fq[X]) (hb : natDegree b ≤ d) (A : Fin m.succ → Fq[X])
    (hA : ∀ i, degree (A i) < degree b) : ∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀

Proof state:
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : ↑j < b.degree
⊢ (A i₁).coeff j = (A i₀).coeff j

Tactic:
apply congr_fun i_eq.symm ⟨j, _⟩

Result:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : ↑j < b.degree
⊢ j < d

Proof state:
case right
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
⊢ A i₁ = A i₀

Tactic:
ext j

Result:
case right.a
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
⊢ (A i₁).coeff j = (A i₀).coeff j
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem nnnorm_smulRight (f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G) :
    ‖f.smulRight z‖₊ = ‖f‖₊ * ‖z‖₊

Proof state:
case refine_2.inr
𝕜 : 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 𝕜
z : G
hz : 0 < ‖z‖₊
m : (i : ι) → E i
⊢ ‖f m‖₊ * ‖z‖₊ ≤ ‖(f.smulRight z) m‖₊

Tactic:
rw [smulRight_apply, nnnorm_smul]

Result:
no goals

Proof state:
case refine_2.inr
𝕜 : 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 𝕜
z : G
hz : 0 < ‖z‖₊
⊢ ‖f‖₊ * ‖z‖₊ ≤ ‖f.smulRight z‖₊

Tactic:
rw [← le_div_iff₀ hz, opNNNorm_le_iff]

Result:
case refine_2.inr
𝕜 : 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 𝕜
z : G
hz : 0 < ‖z‖₊
⊢ ∀ (m : (i : ι) → E i), ‖f m‖₊ ≤ ‖f.smulRight z‖₊ / ‖z‖₊ * ∏ i : ι, ‖m i‖₊

Proof state:
case refine_2.inl
𝕜 : 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 𝕜
z : G
hz : ‖z‖₊ = 0
⊢ ‖f‖₊ * ‖z‖₊ ≤ ‖f.smulRight z‖₊

Tactic:
simp [hz]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Trails.lean
theorem IsEulerian.isTrail {u v : V} {p : G.Walk u v} (h : p.IsEulerian) : p.IsTrail

Proof state:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
he : e ∈ p.edges
⊢ List.count e p.edges ≤ 1

Tactic:
exact (h e (edges_subset_edgeSet _ he)).le

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
⊢ List.count e p.edges ≤ 1

Tactic:
by_cases he : e ∈ p.edges

Result:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
he : e ∈ p.edges
⊢ List.count e p.edges ≤ 1

case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
he : e ∉ p.edges
⊢ List.count e p.edges ≤ 1

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
⊢ p.IsTrail

Tactic:
rw [isTrail_def, List.nodup_iff_count_le_one]

Result:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
⊢ ∀ (a : Sym2 V), List.count a p.edges ≤ 1

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
⊢ ∀ (a : Sym2 V), List.count a p.edges ≤ 1

Tactic:
intro e

Result:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
⊢ List.count e p.edges ≤ 1

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
he : e ∉ p.edges
⊢ List.count e p.edges ≤ 1

Tactic:
simp [List.count_eq_zero_of_not_mem he]

Result:
no goals