harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_one_preimage (s : Set M) :
    t.mulIndicator 1 ⁻¹' s ∈ ({Set.univ, ∅} : Set (Set α))

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
t : Set α
s : Set M
⊢ t.mulIndicator 1 ⁻¹' s ∈ {univ, ∅}

Tactic:
rw [mulIndicator_one', preimage_one]

Result:
α : Type u_1
M : Type u_3
inst✝ : One M
t : Set α
s : Set M
⊢ (if 1 ∈ s then univ else ∅) ∈ {univ, ∅}

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
t : Set α
s : Set M
⊢ t.mulIndicator 1 ⁻¹' s ∈ {univ, ∅}

Tactic:
classical
  rw [mulIndicator_one', preimage_one]
  split_ifs <;> simp

Result:
no goals

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
t : Set α
s : Set M
⊢ (if 1 ∈ s then univ else ∅) ∈ {univ, ∅}

Tactic:
split_ifs <;> simp

Result:
no goals
-- Mathlib/Data/List/TakeDrop.lean
theorem takeD_left' {l₁ l₂ : List α} {n} {a} (h : length l₁ = n) : takeD n (l₁ ++ l₂) a = l₁

Proof state:
α : Type u
l₁ l₂ : List α
n : ℕ
a : α
h : l₁.length = n
⊢ takeD l₁.length (l₁ ++ l₂) a = l₁

Tactic:
apply takeD_left

Result:
no goals

Proof state:
α : Type u
l₁ l₂ : List α
n : ℕ
a : α
h : l₁.length = n
⊢ takeD n (l₁ ++ l₂) a = l₁

Tactic:
rw [← h]

Result:
α : Type u
l₁ l₂ : List α
n : ℕ
a : α
h : l₁.length = n
⊢ takeD l₁.length (l₁ ++ l₂) a = l₁
-- Mathlib/Analysis/Convex/Between.lean
theorem sbtw_midpoint_of_ne {x y : P} (h : x ≠ y) : Sbtw R x (midpoint R x y) y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : x ≠ y
⊢ midpoint R x y ≠ x

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : x ≠ y
⊢ Sbtw R x (midpoint R x y) y

Tactic:
have h : midpoint R x y ≠ x := by simp [h]

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h✝ : x ≠ y
h : midpoint R x y ≠ x
⊢ Sbtw R x (midpoint R x y) y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h✝ : x ≠ y
h : midpoint R x y ≠ x
⊢ Sbtw R x (midpoint R x y) y

Tactic:
convert sbtw_pointReflection_of_ne R h

Result:
case h.e'_10
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h✝ : x ≠ y
h : midpoint R x y ≠ x
⊢ y = (pointReflection R (midpoint R x y)) x

Proof state:
case h.e'_10
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h✝ : x ≠ y
h : midpoint R x y ≠ x
⊢ y = (pointReflection R (midpoint R x y)) x

Tactic:
rw [pointReflection_midpoint_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_eq_default_of_contains_eq_false [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
    m.contains a = false → m.get! a = default

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
a : α
inst✝ : Inhabited (β a)
⊢ m.contains a = false → m.get! a = default

Tactic:
simp_to_raw using Raw₀.get!_eq_default

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Types.lean
theorem typesGrothendieckTopology_eq_canonical :
    typesGrothendieckTopology.{u} = Sheaf.canonicalTopology (Type u)

Proof state:
⊢ typesGrothendieckTopology ∈ Sheaf.finestTopologySingle '' Set.range yoneda.obj

Tactic:
refine ⟨yoneda.obj (ULift Bool), ⟨_, rfl⟩, GrothendieckTopology.ext ?_⟩

Result:
⊢ ⇑(Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) = ⇑typesGrothendieckTopology

Proof state:
case h.h
α : Type u
S : Sieve α
⊢ S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) α ↔ S ∈ typesGrothendieckTopology α

Tactic:
refine ⟨fun hs x => ?_, fun hs β f => Presieve.isSheaf_yoneda' _ fun y => hs _⟩

Result:
case h.h
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) α
x : α
⊢ S.arrows fun x_1 => x

Proof state:
case h
α : Type u
⊢ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) α = typesGrothendieckTopology α

Tactic:
ext S

Result:
case h.h
α : Type u
S : Sieve α
⊢ S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) α ↔ S ∈ typesGrothendieckTopology α

Proof state:
⊢ ⇑(Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) = ⇑typesGrothendieckTopology

Tactic:
funext α

Result:
case h
α : Type u
⊢ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) α = typesGrothendieckTopology α

Proof state:
case h.h
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) α
x : α
hsx : ¬S.arrows fun x_1 => x
⊢ False

Tactic:
have : (fun _ => ULift.up true) = fun _ => ULift.up false :=
  (hs PUnit fun _ => x).isSeparatedFor.ext
    fun β f hf => funext fun y => hsx.elim <| S.2 hf fun _ => y

Result:
case h.h
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) α
x : α
hsx : ¬S.arrows fun x_1 => x
this : (fun x => { down := true }) = fun x => { down := false }
⊢ False

Proof state:
case h.h
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) α
x : α
⊢ S.arrows fun x_1 => x

Tactic:
by_contra hsx

Result:
case h.h
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) α
x : α
hsx : ¬S.arrows fun x_1 => x
⊢ False

Proof state:
case h.h
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) α
x : α
hsx : ¬S.arrows fun x_1 => x
this : (fun x => { down := true }) = fun x => { down := false }
⊢ False

Tactic:
simp [funext_iff] at this

Result:
no goals

Proof state:
⊢ typesGrothendieckTopology = Sheaf.canonicalTopology (Type u)

Tactic:
refine le_antisymm typesGrothendieckTopology.le_canonical (sInf_le ?_)

Result:
⊢ typesGrothendieckTopology ∈ Sheaf.finestTopologySingle '' Set.range yoneda.obj
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem hasStrictDerivAt_const_cpow {x y : ℂ} (h : x ≠ 0 ∨ y ≠ 0) :
    HasStrictDerivAt (fun y => x ^ y) (x ^ y * log x) y

Proof state:
x y : ℂ
h : x ≠ 0 ∨ y ≠ 0
⊢ HasStrictDerivAt (fun y => x ^ y) (x ^ y * log x) y

Tactic:
rcases em (x = 0) with (rfl | hx)

Result:
case inl
y : ℂ
h : 0 ≠ 0 ∨ y ≠ 0
⊢ HasStrictDerivAt (fun y => 0 ^ y) (0 ^ y * log 0) y

case inr
x y : ℂ
h : x ≠ 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ HasStrictDerivAt (fun y => x ^ y) (x ^ y * log x) y

Proof state:
case inl
y : ℂ
h : 0 ≠ 0 ∨ y ≠ 0
⊢ HasStrictDerivAt (fun y => 0 ^ y) (0 ^ y * log 0) y

Tactic:
replace h := h.neg_resolve_left rfl

Result:
case inl
y : ℂ
h : y ≠ 0
⊢ HasStrictDerivAt (fun y => 0 ^ y) (0 ^ y * log 0) y

Proof state:
case inl
y : ℂ
h : y ≠ 0
⊢ HasStrictDerivAt (fun y => 0 ^ y) 0 y

Tactic:
refine (hasStrictDerivAt_const y 0).congr_of_eventuallyEq ?_

Result:
case inl
y : ℂ
h : y ≠ 0
⊢ (fun x => 0) =ᶠ[𝓝 y] fun y => 0 ^ y

Proof state:
case inl
y : ℂ
h : y ≠ 0
⊢ HasStrictDerivAt (fun y => 0 ^ y) (0 ^ y * log 0) y

Tactic:
rw [log_zero, mul_zero]

Result:
case inl
y : ℂ
h : y ≠ 0
⊢ HasStrictDerivAt (fun y => 0 ^ y) 0 y

Proof state:
case inr
x y : ℂ
h : x ≠ 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ HasStrictDerivAt (fun y => x ^ y) (x ^ y * log x) y

Tactic:
simpa only [cpow_def_of_ne_zero hx, mul_one] using
  ((hasStrictDerivAt_id y).const_mul (log x)).cexp

Result:
no goals

Proof state:
case inl
y : ℂ
h : y ≠ 0
⊢ (fun x => 0) =ᶠ[𝓝 y] fun y => 0 ^ y

Tactic:
exact (isOpen_ne.eventually_mem h).mono fun y hy => (zero_cpow hy).symm

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem Fintype.card_subtype_true [Fintype α] {h : Fintype {_a : α // True}} :
    @Fintype.card {_a // True} h = Fintype.card α

Proof state:
case H
α : Type u_1
inst✝ : Fintype α
h : Fintype { _a // True }
⊢ ∀ (x : α), x ∈ univ ↔ True

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Fintype α
h : Fintype { _a // True }
⊢ card { _a // True } = card α

Tactic:
apply Fintype.card_of_subtype

Result:
case H
α : Type u_1
inst✝ : Fintype α
h : Fintype { _a // True }
⊢ ∀ (x : α), x ∈ univ ↔ True
-- Mathlib/Computability/Primrec.lean
theorem tail {n f} (hf : @Primrec' n f) : @Primrec' n.succ fun v => f v.tail :=
  (hf.comp _ fun i => @get _ i.succ).of_eq fun v => by
    rw [← ofFn_get v.tail]; congr; funext i; simp

Proof state:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
⊢ f (ofFn fun i => v.get i.succ) = f v.tail

Tactic:
rw [← ofFn_get v.tail]

Result:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
⊢ f (ofFn fun i => v.get i.succ) = f (ofFn v.tail.get)

Proof state:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
⊢ f (ofFn fun i => v.get i.succ) = f (ofFn v.tail.get)

Tactic:
congr

Result:
case e_a.e_a
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
⊢ (fun i => v.get i.succ) = v.tail.get

Proof state:
case e_a.e_a.h
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
i : Fin n
⊢ v.get i.succ = v.tail.get i

Tactic:
simp

Result:
no goals

Proof state:
case e_a.e_a
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
⊢ (fun i => v.get i.succ) = v.tail.get

Tactic:
funext i

Result:
case e_a.e_a.h
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
i : Fin n
⊢ v.get i.succ = v.tail.get i
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem factors_le {a b : Associates α} : a.factors ≤ b.factors ↔ a ≤ b

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors ≤ b.factors
this : a.factors.prod ≤ b.factors.prod
⊢ a ≤ b

Tactic:
rwa [factors_prod, factors_prod] at this

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
⊢ a.factors ≤ b.factors ↔ a ≤ b

Tactic:
refine ⟨fun h ↦ ?_, factors_mono⟩

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors ≤ b.factors
⊢ a ≤ b

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors ≤ b.factors
⊢ a ≤ b

Tactic:
have : a.factors.prod ≤ b.factors.prod := prod_mono h

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors ≤ b.factors
this : a.factors.prod ≤ b.factors.prod
⊢ a ≤ b
-- Mathlib/Analysis/Calculus/Deriv/Abs.lean
theorem deriv_abs (x : ℝ) : deriv (|·|) x = SignType.sign x

Proof state:
x : ℝ
⊢ deriv (fun x => |x|) x = ↑(SignType.sign x)

Tactic:
obtain rfl | hx := eq_or_ne x 0

Result:
case inl

⊢ deriv (fun x => |x|) 0 = ↑(SignType.sign 0)

case inr
x : ℝ
hx : x ≠ 0
⊢ deriv (fun x => |x|) x = ↑(SignType.sign x)

Proof state:
case inr
x : ℝ
hx : x ≠ 0
⊢ deriv (fun x => |x|) x = ↑(SignType.sign x)

Tactic:
simpa [hx] using (hasDerivAt_abs hx).deriv

Result:
no goals

Proof state:
case inl

⊢ deriv (fun x => |x|) 0 = ↑(SignType.sign 0)

Tactic:
simpa using deriv_abs_zero

Result:
no goals
-- Mathlib/Analysis/Complex/CauchyIntegral.lean
theorem integral_boundary_rect_of_differentiableOn_real (f : ℂ → E) (z w : ℂ)
    (Hd : DifferentiableOn ℝ f ([[z.re, w.re]] ×ℂ [[z.im, w.im]]))
    (Hi : IntegrableOn (fun z => I • fderiv ℝ f z 1 - fderiv ℝ f z I)
      ([[z.re, w.re]] ×ℂ [[z.im, w.im]])) :
    (∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) +
      I • (∫ y : ℝ in z.im..w.im, f (re w + y * I)) -
      I • (∫ y : ℝ in z.im..w.im, f (re z + y * I)) =
      ∫ x : ℝ in z.re..w.re, ∫ y : ℝ in z.im..w.im,
        I • fderiv ℝ f (x + y * I) 1 - fderiv ℝ f (x + y * I) I :=
  integral_boundary_rect_of_hasFDerivAt_real_off_countable f (fderiv ℝ f) z w ∅ countable_empty
    Hd.continuousOn
    (fun x hx => Hd.hasFDerivAt <| by
      simpa only [← mem_interior_iff_mem_nhds, interior_reProdIm, uIcc, interior_Icc] using hx.1)
    Hi

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
z w : ℂ
Hd : DifferentiableOn ℝ f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hi : IntegrableOn (fun z => I • (fderiv ℝ f z) 1 - (fderiv ℝ f z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
x : ℂ
hx : x ∈ Ioo (z.re ⊓ w.re) (z.re ⊔ w.re) ×ℂ Ioo (z.im ⊓ w.im) (z.im ⊔ w.im) \ ∅
⊢ [[z.re, w.re]] ×ℂ [[z.im, w.im]] ∈ 𝓝 x

Tactic:
simpa only [← mem_interior_iff_mem_nhds, interior_reProdIm, uIcc, interior_Icc] using hx.1

Result:
no goals
-- Mathlib/Data/Rat/Cast/CharZero.lean
@[simp, norm_cast] lemma cast_eq_zero : (q : α) = 0 ↔ q = 0

Proof state:
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
q : ℚ≥0
⊢ ↑q = 0 ↔ q = 0

Tactic:
rw [← cast_zero, cast_inj]

Result:
no goals
-- Mathlib/Data/PNat/Xgcd.lean
theorem step_wf (hr : u.r ≠ 0) : SizeOf.sizeOf u.step < SizeOf.sizeOf u

Proof state:
u : XgcdType
hr : u.r ≠ 0
⊢ sizeOf u.step < sizeOf u

Tactic:
change u.r - 1 < u.bp

Result:
u : XgcdType
hr : u.r ≠ 0
⊢ u.r - 1 < u.bp

Proof state:
u : XgcdType
hr : u.r ≠ 0
h₀ : u.r - 1 + 1 = u.r
h₁ : u.r < u.bp + 1
⊢ u.r - 1 < u.bp

Tactic:
rw [← h₀] at h₁

Result:
u : XgcdType
hr : u.r ≠ 0
h₀ : u.r - 1 + 1 = u.r
h₁ : u.r - 1 + 1 < u.bp + 1
⊢ u.r - 1 < u.bp

Proof state:
u : XgcdType
hr : u.r ≠ 0
h₀ : u.r - 1 + 1 = u.r
h₁ : u.r - 1 + 1 < u.bp + 1
⊢ u.r - 1 < u.bp

Tactic:
exact lt_of_succ_lt_succ h₁

Result:
no goals

Proof state:
u : XgcdType
hr : u.r ≠ 0
⊢ u.r - 1 < u.bp

Tactic:
have h₀ : u.r - 1 + 1 = u.r := Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hr)

Result:
u : XgcdType
hr : u.r ≠ 0
h₀ : u.r - 1 + 1 = u.r
⊢ u.r - 1 < u.bp

Proof state:
u : XgcdType
hr : u.r ≠ 0
h₀ : u.r - 1 + 1 = u.r
⊢ u.r - 1 < u.bp

Tactic:
have h₁ : u.r < u.bp + 1 := Nat.mod_lt (u.ap + 1) u.bp.succ_pos

Result:
u : XgcdType
hr : u.r ≠ 0
h₀ : u.r - 1 + 1 = u.r
h₁ : u.r < u.bp + 1
⊢ u.r - 1 < u.bp
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_list_unit [BEq α] {l : List ((_ : α) × Unit)} {k : α}:
    getValue? k l = if containsKey k l = true then some () else none

Proof state:
case pos
α : Type u
inst✝ : BEq α
k : α
hd : (_ : α) × Unit
tl : List ((_ : α) × Unit)
ih : getValue? k tl = if containsKey k tl = true then some () else none
hd_k : (hd.fst == k) = true
⊢ (if (hd.fst == k) = true then some hd.snd else getValue? k tl) =
    if (hd.fst == k) = true ∨ containsKey k tl = true then some () else none

Tactic:
simp [hd_k]

Result:
no goals

Proof state:
case nil
α : Type u
inst✝ : BEq α
k : α
⊢ getValue? k [] = if containsKey k [] = true then some () else none

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u
inst✝ : BEq α
k : α
hd : (_ : α) × Unit
tl : List ((_ : α) × Unit)
ih : getValue? k tl = if containsKey k tl = true then some () else none
⊢ getValue? k (hd :: tl) = if containsKey k (hd :: tl) = true then some () else none

Tactic:
simp only [getValue?, containsKey, Bool.or_eq_true, Bool.cond_eq_ite_iff]

Result:
case cons
α : Type u
inst✝ : BEq α
k : α
hd : (_ : α) × Unit
tl : List ((_ : α) × Unit)
ih : getValue? k tl = if containsKey k tl = true then some () else none
⊢ (if (hd.fst == k) = true then some hd.snd else getValue? k tl) =
    if (hd.fst == k) = true ∨ containsKey k tl = true then some () else none

Proof state:
case neg
α : Type u
inst✝ : BEq α
k : α
hd : (_ : α) × Unit
tl : List ((_ : α) × Unit)
ih : getValue? k tl = if containsKey k tl = true then some () else none
hd_k : ¬(hd.fst == k) = true
⊢ (if (hd.fst == k) = true then some hd.snd else getValue? k tl) =
    if (hd.fst == k) = true ∨ containsKey k tl = true then some () else none

Tactic:
simp [hd_k, ih]

Result:
no goals

Proof state:
case cons
α : Type u
inst✝ : BEq α
k : α
hd : (_ : α) × Unit
tl : List ((_ : α) × Unit)
ih : getValue? k tl = if containsKey k tl = true then some () else none
⊢ (if (hd.fst == k) = true then some hd.snd else getValue? k tl) =
    if (hd.fst == k) = true ∨ containsKey k tl = true then some () else none

Tactic:
by_cases hd_k: (hd.fst == k) = true

Result:
case pos
α : Type u
inst✝ : BEq α
k : α
hd : (_ : α) × Unit
tl : List ((_ : α) × Unit)
ih : getValue? k tl = if containsKey k tl = true then some () else none
hd_k : (hd.fst == k) = true
⊢ (if (hd.fst == k) = true then some hd.snd else getValue? k tl) =
    if (hd.fst == k) = true ∨ containsKey k tl = true then some () else none

case neg
α : Type u
inst✝ : BEq α
k : α
hd : (_ : α) × Unit
tl : List ((_ : α) × Unit)
ih : getValue? k tl = if containsKey k tl = true then some () else none
hd_k : ¬(hd.fst == k) = true
⊢ (if (hd.fst == k) = true then some hd.snd else getValue? k tl) =
    if (hd.fst == k) = true ∨ containsKey k tl = true then some () else none
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem map_valEmbedding_Ioi : (Ioi a).map Fin.valEmbedding = Ioc ↑a (n - 1)

Proof state:
case h.mpr.zero
x : ℕ
a : Fin 0
⊢ ↑a < x ∧ x ≤ 0 - 1 → ∃ a_2, a < a_2 ∧ valEmbedding a_2 = x

Tactic:
exact Fin.elim0 a

Result:
no goals

Proof state:
case h
n : ℕ
a : Fin n
x : ℕ
⊢ x ∈ map valEmbedding (Ioi a) ↔ x ∈ Ioc (↑a) (n - 1)

Tactic:
simp only [exists_prop, Embedding.coe_subtype, mem_Ioi, mem_map, mem_Ioc]

Result:
case h
n : ℕ
a : Fin n
x : ℕ
⊢ (∃ a_1, a < a_1 ∧ valEmbedding a_1 = x) ↔ ↑a < x ∧ x ≤ n - 1

Proof state:
case h.mp
n : ℕ
a : Fin n
x : ℕ
⊢ (∃ a_1, a < a_1 ∧ valEmbedding a_1 = x) → ↑a < x ∧ x ≤ n - 1

Tactic:
rintro ⟨x, hx, rfl⟩

Result:
case h.mp.intro.intro
n : ℕ
a x : Fin n
hx : a < x
⊢ ↑a < valEmbedding x ∧ valEmbedding x ≤ n - 1

Proof state:
case h.mpr.succ
x n✝ : ℕ
a : Fin (n✝ + 1)
⊢ ↑a < x ∧ x ≤ n✝ + 1 - 1 → ∃ a_2, a < a_2 ∧ valEmbedding a_2 = x

Tactic:
exact fun hx => ⟨⟨x, Nat.lt_succ_iff.2 hx.2⟩, hx.1, rfl⟩

Result:
no goals

Proof state:
case h
n : ℕ
a : Fin n
x : ℕ
⊢ (∃ a_1, a < a_1 ∧ valEmbedding a_1 = x) ↔ ↑a < x ∧ x ≤ n - 1

Tactic:
constructor

Result:
case h.mp
n : ℕ
a : Fin n
x : ℕ
⊢ (∃ a_1, a < a_1 ∧ valEmbedding a_1 = x) → ↑a < x ∧ x ≤ n - 1

case h.mpr
n : ℕ
a : Fin n
x : ℕ
⊢ ↑a < x ∧ x ≤ n - 1 → ∃ a_2, a < a_2 ∧ valEmbedding a_2 = x

Proof state:
case h.mp.intro.intro
n : ℕ
a x : Fin n
hx : a < x
⊢ ↑a < valEmbedding x ∧ valEmbedding x ≤ n - 1

Tactic:
exact ⟨hx, Nat.le_sub_of_add_le <| x.2⟩

Result:
no goals

Proof state:
n : ℕ
a : Fin n
⊢ map valEmbedding (Ioi a) = Ioc (↑a) (n - 1)

Tactic:
ext x

Result:
case h
n : ℕ
a : Fin n
x : ℕ
⊢ x ∈ map valEmbedding (Ioi a) ↔ x ∈ Ioc (↑a) (n - 1)

Proof state:
case h.mpr
n : ℕ
a : Fin n
x : ℕ
⊢ ↑a < x ∧ x ≤ n - 1 → ∃ a_2, a < a_2 ∧ valEmbedding a_2 = x

Tactic:
cases n

Result:
case h.mpr.zero
x : ℕ
a : Fin 0
⊢ ↑a < x ∧ x ≤ 0 - 1 → ∃ a_2, a < a_2 ∧ valEmbedding a_2 = x

case h.mpr.succ
x n✝ : ℕ
a : Fin (n✝ + 1)
⊢ ↑a < x ∧ x ≤ n✝ + 1 - 1 → ∃ a_2, a < a_2 ∧ valEmbedding a_2 = x
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mul_eq_left_iff {a b : Cardinal} : a * b = a ↔ max ℵ₀ b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Proof state:
a b : Cardinal.{u_1}
⊢ a * b = a ↔ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

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

Result:
case refine_1
a b : Cardinal.{u_1}
h : a * b = a
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

case refine_2
a b : Cardinal.{u_1}
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0 → a * b = a

Proof state:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ m ≤ 1

Tactic:
rw [← not_lt]

Result:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ ¬1 < m

Proof state:
case right
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≤ a ∧ b ≠ 0

Tactic:
constructor

Result:
case right.left
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≤ a

case right.right
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≠ 0

Proof state:
case neg.h.inr.inr.intro.intro.intro
n : ℕ
h2a : ¬↑n = 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1

Tactic:
rw [← Ne] at h2a

Result:
case neg.h.inr.inr.intro.intro.intro
n : ℕ
h2a : ↑n ≠ 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1

Proof state:
case right.right
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
this : a ≠ 0
h : 0 = a
⊢ a = 0

Tactic:
exact h.symm

Result:
no goals

Proof state:
case right.right
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≠ 0

Tactic:
rintro rfl

Result:
case right.right
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
this : a ≠ 0
h : a * 0 = a
⊢ False

Proof state:
case refine_1.inr
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
right

Result:
case refine_1.inr.h
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
⊢ b = 1 ∨ a = 0
-- Mathlib/Order/Heyting/Regular.lean
theorem isRegular_top : IsRegular (⊤ : α)

Proof state:
α : Type u_1
inst✝ : HeytingAlgebra α
⊢ IsRegular ⊤

Tactic:
rw [IsRegular, compl_top, compl_bot]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
theorem exists_measure_pos_of_not_measure_iUnion_null [Countable ι] {s : ι → Set α}
    (hs : μ (⋃ n, s n) ≠ 0) : ∃ n, 0 < μ (s n)

Proof state:
α : Type u_1
ι : Sort u_5
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), μ (s n) ≤ 0
⊢ μ (⋃ n, s n) = 0

Tactic:
exact measure_iUnion_null fun n => nonpos_iff_eq_zero.1 (hs n)

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_5
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hs : μ (⋃ n, s n) ≠ 0
⊢ ∃ n, 0 < μ (s n)

Tactic:
contrapose! hs

Result:
α : Type u_1
ι : Sort u_5
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), μ (s n) ≤ 0
⊢ μ (⋃ n, s n) = 0
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem toFinsupp_add (a b : SkewMonoidAlgebra k G) :
    (a + b).toFinsupp = a.toFinsupp + b.toFinsupp

Proof state:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a b : SkewMonoidAlgebra k G
⊢ (a + b).toFinsupp = a.toFinsupp + b.toFinsupp

Tactic:
rw [← ofFinsupp_add]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
lemma exists_finset_linearIndependent_of_le_finrank {n : ℕ} (hn : n ≤ finrank R M) :
    ∃ s : Finset M, s.card = n ∧ LinearIndependent R ((↑) : s → M)

Proof state:
case neg
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
h : ¬finrank R M = 0
⊢ ∃ s, s.card = n ∧ LinearIndependent R Subtype.val

Tactic:
exact exists_finset_linearIndependent_of_le_rank
  ((Nat.cast_le.mpr hn).trans_eq (cast_toNat_of_lt_aleph0 (toNat_ne_zero.mp h).2))

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
⊢ LinearIndependent R Subtype.val

Tactic:
convert linearIndependent_empty R M using 2 <;> aesop

Result:
no goals

Proof state:
case pos
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
⊢ ∃ s, s.card = 0 ∧ LinearIndependent R Subtype.val

Tactic:
exact ⟨∅, rfl, by convert linearIndependent_empty R M using 2 <;> aesop⟩

Result:
no goals

Proof state:
case pos
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
⊢ ∃ s, s.card = n ∧ LinearIndependent R Subtype.val

Tactic:
rw [le_zero_iff.mp (hn.trans_eq h)]

Result:
case pos
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
⊢ ∃ s, s.card = 0 ∧ LinearIndependent R Subtype.val

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
⊢ ∃ s, s.card = n ∧ LinearIndependent R Subtype.val

Tactic:
by_cases h : finrank R M = 0

Result:
case pos
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
⊢ ∃ s, s.card = n ∧ LinearIndependent R Subtype.val

case neg
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
h : ¬finrank R M = 0
⊢ ∃ s, s.card = n ∧ LinearIndependent R Subtype.val
-- Mathlib/Analysis/BoxIntegral/Partition/Filter.lean
theorem henstock_le_riemann : Henstock ≤ Riemann

Proof state:
⊢ Henstock ≤ Riemann

Tactic:
trivial

Result:
no goals