harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
lemma isStrictlyLE_iff (n : ℤ) :
    K.IsStrictlyLE n ↔ ∀ (i : ℤ) (_ : n < i), IsZero (K.X i)

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → IsZero (K.X i)
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i
⊢ IsZero (K.X i)

Tactic:
rw [not_mem_range_embeddingUpIntLE_iff] at hi

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → IsZero (K.X i)
i : ℤ
hi : n < i
⊢ IsZero (K.X i)

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ (∀ (i : ℤ), n < i → IsZero (K.X i)) → K.IsStrictlyLE n

Tactic:
intro h

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → IsZero (K.X i)
⊢ K.IsStrictlyLE n

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → IsZero (K.X i)
i : ℤ
hi : n < i
⊢ IsZero (K.X i)

Tactic:
exact h i hi

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsStrictlyLE n → ∀ (i : ℤ), n < i → IsZero (K.X i)

Tactic:
intro _ i hi

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
a✝ : K.IsStrictlyLE n
i : ℤ
hi : n < i
⊢ IsZero (K.X i)

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
a✝ : K.IsStrictlyLE n
i : ℤ
hi : n < i
⊢ IsZero (K.X i)

Tactic:
exact K.isZero_of_isStrictlyLE n i hi

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → IsZero (K.X i)
⊢ K.IsStrictlyLE n

Tactic:
refine IsStrictlySupported.mk (fun i hi ↦ ?_)

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → IsZero (K.X i)
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i
⊢ IsZero (K.X i)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsStrictlyLE n ↔ ∀ (i : ℤ), n < i → IsZero (K.X i)

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsStrictlyLE n → ∀ (i : ℤ), n < i → IsZero (K.X i)

case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ (∀ (i : ℤ), n < i → IsZero (K.X i)) → K.IsStrictlyLE n
-- Mathlib/.lake/packages/batteries/Batteries/Classes/SatisfiesM.lean
theorem map [Functor m] [LawfulFunctor m] {x : m α}
    (hx : SatisfiesM p x) (hf : ∀ {a}, p a → q (f a)) : SatisfiesM q (f <$> x)

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
p : α → Prop
α✝ : Type u_1
q : α✝ → Prop
f : α → α✝
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x : m α
hx✝ : SatisfiesM p x
hf : ∀ {a : α}, p a → q (f a)
x' : m { a // p a }
hx : Subtype.val <$> x' = x
⊢ Subtype.val <$>
      (fun x =>
          match x with
          | ⟨a, h⟩ => ⟨f a, ⋯⟩) <$>
        x' =
    f <$> Subtype.val <$> x'

Tactic:
simp [← comp_map, Function.comp_def]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
p : α → Prop
α✝ : Type u_1
q : α✝ → Prop
f : α → α✝
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x : m α
hx : SatisfiesM p x
hf : ∀ {a : α}, p a → q (f a)
⊢ SatisfiesM q (f <$> x)

Tactic:
let ⟨x', hx⟩ := hx

Result:
m : Type u_1 → Type u_2
α : Type u_1
p : α → Prop
α✝ : Type u_1
q : α✝ → Prop
f : α → α✝
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x : m α
hx✝ : SatisfiesM p x
hf : ∀ {a : α}, p a → q (f a)
x' : m { a // p a }
hx : Subtype.val <$> x' = x
⊢ SatisfiesM q (f <$> x)

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
p : α → Prop
α✝ : Type u_1
q : α✝ → Prop
f : α → α✝
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x : m α
hx✝ : SatisfiesM p x
hf : ∀ {a : α}, p a → q (f a)
x' : m { a // p a }
hx : Subtype.val <$> x' = x
⊢ Subtype.val <$>
      (fun x =>
          match x with
          | ⟨a, h⟩ => ⟨f a, ⋯⟩) <$>
        x' =
    f <$> x

Tactic:
rw [← hx]

Result:
m : Type u_1 → Type u_2
α : Type u_1
p : α → Prop
α✝ : Type u_1
q : α✝ → Prop
f : α → α✝
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x : m α
hx✝ : SatisfiesM p x
hf : ∀ {a : α}, p a → q (f a)
x' : m { a // p a }
hx : Subtype.val <$> x' = x
⊢ Subtype.val <$>
      (fun x =>
          match x with
          | ⟨a, h⟩ => ⟨f a, ⋯⟩) <$>
        x' =
    f <$> Subtype.val <$> x'

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
p : α → Prop
α✝ : Type u_1
q : α✝ → Prop
f : α → α✝
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x : m α
hx✝ : SatisfiesM p x
hf : ∀ {a : α}, p a → q (f a)
x' : m { a // p a }
hx : Subtype.val <$> x' = x
⊢ SatisfiesM q (f <$> x)

Tactic:
refine ⟨(fun ⟨a, h⟩ => ⟨f a, hf h⟩) <$> x', ?_⟩

Result:
m : Type u_1 → Type u_2
α : Type u_1
p : α → Prop
α✝ : Type u_1
q : α✝ → Prop
f : α → α✝
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x : m α
hx✝ : SatisfiesM p x
hf : ∀ {a : α}, p a → q (f a)
x' : m { a // p a }
hx : Subtype.val <$> x' = x
⊢ Subtype.val <$>
      (fun x =>
          match x with
          | ⟨a, h⟩ => ⟨f a, ⋯⟩) <$>
        x' =
    f <$> x
-- Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean
theorem IsLowerSet.memberSubfamily_subset_nonMemberSubfamily (h : IsLowerSet (𝒜 : Set (Finset α))) :
    𝒜.memberSubfamily a ⊆ 𝒜.nonMemberSubfamily a := fun s => by
  rw [mem_memberSubfamily, mem_nonMemberSubfamily]
  exact And.imp_left (h <| subset_insert _ _)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet ↑𝒜
s : Finset α
⊢ s ∈ Finset.memberSubfamily a 𝒜 → s ∈ Finset.nonMemberSubfamily a 𝒜

Tactic:
rw [mem_memberSubfamily, mem_nonMemberSubfamily]

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet ↑𝒜
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ a ∉ s → s ∈ 𝒜 ∧ a ∉ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet ↑𝒜
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ a ∉ s → s ∈ 𝒜 ∧ a ∉ s

Tactic:
exact And.imp_left (h <| subset_insert _ _)

Result:
no goals
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma pairwiseDisjoint_union_disjointOfDiffUnion (hC : IsSetSemiring C) (hs : s ∈ C)
    (hI : ↑I ⊆ C) (h_dis : PairwiseDisjoint (I : Set (Set α)) id) :
    PairwiseDisjoint (I ∪ hC.disjointOfDiffUnion hs hI : Set (Set α)) id

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑I
v : Set α
hv : v ∈ ↑(hC.disjointOfDiffUnion hs hI)
x✝ : u ≠ v
⊢ Disjoint u v

Tactic:
exact disjoint_of_subset (subset_sUnion_of_mem hu) (subset_sUnion_of_mem hv)
  (hC.disjoint_sUnion_disjointOfDiffUnion hs hI)

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑I
v : Set α
hv : v ∈ ↑(hC.disjointOfDiffUnion hs hI)
x✝ : u ≠ v
⊢ Disjoint (id u) (id v)

Tactic:
simp_rw [id]

Result:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑I
v : Set α
hv : v ∈ ↑(hC.disjointOfDiffUnion hs hI)
x✝ : u ≠ v
⊢ Disjoint u v

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
⊢ (↑I).PairwiseDisjoint id ∧
    (↑(hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id ∧
      ∀ ⦃i : Set α⦄, i ∈ ↑I → ∀ ⦃j : Set α⦄, j ∈ ↑(hC.disjointOfDiffUnion hs hI) → i ≠ j → Disjoint (id i) (id j)

Tactic:
refine ⟨h_dis, hC.pairwiseDisjoint_disjointOfDiffUnion hs hI, fun u hu v hv _ ↦ ?_⟩

Result:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑I
v : Set α
hv : v ∈ ↑(hC.disjointOfDiffUnion hs hI)
x✝ : u ≠ v
⊢ Disjoint (id u) (id v)

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
⊢ (↑I ∪ ↑(hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id

Tactic:
rw [pairwiseDisjoint_union]

Result:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
⊢ (↑I).PairwiseDisjoint id ∧
    (↑(hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id ∧
      ∀ ⦃i : Set α⦄, i ∈ ↑I → ∀ ⦃j : Set α⦄, j ∈ ↑(hC.disjointOfDiffUnion hs hI) → i ≠ j → Disjoint (id i) (id j)
-- Mathlib/Computability/Ackermann.lean
theorem ack_pos : ∀ m n, 0 < ack m n
  | 0, n => by simp
  | m + 1, 0 => by
    rw [ack_succ_zero]
    apply ack_pos
  | m + 1, n + 1 => by
    rw [ack_succ_succ]
    apply ack_pos

Proof state:
m : ℕ
⊢ 0 < ack m 1

Tactic:
apply ack_pos

Result:
no goals

Proof state:
m n : ℕ
⊢ 0 < ack m (ack (m + 1) n)

Tactic:
apply ack_pos

Result:
no goals

Proof state:
m : ℕ
⊢ 0 < ack (m + 1) 0

Tactic:
rw [ack_succ_zero]

Result:
m : ℕ
⊢ 0 < ack m 1

Proof state:
m n : ℕ
⊢ 0 < ack (m + 1) (n + 1)

Tactic:
rw [ack_succ_succ]

Result:
m n : ℕ
⊢ 0 < ack m (ack (m + 1) n)

Proof state:
n : ℕ
⊢ 0 < ack 0 n

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty {s₁ s₂ : Set P} :
    affineSpan k s₁ ∥ affineSpan k s₂ ↔ vectorSpan k s₁ = vectorSpan k s₂ ∧ (s₁ = ∅ ↔ s₂ = ∅)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔ (affineSpan k s₁).direction = vectorSpan k s₂ ∧ (affineSpan k s₁ = ⊥ ↔ s₂ = ∅)

Tactic:
rw [← direction_affineSpan, ← affineSpan_eq_bot k]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔
    (affineSpan k s₁).direction = (affineSpan k s₂).direction ∧ (affineSpan k s₁ = ⊥ ↔ affineSpan k s₂ = ⊥)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔ vectorSpan k s₁ = vectorSpan k s₂ ∧ (s₁ = ∅ ↔ s₂ = ∅)

Tactic:
repeat rw [← direction_affineSpan, ← affineSpan_eq_bot k]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔
    (affineSpan k s₁).direction = (affineSpan k s₂).direction ∧ (affineSpan k s₁ = ⊥ ↔ affineSpan k s₂ = ⊥)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔
    (affineSpan k s₁).direction = (affineSpan k s₂).direction ∧ (affineSpan k s₁ = ⊥ ↔ affineSpan k s₂ = ⊥)

Tactic:
exact parallel_iff_direction_eq_and_eq_bot_iff_eq_bot

Result:
no goals
-- Mathlib/Probability/Kernel/Basic.lean
theorem restrict_apply' (κ : Kernel α β) (hs : MeasurableSet s) (a : α) (ht : MeasurableSet t) :
    κ.restrict hs a t = (κ a) (t ∩ s)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
s t : Set β
κ : Kernel α β
hs : MeasurableSet s
a : α
ht : MeasurableSet t
⊢ ((κ.restrict hs) a) t = (κ a) (t ∩ s)

Tactic:
rw [restrict_apply κ hs a, Measure.restrict_apply ht]

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
theorem iff_iff_imp_and_imp {φ ψ : L.BoundedFormula α n} :
    (φ ⇔[T] ψ) ↔ (φ ⟹[T] ψ) ∧ (ψ ⟹[T] φ)

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
⊢ φ ⇔[T] ψ ↔ φ ⟹[T] ψ ∧ ψ ⟹[T] φ

Tactic:
simp only [Theory.Imp, ModelsBoundedFormula, BoundedFormula.realize_imp, ← forall_and,
  Theory.Iff, BoundedFormula.realize_iff, iff_iff_implies_and_implies]

Result:
no goals
-- Mathlib/NumberTheory/FermatPsp.lean
theorem coprime_of_fermatPsp {n b : ℕ} (h : FermatPsp n b) (h₁ : 1 ≤ b) : Nat.Coprime n b

Proof state:
case intro.intro
n b : ℕ
h₁ : 1 ≤ b
hp : n.ProbablePrime b
left✝ : ¬Prime n
hn₂ : 1 < n
⊢ n.Coprime b

Tactic:
exact coprime_of_probablePrime hp (by omega) h₁

Result:
no goals

Proof state:
n b : ℕ
h₁ : 1 ≤ b
hp : n.ProbablePrime b
left✝ : ¬Prime n
hn₂ : 1 < n
⊢ 1 ≤ n

Tactic:
omega

Result:
no goals

Proof state:
n b : ℕ
h : n.FermatPsp b
h₁ : 1 ≤ b
⊢ n.Coprime b

Tactic:
rcases h with ⟨hp, _, hn₂⟩

Result:
case intro.intro
n b : ℕ
h₁ : 1 ≤ b
hp : n.ProbablePrime b
left✝ : ¬Prime n
hn₂ : 1 < n
⊢ n.Coprime b
-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSet_stopping_time_le [TopologicalSpace ι] [SecondCountableTopology ι]
    [OrderTopology ι] [MeasurableSpace ι] [BorelSpace ι] (hτ : IsStoppingTime f τ)
    (hπ : IsStoppingTime f π) : MeasurableSet[hπ.measurableSpace] {ω | τ ω ≤ π ω}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : SecondCountableTopology ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSpace ι
inst✝ : BorelSpace ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ MeasurableSet {ω | τ ω ≤ π ω}

Tactic:
exact measurableSet_le_stopping_time hτ hπ

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : SecondCountableTopology ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSpace ι
inst✝ : BorelSpace ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
this : MeasurableSet {ω | τ ω ≤ π ω} ∧ MeasurableSet {ω | τ ω ≤ π ω}
⊢ MeasurableSet {ω | τ ω ≤ π ω}

Tactic:
exact this.2

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : SecondCountableTopology ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSpace ι
inst✝ : BorelSpace ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
this : MeasurableSet {ω | τ ω ≤ π ω}
⊢ MeasurableSet {ω | τ ω ≤ π ω}

Tactic:
rw [measurableSet_min_iff hτ hπ] at this

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : SecondCountableTopology ι
inst✝² : OrderTopology ι
inst✝¹ : MeasurableSpace ι
inst✝ : BorelSpace ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
this : MeasurableSet {ω | τ ω ≤ π ω} ∧ MeasurableSet {ω | τ ω ≤ π ω}
⊢ MeasurableSet {ω | τ ω ≤ π ω}
-- Mathlib/Topology/Algebra/Order/Field.lean
theorem Filter.Tendsto.neg_mul_atBot {C : 𝕜} (hC : C < 0) (hf : Tendsto f l (𝓝 C))
    (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atTop

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atBot
⊢ Tendsto (fun x => f x * g x) l atTop

Tactic:
simpa only [mul_comm] using hg.atBot_mul_neg hC hf

Result:
no goals
-- Mathlib/Data/Multiset/Fintype.lean
theorem card_toEnumFinset (m : Multiset α) : m.toEnumFinset.card = Multiset.card m

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ m.toEnumFinset.card = m.card

Tactic:
rw [Finset.card, ← Multiset.card_map Prod.fst m.toEnumFinset.val]

Result:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ (map Prod.fst m.toEnumFinset.val).card = m.card

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ (map Prod.fst m.toEnumFinset.val).card = m.card

Tactic:
congr

Result:
case e_a
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ map Prod.fst m.toEnumFinset.val = m

Proof state:
case e_a
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ map Prod.fst m.toEnumFinset.val = m

Tactic:
exact m.map_toEnumFinset_fst

Result:
no goals
-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
private lemma F''_le (p : Nat.Primes) (k : ℕ) : F'' (p, k) ≤ 2 * (p : ℝ)⁻¹ ^ (k + 3 / 2 : ℝ) :=
  calc _
    _ = Real.log p * (p : ℝ)⁻¹ ^ (k + 2)

Proof state:
p : Nat.Primes
k : ℕ
this : 0 < ↑p
⊢ 0 < (↑↑p)⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
p : Nat.Primes
k : ℕ
⊢ ↑↑p ^ (1 / 2) / (1 / 2) * (↑↑p)⁻¹ ^ (k + 2) = 2 * (↑↑p)⁻¹ ^ (-1 / 2) * (↑↑p)⁻¹ ^ (k + 2)

Tactic:
simp only [← div_mul, div_one, mul_comm, neg_div, Real.inv_rpow p.val.cast_nonneg,
  ← Real.rpow_neg p.val.cast_nonneg, neg_neg]

Result:
no goals

Proof state:
p : Nat.Primes
k : ℕ
⊢ 0 < (↑↑p)⁻¹

Tactic:
have := p.prop.pos

Result:
p : Nat.Primes
k : ℕ
this : 0 < ↑p
⊢ 0 < (↑↑p)⁻¹

Proof state:
p : Nat.Primes
k : ℕ
⊢ 2 * (↑↑p)⁻¹ ^ (-1 / 2) * (↑↑p)⁻¹ ^ (k + 2) = 2 * (↑↑p)⁻¹ ^ (↑k + 3 / 2)

Tactic:
rw [mul_assoc, ← Real.rpow_natCast,
  ← Real.rpow_add <| by have := p.prop.pos; positivity, Nat.cast_add, Nat.cast_two,
  add_comm, add_assoc]

Result:
p : Nat.Primes
k : ℕ
⊢ 2 * (↑↑p)⁻¹ ^ (↑k + (2 + -1 / 2)) = 2 * (↑↑p)⁻¹ ^ (↑k + 3 / 2)

Proof state:
p : Nat.Primes
k : ℕ
⊢ ArithmeticFunction.vonMangoldt.F'' (p, k) = Real.log ↑↑p * (↑↑p)⁻¹ ^ (k + 2)

Tactic:
simp only [F'', Function.comp_apply, F', F₀, Prod.map_apply, id_eq, le_add_iff_nonneg_left,
  zero_le, Nat.Prime.not_prime_pow, ↓reduceIte, vonMangoldt_apply_prime p.prop,
  vonMangoldt_apply_pow (Nat.zero_ne_add_one _).symm, Nat.cast_pow, div_eq_mul_inv,
  inv_pow (p : ℝ) (k + 2)]

Result:
no goals

Proof state:
p : Nat.Primes
k : ℕ
⊢ 2 * (↑↑p)⁻¹ ^ (↑k + (2 + -1 / 2)) = 2 * (↑↑p)⁻¹ ^ (↑k + 3 / 2)

Tactic:
norm_num

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedLemmas.lean
theorem mkGateCached.go_decl_eq (aig : AIG α) (input : GateInput aig) :
    ∀ (idx : Nat) (h1) (h2), (go aig input).aig.decls[idx]'h1 = aig.decls[idx]'h2

Proof state:
case h_2.h_2
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
res : Entrypoint α
x✝² : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝² : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
x✝¹ x✝ : Decl α
linv✝ rinv✝ : Bool
heq✝¹ : aig.decls[input.lhs.ref.gate] = Decl.const false
heq✝ : input.lhs.inv = false
hres : { decls := aig.decls, cache := aig.cache, invariant := ⋯ }.mkConstCached false = res
⊢ ∀ (idx : Nat)
    (h1 : idx < ({ decls := aig.decls, cache := aig.cache, invariant := ⋯ }.mkConstCached false).aig.decls.size)
    (h2 : idx < aig.decls.size),
    ({ decls := aig.decls, cache := aig.cache, invariant := ⋯ }.mkConstCached false).aig.decls[idx] = aig.decls[idx]

Tactic:
intros

Result:
case h_2.h_2
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
res : Entrypoint α
x✝² : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝² : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
x✝¹ x✝ : Decl α
linv✝ rinv✝ : Bool
heq✝¹ : aig.decls[input.lhs.ref.gate] = Decl.const false
heq✝ : input.lhs.inv = false
hres : { decls := aig.decls, cache := aig.cache, invariant := ⋯ }.mkConstCached false = res
idx✝ : Nat
h1✝ : idx✝ < ({ decls := aig.decls, cache := aig.cache, invariant := ⋯ }.mkConstCached false).aig.decls.size
h2✝ : idx✝ < aig.decls.size
⊢ ({ decls := aig.decls, cache := aig.cache, invariant := ⋯ }.mkConstCached false).aig.decls[idx✝] = aig.decls[idx✝]
-- Mathlib/Data/Set/Basic.lean
theorem ite_inter_compl_self (t s s' : Set α) : t.ite s s' ∩ tᶜ = s' ∩ tᶜ

Proof state:
α : Type u
t s s' : Set α
⊢ t.ite s s' ∩ tᶜ = s' ∩ tᶜ

Tactic:
rw [← ite_compl, ite_inter_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem sub_right_comm (m n k : Nat) : m - n - k = m - k - n

Proof state:
m n k : Nat
⊢ m - n - k = m - k - n

Tactic:
rw [Nat.sub_sub, Nat.sub_sub, Nat.add_comm]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Cast.lean
theorem Hom.eq_cast_iff_heq {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u ⟶ v) (e' : u' ⟶ v') :
    e' = e.cast hu hv ↔ HEq e' e

Proof state:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ e' = cast hu hv e ↔ HEq e' e

Tactic:
rw [eq_comm, Hom.cast_eq_iff_heq]

Result:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ HEq e e' ↔ HEq e' e

Proof state:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ HEq e e' ↔ HEq e' e

Tactic:
exact ⟨HEq.symm, HEq.symm⟩

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem neg_strictConvexOn_iff : StrictConvexOn 𝕜 s (-f) ↔ StrictConcaveOn 𝕜 s f

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommGroup β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ StrictConvexOn 𝕜 s (-f) → StrictConcaveOn 𝕜 s f

Tactic:
rintro ⟨hconv, h⟩

Result:
case mp.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommGroup β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
hconv : Convex 𝕜 s
h :
  ∀ ⦃x : E⦄,
    x ∈ s →
      ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → (-f) (a • x + b • y) < a • (-f) x + b • (-f) y
⊢ StrictConcaveOn 𝕜 s f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_eq_one {l : Array α} : l.size = 1 ↔ ∃ a, l = #[a]

Proof state:
α : Type u_1
l : Array α
⊢ l.size = 1 ↔ ∃ a, l = #[a]

Tactic:
cases l

Result:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.size = 1 ↔ ∃ a, { toList := toList✝ } = #[a]

Proof state:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.size = 1 ↔ ∃ a, { toList := toList✝ } = #[a]

Tactic:
simpa using List.length_eq_one

Result:
no goals