harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Fold.lean
theorem denote_go_and {aig : AIG α} (acc : AIG.Ref aig) (curr : Nat) (hcurr : curr ≤ len)
    (input : RefVec aig len) :
    ⟦
      (go aig acc curr len input mkAndCached).aig,
      (go aig acc curr len input mkAndCached).ref,
      assign
    ⟧
      =
    (
      ⟦aig, acc, assign⟧
        ∧
      (∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦aig, input.get idx hidx1, assign⟧)
    )

Proof state:
case isTrue.mpr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefVec len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦assign, { aig := aig, ref := acc }⟧ = true
hrest : ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦assign, { aig := aig, ref := input.get idx hidx1 }⟧ = true
⊢ (⟦assign, { aig := aig, ref := acc }⟧ = true ∧ ⟦assign, { aig := aig, ref := input.get curr h✝ }⟧ = true) ∧
    ∀ (idx : Nat) (hidx1 : idx < len),
      curr + 1 ≤ idx →
        ⟦assign,
            { aig := (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig,
              ref := (input.get idx hidx1).cast ⋯ }⟧ =
          true

Tactic:
constructor

Result:
case isTrue.mpr.left
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefVec len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦assign, { aig := aig, ref := acc }⟧ = true
hrest : ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦assign, { aig := aig, ref := input.get idx hidx1 }⟧ = true
⊢ ⟦assign, { aig := aig, ref := acc }⟧ = true ∧ ⟦assign, { aig := aig, ref := input.get curr h✝ }⟧ = true

case isTrue.mpr.right
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefVec len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
hacc : ⟦assign, { aig := aig, ref := acc }⟧ = true
hrest : ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦assign, { aig := aig, ref := input.get idx hidx1 }⟧ = true
⊢ ∀ (idx : Nat) (hidx1 : idx < len),
    curr + 1 ≤ idx →
      ⟦assign,
          { aig := (aig.mkAndCached { lhs := acc, rhs := input.get curr h✝ }).aig,
            ref := (input.get idx hidx1).cast ⋯ }⟧ =
        true
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a fallback : α} :
    (m.erase k).getKeyD a fallback = if k == a then fallback else m.getKeyD a fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a fallback : α
⊢ (m.erase k).getKeyD a fallback = if (k == a) = true then fallback else m.getKeyD a fallback

Tactic:
simp_to_model [erase] using List.getKeyD_eraseKey

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
/-- If there is a solution then there is a minimal one. -/
lemma Solution.exists_minimal : ∃ (S₁ : Solution hζ), S₁.isMinimal

Proof state:
case intro
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
T : Set ℕ := {n | ∃ S', S'.multiplicity = n}
S₁ : Solution hζ
hS₁ : S₁.multiplicity = Nat.find ⋯
⊢ ∃ S₁, S₁.isMinimal

Tactic:
exact ⟨S₁, fun S'' ↦ hS₁ ▸ Nat.find_min' _ ⟨S'', rfl⟩⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
T : Set ℕ := {n | ∃ S', S'.multiplicity = n}
⊢ ∃ S₁, S₁.isMinimal

Tactic:
rcases Nat.find_spec (⟨S.multiplicity, ⟨S, rfl⟩⟩ : T.Nonempty) with ⟨S₁, hS₁⟩

Result:
case intro
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
T : Set ℕ := {n | ∃ S', S'.multiplicity = n}
S₁ : Solution hζ
hS₁ : S₁.multiplicity = Nat.find ⋯
⊢ ∃ S₁, S₁.isMinimal

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
⊢ ∃ S₁, S₁.isMinimal

Tactic:
let T := {n | ∃ (S' : Solution hζ), S'.multiplicity = n}

Result:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
T : Set ℕ := {n | ∃ S', S'.multiplicity = n}
⊢ ∃ S₁, S₁.isMinimal

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
⊢ ∃ S₁, S₁.isMinimal

Tactic:
classical
let T := {n | ∃ (S' : Solution hζ), S'.multiplicity = n}
rcases Nat.find_spec (⟨S.multiplicity, ⟨S, rfl⟩⟩ : T.Nonempty) with ⟨S₁, hS₁⟩
exact ⟨S₁, fun S'' ↦ hS₁ ▸ Nat.find_min' _ ⟨S'', rfl⟩⟩

Result:
no goals
-- Mathlib/NumberTheory/WellApproximable.lean
theorem mem_approxAddOrderOf_iff {δ : ℝ} {x : UnitAddCircle} {n : ℕ} (hn : 0 < n) :
    x ∈ approxAddOrderOf UnitAddCircle n δ ↔ ∃ m < n, gcd m n = 1 ∧ ‖x - ↑((m : ℝ) / n)‖ < δ

Proof state:
case mp.intro.intro.intro.intro.intro
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
m : ℕ
hm₁ : m < n
hm₂ : m.gcd n = 1
hx : ‖x - ↑(↑m / ↑n)‖ < δ
⊢ ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ

Tactic:
exact ⟨m, hm₁, hm₂, hx⟩

Result:
no goals

Proof state:
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
⊢ (∃ b, (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n) = b) ∧ ‖x - b‖ < δ) ↔ ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ

Tactic:
constructor

Result:
case mp
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
⊢ (∃ b, (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n) = b) ∧ ‖x - b‖ < δ) → ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ

case mpr
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
⊢ (∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ) → ∃ b, (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n) = b) ∧ ‖x - b‖ < δ

Proof state:
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
⊢ x ∈ approxAddOrderOf UnitAddCircle n δ ↔ ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ

Tactic:
simp only [mem_approx_add_orderOf_iff, mem_setOf_eq, ball, exists_prop, dist_eq_norm,
  AddCircle.addOrderOf_eq_pos_iff hn, mul_one]

Result:
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
⊢ (∃ b, (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n) = b) ∧ ‖x - b‖ < δ) ↔ ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ

Proof state:
case mp
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
⊢ (∃ b, (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n) = b) ∧ ‖x - b‖ < δ) → ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ

Tactic:
rintro ⟨y, ⟨m, hm₁, hm₂, rfl⟩, hx⟩

Result:
case mp.intro.intro.intro.intro.intro
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
m : ℕ
hm₁ : m < n
hm₂ : m.gcd n = 1
hx : ‖x - ↑(↑m / ↑n)‖ < δ
⊢ ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ

Proof state:
case mpr
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
⊢ (∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ) → ∃ b, (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n) = b) ∧ ‖x - b‖ < δ

Tactic:
rintro ⟨m, hm₁, hm₂, hx⟩

Result:
case mpr.intro.intro.intro
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
m : ℕ
hm₁ : m < n
hm₂ : gcd m n = 1
hx : ‖x - ↑(↑m / ↑n)‖ < δ
⊢ ∃ b, (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n) = b) ∧ ‖x - b‖ < δ

Proof state:
case mpr.intro.intro.intro
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
m : ℕ
hm₁ : m < n
hm₂ : gcd m n = 1
hx : ‖x - ↑(↑m / ↑n)‖ < δ
⊢ ∃ b, (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n) = b) ∧ ‖x - b‖ < δ

Tactic:
exact ⟨↑((m : ℝ) / n), ⟨m, hm₁, hm₂, rfl⟩, hx⟩

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
theorem contDiffGroupoid_le (h : m ≤ n) : contDiffGroupoid n I ≤ contDiffGroupoid m I

Proof state:
case h
m n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
h : m ≤ n
⊢ ∀ (f : H → H) (s : Set H), (contDiffPregroupoid n I).property f s → (contDiffPregroupoid m I).property f s

Tactic:
intro f s hfs

Result:
case h
m n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
h : m ≤ n
f : H → H
s : Set H
hfs : (contDiffPregroupoid n I).property f s
⊢ (contDiffPregroupoid m I).property f s

Proof state:
case h
m n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
h : m ≤ n
f : H → H
s : Set H
hfs : (contDiffPregroupoid n I).property f s
⊢ (contDiffPregroupoid m I).property f s

Tactic:
exact ContDiffOn.of_le hfs h

Result:
no goals

Proof state:
m n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
h : m ≤ n
⊢ contDiffGroupoid n I ≤ contDiffGroupoid m I

Tactic:
rw [contDiffGroupoid, contDiffGroupoid]

Result:
m n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
h : m ≤ n
⊢ (contDiffPregroupoid n I).groupoid ≤ (contDiffPregroupoid m I).groupoid

Proof state:
m n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
h : m ≤ n
⊢ (contDiffPregroupoid n I).groupoid ≤ (contDiffPregroupoid m I).groupoid

Tactic:
apply groupoid_of_pregroupoid_le

Result:
case h
m n : WithTop ℕ∞
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
h : m ≤ n
⊢ ∀ (f : H → H) (s : Set H), (contDiffPregroupoid n I).property f s → (contDiffPregroupoid m I).property f s
-- Mathlib/FieldTheory/Finite/GaloisField.lean
theorem finrank {n} (h : n ≠ 0) : Module.finrank (ZMod p) (GaloisField p n) = n

Proof state:
case succ.refine_4
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ ∀ (x y : GaloisField (n✝ + 1) n),
    x ∈
        Subring.closure
          (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
            (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField) →
      y ∈
          Subring.closure
            (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
              (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField) →
        (aeval x) (X ^ (n✝ + 1) ^ n - X) = 0 →
          (aeval y) (X ^ (n✝ + 1) ^ n - X) = 0 → (aeval (x + y)) (X ^ (n✝ + 1) ^ n - X) = 0

Tactic:
simp only [g_poly, aeval_X_pow, aeval_X, map_sub, add_pow_char_pow, sub_eq_zero]

Result:
case succ.refine_4
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ ∀ (x y : GaloisField (n✝ + 1) n),
    x ∈
        Subring.closure
          (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
            (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField) →
      y ∈
          Subring.closure
            (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
              (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField) →
        x ^ (n✝ + 1) ^ n = x → y ^ (n✝ + 1) ^ n = y → x ^ (n✝ + 1) ^ n + y ^ (n✝ + 1) ^ n = x + y
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive neg_one_zsmul_add]
lemma mul_zpow_neg_one (a b : α) : (a * b) ^ (-1 : ℤ) = b ^ (-1 : ℤ) * a ^ (-1 : ℤ)

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
⊢ (a * b) ^ (-1) = b ^ (-1) * a ^ (-1)

Tactic:
simp only [zpow_neg, zpow_one, mul_inv_rev]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Field.lean
@[simp]
lemma cast_div (hnm : n ∣ m) (hn : (n : K) ≠ 0) : (↑(m / n) : K) = m / n

Proof state:
K : Type u_1
inst✝ : DivisionSemiring K
m n : ℕ
hnm : n ∣ m
hn : ↑n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
obtain ⟨k, rfl⟩ := hnm

Result:
case intro
K : Type u_1
inst✝ : DivisionSemiring K
n : ℕ
hn : ↑n ≠ 0
k : ℕ
⊢ ↑(n * k / n) = ↑(n * k) / ↑n

Proof state:
case intro
K : Type u_1
inst✝ : DivisionSemiring K
n : ℕ
hn : ↑n ≠ 0
k : ℕ
⊢ ↑(n * k / n) = ↑(n * k) / ↑n

Tactic:
have : n ≠ 0 := by rintro rfl; simp at hn

Result:
case intro
K : Type u_1
inst✝ : DivisionSemiring K
n : ℕ
hn : ↑n ≠ 0
k : ℕ
this : n ≠ 0
⊢ ↑(n * k / n) = ↑(n * k) / ↑n

Proof state:
K : Type u_1
inst✝ : DivisionSemiring K
n : ℕ
hn : ↑n ≠ 0
k : ℕ
⊢ n ≠ 0

Tactic:
rintro rfl

Result:
K : Type u_1
inst✝ : DivisionSemiring K
k : ℕ
hn : ↑0 ≠ 0
⊢ False

Proof state:
K : Type u_1
inst✝ : DivisionSemiring K
k : ℕ
hn : ↑0 ≠ 0
⊢ False

Tactic:
simp at hn

Result:
no goals

Proof state:
case intro
K : Type u_1
inst✝ : DivisionSemiring K
n : ℕ
hn : ↑n ≠ 0
k : ℕ
this : n ≠ 0
⊢ ↑(n * k / n) = ↑(n * k) / ↑n

Tactic:
rw [Nat.mul_div_cancel_left _ <| zero_lt_of_ne_zero this, mul_comm n,
  cast_mul, mul_div_cancel_right₀ _ hn]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem nhds_eq_of_basis {ι : Sort*} {p : ι → Prop} {V : ι → Set (β × β)}
    (h : (𝓤 β).HasBasis p V) (f : α →ᵤ[𝔖] β) :
    𝓝 f = ⨅ s ∈ 𝔖, ⨅ (i) (_ : p i), 𝓟 {g | ∀ x ∈ s, (toFun 𝔖 f x, toFun 𝔖 g x) ∈ V i}

Proof state:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
f : α →ᵤ[𝔖] β
⊢ 𝓝 f = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V i}

Tactic:
simp_rw [nhds_eq_comap_uniformity, UniformOnFun.uniformity_eq_of_basis _ _ h, comap_iInf,
  comap_principal, UniformOnFun.gen, preimage_setOf_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem ae_tendsto_lintegral_enorm_sub_div'_of_integrable {f : α → E} (hf : Integrable f μ)
    (h'f : StronglyMeasurable f) :
    ∀ᵐ x ∂μ, Tendsto (fun a => (∫⁻ y in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)

Proof state:
case intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure t
main :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ c ∈ t,
        Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
          (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
x : α
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
c : E
hc : c ∈ t
n : ℕ
xn : x ∈ A.set n
hx :
  Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
    (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
⊢ Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 ‖f x - c‖ₑ)

Tactic:
simp only [xn, indicator_of_mem] at hx

Result:
case intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure t
main :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ c ∈ t,
        Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
          (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
x : α
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
c : E
hc : c ∈ t
n : ℕ
xn : x ∈ A.set n
hx :
  Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
    (𝓝 ‖f x - c‖ₑ)
⊢ Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 ‖f x - c‖ₑ)
-- Mathlib/Data/Nat/Log.lean
theorem clog_mono_right (b : ℕ) {n m : ℕ} (h : n ≤ m) : clog b n ≤ clog b m

Proof state:
case inl
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ clog b n ≤ clog b m

Tactic:
rw [clog_of_left_le_one hb]

Result:
case inl
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ 0 ≤ clog b m

Proof state:
case inr
b n m : ℕ
h : n ≤ m
hb : 1 < b
⊢ n ≤ b ^ clog b m

Tactic:
exact h.trans (le_pow_clog hb _)

Result:
no goals

Proof state:
case inr
b n m : ℕ
h : n ≤ m
hb : 1 < b
⊢ clog b n ≤ clog b m

Tactic:
rw [← le_pow_iff_clog_le hb]

Result:
case inr
b n m : ℕ
h : n ≤ m
hb : 1 < b
⊢ n ≤ b ^ clog b m

Proof state:
case inl
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ 0 ≤ clog b m

Tactic:
exact zero_le _

Result:
no goals

Proof state:
b n m : ℕ
h : n ≤ m
⊢ clog b n ≤ clog b m

Tactic:
rcases le_or_lt b 1 with hb | hb

Result:
case inl
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ clog b n ≤ clog b m

case inr
b n m : ℕ
h : n ≤ m
hb : 1 < b
⊢ clog b n ≤ clog b m
-- Mathlib/Topology/Sequences.lean
theorem UniformSpace.compactSpace_iff_seqCompactSpace : CompactSpace X ↔ SeqCompactSpace X

Proof state:
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
⊢ CompactSpace X ↔ SeqCompactSpace X

Tactic:
simp only [← isCompact_univ_iff, seqCompactSpace_iff, UniformSpace.isCompact_iff_isSeqCompact]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/ListOfFn.lean
theorem mem_prod_list_ofFn {a : α} {s : Fin n → Set α} :
    a ∈ (List.ofFn s).prod ↔ ∃ f : ∀ i : Fin n, s i, (List.ofFn fun i ↦ (f i : α)).prod = a

Proof state:
case succ
α : Type u_1
inst✝ : Monoid α
n✝ n : ℕ
ih : ∀ {a : α} {s : Fin n → Set α}, a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a
a : α
s : Fin (n + 1) → Set α
⊢ a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a

Tactic:
simp_rw [List.ofFn_succ, List.prod_cons, Fin.exists_fin_succ_pi, Fin.cons_zero, Fin.cons_succ,
  mem_mul, @ih, exists_exists_eq_and, SetCoe.exists, exists_prop]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Monoid α
n : ℕ
a : α
s : Fin n → Set α
⊢ a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a

Tactic:
induction' n with n ih generalizing a

Result:
case zero
α : Type u_1
inst✝ : Monoid α
n : ℕ
a : α
s : Fin 0 → Set α
⊢ a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a

case succ
α : Type u_1
inst✝ : Monoid α
n✝ n : ℕ
ih : ∀ {a : α} {s : Fin n → Set α}, a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a
a : α
s : Fin (n + 1) → Set α
⊢ a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a

Proof state:
case zero
α : Type u_1
inst✝ : Monoid α
n : ℕ
a : α
s : Fin 0 → Set α
⊢ a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a

Tactic:
simp_rw [List.ofFn_zero, List.prod_nil, Fin.exists_fin_zero_pi, eq_comm, Set.mem_one]

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Defs.lean
@[simp] lemma nilpotencyClass_eq_zero_of_subsingleton [Subsingleton R] :
    nilpotencyClass x = 0

Proof state:
R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
s : Set ℕ := {k | x ^ k = 0}
this : {k | x ^ k = 0} = univ
⊢ sInf {k | x ^ k = 0} = 0

Tactic:
simp [this]

Result:
no goals

Proof state:
R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
s : Set ℕ := {k | x ^ k = 0}
⊢ s = univ

Tactic:
exact eq_univ_iff_forall.mpr fun k ↦ Subsingleton.elim _ _

Result:
no goals

Proof state:
R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
s : Set ℕ := {k | x ^ k = 0}
this : s = univ
⊢ nilpotencyClass x = 0

Tactic:
change sInf _ = 0

Result:
R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
s : Set ℕ := {k | x ^ k = 0}
this : s = univ
⊢ sInf {k | x ^ k = 0} = 0

Proof state:
R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
⊢ nilpotencyClass x = 0

Tactic:
let s : Set ℕ := {k | x ^ k = 0}

Result:
R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
s : Set ℕ := {k | x ^ k = 0}
⊢ nilpotencyClass x = 0

Proof state:
R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
s : Set ℕ := {k | x ^ k = 0}
⊢ nilpotencyClass x = 0

Tactic:
suffices s = univ by change sInf _ = 0; simp [s] at this; simp [this]

Result:
R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
s : Set ℕ := {k | x ^ k = 0}
⊢ s = univ

Proof state:
R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
s : Set ℕ := {k | x ^ k = 0}
this : s = univ
⊢ sInf {k | x ^ k = 0} = 0

Tactic:
simp [s] at this

Result:
R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
s : Set ℕ := {k | x ^ k = 0}
this : {k | x ^ k = 0} = univ
⊢ sInf {k | x ^ k = 0} = 0
-- Mathlib/CategoryTheory/GuitartExact/VerticalComposition.lean
lemma vComp_iff_of_equivalences (eL : C₂ ≌ C₃) (eR : D₂ ≌ D₃)
    (w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃) :
    (w ≫ᵥ w'.hom).GuitartExact ↔ w.GuitartExact

Proof state:
case mp
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{u_11, u_1} C₁
inst✝⁴ : Category.{u_7, u_2} C₂
inst✝³ : Category.{u_8, u_3} C₃
inst✝² : Category.{u_12, u_4} D₁
inst✝¹ : Category.{u_9, u_5} D₂
inst✝ : Category.{u_10, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this : CatCommSq H₂ eL.functor eR.functor H₃ := { iso' := w' }
⊢ w.GuitartExact

Tactic:
have hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w' := rfl

Result:
case mp
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{u_11, u_1} C₁
inst✝⁴ : Category.{u_7, u_2} C₂
inst✝³ : Category.{u_8, u_3} C₃
inst✝² : Category.{u_12, u_4} D₁
inst✝¹ : Category.{u_9, u_5} D₂
inst✝ : Category.{u_10, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this : CatCommSq H₂ eL.functor eR.functor H₃ := { iso' := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
⊢ w.GuitartExact