harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MinMax.lean
theorem max?_le_iff [Max α] [LE α]
    (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) :
    {xs : List α} → xs.max? = some a → ∀ {x}, a ≤ x ↔ ∀ b ∈ xs, b ≤ x
  | nil => by simp
  | cons x xs => by
    rw [max?]; rintro ⟨⟩ y
    induction xs generalizing x with
    | nil => simp
    | cons y xs ih => simp [ih, max_le_iff, and_assoc]

Proof state:
α : Type u_1
a : α
inst✝¹ : Max α
inst✝ : LE α
max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a
x : α
xs : List α
⊢ some (foldl max x xs) = some a → ∀ {x_1 : α}, a ≤ x_1 ↔ ∀ (b : α), b ∈ x :: xs → b ≤ x_1

Tactic:
rintro ⟨⟩ y

Result:
case refl
α : Type u_1
inst✝¹ : Max α
inst✝ : LE α
max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a
x : α
xs : List α
y : α
⊢ foldl max x xs ≤ y ↔ ∀ (b : α), b ∈ x :: xs → b ≤ y

Proof state:
case refl
α : Type u_1
inst✝¹ : Max α
inst✝ : LE α
max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a
x : α
xs : List α
y : α
⊢ foldl max x xs ≤ y ↔ ∀ (b : α), b ∈ x :: xs → b ≤ y

Tactic:
induction xs generalizing x with
| nil => simp
| cons y xs ih => simp [ih, max_le_iff, and_assoc]

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝¹ : Max α
inst✝ : LE α
max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a
x : α
xs : List α
⊢ (x :: xs).max? = some a → ∀ {x_1 : α}, a ≤ x_1 ↔ ∀ (b : α), b ∈ x :: xs → b ≤ x_1

Tactic:
rw [max?]

Result:
α : Type u_1
a : α
inst✝¹ : Max α
inst✝ : LE α
max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a
x : α
xs : List α
⊢ some (foldl max x xs) = some a → ∀ {x_1 : α}, a ≤ x_1 ↔ ∀ (b : α), b ∈ x :: xs → b ≤ x_1

Proof state:
α : Type u_1
a : α
inst✝¹ : Max α
inst✝ : LE α
max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a
⊢ [].max? = some a → ∀ {x : α}, a ≤ x ↔ ∀ (b : α), b ∈ [] → b ≤ x

Tactic:
simp

Result:
no goals

Proof state:
case refl.cons
α : Type u_1
inst✝¹ : Max α
inst✝ : LE α
max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a
y✝ y : α
xs : List α
ih : ∀ (x : α), foldl max x xs ≤ y✝ ↔ ∀ (b : α), b ∈ x :: xs → b ≤ y✝
x : α
⊢ foldl max x (y :: xs) ≤ y✝ ↔ ∀ (b : α), b ∈ x :: y :: xs → b ≤ y✝

Tactic:
simp [ih, max_le_iff, and_assoc]

Result:
no goals

Proof state:
case refl.nil
α : Type u_1
inst✝¹ : Max α
inst✝ : LE α
max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a
y x : α
⊢ foldl max x [] ≤ y ↔ ∀ (b : α), b ∈ [x] → b ≤ y

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_erase [LawfulBEq α] (h : m.1.WF) {k a : α} {h'} :
    (m.erase k).get a h' = m.get a (contains_of_contains_erase _ h h')

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k a : α
h' : (m.erase k).contains a = true
⊢ (m.erase k).get a h' = m.get a ⋯

Tactic:
simp_to_model [erase] using List.getValueCast_eraseKey

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem unzip_eq_map (l : Vector (α × β) n) : unzip l = (l.map Prod.fst, l.map Prod.snd)

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
toArray✝ : Array (α × β)
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.unzip =
    (map Prod.fst { toArray := toArray✝, size_toArray := size_toArray✝ },
      map Prod.snd { toArray := toArray✝, size_toArray := size_toArray✝ })

Tactic:
simp [List.unzip_eq_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
l : Vector (α × β) n
⊢ l.unzip = (map Prod.fst l, map Prod.snd l)

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
toArray✝ : Array (α × β)
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.unzip =
    (map Prod.fst { toArray := toArray✝, size_toArray := size_toArray✝ },
      map Prod.snd { toArray := toArray✝, size_toArray := size_toArray✝ })
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
lemma isSFiniteKernel_prodMkRight_unit {κ : Kernel α β} :
    IsSFiniteKernel (prodMkRight Unit κ) ↔ IsSFiniteKernel κ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
x✝ : IsSFiniteKernel (prodMkRight Unit κ)
⊢ IsSFiniteKernel ((prodMkRight Unit κ).comap (fun a => (a, ())) ⋯)

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
x✝ : IsSFiniteKernel (prodMkRight Unit κ)
⊢ IsSFiniteKernel κ

Tactic:
change IsSFiniteKernel ((prodMkRight Unit κ).comap (fun a ↦ (a, ())) (by fun_prop))

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
x✝ : IsSFiniteKernel (prodMkRight Unit κ)
⊢ IsSFiniteKernel ((prodMkRight Unit κ).comap (fun a => (a, ())) ⋯)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
x✝ : IsSFiniteKernel (prodMkRight Unit κ)
⊢ Measurable fun a => (a, ())

Tactic:
fun_prop

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsSFiniteKernel (prodMkRight Unit κ) ↔ IsSFiniteKernel κ

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
x✝ : IsSFiniteKernel (prodMkRight Unit κ)
⊢ IsSFiniteKernel κ
-- Mathlib/Algebra/Group/Nat/Even.lean
theorem one_lt_of_ne_zero_of_even (h0 : n ≠ 0) (hn : Even n) : 1 < n

Proof state:
n : ℕ
h0 : n ≠ 0
hn : Even n
h : n = 1
⊢ False

Tactic:
rw [h] at hn

Result:
n : ℕ
h0 : n ≠ 0
hn : Even 1
h : n = 1
⊢ False

Proof state:
n : ℕ
h0 : n ≠ 0
hn : Even 1
h : n = 1
⊢ False

Tactic:
exact Nat.not_even_one hn

Result:
no goals

Proof state:
n : ℕ
h0 : n ≠ 0
hn : Even n
⊢ 1 < n

Tactic:
refine Nat.one_lt_iff_ne_zero_and_ne_one.mpr (And.intro h0 ?_)

Result:
n : ℕ
h0 : n ≠ 0
hn : Even n
⊢ n ≠ 1

Proof state:
n : ℕ
h0 : n ≠ 0
hn : Even n
⊢ n ≠ 1

Tactic:
intro h

Result:
n : ℕ
h0 : n ≠ 0
hn : Even n
h : n = 1
⊢ False
-- Mathlib/Data/ZMod/Basic.lean
theorem add_self_eq_zero_iff_eq_zero {n : ℕ} (hn : Odd n) {a : ZMod n} :
    a + a = 0 ↔ a = 0

Proof state:
n : ℕ
hn : Odd n
a : ZMod n
⊢ a + a = 0 ↔ a = 0

Tactic:
rw [Nat.odd_iff, ← Nat.two_dvd_ne_zero, ← Nat.prime_two.coprime_iff_not_dvd] at hn

Result:
n : ℕ
hn : Nat.Coprime 2 n
a : ZMod n
⊢ a + a = 0 ↔ a = 0

Proof state:
n : ℕ
hn : Nat.Coprime 2 n
a : ZMod n
⊢ a + a = 0 ↔ a = 0

Tactic:
rw [← mul_two, ← @Nat.cast_two (ZMod n), ← ZMod.coe_unitOfCoprime 2 hn, Units.mul_left_eq_zero]

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem factorial_inj (hn : 1 < n) : n ! = m ! ↔ n = m

Proof state:
m n : ℕ
hn : 1 < n
h : n ! = m !
⊢ n = m

Tactic:
obtain hnm | rfl | hnm := lt_trichotomy n m

Result:
case inl
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : n < m
⊢ n = m

case inr.inl
n : ℕ
hn : 1 < n
h : n ! = n !
⊢ n = n

case inr.inr
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : m < n
⊢ n = m

Proof state:
case inr.inl
n : ℕ
hn : 1 < n
h : n ! = n !
⊢ n = n

Tactic:
rfl

Result:
no goals

Proof state:
m n : ℕ
hn : 1 < n
⊢ n ! = m ! ↔ n = m

Tactic:
refine ⟨fun h => ?_, congr_arg _⟩

Result:
m n : ℕ
hn : 1 < n
h : n ! = m !
⊢ n = m

Proof state:
case inr.inr
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m < n
⊢ n = m

Tactic:
rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm

Result:
case inr.inr
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m ! < m !
⊢ n = m

Proof state:
case inr.inr
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m ! < m !
⊢ n = m

Tactic:
cases lt_irrefl _ hnm

Result:
no goals

Proof state:
case inr.inr
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : m < n
⊢ n = m

Tactic:
rw [← one_lt_factorial, h, one_lt_factorial] at hn

Result:
case inr.inr
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m < n
⊢ n = m

Proof state:
case inl
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : n < m
⊢ n = m

Tactic:
rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm

Result:
case inl
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : m ! < m !
⊢ n = m

Proof state:
case inl
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : m ! < m !
⊢ n = m

Tactic:
cases lt_irrefl _ hnm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem of_findIdx?_eq_some {xs : Array α} {p : α → Bool} (w : xs.findIdx? p = some i) :
    match xs[i]? with | some a => p a | none => false

Proof state:
α : Type u_1
i : Nat
p : α → Bool
xs : List α
w : findIdx? p { toList := xs } = some i
⊢ List.findIdx? p xs = some i

Tactic:
simpa using w

Result:
no goals

Proof state:
α : Type u_1
i : Nat
xs : Array α
p : α → Bool
w : findIdx? p xs = some i
⊢ match xs[i]? with
  | some a => p a = true
  | none => false = true

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
i : Nat
p : α → Bool
xs : List α
w : findIdx? p { toList := xs } = some i
⊢ match { toList := xs }[i]? with
  | some a => p a = true
  | none => false = true

Proof state:
case mk
α : Type u_1
i : Nat
p : α → Bool
xs : List α
w : findIdx? p { toList := xs } = some i
⊢ match { toList := xs }[i]? with
  | some a => p a = true
  | none => false = true

Tactic:
simpa using List.of_findIdx?_eq_some (by simpa using w)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem sin_arg (x : ℂ) : Real.sin (arg x) = x.im / ‖x‖

Proof state:
x : ℂ
⊢ Real.sin x.arg = x.im / ‖x‖

Tactic:
unfold arg

Result:
x : ℂ
⊢ Real.sin
      (if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ x.im then Real.arcsin ((-x).im / ‖x‖) + π else Real.arcsin ((-x).im / ‖x‖) - π) =
    x.im / ‖x‖

Proof state:
x : ℂ
⊢ Real.sin
      (if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ x.im then Real.arcsin ((-x).im / ‖x‖) + π else Real.arcsin ((-x).im / ‖x‖) - π) =
    x.im / ‖x‖

Tactic:
split_ifs <;>
simp [sub_eq_add_neg, arg, Real.sin_arcsin (abs_le.1 (abs_im_div_norm_le_one x)).1
(abs_le.1 (abs_im_div_norm_le_one x)).2, Real.sin_add, neg_div, Real.arcsin_neg, Real.sin_neg]

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem IsSuccPrelimit.isMin_of_noMax (h : IsSuccPrelimit a) : IsMin a

Proof state:
case intro.zero
α : Type u_1
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
b : α
h : IsSuccPrelimit (succ^[0] b)
hb : b ≤ succ^[0] b
⊢ succ^[0] b ≤ b

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case intro.succ
α : Type u_1
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
b : α
n : ℕ
h : IsSuccPrelimit (succ (succ^[n] b))
hb : b ≤ succ^[n + 1] b
⊢ succ^[n + 1] b ≤ b

Tactic:
exact (not_isSuccPrelimit_succ _ h).elim

Result:
no goals

Proof state:
case intro.succ
α : Type u_1
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
b : α
n : ℕ
h : IsSuccPrelimit (succ^[n + 1] b)
hb : b ≤ succ^[n + 1] b
⊢ succ^[n + 1] b ≤ b

Tactic:
rw [iterate_succ_apply'] at h

Result:
case intro.succ
α : Type u_1
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
b : α
n : ℕ
h : IsSuccPrelimit (succ (succ^[n] b))
hb : b ≤ succ^[n + 1] b
⊢ succ^[n + 1] b ≤ b

Proof state:
α : Type u_1
a : α
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
h : IsSuccPrelimit a
⊢ IsMin a

Tactic:
intro b hb

Result:
α : Type u_1
a : α
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
h : IsSuccPrelimit a
b : α
hb : b ≤ a
⊢ a ≤ b

Proof state:
α : Type u_1
a : α
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
h : IsSuccPrelimit a
b : α
hb : b ≤ a
⊢ a ≤ b

Tactic:
rcases hb.exists_succ_iterate with ⟨_ | n, rfl⟩

Result:
case intro.zero
α : Type u_1
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
b : α
h : IsSuccPrelimit (succ^[0] b)
hb : b ≤ succ^[0] b
⊢ succ^[0] b ≤ b

case intro.succ
α : Type u_1
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
b : α
n : ℕ
h : IsSuccPrelimit (succ^[n + 1] b)
hb : b ≤ succ^[n + 1] b
⊢ succ^[n + 1] b ≤ b
-- Mathlib/Data/Int/Log.lean
theorem clog_of_right_le_one (b : ℕ) {r : R} (hr : r ≤ 1) : clog b r = -Nat.log b ⌊r⁻¹⌋₊

Proof state:
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr✝ : r ≤ 1
hr : r < 1
⊢ clog b r = -↑(Nat.log b ⌊r⁻¹⌋₊)

Tactic:
exact if_neg hr.not_le

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hr : 1 ≤ 1
⊢ clog b 1 = -↑(Nat.log b ⌊1⁻¹⌋₊)

Tactic:
rw [clog, if_pos hr, inv_one, Nat.ceil_one, Nat.floor_one, Nat.log_one_right,
  Nat.clog_one_right, Int.ofNat_zero, neg_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 1
⊢ clog b r = -↑(Nat.log b ⌊r⁻¹⌋₊)

Tactic:
obtain rfl | hr := hr.eq_or_lt

Result:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hr : 1 ≤ 1
⊢ clog b 1 = -↑(Nat.log b ⌊1⁻¹⌋₊)

case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr✝ : r ≤ 1
hr : r < 1
⊢ clog b r = -↑(Nat.log b ⌊r⁻¹⌋₊)
-- Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
theorem abs_discr_gt_two (h : 1 < finrank ℚ K) : 2 < |discr K|

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
⊢ 2 < |discr K|

Tactic:
rify

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
⊢ 2 < |↑(discr K)|

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
⊢ 4 / 9 * (3 * π / 4) ^ 2 ≤ 4 / 9 * (3 * π / 4) ^ finrank ℚ K

Tactic:
gcongr

Result:
case h.ha
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
⊢ 1 ≤ 3 * π / 4

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
⊢ 2 < |↑(discr K)|

Tactic:
calc
  (2 : ℝ) < (4 / 9) * (3 * π / 4) ^ 2 := by
    nlinarith [Real.pi_gt_three]
  _ ≤ (4 / 9 : ℝ) * (3 * π / 4) ^ finrank ℚ K := by
    gcongr
    linarith [Real.pi_gt_three]
  _ ≤ |(discr K : ℝ)| := mod_cast abs_discr_ge h

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
⊢ 2 < 4 / 9 * (3 * π / 4) ^ 2

Tactic:
nlinarith [Real.pi_gt_three]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
⊢ 2 < |discr K|

Tactic:
rw [← Nat.succ_le_iff] at h

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
⊢ 2 < |discr K|

Proof state:
case h.ha
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
⊢ 1 ≤ 3 * π / 4

Tactic:
linarith [Real.pi_gt_three]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_eq_false_iff_exists_isSome_getEntry? [BEq α] [ReflBEq α] :
    {l : List ((a : α) × β a)} → l.isEmpty = false ↔ ∃ a, (getEntry? a l).isSome
  | [] => by simp
  | (⟨k, v⟩::l) => by simpa using ⟨k, by simp⟩

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : ReflBEq α
k : α
v : β k
l : List ((a : α) × β a)
⊢ (⟨k, v⟩ :: l).isEmpty = false ↔ ∃ a, (getEntry? a (⟨k, v⟩ :: l)).isSome = true

Tactic:
simpa using ⟨k, by simp⟩

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : ReflBEq α
⊢ [].isEmpty = false ↔ ∃ a, (getEntry? a []).isSome = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : ReflBEq α
k : α
v : β k
l : List ((a : α) × β a)
⊢ (getEntry? k (⟨k, v⟩ :: l)).isSome = true

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[ext 1100]
lemma ext₀ (z₁ z₂ : Cochain F G 0)
    (h : ∀ (p : ℤ), z₁.v p p (add_zero p) = z₂.v p p (add_zero p)) : z₁ = z₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
z₁ z₂ : Cochain F G 0
h : ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯
p q : ℤ
hpq : p + 0 = q
⊢ q = p

Tactic:
rw [← hpq, add_zero]

Result:
no goals

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
z₁ z₂ : Cochain F G 0
h : ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯
q : ℤ
hpq : q + 0 = q
⊢ z₁.v q q hpq = z₂.v q q hpq

Tactic:
exact h q

Result:
no goals

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
z₁ z₂ : Cochain F G 0
h : ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯
p q : ℤ
hpq : p + 0 = q
⊢ z₁.v p q hpq = z₂.v p q hpq

Tactic:
obtain rfl : q = p := by rw [← hpq, add_zero]

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
z₁ z₂ : Cochain F G 0
h : ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯
q : ℤ
hpq : q + 0 = q
⊢ z₁.v q q hpq = z₂.v q q hpq

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
z₁ z₂ : Cochain F G 0
h : ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯
⊢ z₁ = z₂

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
z₁ z₂ : Cochain F G 0
h : ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯
p q : ℤ
hpq : p + 0 = q
⊢ z₁.v p q hpq = z₂.v p q hpq
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
theorem coe_piCongrLeft (f : δ ≃ δ') :
    ⇑(MeasurableEquiv.piCongrLeft π f) = f.piCongrLeft π

Proof state:
δ : Type u_4
δ' : Type u_5
π : δ' → Type u_6
inst✝ : (x : δ') → MeasurableSpace (π x)
f : δ ≃ δ'
⊢ ⇑(piCongrLeft π f) = ⇑(Equiv.piCongrLeft π f)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/BooleanAlgebra.lean
@[simp] lemma subtype_univ [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype {a // p a}] :
    univ.subtype p = univ

Proof state:
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ Finset.subtype p univ = univ

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem direction_bot : (⊥ : AffineSubspace k P).direction = ⊥

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
⊢ ⊥.direction = ⊥

Tactic:
rw [direction_eq_vectorSpan, bot_coe, vectorSpan_def, vsub_empty, Submodule.span_empty]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Basic.lean
theorem unsat_def (f : CNF α) : Unsat f ↔ (∀ a, eval a f = false)

Proof state:
α : Type u_1
f : CNF α
⊢ f.Unsat ↔ ∀ (a : α → Bool), eval a f = false

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem le_seminorm' (k n : ℕ) (f : 𝓢(ℝ, F)) (x : ℝ) :
    |x| ^ k * ‖iteratedDeriv n f x‖ ≤ SchwartzMap.seminorm 𝕜 k n f

Proof state:
𝕜 : Type u_1
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
x : ℝ
⊢ |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f

Tactic:
have := le_seminorm 𝕜 k n f x

Result:
𝕜 : Type u_1
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
x : ℝ
this : ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f
⊢ |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f

Proof state:
𝕜 : Type u_1
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
x : ℝ
this : ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f
⊢ |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f

Tactic:
rwa [← Real.norm_eq_abs, ← norm_iteratedFDeriv_eq_norm_iteratedDeriv]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
lemma hasCoproduct_of_equiv_of_iso (f : α → C) (g : β → C)
    [HasCoproduct f] (e : β ≃ α) (iso : ∀ j, g j ≅ f (e j)) : HasCoproduct g

Proof state:
β : Type w
α✝ : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α✝ → C
g : β → C
inst✝ : HasCoproduct f
e : β ≃ α✝
iso : (j : β) → g j ≅ f (e j)
this : HasColimit ((Discrete.equivalence e).functor ⋙ Discrete.functor f)
α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f
⊢ HasCoproduct g

Tactic:
exact hasColimitOfIso α

Result:
no goals

Proof state:
β : Type w
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
g : β → C
inst✝ : HasCoproduct f
e : β ≃ α
iso : (j : β) → g j ≅ f (e j)
this : HasColimit ((Discrete.equivalence e).functor ⋙ Discrete.functor f)
⊢ HasCoproduct g

Tactic:
have α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f :=
  Discrete.natIso (fun ⟨j⟩ => iso j)

Result:
β : Type w
α✝ : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α✝ → C
g : β → C
inst✝ : HasCoproduct f
e : β ≃ α✝
iso : (j : β) → g j ≅ f (e j)
this : HasColimit ((Discrete.equivalence e).functor ⋙ Discrete.functor f)
α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f
⊢ HasCoproduct g

Proof state:
β : Type w
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
g : β → C
inst✝ : HasCoproduct f
e : β ≃ α
iso : (j : β) → g j ≅ f (e j)
⊢ HasCoproduct g

Tactic:
have : HasColimit ((Discrete.equivalence e).functor ⋙ Discrete.functor f) :=
  hasColimit_equivalence_comp _

Result:
β : Type w
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
g : β → C
inst✝ : HasCoproduct f
e : β ≃ α
iso : (j : β) → g j ≅ f (e j)
this : HasColimit ((Discrete.equivalence e).functor ⋙ Discrete.functor f)
⊢ HasCoproduct g
-- Mathlib/Algebra/Star/Pointwise.lean
theorem image_star [InvolutiveStar α] : Star.star '' s = s⋆

Proof state:
α : Type u_1
s : Set α
inst✝ : InvolutiveStar α
⊢ star '' s = s⋆

Tactic:
simp only [← star_preimage]

Result:
α : Type u_1
s : Set α
inst✝ : InvolutiveStar α
⊢ star '' s = star ⁻¹' s

Proof state:
α : Type u_1
s : Set α
inst✝ : InvolutiveStar α
⊢ star '' s = star ⁻¹' s

Tactic:
rw [image_eq_preimage_of_inverse] <;> intro <;> simp only [star_star]

Result:
no goals