harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/CommutingProbability.lean
theorem Subgroup.commProb_subgroup_le : commProb H ≤ commProb G * (H.index : ℚ) ^ 2

Proof state:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ Nat.card { p // Commute p.1 p.2 } ≤ Nat.card { p // Commute p.1 p.2 }

Tactic:
refine Finite.card_le_of_injective (fun p ↦ ⟨⟨p.1.1, p.1.2⟩, Subtype.ext_iff.mp p.2⟩) ?_

Result:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ Function.Injective fun p => ⟨(↑(↑p).1, ↑(↑p).2), ⋯⟩

Proof state:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
p q : { p // Commute p.1 p.2 }
h : (fun p => ⟨(↑(↑p).1, ↑(↑p).2), ⋯⟩) p = (fun p => ⟨(↑(↑p).1, ↑(↑p).2), ⋯⟩) q
⊢ p = q

Tactic:
simpa only [Subtype.ext_iff, Prod.ext_iff] using h

Result:
no goals

Proof state:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ commProb ↥H ≤ commProb G * ↑H.index ^ 2

Tactic:
rw [commProb_def, commProb_def, div_le_iff₀, mul_assoc, ← mul_pow, ← Nat.cast_mul,
  mul_comm H.index, H.card_mul_index, div_mul_cancel₀, Nat.cast_le]

Result:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ Nat.card { p // Commute p.1 p.2 } ≤ Nat.card { p // Commute p.1 p.2 }

case h
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ ↑(Nat.card G) ^ 2 ≠ 0

G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ 0 < ↑(Nat.card ↥H) ^ 2

Proof state:
case h
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ ↑(Nat.card G) ^ 2 ≠ 0

Tactic:
exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr Finite.card_pos.ne')

Result:
no goals

Proof state:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ 0 < ↑(Nat.card ↥H) ^ 2

Tactic:
exact pow_pos (Nat.cast_pos.mpr Finite.card_pos) 2

Result:
no goals

Proof state:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ Function.Injective fun p => ⟨(↑(↑p).1, ↑(↑p).2), ⋯⟩

Tactic:
exact fun p q h ↦ by simpa only [Subtype.ext_iff, Prod.ext_iff] using h

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem compQuasiMeasurePreserving_eq_mk (g : β →ₘ[ν] γ) (hf : QuasiMeasurePreserving f μ ν) :
    g.compQuasiMeasurePreserving f hf =
      mk (g ∘ f) (g.aestronglyMeasurable.comp_quasiMeasurePreserving hf)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
inst✝ : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : QuasiMeasurePreserving f μ ν
⊢ g.compQuasiMeasurePreserving f hf = mk (↑g ∘ f) ⋯

Tactic:
rw [← compQuasiMeasurePreserving_mk g.aestronglyMeasurable hf, mk_coeFn]

Result:
no goals
-- Mathlib/Algebra/Squarefree/Basic.lean
theorem pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right {k : ℕ}
    (hx : Squarefree x) (hp : Prime p) (h : p ^ (k + 1) ∣ x * y) :
    p ^ k ∣ y

Proof state:
case pos.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
hx' : ¬p ∣ x'
h : p ^ k ∣ x' * y
⊢ p ^ k ∣ y

Tactic:
exact hp.pow_dvd_of_dvd_mul_left _ hx' h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p * p ^ k ∣ p * (x' * y)
hx' : ¬p ∣ x'
⊢ p ^ k ∣ x' * y

Tactic:
exact (mul_dvd_mul_iff_left hp.ne_zero).mp h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x y p : R
k : ℕ
hx : Squarefree x
hp : Prime p
h : p ^ (k + 1) ∣ x * y
⊢ p ^ k ∣ y

Tactic:
by_cases hxp : p ∣ x

Result:
case pos
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x y p : R
k : ℕ
hx : Squarefree x
hp : Prime p
h : p ^ (k + 1) ∣ x * y
hxp : p ∣ x
⊢ p ^ k ∣ y

case neg
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x y p : R
k : ℕ
hx : Squarefree x
hp : Prime p
h : p ^ (k + 1) ∣ x * y
hxp : ¬p ∣ x
⊢ p ^ k ∣ y

Proof state:
case pos
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x y p : R
k : ℕ
hx : Squarefree x
hp : Prime p
h : p ^ (k + 1) ∣ x * y
hxp : p ∣ x
⊢ p ^ k ∣ y

Tactic:
obtain ⟨x', rfl⟩ := hxp

Result:
case pos.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p ^ (k + 1) ∣ p * x' * y
⊢ p ^ k ∣ y

Proof state:
case pos.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p ^ (k + 1) ∣ p * x' * y
⊢ p ^ k ∣ y

Tactic:
have hx' : ¬ p ∣ x' := fun contra ↦ hp.not_unit <| hx p (mul_dvd_mul_left p contra)

Result:
case pos.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p ^ (k + 1) ∣ p * x' * y
hx' : ¬p ∣ x'
⊢ p ^ k ∣ y

Proof state:
case pos.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p ^ (k + 1) ∣ p * x' * y
hx' : ¬p ∣ x'
⊢ p ^ k ∣ y

Tactic:
replace h : p ^ k ∣ x' * y := by
  rw [pow_succ', mul_assoc] at h
  exact (mul_dvd_mul_iff_left hp.ne_zero).mp h

Result:
case pos.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
hx' : ¬p ∣ x'
h : p ^ k ∣ x' * y
⊢ p ^ k ∣ y

Proof state:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p ^ (k + 1) ∣ p * x' * y
hx' : ¬p ∣ x'
⊢ p ^ k ∣ x' * y

Tactic:
rw [pow_succ', mul_assoc] at h

Result:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p * p ^ k ∣ p * (x' * y)
hx' : ¬p ∣ x'
⊢ p ^ k ∣ x' * y

Proof state:
case neg
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x y p : R
k : ℕ
hx : Squarefree x
hp : Prime p
h : p ^ (k + 1) ∣ x * y
hxp : ¬p ∣ x
⊢ p ^ k ∣ y

Tactic:
exact (pow_dvd_pow _ k.le_succ).trans (hp.pow_dvd_of_dvd_mul_left _ hxp h)

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
/-- This is a special case of `tsub_le_iff_right`, which should be used instead of this.
This is needed to prove `OrderedSub (Multiset α)`. -/
protected lemma sub_le_iff_le_add : s - t ≤ u ↔ s ≤ u + t

Proof state:
case empty
α : Type u_1
inst✝ : DecidableEq α
u s : Multiset α
⊢ s - 0 ≤ u ↔ s ≤ u + 0

Tactic:
simp [Multiset.sub_zero]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
u : Multiset α
a : α
s✝ : Multiset α
IH : ∀ {s : Multiset α}, s - s✝ ≤ u ↔ s ≤ u + s✝
s : Multiset α
⊢ s - a ::ₘ s✝ ≤ u ↔ s ≤ u + a ::ₘ s✝

Tactic:
simp [IH, erase_le_iff_le_cons]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s - t ≤ u ↔ s ≤ u + t

Tactic:
induction t using Multiset.induction_on generalizing s with
| empty => simp [Multiset.sub_zero]
| cons a s IH => simp [IH, erase_le_iff_le_cons]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem succ_ofInt' : ∀ n, ZNum.ofInt' (n + 1) = ZNum.ofInt' n + 1
  | (n : ℕ) => by
    change ZNum.ofInt' (n + 1 : ℕ) = ZNum.ofInt' (n : ℕ) + 1
    dsimp only [ZNum.ofInt', ZNum.ofInt']
    rw [Num.ofNat'_succ, Num.add_one, toZNum_succ, ZNum.add_one]
  | -[0+1] => by
    change ZNum.ofInt' 0 = ZNum.ofInt' (-[0+1]) + 1
    dsimp only [ZNum.ofInt', ZNum.ofInt']
    rw [ofNat'_succ, ofNat'_zero]; rfl
  | -[(n + 1)+1] => by
    change ZNum.ofInt' -[n+1] = ZNum.ofInt' -[(n + 1)+1] + 1
    dsimp only [ZNum.ofInt', ZNum.ofInt']
    rw [@Num.ofNat'_succ (n + 1), Num.add_one, toZNumNeg_succ,
      @ofNat'_succ n, Num.add_one, ZNum.add_one, pred_succ]

Proof state:
n : ℕ
⊢ ZNum.ofInt' ↑(n + 1) = ZNum.ofInt' ↑n + 1

Tactic:
dsimp only [ZNum.ofInt', ZNum.ofInt']

Result:
n : ℕ
⊢ (ofNat' (n + 1)).toZNum = (ofNat' n).toZNum + 1

Proof state:
n : ℕ
⊢ (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1 + 1)).toZNumNeg + 1

Tactic:
rw [@Num.ofNat'_succ (n + 1), Num.add_one, toZNumNeg_succ,
  @ofNat'_succ n, Num.add_one, ZNum.add_one, pred_succ]

Result:
no goals

Proof state:
⊢ ZNum.ofInt' 0 = ZNum.ofInt' -[0+1] + 1

Tactic:
dsimp only [ZNum.ofInt', ZNum.ofInt']

Result:
⊢ (ofNat' 0).toZNum = (ofNat' (0 + 1)).toZNumNeg + 1

Proof state:
n : ℕ
⊢ ZNum.ofInt' (-[n + 1+1] + 1) = ZNum.ofInt' -[n + 1+1] + 1

Tactic:
change ZNum.ofInt' -[n+1] = ZNum.ofInt' -[(n + 1)+1] + 1

Result:
n : ℕ
⊢ ZNum.ofInt' -[n+1] = ZNum.ofInt' -[n + 1+1] + 1

Proof state:
⊢ (ofNat' 0).toZNum = (ofNat' (0 + 1)).toZNumNeg + 1

Tactic:
rw [ofNat'_succ, ofNat'_zero]

Result:
⊢ toZNum 0 = (0 + 1).toZNumNeg + 1

Proof state:
n : ℕ
⊢ ZNum.ofInt' -[n+1] = ZNum.ofInt' -[n + 1+1] + 1

Tactic:
dsimp only [ZNum.ofInt', ZNum.ofInt']

Result:
n : ℕ
⊢ (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1 + 1)).toZNumNeg + 1

Proof state:
n : ℕ
⊢ (ofNat' (n + 1)).toZNum = (ofNat' n).toZNum + 1

Tactic:
rw [Num.ofNat'_succ, Num.add_one, toZNum_succ, ZNum.add_one]

Result:
no goals

Proof state:
⊢ ZNum.ofInt' (-[0+1] + 1) = ZNum.ofInt' -[0+1] + 1

Tactic:
change ZNum.ofInt' 0 = ZNum.ofInt' (-[0+1]) + 1

Result:
⊢ ZNum.ofInt' 0 = ZNum.ofInt' -[0+1] + 1

Proof state:
n : ℕ
⊢ ZNum.ofInt' (↑n + 1) = ZNum.ofInt' ↑n + 1

Tactic:
change ZNum.ofInt' (n + 1 : ℕ) = ZNum.ofInt' (n : ℕ) + 1

Result:
n : ℕ
⊢ ZNum.ofInt' ↑(n + 1) = ZNum.ofInt' ↑n + 1

Proof state:
⊢ toZNum 0 = (0 + 1).toZNumNeg + 1

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Subspace.lean
theorem span_eq_sInf {S : Set (ℙ K V)} : span S = sInf { W : Subspace K V| S ⊆ W }

Proof state:
case carrier.h.refine_1
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : ∀ (W : Subspace K V), S ⊆ ↑W → x ∈ W
⊢ x ∈ sInf {W | S ⊆ ↑W}

Tactic:
rintro W ⟨T, hT, rfl⟩

Result:
case carrier.h.refine_1.intro.intro
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : ∀ (W : Subspace K V), S ⊆ ↑W → x ∈ W
T : Subspace K V
hT : T ∈ {W | S ⊆ ↑W}
⊢ x ∈ ↑T

Proof state:
case carrier.h
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
⊢ x ∈ (span S).carrier ↔ x ∈ (sInf {W | S ⊆ ↑W}).carrier

Tactic:
simp_rw [mem_carrier_iff, mem_span x]

Result:
case carrier.h
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
⊢ (∀ (W : Subspace K V), S ⊆ ↑W → x ∈ W) ↔ x ∈ sInf {W | S ⊆ ↑W}

Proof state:
case carrier.h.refine_2
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : x ∈ sInf {W | S ⊆ ↑W}
W : Subspace K V
hW : S ⊆ ↑W
⊢ x ∈ W

Tactic:
exact (@sInf_le _ _ { W : Subspace K V | S ⊆ ↑W } W hW) hx

Result:
no goals

Proof state:
case carrier.h.refine_1.intro.intro
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : ∀ (W : Subspace K V), S ⊆ ↑W → x ∈ W
T : Subspace K V
hT : T ∈ {W | S ⊆ ↑W}
⊢ x ∈ ↑T

Tactic:
exact hx T hT

Result:
no goals

Proof state:
case carrier.h
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
⊢ (∀ (W : Subspace K V), S ⊆ ↑W → x ∈ W) ↔ x ∈ sInf {W | S ⊆ ↑W}

Tactic:
refine ⟨fun hx => ?_, fun hx W hW => ?_⟩

Result:
case carrier.h.refine_1
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : ∀ (W : Subspace K V), S ⊆ ↑W → x ∈ W
⊢ x ∈ sInf {W | S ⊆ ↑W}

case carrier.h.refine_2
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : x ∈ sInf {W | S ⊆ ↑W}
W : Subspace K V
hW : S ⊆ ↑W
⊢ x ∈ W

Proof state:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
⊢ span S = sInf {W | S ⊆ ↑W}

Tactic:
ext x

Result:
case carrier.h
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
⊢ x ∈ (span S).carrier ↔ x ∈ (sInf {W | S ⊆ ↑W}).carrier
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem polynomial_not_isField : ¬IsField R[X]

Proof state:
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
⊢ ¬IsField R[X]

Tactic:
intro hR

Result:
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
⊢ False

Proof state:
case intro
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p = 0
⊢ False

Tactic:
exact hp0 this

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
⊢ False

Tactic:
obtain ⟨p, hp⟩ := hR.mul_inv_cancel X_ne_zero

Result:
case intro
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
⊢ False

Proof state:
case intro
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
⊢ False

Tactic:
have hp0 : p ≠ 0 := right_ne_zero_of_mul_eq_one hp

Result:
case intro
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
⊢ False

Proof state:
case intro
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p.degree < (p * X).degree
⊢ False

Tactic:
rw [← X_mul, congr_arg degree hp, degree_one, Nat.WithBot.lt_zero_iff, degree_eq_bot] at this

Result:
case intro
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p = 0
⊢ False

Proof state:
case intro
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
⊢ False

Tactic:
have := degree_lt_degree_mul_X hp0

Result:
case intro
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p.degree < (p * X).degree
⊢ False

Proof state:
R : Type u
inst✝ : Ring R
⊢ ¬IsField R[X]

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
⊢ ¬IsField R[X]
-- Mathlib/Algebra/Module/Submodule/Pointwise.lean
lemma mem_singleton_set_smul [SMulCommClass R S M] (r : S) (x : M) :
    x ∈ ({r} : Set S) • N ↔ ∃ (m : M), m ∈ N ∧ x = r • m

Proof state:
case mp.add
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass R S M
r : S
x m₁ m₂ : M
mem₁ : m₁ ∈ {r} • N
mem₂ : m₂ ∈ {r} • N
h₁ : ∃ m ∈ N, m₁ = r • m
h₂ : ∃ m ∈ N, m₂ = r • m
⊢ ∃ m ∈ N, m₁ + m₂ = r • m

Tactic:
rcases h₁ with ⟨m₁, h₁, rfl⟩

Result:
case mp.add.intro.intro
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass R S M
r : S
x m₂ : M
mem₂ : m₂ ∈ {r} • N
h₂ : ∃ m ∈ N, m₂ = r • m
m₁ : M
h₁ : m₁ ∈ N
mem₁ : r • m₁ ∈ {r} • N
⊢ ∃ m ∈ N, r • m₁ + m₂ = r • m
-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
lemma netEntropyInfEntourage_univ (T : X → X) {F : Set X} (h : F.Nonempty) :
    netEntropyInfEntourage T F univ = 0

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
⊢ netEntropyInfEntourage T F univ = 0

Tactic:
simp [netEntropyInfEntourage, netMaxcard_univ T h]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigOWith.eq_zero_imp (h : IsBigOWith c l f'' g'') : ∀ᶠ x in l, g'' x = 0 → f'' x = 0 :=
  Eventually.mono h.bound fun x hx hg => norm_le_zero_iff.1 <| by simpa [hg] using hx

Proof state:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
c : ℝ
f'' : α → E''
g'' : α → F''
l : Filter α
h : IsBigOWith c l f'' g''
x : α
hx : ‖f'' x‖ ≤ c * ‖g'' x‖
hg : g'' x = 0
⊢ ‖f'' x‖ ≤ 0

Tactic:
simpa [hg] using hx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem foldrM_attachWith [Monad m] [LawfulMonad m]
    (l : Array α) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : { x // q x} → β → m β} {b} (w : start = l.size):
    (l.attachWith q H).foldrM f b start 0 =
      l.attach.foldrM (fun a acc => f ⟨a.1, H _ a.2⟩ acc) b

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
q : α → Prop
H : ∀ (a : α), a ∈ l → q a
f : { x // q x } → β → m β
b : β
⊢ foldrM f b (l.attachWith q H) l.size = foldrM (fun a acc => f ⟨a.val, ⋯⟩ acc) b l.attach

Tactic:
rcases l with ⟨l⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
q : α → Prop
f : { x // q x } → β → m β
b : β
l : List α
H : ∀ (a : α), a ∈ { toList := l } → q a
⊢ foldrM f b ({ toList := l }.attachWith q H) { toList := l }.size =
    foldrM (fun a acc => f ⟨a.val, ⋯⟩ acc) b { toList := l }.attach

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
start : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
q : α → Prop
H : ∀ (a : α), a ∈ l → q a
f : { x // q x } → β → m β
b : β
w : start = l.size
⊢ foldrM f b (l.attachWith q H) start = foldrM (fun a acc => f ⟨a.val, ⋯⟩ acc) b l.attach

Tactic:
subst w

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
q : α → Prop
H : ∀ (a : α), a ∈ l → q a
f : { x // q x } → β → m β
b : β
⊢ foldrM f b (l.attachWith q H) l.size = foldrM (fun a acc => f ⟨a.val, ⋯⟩ acc) b l.attach

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
q : α → Prop
f : { x // q x } → β → m β
b : β
l : List α
H : ∀ (a : α), a ∈ { toList := l } → q a
⊢ foldrM f b ({ toList := l }.attachWith q H) { toList := l }.size =
    foldrM (fun a acc => f ⟨a.val, ⋯⟩ acc) b { toList := l }.attach

Tactic:
simp [List.foldrM_map]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Triangulated.lean
lemma essImageDistTriang_mem_of_iso {T₁ T₂ : Triangle D} (e : T₂ ≅ T₁)
    (h : T₁ ∈ L.essImageDistTriang) : T₂ ∈ L.essImageDistTriang

Proof state:
case intro.intro
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : HasShift D ℤ
inst✝ : L.CommShift ℤ
T₁ T₂ : Triangle D
e : T₂ ≅ T₁
T' : Triangle C
e' : T₁ ≅ L.mapTriangle.obj T'
hT' : T' ∈ distinguishedTriangles
⊢ T₂ ∈ L.essImageDistTriang

Tactic:
exact ⟨T', e ≪≫ e', hT'⟩

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : HasShift D ℤ
inst✝ : L.CommShift ℤ
T₁ T₂ : Triangle D
e : T₂ ≅ T₁
h : T₁ ∈ L.essImageDistTriang
⊢ T₂ ∈ L.essImageDistTriang

Tactic:
obtain ⟨T', e', hT'⟩ := h

Result:
case intro.intro
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : HasShift D ℤ
inst✝ : L.CommShift ℤ
T₁ T₂ : Triangle D
e : T₂ ≅ T₁
T' : Triangle C
e' : T₁ ≅ L.mapTriangle.obj T'
hT' : T' ∈ distinguishedTriangles
⊢ T₂ ∈ L.essImageDistTriang
-- Mathlib/Analysis/InnerProductSpace/Positive.lean
theorem IsPositive.conj_orthogonalProjection (U : Submodule 𝕜 E) {T : E →L[𝕜] E} (hT : T.IsPositive)
    [CompleteSpace U] :
    (U.subtypeL ∘L
        orthogonalProjection U ∘L T ∘L U.subtypeL ∘L orthogonalProjection U).IsPositive

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
U : Submodule 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
inst✝ : CompleteSpace ↥U
this :
  ((U.subtypeL.comp (orthogonalProjection U)).comp
      (T.comp (adjoint (U.subtypeL.comp (orthogonalProjection U))))).IsPositive
⊢ (U.subtypeL.comp ((orthogonalProjection U).comp (T.comp (U.subtypeL.comp (orthogonalProjection U))))).IsPositive

Tactic:
rwa [(orthogonalProjection_isSelfAdjoint U).adjoint_eq] at this

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
U : Submodule 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
inst✝ : CompleteSpace ↥U
⊢ (U.subtypeL.comp ((orthogonalProjection U).comp (T.comp (U.subtypeL.comp (orthogonalProjection U))))).IsPositive

Tactic:
have := hT.conj_adjoint (U.subtypeL ∘L orthogonalProjection U)

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
U : Submodule 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
inst✝ : CompleteSpace ↥U
this :
  ((U.subtypeL.comp (orthogonalProjection U)).comp
      (T.comp (adjoint (U.subtypeL.comp (orthogonalProjection U))))).IsPositive
⊢ (U.subtypeL.comp ((orthogonalProjection U).comp (T.comp (U.subtypeL.comp (orthogonalProjection U))))).IsPositive
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mlieBracketWithin_add_left
    (hV : MDifferentiableWithinAt I I.tangent (fun x ↦ (V x : TangentBundle I M)) s x)
    (hV₁ : MDifferentiableWithinAt I I.tangent (fun x ↦ (V₁ x : TangentBundle I M)) s x)
    (hs : UniqueMDiffWithinAt I s x) :
    mlieBracketWithin I (V + V₁) W s x =
      mlieBracketWithin I V W s x + mlieBracketWithin I V₁ W s x

Proof state:
case hs
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W V₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) s x
hV₁ : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V₁ x }) s x
hs : UniqueMDiffWithinAt I s x
⊢ UniqueDiffWithinAt 𝕜 (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
exact uniqueMDiffWithinAt_iff_inter_range.1 hs

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_filterMap' (f : α → Option β) (l : Array α) (w : stop = l.size) :
    (l.filterMap f 0 stop).toList = l.toList.filterMap f

Proof state:
case refine_3
α : Type u_1
β : Type u_2
f : α → Option β
l✝ : Array α
l : List α
this : ∀ (a : Array β), (List.foldlM ?refine_1 a l).run.toList = a.toList ++ List.filterMap f l
⊢ (List.foldlM
          (fun bs a => do
            let __do_lift ← f a
            match __do_lift with
              | some b => pure (bs.push b)
              | none => pure bs)
          #[] l).run.toList =
    List.filterMap f l

case refine_1
α : Type u_1
β : Type u_2
f : α → Option β
l✝ : Array α
l : List α
a : Array β
⊢ Array β → α → Id (Array β)

case refine_2
α : Type u_1
β : Type u_2
f : α → Option β
l✝ : Array α
l : List α
⊢ ∀ (a : Array β), (List.foldlM ?refine_1 a l).run.toList = a.toList ++ List.filterMap f l

Tactic:
exact this #[]

Result:
case refine_2
α : Type u_1
β : Type u_2
f : α → Option β
l✝ : Array α
l : List α
⊢ ∀ (a : Array β),
    (List.foldlM
            (fun bs a => do
              let __do_lift ← f a
              match __do_lift with
                | some b => pure (bs.push b)
                | none => pure bs)
            a l).run.toList =
      a.toList ++ List.filterMap f l
-- Mathlib/Order/LiminfLimsup.lean
theorem limsup_compl : (limsup u f)ᶜ = liminf (compl ∘ u) f

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
⊢ (limsup u f)ᶜ = liminf (compl ∘ u) f

Tactic:
simp only [limsup_eq_iInf_iSup, compl_iInf, compl_iSup, liminf_eq_iSup_iInf, Function.comp_apply]

Result:
no goals