harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Primorial.lean
theorem primorial_le_4_pow (n : ℕ) : n# ≤ 4 ^ n

Proof state:
case h.succ.inr
n : ℕ
ihn : ∀ m < n + 1, m# ≤ 4 ^ m
ho : Odd n
⊢ (n + 1)# ≤ 4 ^ (n + 1)

Tactic:
rcases Decidable.eq_or_ne n 1 with (rfl | hn)

Result:
case h.succ.inr.inl
ihn : ∀ m < 1 + 1, m# ≤ 4 ^ m
ho : Odd 1
⊢ (1 + 1)# ≤ 4 ^ (1 + 1)

case h.succ.inr.inr
n : ℕ
ihn : ∀ m < n + 1, m# ≤ 4 ^ m
ho : Odd n
hn : n ≠ 1
⊢ (n + 1)# ≤ 4 ^ (n + 1)

Proof state:
case h.zero
ihn : ∀ m < 0, m# ≤ 4 ^ m
⊢ 0# ≤ 4 ^ 0

Tactic:
rfl

Result:
no goals

Proof state:
case h.succ.inl.intro
m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1# ≤ 4 ^ m_1
⊢ (m + m + 1)# ≤ 4 ^ (m + m + 1)

Tactic:
rcases m.eq_zero_or_pos with (rfl | hm)

Result:
case h.succ.inl.intro.inl
ihn : ∀ m < 0 + 0 + 1, m# ≤ 4 ^ m
⊢ (0 + 0 + 1)# ≤ 4 ^ (0 + 0 + 1)

case h.succ.inl.intro.inr
m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1# ≤ 4 ^ m_1
hm : m > 0
⊢ (m + m + 1)# ≤ 4 ^ (m + m + 1)

Proof state:
m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1# ≤ 4 ^ m_1
hm : m > 0
⊢ (m + 1)# * (m + 1 + m).choose (m + 1) = (m + 1)# * (2 * m + 1).choose m

Tactic:
rw [choose_symm_add, two_mul, add_right_comm]

Result:
no goals

Proof state:
m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1# ≤ 4 ^ m_1
hm : m > 0
⊢ 4 ^ (m + 1) * 4 ^ m ≤ 4 ^ (m + m + 1)

Tactic:
rw [← pow_add, add_right_comm]

Result:
no goals

Proof state:
case h.succ.inl.intro.inl
ihn : ∀ m < 0 + 0 + 1, m# ≤ 4 ^ m
⊢ (0 + 0 + 1)# ≤ 4 ^ (0 + 0 + 1)

Tactic:
decide

Result:
no goals

Proof state:
case h.succ.inr.inl
ihn : ∀ m < 1 + 1, m# ≤ 4 ^ m
ho : Odd 1
⊢ (1 + 1)# ≤ 4 ^ (1 + 1)

Tactic:
decide

Result:
no goals

Proof state:
case h
n : ℕ
ihn : ∀ m < n, m# ≤ 4 ^ m
⊢ n# ≤ 4 ^ n

Tactic:
rcases n with - | n

Result:
case h.zero
ihn : ∀ m < 0, m# ≤ 4 ^ m
⊢ 0# ≤ 4 ^ 0

case h.succ
n : ℕ
ihn : ∀ m < n + 1, m# ≤ 4 ^ m
⊢ (n + 1)# ≤ 4 ^ (n + 1)

Proof state:
m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1# ≤ 4 ^ m_1
hm : m > 0
⊢ (m + m + 1)# = (m + 1 + m)#

Tactic:
rw [add_right_comm]

Result:
no goals

Proof state:
case h.succ.inr.inr
n : ℕ
ihn : ∀ m < n + 1, m# ≤ 4 ^ m
ho : Odd n
hn : n ≠ 1
⊢ (n + 1)# ≤ 4 ^ (n + 1)

Tactic:
calc
  (n + 1)# = n# := primorial_succ hn ho
  _ ≤ 4 ^ n := ihn n n.lt_succ_self
  _ ≤ 4 ^ (n + 1) := pow_le_pow_of_le_right four_pos n.le_succ

Result:
no goals

Proof state:
case h.succ.inl.intro.inr
m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1# ≤ 4 ^ m_1
hm : m > 0
⊢ (m + m + 1)# ≤ 4 ^ (m + m + 1)

Tactic:
calc
  (m + m + 1)# = (m + 1 + m)# := by rw [add_right_comm]
  _ ≤ (m + 1)# * choose (m + 1 + m) (m + 1) := primorial_add_le m.le_succ
  _ = (m + 1)# * choose (2 * m + 1) m := by rw [choose_symm_add, two_mul, add_right_comm]
  _ ≤ 4 ^ (m + 1) * 4 ^ m :=
    mul_le_mul' (ihn _ <| succ_lt_succ <| (lt_add_iff_pos_left _).2 hm) (choose_middle_le_pow _)
  _ ≤ 4 ^ (m + m + 1) := by rw [← pow_add, add_right_comm]

Result:
no goals

Proof state:
case h.succ
n : ℕ
ihn : ∀ m < n + 1, m# ≤ 4 ^ m
⊢ (n + 1)# ≤ 4 ^ (n + 1)

Tactic:
rcases n.even_or_odd with (⟨m, rfl⟩ | ho)

Result:
case h.succ.inl.intro
m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1# ≤ 4 ^ m_1
⊢ (m + m + 1)# ≤ 4 ^ (m + m + 1)

case h.succ.inr
n : ℕ
ihn : ∀ m < n + 1, m# ≤ 4 ^ m
ho : Odd n
⊢ (n + 1)# ≤ 4 ^ (n + 1)
-- Mathlib/Algebra/EuclideanDomain/Defs.lean
theorem mul_right_not_lt {a : R} (b) (h : a ≠ 0) : ¬a * b ≺ b

Proof state:
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬a * b ≺ b

Tactic:
rw [mul_comm]

Result:
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬b * a ≺ b

Proof state:
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬b * a ≺ b

Tactic:
exact mul_left_not_lt b h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatMap_assoc {α β} (l : Vector α n) (f : α → Vector β m) (g : β → Vector γ k) :
    (l.flatMap f).flatMap g = (l.flatMap fun x => (f x).flatMap g).cast (by simp [Nat.mul_assoc])

Proof state:
case mk
m : Nat
γ : Type u_1
k : Nat
α : Type u_2
β : Type u_3
f : α → Vector β m
g : β → Vector γ k
l : Array α
⊢ ({ toArray := l, size_toArray := ⋯ }.flatMap f).flatMap g =
    Vector.cast ⋯ ({ toArray := l, size_toArray := ⋯ }.flatMap fun x => (f x).flatMap g)

Tactic:
simp [Array.flatMap_assoc]

Result:
no goals

Proof state:
n m : Nat
γ : Type ?u.331828
k : Nat
α : Type ?u.331818
β : Type ?u.331823
l : Vector α n
f : α → Vector β m
g : β → Vector γ k
⊢ n * (m * k) = n * m * k

Tactic:
simp [Nat.mul_assoc]

Result:
no goals

Proof state:
n m : Nat
γ : Type u_1
k : Nat
α : Type u_2
β : Type u_3
l : Vector α n
f : α → Vector β m
g : β → Vector γ k
⊢ (l.flatMap f).flatMap g = Vector.cast ⋯ (l.flatMap fun x => (f x).flatMap g)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
m : Nat
γ : Type u_1
k : Nat
α : Type u_2
β : Type u_3
f : α → Vector β m
g : β → Vector γ k
l : Array α
⊢ ({ toArray := l, size_toArray := ⋯ }.flatMap f).flatMap g =
    Vector.cast ⋯ ({ toArray := l, size_toArray := ⋯ }.flatMap fun x => (f x).flatMap g)
-- Mathlib/RingTheory/OreLocalization/Basic.lean
theorem neg_add_cancel (x : X[S⁻¹]) : -x + x = 0

Proof state:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddGroup X
inst✝ : DistribMulAction R X
r : X
s : ↥S
⊢ -(r /ₒ s) + r /ₒ s = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddGroup X
inst✝ : DistribMulAction R X
x : OreLocalization S X
⊢ -x + x = 0

Tactic:
induction' x with r s

Result:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddGroup X
inst✝ : DistribMulAction R X
r : X
s : ↥S
⊢ -(r /ₒ s) + r /ₒ s = 0
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
theorem compression_idem (a : α) (𝒜 : Finset (Finset α)) : 𝓓 a (𝓓 a 𝒜) = 𝓓 a 𝒜

Proof state:
case h.inr
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : s ∉ 𝓓 a 𝒜 ∧ insert a s ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜

Tactic:
cases h.1 (mem_compression_of_insert_mem_compression h.2)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ 𝓓 a (𝓓 a 𝒜) = 𝓓 a 𝒜

Tactic:
ext s

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝓓 a (𝓓 a 𝒜) ↔ s ∈ 𝓓 a 𝒜

Proof state:
case h.inl
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝓓 a 𝒜 ∧ s.erase a ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜

Tactic:
exact h.1

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝓓 a (𝓓 a 𝒜) ↔ s ∈ 𝓓 a 𝒜

Tactic:
refine mem_compression.trans ⟨?_, fun h => Or.inl ⟨h, erase_mem_compression_of_mem_compression h⟩⟩

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝓓 a 𝒜 ∧ s.erase a ∈ 𝓓 a 𝒜 ∨ s ∉ 𝓓 a 𝒜 ∧ insert a s ∈ 𝓓 a 𝒜 → s ∈ 𝓓 a 𝒜

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝓓 a 𝒜 ∧ s.erase a ∈ 𝓓 a 𝒜 ∨ s ∉ 𝓓 a 𝒜 ∧ insert a s ∈ 𝓓 a 𝒜 → s ∈ 𝓓 a 𝒜

Tactic:
rintro (h | h)

Result:
case h.inl
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝓓 a 𝒜 ∧ s.erase a ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜

case h.inr
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : s ∉ 𝓓 a 𝒜 ∧ insert a s ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integral_comp_mul_deriv_Ioi {f f' : ℝ → ℝ} {g : ℝ → ℝ} {a : ℝ}
    (hf : ContinuousOn f <| Ici a) (hft : Tendsto f atTop atTop)
    (hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x)
    (hg_cont : ContinuousOn g <| f '' Ioi a) (hg1 : IntegrableOn g <| f '' Ici a)
    (hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) (Ici a)) :
    (∫ x in Ioi a, (g ∘ f) x * f' x) = ∫ u in Ioi (f a), g u

Proof state:
f f' g : ℝ → ℝ
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a) volume
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) (Ici a) volume
⊢ ∫ (x : ℝ) in Ioi a, (g ∘ f) x * f' x = ∫ (u : ℝ) in Ioi (f a), g u

Tactic:
have hg2' : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a) := by simpa [mul_comm] using hg2

Result:
f f' g : ℝ → ℝ
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a) volume
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) (Ici a) volume
hg2' : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a) volume
⊢ ∫ (x : ℝ) in Ioi a, (g ∘ f) x * f' x = ∫ (u : ℝ) in Ioi (f a), g u

Proof state:
f f' g : ℝ → ℝ
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a) volume
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) (Ici a) volume
hg2' : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a) volume
⊢ ∫ (x : ℝ) in Ioi a, (g ∘ f) x * f' x = ∫ (u : ℝ) in Ioi (f a), g u

Tactic:
simpa [mul_comm] using integral_comp_smul_deriv_Ioi hf hft hff' hg_cont hg1 hg2'

Result:
no goals

Proof state:
f f' g : ℝ → ℝ
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a) volume
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) (Ici a) volume
⊢ IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a) volume

Tactic:
simpa [mul_comm] using hg2

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem preimage_coe_Iio_top : (some : α → WithTop α) ⁻¹' Iio ⊤ = univ

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ some ⁻¹' Iio ⊤ = univ

Tactic:
rw [← range_coe, preimage_range]

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma primitiveCharacter_isPrimitive : IsPrimitive (χ.primitiveCharacter)

Proof state:
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
h : ¬χ.conductor = 0
⊢ χ.primitiveCharacter.IsPrimitive

Tactic:
exact le_antisymm (Nat.le_of_dvd (Nat.pos_of_ne_zero h) (conductor_dvd_level _)) <|
  conductor_le_conductor_mem_conductorSet <| conductor_mem_conductorSet χ

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
h : χ.conductor = 0
⊢ χ.primitiveCharacter.conductor = χ.conductor

Tactic:
convert conductor_eq_zero_iff_level_eq_zero.mpr h

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
h : χ.conductor = 0
⊢ χ.primitiveCharacter.IsPrimitive

Tactic:
rw [isPrimitive_def]

Result:
case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
h : χ.conductor = 0
⊢ χ.primitiveCharacter.conductor = χ.conductor

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ χ.primitiveCharacter.IsPrimitive

Tactic:
by_cases h : χ.conductor = 0

Result:
case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
h : χ.conductor = 0
⊢ χ.primitiveCharacter.IsPrimitive

case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
h : ¬χ.conductor = 0
⊢ χ.primitiveCharacter.IsPrimitive
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_neg : ⌈-a⌉ = -⌊a⌋ :=
  eq_of_forall_ge_iff fun z => by rw [neg_le, ceil_le, le_floor, Int.cast_neg, neg_le]

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
z : ℤ
⊢ ⌈-a⌉ ≤ z ↔ -⌊a⌋ ≤ z

Tactic:
rw [neg_le, ceil_le, le_floor, Int.cast_neg, neg_le]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Basic.lean
theorem mul_eq_one_iff : s * t = 1 ↔ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1

Proof state:
case coe.bot
α : Type u_2
inst✝ : OrderedCommGroup α
a✝ : NonemptyInterval α
⊢ ↑a✝ * ⊥ = 1 ↔ ∃ a b, ↑a✝ = pure a ∧ ⊥ = pure b ∧ a * b = 1

Tactic:
simp

Result:
no goals

Proof state:
case bot
α : Type u_2
inst✝ : OrderedCommGroup α
t : Interval α
⊢ ⊥ * t = 1 ↔ ∃ a b, ⊥ = pure a ∧ t = pure b ∧ a * b = 1

Tactic:
simp

Result:
no goals

Proof state:
case coe.coe
α : Type u_2
inst✝ : OrderedCommGroup α
a✝¹ a✝ : NonemptyInterval α
⊢ a✝¹ * a✝ = 1 ↔ ∃ a b, a✝¹ = NonemptyInterval.pure a ∧ a✝ = NonemptyInterval.pure b ∧ a * b = 1

Tactic:
exact NonemptyInterval.mul_eq_one_iff

Result:
no goals

Proof state:
case coe
α : Type u_2
inst✝ : OrderedCommGroup α
t : Interval α
a✝ : NonemptyInterval α
⊢ ↑a✝ * t = 1 ↔ ∃ a b, ↑a✝ = pure a ∧ t = pure b ∧ a * b = 1

Tactic:
cases t

Result:
case coe.bot
α : Type u_2
inst✝ : OrderedCommGroup α
a✝ : NonemptyInterval α
⊢ ↑a✝ * ⊥ = 1 ↔ ∃ a b, ↑a✝ = pure a ∧ ⊥ = pure b ∧ a * b = 1

case coe.coe
α : Type u_2
inst✝ : OrderedCommGroup α
a✝¹ a✝ : NonemptyInterval α
⊢ ↑a✝¹ * ↑a✝ = 1 ↔ ∃ a b, ↑a✝¹ = pure a ∧ ↑a✝ = pure b ∧ a * b = 1

Proof state:
case coe.coe
α : Type u_2
inst✝ : OrderedCommGroup α
a✝¹ a✝ : NonemptyInterval α
⊢ ↑a✝¹ * ↑a✝ = 1 ↔ ∃ a b, ↑a✝¹ = pure a ∧ ↑a✝ = pure b ∧ a * b = 1

Tactic:
simp_rw [← NonemptyInterval.coe_mul_interval, ← NonemptyInterval.coe_one_interval,
  WithBot.coe_inj, NonemptyInterval.coe_eq_pure]

Result:
case coe.coe
α : Type u_2
inst✝ : OrderedCommGroup α
a✝¹ a✝ : NonemptyInterval α
⊢ a✝¹ * a✝ = 1 ↔ ∃ a b, a✝¹ = NonemptyInterval.pure a ∧ a✝ = NonemptyInterval.pure b ∧ a * b = 1

Proof state:
α : Type u_2
inst✝ : OrderedCommGroup α
s t : Interval α
⊢ s * t = 1 ↔ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1

Tactic:
cases s

Result:
case bot
α : Type u_2
inst✝ : OrderedCommGroup α
t : Interval α
⊢ ⊥ * t = 1 ↔ ∃ a b, ⊥ = pure a ∧ t = pure b ∧ a * b = 1

case coe
α : Type u_2
inst✝ : OrderedCommGroup α
t : Interval α
a✝ : NonemptyInterval α
⊢ ↑a✝ * t = 1 ↔ ∃ a b, ↑a✝ = pure a ∧ t = pure b ∧ a * b = 1
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_eraseKey [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k a : α} {h}
    (hl : DistinctKeys l) : getKey a (eraseKey k l) h =
      getKey a l (containsKey_of_containsKey_eraseKey hl h)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
k a : α
h✝ : containsKey a (eraseKey k l) = true
h : (k == a) = false ∧ containsKey a l = true
hl : DistinctKeys l
⊢ (if false = true then none else getKey? a l) = some (getKey a l ⋯)

Tactic:
simp [← getKey?_eq_some_getKey]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
k a : α
h✝ : containsKey a (eraseKey k l) = true
h : (k == a) = false ∧ containsKey a l = true
hl : DistinctKeys l
⊢ getKey a (eraseKey k l) h✝ = getKey a l ⋯

Tactic:
rw [← Option.some_inj, ← getKey?_eq_some_getKey, getKey?_eraseKey hl, h.1]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
k a : α
h✝ : containsKey a (eraseKey k l) = true
h : (k == a) = false ∧ containsKey a l = true
hl : DistinctKeys l
⊢ (if false = true then none else getKey? a l) = some (getKey a l ⋯)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
k a : α
h : containsKey a (eraseKey k l) = true
hl : DistinctKeys l
⊢ getKey a (eraseKey k l) h = getKey a l ⋯

Tactic:
rw [containsKey_eraseKey hl, Bool.and_eq_true, Bool.not_eq_true'] at h

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
k a : α
h✝ : containsKey a (eraseKey k l) = true
h : (k == a) = false ∧ containsKey a l = true
hl : DistinctKeys l
⊢ getKey a (eraseKey k l) h✝ = getKey a l ⋯
-- Mathlib/Data/Finset/Card.lean
/-- Reorder a finset.

The difference with `Finset.card_nbij'` is that the bijection is specified as a surjective
injection, rather than by an inverse function.

The difference with `Finset.card_bij` is that the bijection is a non-dependent function, rather than
being allowed to use membership of the domain. -/
lemma card_nbij (i : α → β) (hi : ∀ a ∈ s, i a ∈ t) (i_inj : (s : Set α).InjOn i)
    (i_surj : (s : Set α).SurjOn i t) : #s = #t :=
  card_bij (fun a _ ↦ i a) hi i_inj (by simpa using i_surj)

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : α → β
hi : ∀ a ∈ s, i a ∈ t
i_inj : Set.InjOn i ↑s
i_surj : Set.SurjOn i ↑s ↑t
⊢ ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), (fun a x => i a) a ha = b

Tactic:
simpa using i_surj

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero (s : ℝ) (b : ℝ) (hb : 0 < b) :
    Tendsto (fun x : ℝ => x ^ s * exp (-b * x)) atTop (𝓝 0)

Proof state:
s b : ℝ
hb : 0 < b
x : ℝ
⊢ (fun x => rexp (b * x) / x ^ s)⁻¹ x = x ^ s * rexp (-b * x)

Tactic:
simp [exp_neg, inv_div, div_eq_mul_inv _ (exp _)]

Result:
no goals

Proof state:
s b : ℝ
hb : 0 < b
⊢ Tendsto (fun x => x ^ s * rexp (-b * x)) atTop (𝓝 0)

Tactic:
refine (tendsto_exp_mul_div_rpow_atTop s b hb).inv_tendsto_atTop.congr' ?_

Result:
s b : ℝ
hb : 0 < b
⊢ (fun x => rexp (b * x) / x ^ s)⁻¹ =ᶠ[atTop] fun x => x ^ s * rexp (-b * x)

Proof state:
s b : ℝ
hb : 0 < b
⊢ (fun x => rexp (b * x) / x ^ s)⁻¹ =ᶠ[atTop] fun x => x ^ s * rexp (-b * x)

Tactic:
filter_upwards with x using by simp [exp_neg, inv_div, div_eq_mul_inv _ (exp _)]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_one : μ.withDensity 1 = μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ.withDensity 1 = μ

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity 1) s = μ s

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity 1) s = μ s

Tactic:
simp [withDensity_apply _ hs]

Result:
no goals
-- Mathlib/Order/SemiconjSup.lean
theorem Semiconj.symm_adjoint [PartialOrder α] [Preorder β] {fa : α ≃o α} {fb : β ↪o β} {g : α → β}
    (h : Function.Semiconj g fa fb) {g' : β → α} (hg' : IsOrderRightAdjoint g g') :
    Function.Semiconj g' fb fa

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ⇑fa ⇑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
y : β
⊢ IsLUB (⇑fa '' {a | g (fa a) ≤ fb y}) (fa (g' y))

Tactic:
simp only [h.eq, fb.le_iff_le, fa.leftOrdContinuous (hg' _)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ⇑fa ⇑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
⊢ Semiconj g' ⇑fb ⇑fa

Tactic:
refine fun y => (hg' _).unique ?_

Result:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ⇑fa ⇑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
y : β
⊢ IsLUB {x | g x ≤ fb y} (fa (g' y))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ⇑fa ⇑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
y : β
⊢ IsLUB {x | g x ≤ fb y} (fa (g' y))

Tactic:
rw [← fa.surjective.image_preimage { x | g x ≤ fb y }, preimage_setOf_eq]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ⇑fa ⇑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
y : β
⊢ IsLUB (⇑fa '' {a | g (fa a) ≤ fb y}) (fa (g' y))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt_add_of_neg_add_lt {a b c : Int} (h : -b + a < c) : a < b + c

Proof state:
a b c : Int
h : -b + a < c
⊢ a < b + c

Tactic:
have h := Int.add_lt_add_left h b

Result:
a b c : Int
h✝ : -b + a < c
h : b + (-b + a) < b + c
⊢ a < b + c

Proof state:
a b c : Int
h✝ : -b + a < c
h : b + (-b + a) < b + c
⊢ a < b + c

Tactic:
rwa [Int.add_neg_cancel_left] at h

Result:
no goals
-- Mathlib/RingTheory/Support.lean
lemma Module.mem_support_iff' :
    p ∈ Module.support R M ↔ ∃ m : M, ∀ r ∉ p.asIdeal, r • m ≠ 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
⊢ (∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0) ↔ ∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
⊢ p ∈ support R M ↔ ∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0

Tactic:
rw [← @not_not (_ ∈ _), not_mem_support_iff']

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
⊢ (¬∀ (m : M), ∃ r ∉ p.asIdeal, r • m = 0) ↔ ∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
⊢ (¬∀ (m : M), ∃ r ∉ p.asIdeal, r • m = 0) ↔ ∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0

Tactic:
push_neg

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
⊢ (∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0) ↔ ∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem true_imp_eq (p : Prop) : (True → p) = p

Proof state:
p : Prop
⊢ (True → p) = p

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem tendsto_comp_coe_Iio_atTop :
    Tendsto (fun x : Iio a => f x) atTop l ↔ Tendsto f (𝓝[<] a) l

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
l : Filter β
f : α → β
⊢ Tendsto (fun x => f ↑x) atTop l ↔ Tendsto f (𝓝[<] a) l

Tactic:
rw [← map_coe_Iio_atTop, tendsto_map'_iff]

Result:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
l : Filter β
f : α → β
⊢ Tendsto (fun x => f ↑x) atTop l ↔ Tendsto (f ∘ Subtype.val) atTop l

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
l : Filter β
f : α → β
⊢ Tendsto (fun x => f ↑x) atTop l ↔ Tendsto (f ∘ Subtype.val) atTop l

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive]
lemma orderOf_pow_orderOf_div {x : G} {n : ℕ} (hx : orderOf x ≠ 0) (hn : n ∣ orderOf x) :
    orderOf (x ^ (orderOf x / n)) = n

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x / n * n ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0

Tactic:
exact left_ne_zero_of_mul hx

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0

Tactic:
rw [← Nat.div_mul_cancel hn] at hx

Result:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x / n * n ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ orderOf (x ^ (orderOf x / n)) = n

Tactic:
rw [orderOf_pow_of_dvd _ (Nat.div_dvd_of_dvd hn), Nat.div_div_self hn hx]

Result:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0
-- Mathlib/Data/NNReal/Defs.lean
@[simp]
lemma natCastle_toNNReal' {n : ℕ} {r : ℝ} : ↑n ≤ r.toNNReal ↔ n ≤ r ∨ n = 0

Proof state:
n : ℕ
r : ℝ
⊢ ↑n ≤ r.toNNReal ↔ ↑n ≤ r ∨ n = 0

Tactic:
simpa [n.cast_nonneg.le_iff_eq] using toNNReal_le_toNNReal_iff' (r := n)

Result:
no goals