harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/Laurent.lean
theorem taylor_mem_nonZeroDivisors (hp : p ∈ R[X]⁰) : taylor r p ∈ R[X]⁰

Proof state:
R : Type u
inst✝ : CommRing R
r : R
p : R[X]
hp : p ∈ R[X]⁰
x : R[X]
hx : x * (taylor r) p = 0
this : x = (taylor (r - r)) x
⊢ x = 0

Tactic:
rwa [this, sub_eq_add_neg, ← taylor_taylor, ← taylor_mul,
  LinearMap.map_eq_zero_iff _ (taylor_injective _), mul_right_mem_nonZeroDivisors_eq_zero_iff hp,
  LinearMap.map_eq_zero_iff _ (taylor_injective _)] at hx

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
r : R
p : R[X]
hp : p ∈ R[X]⁰
x : R[X]
hx : x * (taylor r) p = 0
⊢ x = 0

Tactic:
have : x = taylor (r - r) x := by simp

Result:
R : Type u
inst✝ : CommRing R
r : R
p : R[X]
hp : p ∈ R[X]⁰
x : R[X]
hx : x * (taylor r) p = 0
this : x = (taylor (r - r)) x
⊢ x = 0

Proof state:
R : Type u
inst✝ : CommRing R
r : R
p : R[X]
hp : p ∈ R[X]⁰
x : R[X]
hx : x * (taylor r) p = 0
⊢ x = (taylor (r - r)) x

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
r : R
p : R[X]
hp : p ∈ R[X]⁰
⊢ (taylor r) p ∈ R[X]⁰

Tactic:
rw [mem_nonZeroDivisors_iff]

Result:
R : Type u
inst✝ : CommRing R
r : R
p : R[X]
hp : p ∈ R[X]⁰
⊢ ∀ (x : R[X]), x * (taylor r) p = 0 → x = 0

Proof state:
R : Type u
inst✝ : CommRing R
r : R
p : R[X]
hp : p ∈ R[X]⁰
⊢ ∀ (x : R[X]), x * (taylor r) p = 0 → x = 0

Tactic:
intro x hx

Result:
R : Type u
inst✝ : CommRing R
r : R
p : R[X]
hp : p ∈ R[X]⁰
x : R[X]
hx : x * (taylor r) p = 0
⊢ x = 0
-- Mathlib/Topology/VectorBundle/Basic.lean
theorem linearMapAt_apply (e : Pretrivialization F (π F E)) [e.IsLinear R] {b : B} (y : E b) :
    e.linearMapAt R b y = if b ∈ e.baseSet then (e ⟨b, y⟩).2 else 0

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
y : E b
⊢ (Pretrivialization.linearMapAt R e b) y = if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0

Tactic:
rw [coe_linearMapAt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
theorem contains_iff :
    ∀ (c : DefaultClause n) (l : Literal (PosFin n)), contains c l = true ↔ l ∈ toList c

Proof state:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ c.contains l = true ↔ l ∈ c.toList

Tactic:
simp only [contains, List.contains]

Result:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ List.elem l c.clause = true ↔ l ∈ c.toList

Proof state:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ List.elem l c.clause = true ↔ l ∈ c.toList

Tactic:
constructor

Result:
case mp
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ List.elem l c.clause = true → l ∈ c.toList

case mpr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ l ∈ c.toList → List.elem l c.clause = true

Proof state:
case mpr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ l ∈ c.toList → List.elem l c.clause = true

Tactic:
exact List.elem_eq_true_of_mem

Result:
no goals

Proof state:
case mp
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ List.elem l c.clause = true → l ∈ c.toList

Tactic:
exact List.mem_of_elem_eq_true

Result:
no goals

Proof state:
n : Nat
⊢ ∀ (c : DefaultClause n) (l : Literal (PosFin n)), c.contains l = true ↔ l ∈ c.toList

Tactic:
intro c l

Result:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ c.contains l = true ↔ l ∈ c.toList
-- Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean
lemma strictConcaveOn_sqrt : StrictConcaveOn ℝ≥0 univ NNReal.sqrt

Proof state:
⊢ StrictConcaveOn ℝ≥0 univ ⇑sqrt

Tactic:
have : NNReal.sqrt = fun x : ℝ≥0 ↦ x ^ (1 / (2 : ℝ)) := by
  ext x; exact mod_cast NNReal.sqrt_eq_rpow x

Result:
this : ⇑sqrt = fun x => x ^ (1 / 2)
⊢ StrictConcaveOn ℝ≥0 univ ⇑sqrt

Proof state:
⊢ ⇑sqrt = fun x => x ^ (1 / 2)

Tactic:
ext x

Result:
case h.a
x : ℝ≥0
⊢ ↑(sqrt x) = ↑(x ^ (1 / 2))

Proof state:
this : ⇑sqrt = fun x => x ^ (1 / 2)
⊢ StrictConcaveOn ℝ≥0 univ ⇑sqrt

Tactic:
rw [this]

Result:
this : ⇑sqrt = fun x => x ^ (1 / 2)
⊢ StrictConcaveOn ℝ≥0 univ fun x => x ^ (1 / 2)

Proof state:
this : ⇑sqrt = fun x => x ^ (1 / 2)
⊢ 1 / 2 < 1

Tactic:
linarith

Result:
no goals

Proof state:
this : ⇑sqrt = fun x => x ^ (1 / 2)
⊢ StrictConcaveOn ℝ≥0 univ fun x => x ^ (1 / 2)

Tactic:
exact strictConcaveOn_rpow (by positivity) (by linarith)

Result:
no goals

Proof state:
this : ⇑sqrt = fun x => x ^ (1 / 2)
⊢ 0 < 1 / 2

Tactic:
positivity

Result:
no goals

Proof state:
case h.a
x : ℝ≥0
⊢ ↑(sqrt x) = ↑(x ^ (1 / 2))

Tactic:
exact mod_cast NNReal.sqrt_eq_rpow x

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Multiset.lean
lemma map_add_right_Ioc (a b c : α) : ((Ioc a b).map fun x => x + c) = Ioc (a + c) (b + c)

Proof state:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => x + c) (Ioc a b) = Ioc (a + c) (b + c)

Tactic:
simp_rw [add_comm _ c]

Result:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Ioc a b) = Ioc (c + a) (c + b)

Proof state:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Ioc a b) = Ioc (c + a) (c + b)

Tactic:
exact map_add_left_Ioc _ _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem alterKey_cons_perm {k : α} {f : Option β → Option β} {k' : α} {v' : β}
    {l : List ((_ : α) × β)} :
    Perm (alterKey k f (⟨k', v'⟩ :: l))
      (if k' == k then
        match f (some v') with
          | none => l
          | some v => ⟨k, v⟩ :: l
        else
          ⟨k', v'⟩ :: alterKey k f l)

Proof state:
case neg
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
hk' : (k' == k) = false
⊢ (match f (getValue? k l) with
      | none => ⟨k', v'⟩ :: eraseKey k l
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if False then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else
      ⟨k', v'⟩ ::
        match f (getValue? k l) with
        | none => eraseKey k l
        | some v => insertEntry k v l)

Tactic:
split

Result:
case neg.h_1
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
hk' : (k' == k) = false
x✝ : Option β
heq✝ : f (getValue? k l) = none
⊢ (⟨k', v'⟩ :: eraseKey k l).Perm
    (if False then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: eraseKey k l)

case neg.h_2
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
hk' : (k' == k) = false
x✝ : Option β
v✝ : β
heq✝ : f (getValue? k l) = some v✝
⊢ (insertEntry k v✝ (⟨k', v'⟩ :: l)).Perm
    (if False then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: insertEntry k v✝ l)

Proof state:
case pos
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
hk' : (k' == k) = true
⊢ (match f (getValue? k (⟨k', v'⟩ :: l)) with
      | none => eraseKey k (⟨k', v'⟩ :: l)
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if True then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: alterKey k f l)

Tactic:
rw [getValue?_cons_of_true hk', eraseKey_cons_of_beq hk']

Result:
case pos
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
hk' : (k' == k) = true
⊢ (match f (some v') with
      | none => l
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if True then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: alterKey k f l)

Proof state:
case pos
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
k' : α
v' : β
l : List ((_ : α) × β)
hk' : (k' == k) = true
⊢ (match f (some v') with
      | none => l
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (if True then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: alterKey k f l)

Tactic:
simp [insertEntry_cons_of_beq hk']

Result:
no goals
-- Mathlib/Analysis/Complex/RealDeriv.lean
theorem HasStrictDerivAt.complexToReal_fderiv' {f : ℂ → E} {x : ℂ} {f' : E}
    (h : HasStrictDerivAt f f' x) :
    HasStrictFDerivAt f (reCLM.smulRight f' + I • imCLM.smulRight f') x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
x : ℂ
f' : E
h : HasStrictDerivAt f f' x
⊢ HasStrictFDerivAt f (reCLM.smulRight f' + I • imCLM.smulRight f') x

Tactic:
simpa only [Complex.restrictScalars_one_smulRight'] using
  h.hasStrictFDerivAt.restrictScalars ℝ

Result:
no goals
-- Mathlib/Topology/GDelta/UniformSpace.lean
theorem IsClosed.isGδ {X : Type*} [UniformSpace X] [IsCountablyGenerated (𝓤 X)] {s : Set X}
    (hs : IsClosed s) : IsGδ s

Proof state:
case intro.intro.mk
X : Type u_3
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
s : Set X
hs : IsClosed s
U : ℕ → Set (X × X)
hUo : ∀ (i : ℕ), U i ∈ 𝓤 X ∧ IsOpen (U i)
hU : (𝓤 X).HasBasis (fun x => True) fun i => id (U i)
⊢ IsGδ (⋂ i, ⋂ (_ : True), ⋃ x ∈ s, UniformSpace.ball x (id (U i)))

Tactic:
refine .biInter (to_countable _) fun n _ => IsOpen.isGδ ?_

Result:
case intro.intro.mk
X : Type u_3
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
s : Set X
hs : IsClosed s
U : ℕ → Set (X × X)
hUo : ∀ (i : ℕ), U i ∈ 𝓤 X ∧ IsOpen (U i)
hU : (𝓤 X).HasBasis (fun x => True) fun i => id (U i)
n : ℕ
x✝ : n ∈ fun i => True
⊢ IsOpen (⋃ x ∈ s, UniformSpace.ball x (id (U n)))

Proof state:
case intro.intro.mk
X : Type u_3
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
s : Set X
hs : IsClosed s
U : ℕ → Set (X × X)
hUo : ∀ (i : ℕ), U i ∈ 𝓤 X ∧ IsOpen (U i)
hU : (𝓤 X).HasBasis (fun x => True) fun i => id (U i)
⊢ IsGδ s

Tactic:
rw [← hs.closure_eq, ← hU.biInter_biUnion_ball]

Result:
case intro.intro.mk
X : Type u_3
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
s : Set X
hs : IsClosed s
U : ℕ → Set (X × X)
hUo : ∀ (i : ℕ), U i ∈ 𝓤 X ∧ IsOpen (U i)
hU : (𝓤 X).HasBasis (fun x => True) fun i => id (U i)
⊢ IsGδ (⋂ i, ⋂ (_ : True), ⋃ x ∈ s, UniformSpace.ball x (id (U i)))

Proof state:
case intro.intro.mk
X : Type u_3
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
s : Set X
hs : IsClosed s
U : ℕ → Set (X × X)
hUo : ∀ (i : ℕ), U i ∈ 𝓤 X ∧ IsOpen (U i)
hU : (𝓤 X).HasBasis (fun x => True) fun i => id (U i)
n : ℕ
x✝ : n ∈ fun i => True
⊢ IsOpen (⋃ x ∈ s, UniformSpace.ball x (id (U n)))

Tactic:
exact isOpen_biUnion fun x _ => UniformSpace.isOpen_ball _ (hUo _).2

Result:
no goals

Proof state:
X : Type u_3
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
s : Set X
hs : IsClosed s
⊢ IsGδ s

Tactic:
rcases (@uniformity_hasBasis_open X _).exists_antitone_subbasis with ⟨U, hUo, hU, -⟩

Result:
case intro.intro.mk
X : Type u_3
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
s : Set X
hs : IsClosed s
U : ℕ → Set (X × X)
hUo : ∀ (i : ℕ), U i ∈ 𝓤 X ∧ IsOpen (U i)
hU : (𝓤 X).HasBasis (fun x => True) fun i => id (U i)
⊢ IsGδ s
-- Mathlib/RingTheory/RingHom/Locally.lean
/-- If `P` is stable under composition with localization away maps on the right,
then so is `Locally P`. -/
lemma locally_StableUnderCompositionWithLocalizationAwayTarget
    (hP0 : RespectsIso P)
    (hPa : StableUnderCompositionWithLocalizationAwayTarget P) :
    StableUnderCompositionWithLocalizationAwayTarget (Locally P)

Proof state:
case intro.intro.refine_2.intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP0 : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
t : S
inst✝ : IsLocalization.Away t T
f : R →+* S
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [inst_2 : IsLocalization.Away t Sₜ],
      P ((algebraMap S Sₜ).comp f)
a : S
ha : a ∈ ↑s
this✝² : Algebra (Localization.Away a) (Localization.Away ((algebraMap S T) a)) :=
  (IsLocalization.Away.map (Localization.Away a) (Localization.Away ((algebraMap S T) a)) (algebraMap S T) a).toAlgebra
this✝¹ :
  (algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
      (algebraMap S (Localization.Away a)) =
    (algebraMap T (Localization.Away ((algebraMap S T) a))).comp (algebraMap S T)
this✝ : IsScalarTower S (Localization.Away a) (Localization.Away ((algebraMap S T) a))
this : IsLocalization.Away ((algebraMap S (Localization.Away a)) t) (Localization.Away ((algebraMap S T) a))
⊢ P
    ((algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
      ((algebraMap S (Localization.Away a)).comp f))

Tactic:
apply hPa _ (algebraMap S (Localization.Away a) t)

Result:
case intro.intro.refine_2.intro.intro.a
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP0 : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
t : S
inst✝ : IsLocalization.Away t T
f : R →+* S
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [inst_2 : IsLocalization.Away t Sₜ],
      P ((algebraMap S Sₜ).comp f)
a : S
ha : a ∈ ↑s
this✝² : Algebra (Localization.Away a) (Localization.Away ((algebraMap S T) a)) :=
  (IsLocalization.Away.map (Localization.Away a) (Localization.Away ((algebraMap S T) a)) (algebraMap S T) a).toAlgebra
this✝¹ :
  (algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
      (algebraMap S (Localization.Away a)) =
    (algebraMap T (Localization.Away ((algebraMap S T) a))).comp (algebraMap S T)
this✝ : IsScalarTower S (Localization.Away a) (Localization.Away ((algebraMap S T) a))
this : IsLocalization.Away ((algebraMap S (Localization.Away a)) t) (Localization.Away ((algebraMap S T) a))
⊢ P ((algebraMap S (Localization.Away a)).comp f)
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma one_add_smoothingFn_le_two {x : ℝ} (hx : exp 1 ≤ x) : 1 + ε x ≤ 2

Proof state:
case bc
x : ℝ
hx : rexp 1 ≤ x
this : 1 < x
⊢ 1 ≤ log x

Tactic:
calc 1 = log (exp 1) := by simp
     _ ≤ log x := log_le_log (exp_pos _) hx

Result:
no goals

Proof state:
case bc
x : ℝ
hx : rexp 1 ≤ x
⊢ 1 / log x ≤ 1

Tactic:
have : 1 < x := by
  calc 1 = exp 0 := by simp
       _ < exp 1 := by simp
       _ ≤ x := hx

Result:
case bc
x : ℝ
hx : rexp 1 ≤ x
this : 1 < x
⊢ 1 / log x ≤ 1

Proof state:
x : ℝ
hx : rexp 1 ≤ x
⊢ 1 < x

Tactic:
calc 1 = exp 0 := by simp
     _ < exp 1 := by simp
     _ ≤ x := hx

Result:
no goals

Proof state:
case bc
x : ℝ
hx : rexp 1 ≤ x
this : 1 < x
⊢ 1 / log x ≤ 1

Tactic:
rw [div_le_one (log_pos this)]

Result:
case bc
x : ℝ
hx : rexp 1 ≤ x
this : 1 < x
⊢ 1 ≤ log x

Proof state:
x : ℝ
hx : rexp 1 ≤ x
⊢ 1 = rexp 0

Tactic:
simp

Result:
no goals

Proof state:
x : ℝ
hx : rexp 1 ≤ x
⊢ 1 + 1 / log x ≤ 1 + 1

Tactic:
gcongr

Result:
case bc
x : ℝ
hx : rexp 1 ≤ x
⊢ 1 / log x ≤ 1

Proof state:
x : ℝ
hx : rexp 1 ≤ x
this : 1 < x
⊢ 1 = log (rexp 1)

Tactic:
simp

Result:
no goals

Proof state:
x : ℝ
hx : rexp 1 ≤ x
⊢ 1 + ε x ≤ 2

Tactic:
simp only [smoothingFn, ← one_add_one_eq_two]

Result:
x : ℝ
hx : rexp 1 ≤ x
⊢ 1 + 1 / log x ≤ 1 + 1

Proof state:
x : ℝ
hx : rexp 1 ≤ x
⊢ rexp 0 < rexp 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Invertible/Defs.lean
theorem invOf_mul_cancel_right' [Monoid α] (a b : α) {_ : Invertible b} : a * ⅟ b * b = a

Proof state:
α : Type u
inst✝ : Monoid α
a b : α
x✝ : Invertible b
⊢ a * ⅟b * b = a

Tactic:
simp [mul_assoc]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem rpow_logb_eq_abs (hx : x ≠ 0) : b ^ logb b x = |x|

Proof state:
case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ log x / log b * log b = log x

Tactic:
field_simp [log_b_ne_zero b_pos b_ne_one]

Result:
no goals

Proof state:
case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ log (b ^ logb b x) = log |x|

Tactic:
rw [log_rpow b_pos, logb, log_abs]

Result:
case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ log x / log b * log b = log x

Proof state:
case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ |x| ∈ Ioi 0

Tactic:
simp only [abs_pos, mem_Ioi, Ne, hx, not_false_iff]

Result:
no goals

Proof state:
case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ 0 < b ^ logb b x

Tactic:
apply rpow_pos_of_pos b_pos

Result:
no goals

Proof state:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ b ^ logb b x = |x|

Tactic:
apply log_injOn_pos

Result:
case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ b ^ logb b x ∈ Ioi 0

case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ |x| ∈ Ioi 0

case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ log (b ^ logb b x) = log |x|

Proof state:
case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ b ^ logb b x ∈ Ioi 0

Tactic:
simp only [Set.mem_Ioi]

Result:
case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ 0 < b ^ logb b x
-- Mathlib/Algebra/GroupWithZero/Pointwise/Set/Basic.lean
lemma zero_div_subset (s : Set α) : 0 / s ⊆ 0

Proof state:
α : Type u_1
inst✝ : GroupWithZero α
s : Set α
⊢ 0 / s ⊆ 0

Tactic:
simp [subset_def, mem_div]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem hasStrictFDerivAt_list_prod_finRange' {n : ℕ} {x : Fin n → 𝔸} :
    HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ ((List.finRange n).map x).prod)
      (∑ i : Fin n, (((List.finRange n).take i).map x).prod •
        smulRight (proj i) (((List.finRange n).drop (.succ i)).map x).prod) x :=
  hasStrictFDerivAt_list_prod'.congr_fderiv <|
    Finset.sum_equiv (finCongr (List.length_finRange n)) (by simp) (by simp [Fin.forall_iff])

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
n : ℕ
x : Fin n → 𝔸
⊢ ∀ i ∈ Finset.univ,
    (List.map x (List.take (↑i) (List.finRange n))).prod •
        (proj (List.finRange n)[i]).smulRight (List.map x (List.drop (↑i).succ (List.finRange n))).prod =
      (List.map x (List.take (↑((finCongr ⋯) i)) (List.finRange n))).prod •
        (proj ((finCongr ⋯) i)).smulRight (List.map x (List.drop (↑((finCongr ⋯) i)).succ (List.finRange n))).prod

Tactic:
simp [Fin.forall_iff]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
n : ℕ
x : Fin n → 𝔸
⊢ ∀ (i : Fin (List.finRange n).length), i ∈ Finset.univ ↔ (finCongr ⋯) i ∈ Finset.univ

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem toReal_sub {x y : EReal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) (hy : y ≠ ⊤) (h'y : y ≠ ⊥) :
    toReal (x - y) = toReal x - toReal y

Proof state:
case intro.intro
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
y : ℝ
hy : ↑y ≠ ⊤
h'y : ↑y ≠ ⊥
⊢ (↑x - ↑y).toReal = (↑x).toReal - (↑y).toReal

Tactic:
rfl

Result:
no goals

Proof state:
x y : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
hy : y ≠ ⊤
h'y : y ≠ ⊥
⊢ (x - y).toReal = x.toReal - y.toReal

Tactic:
lift x to ℝ using ⟨hx, h'x⟩

Result:
case intro
y : EReal
hy : y ≠ ⊤
h'y : y ≠ ⊥
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
⊢ (↑x - y).toReal = (↑x).toReal - y.toReal

Proof state:
case intro
y : EReal
hy : y ≠ ⊤
h'y : y ≠ ⊥
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
⊢ (↑x - y).toReal = (↑x).toReal - y.toReal

Tactic:
lift y to ℝ using ⟨hy, h'y⟩

Result:
case intro.intro
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
y : ℝ
hy : ↑y ≠ ⊤
h'y : ↑y ≠ ⊥
⊢ (↑x - ↑y).toReal = (↑x).toReal - (↑y).toReal
-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
lemma netMaxcard_eq_zero_iff (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) :
    netMaxcard T F U n = 0 ↔ F = ∅

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n = 0
x : X
x_F : x ∈ F
key : IsDynNetIn T F U n {x}
⊢ False

Tactic:
rw [← Finset.coe_singleton] at key

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n = 0
x : X
x_F : x ∈ F
key : IsDynNetIn T F U n ↑{x}
⊢ False

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n = 0
x : X
x_F : x ∈ F
key : IsDynNetIn T F U n ↑{x}
⊢ False

Tactic:
replace key := key.card_le_netMaxcard

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n = 0
x : X
x_F : x ∈ F
key : ↑{x}.card ≤ netMaxcard T F U n
⊢ False

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n = 0
⊢ ∀ (x : X), x ∉ F

Tactic:
intro x x_F

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n = 0
x : X
x_F : x ∈ F
⊢ False

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n = 0
x : X
x_F : x ∈ F
key : ↑{x}.card ≤ netMaxcard T F U n
⊢ False

Tactic:
rw [Finset.card_singleton, Nat.cast_one, h] at key

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n = 0
x : X
x_F : x ∈ F
key : 1 ≤ 0
⊢ False

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n = 0
x : X
x_F : x ∈ F
⊢ False

Tactic:
have key := isDynNetIn_singleton T U n x_F

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n = 0
x : X
x_F : x ∈ F
key : IsDynNetIn T F U n {x}
⊢ False

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n = 0
⊢ F = ∅

Tactic:
rw [eq_empty_iff_forall_not_mem]

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n = 0
⊢ ∀ (x : X), x ∉ F

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
⊢ netMaxcard T F U n = 0 ↔ F = ∅

Tactic:
refine Iff.intro (fun h ↦ ?_) (fun h ↦ by rw [h, netMaxcard_empty])

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n = 0
⊢ F = ∅

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : F = ∅
⊢ netMaxcard T F U n = 0

Tactic:
rw [h, netMaxcard_empty]

Result:
no goals

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n = 0
x : X
x_F : x ∈ F
key : 1 ≤ 0
⊢ False

Tactic:
exact key.not_lt zero_lt_one

Result:
no goals