harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem getElem_zero_filterMap (f : α → Option β) (l : Array α) (h) :
    (l.filterMap f)[0] = (l.findSome? f).get (by cases l; simpa [List.length_filterMap_eq_countP] using h)

Proof state:
α : Type ?u.7118
β : Type ?u.7115
f : α → Option β
l : Array α
h : 0 < (filterMap f l).size
⊢ (findSome? f l).isSome = true

Tactic:
cases l

Result:
case mk
α : Type ?u.7118
β : Type ?u.7115
f : α → Option β
toList✝ : List α
h : 0 < (filterMap f { toList := toList✝ }).size
⊢ (findSome? f { toList := toList✝ }).isSome = true

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
h : 0 < (filterMap f l).size
⊢ (filterMap f l)[0] = (findSome? f l).get ⋯

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
h : 0 < (filterMap f { toList := toList✝ }).size
⊢ (filterMap f { toList := toList✝ })[0] = (findSome? f { toList := toList✝ }).get ⋯

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
h : 0 < (filterMap f { toList := toList✝ }).size
⊢ (filterMap f { toList := toList✝ })[0] = (findSome? f { toList := toList✝ }).get ⋯

Tactic:
simp [← List.head_eq_getElem, ← getElem?_zero_filterMap]

Result:
no goals

Proof state:
case mk
α : Type ?u.7118
β : Type ?u.7115
f : α → Option β
toList✝ : List α
h : 0 < (filterMap f { toList := toList✝ }).size
⊢ (findSome? f { toList := toList✝ }).isSome = true

Tactic:
simpa [List.length_filterMap_eq_countP] using h

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem isOpen_singleton_iff : IsOpen ({a} : Set Ordinal) ↔ ¬IsLimit a

Proof state:
case refine_2.inr.inl.intro
b : Ordinal.{u}
ha : ¬(succ b).IsLimit
⊢ IsOpen (Set.Ioo b (succ (succ b)))

Tactic:
exact isOpen_Ioo

Result:
no goals

Proof state:
case refine_1.intro.intro.intro
a : Ordinal.{u}
h : IsOpen {a}
ha : a.IsLimit
b c : Ordinal.{u}
hbc : a ∈ Set.Ioo b c
hbc' : Set.Ioo b c ⊆ {a}
⊢ False

Tactic:
have hba := ha.succ_lt hbc.1

Result:
case refine_1.intro.intro.intro
a : Ordinal.{u}
h : IsOpen {a}
ha : a.IsLimit
b c : Ordinal.{u}
hbc : a ∈ Set.Ioo b c
hbc' : Set.Ioo b c ⊆ {a}
hba : succ b < a
⊢ False

Proof state:
case refine_2.inr.inr
a : Ordinal.{u}
ha : ¬a.IsLimit
ha' : a.IsLimit
⊢ IsOpen {a}

Tactic:
exact (ha ha').elim

Result:
no goals

Proof state:
case refine_1
a : Ordinal.{u}
h : IsOpen {a}
ha : a.IsLimit
⊢ False

Tactic:
obtain ⟨b, c, hbc, hbc'⟩ :=
  (mem_nhds_iff_exists_Ioo_subset' ⟨0, ha.pos⟩ ⟨_, lt_succ a⟩).1
    (h.mem_nhds rfl)

Result:
case refine_1.intro.intro.intro
a : Ordinal.{u}
h : IsOpen {a}
ha : a.IsLimit
b c : Ordinal.{u}
hbc : a ∈ Set.Ioo b c
hbc' : Set.Ioo b c ⊆ {a}
⊢ False

Proof state:
case refine_2.inr.inl.intro
b : Ordinal.{u}
ha : ¬(succ b).IsLimit
⊢ IsOpen {succ b}

Tactic:
rw [← Set.Icc_self, Icc_succ_left, ← Ioo_succ_right]

Result:
case refine_2.inr.inl.intro
b : Ordinal.{u}
ha : ¬(succ b).IsLimit
⊢ IsOpen (Set.Ioo b (succ (succ b)))

Proof state:
case refine_2.inl
ha : ¬IsLimit 0
⊢ IsOpen {0}

Tactic:
rw [← bot_eq_zero, ← Set.Iic_bot, ← Iio_succ]

Result:
case refine_2.inl
ha : ¬IsLimit 0
⊢ IsOpen (Set.Iio (succ ⊥))

Proof state:
case refine_2.inl
ha : ¬IsLimit 0
⊢ IsOpen (Set.Iio (succ ⊥))

Tactic:
exact isOpen_Iio

Result:
no goals

Proof state:
case refine_2
a : Ordinal.{u}
ha : ¬a.IsLimit
⊢ IsOpen {a}

Tactic:
rcases zero_or_succ_or_limit a with (rfl | ⟨b, rfl⟩ | ha')

Result:
case refine_2.inl
ha : ¬IsLimit 0
⊢ IsOpen {0}

case refine_2.inr.inl.intro
b : Ordinal.{u}
ha : ¬(succ b).IsLimit
⊢ IsOpen {succ b}

case refine_2.inr.inr
a : Ordinal.{u}
ha : ¬a.IsLimit
ha' : a.IsLimit
⊢ IsOpen {a}

Proof state:
case refine_1.intro.intro.intro
a : Ordinal.{u}
h : IsOpen {a}
ha : a.IsLimit
b c : Ordinal.{u}
hbc : a ∈ Set.Ioo b c
hbc' : Set.Ioo b c ⊆ {a}
hba : succ b < a
⊢ False

Tactic:
exact hba.ne (hbc' ⟨lt_succ b, hba.trans hbc.2⟩)

Result:
no goals

Proof state:
a : Ordinal.{u}
⊢ IsOpen {a} ↔ ¬a.IsLimit

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

Result:
case refine_1
a : Ordinal.{u}
h : IsOpen {a}
ha : a.IsLimit
⊢ False

case refine_2
a : Ordinal.{u}
ha : ¬a.IsLimit
⊢ IsOpen {a}
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem SameCycle.exists_pow_eq' [Finite α] : SameCycle f x y → ∃ i < orderOf f, (f ^ i) x = y

Proof state:
case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ (k % ↑(orderOf f)).natAbs < orderOf f ∧ (f ^ (k % ↑(orderOf f)).natAbs) x = (f ^ k) x

Tactic:
rw [← zpow_natCast, Int.natAbs_of_nonneg h₁, zpow_mod_orderOf]

Result:
case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ (k % ↑(orderOf f)).natAbs < orderOf f ∧ (f ^ k) x = (f ^ k) x

Proof state:
case intro
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
⊢ ∃ i < orderOf f, (f ^ i) x = (f ^ k) x

Tactic:
use (k % orderOf f).natAbs

Result:
case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
⊢ (k % ↑(orderOf f)).natAbs < orderOf f ∧ (f ^ (k % ↑(orderOf f)).natAbs) x = (f ^ k) x

Proof state:
case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ k % ↑(orderOf f) < ↑(orderOf f)

Tactic:
exact Int.emod_lt_of_pos _ h₀

Result:
no goals

Proof state:
case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
⊢ (k % ↑(orderOf f)).natAbs < orderOf f ∧ (f ^ (k % ↑(orderOf f)).natAbs) x = (f ^ k) x

Tactic:
have h₁ := Int.emod_nonneg k h₀.ne'

Result:
case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ (k % ↑(orderOf f)).natAbs < orderOf f ∧ (f ^ (k % ↑(orderOf f)).natAbs) x = (f ^ k) x

Proof state:
α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
⊢ f.SameCycle x y → ∃ i < orderOf f, (f ^ i) x = y

Tactic:
rintro ⟨k, rfl⟩

Result:
case intro
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
⊢ ∃ i < orderOf f, (f ^ i) x = (f ^ k) x

Proof state:
case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
⊢ (k % ↑(orderOf f)).natAbs < orderOf f ∧ (f ^ (k % ↑(orderOf f)).natAbs) x = (f ^ k) x

Tactic:
have h₀ := Int.natCast_pos.mpr (orderOf_pos f)

Result:
case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
⊢ (k % ↑(orderOf f)).natAbs < orderOf f ∧ (f ^ (k % ↑(orderOf f)).natAbs) x = (f ^ k) x

Proof state:
case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ (k % ↑(orderOf f)).natAbs < orderOf f

Tactic:
rw [← Int.ofNat_lt, Int.natAbs_of_nonneg h₁]

Result:
case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ k % ↑(orderOf f) < ↑(orderOf f)

Proof state:
case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ (k % ↑(orderOf f)).natAbs < orderOf f ∧ (f ^ k) x = (f ^ k) x

Tactic:
refine ⟨?_, by rfl⟩

Result:
case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ (k % ↑(orderOf f)).natAbs < orderOf f

Proof state:
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ (f ^ k) x = (f ^ k) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Bits.lean
theorem bit_ne_zero (b) {n} (h : n ≠ 0) : bit b n ≠ 0

Proof state:
b : Bool
n : ℕ
h : n ≠ 0
⊢ bit b n ≠ 0

Tactic:
cases b <;> dsimp [bit] <;> omega

Result:
no goals
-- Mathlib/Data/Matroid/Sum.lean
@[simp] lemma sum'_isBase_iff {B} :
    (Matroid.sum' M).IsBase B ↔ ∀ i, (M i).IsBase (Prod.mk i ⁻¹' B)

Proof state:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
B : Set (ι × α)
⊢ (Matroid.sum' M).IsBase B ↔ ∀ (i : ι), (M i).IsBase (Prod.mk i ⁻¹' B)

Tactic:
simp only [Matroid.sum', mapEquiv_isBase_iff, Equiv.sigmaEquivProd_symm_apply, sigma_isBase_iff]

Result:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
B : Set (ι × α)
⊢ (∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' B))) ↔ ∀ (i : ι), (M i).IsBase (Prod.mk i ⁻¹' B)

Proof state:
case h.e'_2.h.h.e'_3.h
α : Type u_1
ι : Type u_2
M : ι → Matroid α
B : Set (ι × α)
a✝ : ι
x✝ : α
⊢ x✝ ∈ Prod.mk a✝ ⁻¹' B ↔ x✝ ∈ Sigma.mk a✝ ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' B)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_2.h.h.e'_3
α : Type u_1
ι : Type u_2
M : ι → Matroid α
B : Set (ι × α)
a✝ : ι
⊢ Prod.mk a✝ ⁻¹' B = Sigma.mk a✝ ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' B)

Tactic:
ext

Result:
case h.e'_2.h.h.e'_3.h
α : Type u_1
ι : Type u_2
M : ι → Matroid α
B : Set (ι × α)
a✝ : ι
x✝ : α
⊢ x✝ ∈ Prod.mk a✝ ⁻¹' B ↔ x✝ ∈ Sigma.mk a✝ ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' B)

Proof state:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
B : Set (ι × α)
⊢ (∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' B))) ↔ ∀ (i : ι), (M i).IsBase (Prod.mk i ⁻¹' B)

Tactic:
convert Iff.rfl

Result:
case h.e'_2.h.h.e'_3
α : Type u_1
ι : Type u_2
M : ι → Matroid α
B : Set (ι × α)
a✝ : ι
⊢ Prod.mk a✝ ⁻¹' B = Sigma.mk a✝ ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' B)
-- Mathlib/Order/LiminfLimsup.lean
theorem OrderIso.limsup_apply {γ} [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ]
    {f : Filter α} {u : α → β} (g : β ≃o γ)
    (hu : f.IsBoundedUnder (· ≤ ·) u

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hf : u = fun i => g.symm (g (u i))
⊢ g.symm (limsup (fun x => g (u x)) f) ≤ limsup (fun i => g.symm (g (u i))) f

Tactic:
refine (OrderIso.to_galoisConnection g.symm).l_limsup_le ?_ hgu_co

Result:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hf : u = fun i => g.symm (g (u i))
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g.symm (g (u x))
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
@[to_additive]
lemma isBlock_iff_smul_eq_of_mem :
    IsBlock G B ↔ ∀ ⦃g : G⦄ ⦃a : X⦄, a ∈ B → g • a ∈ B → g • B = B

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
⊢ IsBlock G B ↔ ∀ ⦃g : G⦄ ⦃a : X⦄, a ∈ B → g • a ∈ B → g • B = B

Tactic:
simp [isBlock_iff_smul_eq_of_nonempty, Set.Nonempty, mem_smul_set]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Units/Regulator.lean
theorem finrank_mul_regulator_eq_det (w' : InfinitePlace K) (e : {w // w ≠ w'} ≃ Fin (rank K)) :
    finrank ℚ K * regulator K =
      |(Matrix.of (fun i w : InfinitePlace K ↦
        if h : i = w' then (w.mult : ℝ) else w.mult * (w (fundSystem K (e ⟨i, h⟩))).log)).det|

Proof state:
case e_a.e_a.e_M.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
i j : Fin (rank K)
⊢ (Matrix.reindex g g) (Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e i))))) i
      j =
    (Matrix.of fun i w =>
          if h : i = w' then ↑w.mult
          else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨i, h⟩))))).submatrix
      (fun x => f ((f.symm w').succAbove x)) (fun x => f ((f.symm w').succAbove x)) i j

Tactic:
rw [Matrix.reindex_apply, Matrix.submatrix_apply, Matrix.submatrix_apply, Matrix.of_apply,
  Matrix.of_apply, dif_neg]

Result:
case e_a.e_a.e_M.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
i j : Fin (rank K)
⊢ ↑(↑(g.symm j)).mult * Real.log (↑(g.symm j) ((algebraMap (𝓞 K) K) ↑(fundSystem K (e (g.symm i))))) =
    ↑(f ((f.symm w').succAbove j)).mult *
      Real.log
        ((f ((f.symm w').succAbove j))
          ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨f ((f.symm w').succAbove i), ?e_a.e_a.e_M.a.hnc✝⟩))))

case e_a.e_a.e_M.a.hnc
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
i j : Fin (rank K)
⊢ ¬f ((f.symm w').succAbove i) = w'
-- Mathlib/RingTheory/Norm/Transitivity.lean
theorem Matrix.det_det [Fintype m] [Fintype n] (f : S →+* Matrix n n R) :
    (f M.det).det = ((M.map f).comp m m n n R).det

Proof state:
case succ
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    l = Fintype.card m → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
card : l + 1 = Fintype.card m
k : m
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
let f' := f.polyToMatrix

Result:
case succ
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    l = Fintype.card m → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
card : l + 1 = Fintype.card m
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldr_append (f : α → β → β) (b) (l : Vector α n) (l' : Vector α k) :
    (l ++ l').foldr f b = l.foldr f (l'.foldr f b)

Proof state:
α : Type u_1
β : Type u_2
n k : Nat
f : α → β → β
b : β
l : Vector α n
l' : Vector α k
⊢ foldr f b (l ++ l') = foldr f (foldr f b l') l

Tactic:
simp [foldr_eq_foldrM]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem or_eq_zero_iff {x y : BitVec w} : (x ||| y) = 0#w ↔ x = 0#w ∧ y = 0#w

Proof state:
case mpr
w : Nat
x y : BitVec w
h : x = 0#w ∧ y = 0#w
⊢ x ||| y = 0#w

Tactic:
simp [h]

Result:
no goals

Proof state:
case mp
w : Nat
x y : BitVec w
h : x ||| y = 0#w
⊢ x = 0#w ∧ y = 0#w

Tactic:
constructor

Result:
case mp.left
w : Nat
x y : BitVec w
h : x ||| y = 0#w
⊢ x = 0#w

case mp.right
w : Nat
x y : BitVec w
h : x ||| y = 0#w
⊢ y = 0#w

Proof state:
case mp
w : Nat
x y : BitVec w
⊢ x ||| y = 0#w → x = 0#w ∧ y = 0#w

Tactic:
intro h

Result:
case mp
w : Nat
x y : BitVec w
h : x ||| y = 0#w
⊢ x = 0#w ∧ y = 0#w

Proof state:
case mpr
w : Nat
x y : BitVec w
⊢ x = 0#w ∧ y = 0#w → x ||| y = 0#w

Tactic:
intro h

Result:
case mpr
w : Nat
x y : BitVec w
h : x = 0#w ∧ y = 0#w
⊢ x ||| y = 0#w

Proof state:
w : Nat
x y : BitVec w
⊢ x ||| y = 0#w ↔ x = 0#w ∧ y = 0#w

Tactic:
constructor

Result:
case mp
w : Nat
x y : BitVec w
⊢ x ||| y = 0#w → x = 0#w ∧ y = 0#w

case mpr
w : Nat
x y : BitVec w
⊢ x = 0#w ∧ y = 0#w → x ||| y = 0#w

Proof state:
case mp.right
w : Nat
x y : BitVec w
h : x ||| y = 0#w
⊢ y = 0#w

Tactic:
ext i ih

Result:
case mp.right.pred
w : Nat
x y : BitVec w
h : x ||| y = 0#w
i : Nat
ih : i < w
⊢ y.getLsbD i = (0#w).getLsbD i

Proof state:
case mp.right.pred
w : Nat
x y : BitVec w
h : x ||| y = 0#w
i : Nat
ih : i < w
this : x.getLsbD i = false ∧ y.getLsbD i = false
⊢ y.getLsbD i = (0#w).getLsbD i

Tactic:
simp [this]

Result:
no goals

Proof state:
case mp.right.pred
w : Nat
x y : BitVec w
h : x ||| y = 0#w
i : Nat
ih : i < w
this : (x ||| y).getLsbD i = (0#w).getLsbD i
⊢ y.getLsbD i = (0#w).getLsbD i

Tactic:
simp only [getLsbD_or, getLsbD_zero, Bool.or_eq_false_iff] at this

Result:
case mp.right.pred
w : Nat
x y : BitVec w
h : x ||| y = 0#w
i : Nat
ih : i < w
this : x.getLsbD i = false ∧ y.getLsbD i = false
⊢ y.getLsbD i = (0#w).getLsbD i

Proof state:
case mp.right.pred
w : Nat
x y : BitVec w
h : x ||| y = 0#w
i : Nat
ih : i < w
⊢ y.getLsbD i = (0#w).getLsbD i

Tactic:
have := BitVec.eq_of_getLsbD_eq_iff.mp h i ih

Result:
case mp.right.pred
w : Nat
x y : BitVec w
h : x ||| y = 0#w
i : Nat
ih : i < w
this : (x ||| y).getLsbD i = (0#w).getLsbD i
⊢ y.getLsbD i = (0#w).getLsbD i
-- Mathlib/Geometry/Manifold/VectorField.lean
@[simp] lemma mlieBracketWithin_self : mlieBracketWithin I V V = 0

Proof state:
case h.h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
V : (x : M) → TangentSpace I x
x : Set M
x✝ : M
⊢ mlieBracketWithin I V V x x✝ = 0 x x✝

Tactic:
simp [mlieBracketWithin, mpullback]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
V : (x : M) → TangentSpace I x
⊢ mlieBracketWithin I V V = 0

Tactic:
ext x

Result:
case h.h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
V : (x : M) → TangentSpace I x
x : Set M
x✝ : M
⊢ mlieBracketWithin I V V x x✝ = 0 x x✝
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoLocallyUniformly.comp [TopologicalSpace γ] (h : TendstoLocallyUniformly F f p)
    (g : γ → α) (cg : Continuous g) : TendstoLocallyUniformly (fun n => F n ∘ g) (f ∘ g) p

Proof state:
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformly F f p
g : γ → α
cg : Continuous g
⊢ TendstoLocallyUniformly (fun n => F n ∘ g) (f ∘ g) p

Tactic:
rw [← tendstoLocallyUniformlyOn_univ] at h ⊢

Result:
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformlyOn F f p univ
g : γ → α
cg : Continuous g
⊢ TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p univ

Proof state:
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformlyOn F f p univ
g : γ → α
cg : Continuous g
⊢ TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p univ

Tactic:
rw [continuous_iff_continuousOn_univ] at cg

Result:
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformlyOn F f p univ
g : γ → α
cg : ContinuousOn g univ
⊢ TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p univ

Proof state:
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformlyOn F f p univ
g : γ → α
cg : ContinuousOn g univ
⊢ TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p univ

Tactic:
exact h.comp _ (mapsTo_univ _ _) cg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/OfFn.lean
theorem length_ofFn (f : Fin n → α) : (ofFn f).length = n

Proof state:
case succ
α : Type u_1
n : Nat
ih : ∀ (f : Fin n → α), (Fin.foldr n (fun x1 x2 => f x1 :: x2) []).length = n
f : Fin (n + 1) → α
⊢ (Fin.foldr (n + 1) (fun x1 x2 => f x1 :: x2) []).length = n + 1

Tactic:
simp [Fin.foldr_succ, ih]

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
⊢ (Fin.foldr n (fun x1 x2 => f x1 :: x2) []).length = n

Tactic:
induction n with
| zero => simp
| succ n ih => simp [Fin.foldr_succ, ih]

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
⊢ (ofFn f).length = n

Tactic:
simp only [ofFn]

Result:
n : Nat
α : Type u_1
f : Fin n → α
⊢ (Fin.foldr n (fun x1 x2 => f x1 :: x2) []).length = n

Proof state:
case zero
α : Type u_1
f : Fin 0 → α
⊢ (Fin.foldr 0 (fun x1 x2 => f x1 :: x2) []).length = 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma CotangentSpace.compEquiv_symm_inr :
    (compEquiv Q P).symm.toLinearMap ∘ₗ
      LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) =
        (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom).liftBaseChange T

Proof state:
case a
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : P.vars
⊢ (Q.comp P).cotangentSpaceBasis.repr
      ((↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
        ((Basis.baseChange T P.cotangentSpaceBasis) i)) =
    (Q.comp P).cotangentSpaceBasis.repr
      ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
        ((Basis.baseChange T P.cotangentSpaceBasis) i))

Tactic:
ext j

Result:
case a.h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : P.vars
j : (Q.comp P).vars
⊢ ((Q.comp P).cotangentSpaceBasis.repr
        ((↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
          ((Basis.baseChange T P.cotangentSpaceBasis) i)))
      j =
    ((Q.comp P).cotangentSpaceBasis.repr
        ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
          ((Basis.baseChange T P.cotangentSpaceBasis) i)))
      j