harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean
theorem analyticOnNhd_cexp : AnalyticOnNhd ℂ exp univ

Proof state:
⊢ AnalyticOnNhd ℂ (NormedSpace.exp ℂ) univ

Tactic:
exact fun x _ ↦ NormedSpace.exp_analytic x

Result:
no goals

Proof state:
⊢ AnalyticOnNhd ℂ cexp univ

Tactic:
rw [Complex.exp_eq_exp_ℂ]

Result:
⊢ AnalyticOnNhd ℂ (NormedSpace.exp ℂ) univ
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_lt_one_iff : a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a

Proof state:
case inl
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : b < 0
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a

Tactic:
simp [hb, hb.not_lt, hb.ne, div_lt_one_of_neg]

Result:
no goals

Proof state:
case inr.inr
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : 0 < b
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a

Tactic:
simp [hb, hb.not_lt, div_lt_one, hb.ne.symm]

Result:
no goals

Proof state:
case inr.inl
α : Type u_2
inst✝ : LinearOrderedField α
a : α
⊢ a / 0 < 1 ↔ 0 < 0 ∧ a < 0 ∨ 0 = 0 ∨ 0 < 0 ∧ 0 < a

Tactic:
simp [zero_lt_one]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a

Tactic:
rcases lt_trichotomy b 0 with (hb | rfl | hb)

Result:
case inl
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : b < 0
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a

case inr.inl
α : Type u_2
inst✝ : LinearOrderedField α
a : α
⊢ a / 0 < 1 ↔ 0 < 0 ∧ a < 0 ∨ 0 = 0 ∨ 0 < 0 ∧ 0 < a

case inr.inr
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : 0 < b
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
-- Mathlib/Topology/IndicatorConstPointwise.lean
lemma tendsto_indicator_const_iff_tendsto_pi_pure'
    (b : β) (nhd_b : {0}ᶜ ∈ 𝓝 b) (nhd_o : {b}ᶜ ∈ 𝓝 0) :
    Tendsto (fun i ↦ (As i).indicator (fun (_ : α) ↦ b)) L (𝓝 (A.indicator (fun (_ : α) ↦ b)))
      ↔ (Tendsto As L <| Filter.pi (pure <| · ∈ A))

Proof state:
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun x => As x i) L (pure (i ∈ A))

Tactic:
simp_rw [tendsto_pure]

Result:
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), ∀ᶠ (x : ι) in L, As x i = (i ∈ A)

Proof state:
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), ∀ᶠ (x : ι) in L, As x i = (i ∈ A)

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
⊢ Tendsto (fun i => (As i).indicator fun x => b) L (𝓝 (A.indicator fun x => b)) ↔
    Tendsto As L (pi fun x => pure (x ∈ A))

Tactic:
rw [tendsto_indicator_const_iff_forall_eventually' _ b nhd_b nhd_o, tendsto_pi]

Result:
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun x => As x i) L (pure (i ∈ A))
-- Mathlib/RingTheory/Trace/Basic.lean
theorem Algebra.trace_surjective [FiniteDimensional K L] [Algebra.IsSeparable K L] :
    Function.Surjective (Algebra.trace K L)

Proof state:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
⊢ ¬trace K L = 0

Tactic:
exact Algebra.trace_ne_zero K L

Result:
no goals

Proof state:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
⊢ range (trace K L) = ⊤

Tactic:
apply (IsSimpleOrder.eq_bot_or_eq_top (α := Ideal K) _).resolve_left

Result:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
⊢ ¬range (trace K L) = ⊥

Proof state:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
⊢ Function.Surjective ⇑(trace K L)

Tactic:
rw [← LinearMap.range_eq_top]

Result:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
⊢ range (trace K L) = ⊤

Proof state:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
⊢ ¬range (trace K L) = ⊥

Tactic:
rw [LinearMap.range_eq_bot]

Result:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
⊢ ¬trace K L = 0
-- Mathlib/Control/Bitraversable/Lemmas.lean
theorem tfst_tsnd {α₀ α₁ β₀ β₁} (f : α₀ → F α₁) (f' : β₀ → G β₁) (x : t α₀ β₀) :
    Comp.mk (tfst f <$> tsnd f' x)
      = bitraverse (Comp.mk ∘ pure ∘ f) (Comp.mk ∘ map pure ∘ f') x

Proof state:
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
⊢ Comp.mk (tfst f <$> tsnd f' x) = bitraverse (Comp.mk ∘ pure ∘ f) (Comp.mk ∘ map pure ∘ f') x

Tactic:
rw [← comp_bitraverse]

Result:
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
⊢ bitraverse (Comp.mk ∘ map f ∘ pure) (Comp.mk ∘ map pure ∘ f') x =
    bitraverse (Comp.mk ∘ pure ∘ f) (Comp.mk ∘ map pure ∘ f') x

Proof state:
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
⊢ bitraverse (Comp.mk ∘ map f ∘ pure) (Comp.mk ∘ map pure ∘ f') x =
    bitraverse (Comp.mk ∘ pure ∘ f) (Comp.mk ∘ map pure ∘ f') x

Tactic:
simp only [Function.comp_def, map_pure]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem mem_factorSet_top {p : Associates α} {hp : Irreducible p} : p ∈ (⊤ : FactorSet α)

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : Associates α
hp : Irreducible p
⊢ BfactorSetMem ⟨p, hp⟩ ⊤

Tactic:
exact trivial

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : Associates α
hp : Irreducible p
⊢ if hp : Irreducible p then BfactorSetMem ⟨p, hp⟩ ⊤ else False

Tactic:
split_ifs

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : Associates α
hp : Irreducible p
⊢ BfactorSetMem ⟨p, hp⟩ ⊤

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : Associates α
hp : Irreducible p
⊢ FactorSetMem ⊤ p

Tactic:
dsimp only [FactorSetMem]

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : Associates α
hp : Irreducible p
⊢ if hp : Irreducible p then BfactorSetMem ⟨p, hp⟩ ⊤ else False

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : Associates α
hp : Irreducible p
⊢ p ∈ ⊤

Tactic:
dsimp only [Membership.mem]

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : Associates α
hp : Irreducible p
⊢ FactorSetMem ⊤ p
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem factorThru_eq_zero [HasZeroMorphisms C] {X Y : C} {P : Subobject Y} {f : X ⟶ Y}
    {h : Factors P f} : P.factorThru f h = 0 ↔ f = 0

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
h : P.Factors 0
⊢ P.factorThru 0 h = 0

Tactic:
ext

Result:
case mpr.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
h : P.Factors 0
⊢ P.factorThru 0 h ≫ P.arrow = 0 ≫ P.arrow

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : P.Factors f
w : P.factorThru f h = 0
⊢ f = 0

Tactic:
replace w := w =≫ P.arrow

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : P.Factors f
w : P.factorThru f h ≫ P.arrow = 0 ≫ P.arrow
⊢ f = 0

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : P.Factors f
⊢ P.factorThru f h = 0 ↔ f = 0

Tactic:
fconstructor

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : P.Factors f
⊢ P.factorThru f h = 0 → f = 0

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : P.Factors f
⊢ f = 0 → P.factorThru f h = 0

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : P.Factors f
⊢ P.factorThru f h = 0 → f = 0

Tactic:
intro w

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : P.Factors f
w : P.factorThru f h = 0
⊢ f = 0

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : P.Factors f
w : P.factorThru f h ≫ P.arrow = 0 ≫ P.arrow
⊢ f = 0

Tactic:
simpa using w

Result:
no goals

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : P.Factors f
⊢ f = 0 → P.factorThru f h = 0

Tactic:
rintro rfl

Result:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
h : P.Factors 0
⊢ P.factorThru 0 h = 0

Proof state:
case mpr.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
h : P.Factors 0
⊢ P.factorThru 0 h ≫ P.arrow = 0 ≫ P.arrow

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive (attr := simp)]
lemma stabilizer_subgroup (s : Subgroup G) : stabilizer G (s : Set G) = s

Proof state:
G : Type u_1
inst✝ : Group G
s : Subgroup G
⊢ stabilizer G ↑s = s

Tactic:
simp_rw [SetLike.ext_iff, mem_stabilizer_set]

Result:
G : Type u_1
inst✝ : Group G
s : Subgroup G
⊢ ∀ (x : G), (∀ (b : G), x • b ∈ ↑s ↔ b ∈ ↑s) ↔ x ∈ s

Proof state:
G : Type u_1
inst✝ : Group G
s : Subgroup G
a : G
h : ∀ (b : G), a • b ∈ ↑s ↔ b ∈ ↑s
⊢ a ∈ s

Tactic:
simpa only [smul_eq_mul, SetLike.mem_coe, mul_one] using (h 1).2 s.one_mem

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
s : Subgroup G
⊢ ∀ (x : G), (∀ (b : G), x • b ∈ ↑s ↔ b ∈ ↑s) ↔ x ∈ s

Tactic:
refine fun a ↦ ⟨fun h ↦ ?_, fun ha b ↦ s.mul_mem_cancel_left ha⟩

Result:
G : Type u_1
inst✝ : Group G
s : Subgroup G
a : G
h : ∀ (b : G), a • b ∈ ↑s ↔ b ∈ ↑s
⊢ a ∈ s
-- Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean
theorem associator_hom_fst (X Y Z : C) :
    (α_ X Y Z).hom ≫ prod.fst = prod.fst ≫ prod.fst

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y Z : C
⊢ (α_ X Y Z).hom ≫ prod.fst = prod.fst ≫ prod.fst

Tactic:
simp [associator_hom]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Induced.lean
@[simp]
lemma zero_inv_app_obj (X : C) :
    (zero F s i).inv.app (F.obj X) =
      F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X

Proof state:
C : Type u_4
D : Type u_2
inst✝⁵ : Category.{u_3, u_4} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
X : C
h :
  whiskerLeft F (zero F s i).inv =
    (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).inv
⊢ (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).inv.app X =
    F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_4
D : Type u_2
inst✝⁵ : Category.{u_3, u_4} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
X : C
⊢ (zero F s i).inv.app (F.obj X) = F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X

Tactic:
have h : whiskerLeft F (zero F s i).inv = _ :=
  ((whiskeringLeft C D D).obj F).map_preimage _

Result:
C : Type u_4
D : Type u_2
inst✝⁵ : Category.{u_3, u_4} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
X : C
h :
  whiskerLeft F (zero F s i).inv =
    (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).inv
⊢ (zero F s i).inv.app (F.obj X) = F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X

Proof state:
C : Type u_4
D : Type u_2
inst✝⁵ : Category.{u_3, u_4} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
X : C
h :
  whiskerLeft F (zero F s i).inv =
    (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).inv
⊢ (zero F s i).inv.app (F.obj X) = F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X

Tactic:
exact (NatTrans.congr_app h X).trans (by simp)

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem le_iff_uniformContinuous_id {u v : UniformSpace α} :
    u ≤ v ↔ @UniformContinuous _ _ u v id

Proof state:
α : Type ua
u v : UniformSpace α
⊢ u ≤ v ↔ UniformContinuous id

Tactic:
rw [uniformContinuous_iff, uniformSpace_comap_id, id]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem map_volume_mul_right {a : ℝ} (h : a ≠ 0) :
    Measure.map (· * a) volume = ENNReal.ofReal |a⁻¹| • volume

Proof state:
a : ℝ
h : a ≠ 0
⊢ Measure.map (fun x => x * a) volume = ofReal |a⁻¹| • volume

Tactic:
simpa only [mul_comm] using Real.map_volume_mul_left h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem not_append {x : BitVec w} {y : BitVec v} : ~~~ (x ++ y) = (~~~ x) ++ (~~~ y)

Proof state:
case pred
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
a✝ : i < w + v
⊢ (decide (i < w + v) && !if i < v then y.getLsbD i else x.getLsbD (i - v)) =
    if i < v then decide (i < v) && !y.getLsbD i else decide (i - v < w) && !x.getLsbD (i - v)

Tactic:
split

Result:
case pred.isTrue
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
a✝ : i < w + v
h✝ : i < v
⊢ (decide (i < w + v) && !y.getLsbD i) = (decide (i < v) && !y.getLsbD i)

case pred.isFalse
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
a✝ : i < w + v
h✝ : ¬i < v
⊢ (decide (i < w + v) && !x.getLsbD (i - v)) = (decide (i - v < w) && !x.getLsbD (i - v))

Proof state:
case pred
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
a✝ : i < w + v
⊢ (~~~(x ++ y)).getLsbD i = (~~~x ++ ~~~y).getLsbD i

Tactic:
simp only [getLsbD_not, getLsbD_append, cond_eq_if]

Result:
case pred
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
a✝ : i < w + v
⊢ (decide (i < w + v) && !if i < v then y.getLsbD i else x.getLsbD (i - v)) =
    if i < v then decide (i < v) && !y.getLsbD i else decide (i - v < w) && !x.getLsbD (i - v)

Proof state:
case pred.isFalse
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
a✝ : i < w + v
h✝ : ¬i < v
⊢ (decide (i < w + v) && !x.getLsbD (i - v)) = (decide (i - v < w) && !x.getLsbD (i - v))

Tactic:
simp_all

Result:
case pred.isFalse
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
a✝ : i < w + v
h✝ : v ≤ i
⊢ x.getLsbD (i - v) = false → i - v < w

Proof state:
w v : Nat
x : BitVec w
y : BitVec v
⊢ ~~~(x ++ y) = ~~~x ++ ~~~y

Tactic:
ext i

Result:
case pred
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
a✝ : i < w + v
⊢ (~~~(x ++ y)).getLsbD i = (~~~x ++ ~~~y).getLsbD i

Proof state:
case pred.isTrue
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
a✝ : i < w + v
h✝ : i < v
⊢ (decide (i < w + v) && !y.getLsbD i) = (decide (i < v) && !y.getLsbD i)

Tactic:
simp_all

Result:
no goals

Proof state:
case pred.isFalse
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
a✝ : i < w + v
h✝ : v ≤ i
⊢ x.getLsbD (i - v) = false → i - v < w

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem filter_attachWith {q : α → Prop} {l : List α} {p : {x // q x} → Bool} (H) :
    (l.attachWith q H).filter p =
      (l.attach.filter (fun ⟨x, h⟩ => p ⟨x, H _ h⟩)).map (fun ⟨x, h⟩ => ⟨x, H _ h⟩)

Proof state:
α : Type u_1
q : α → Prop
l : List α
p : { x // q x } → Bool
H : ∀ (x : α), x ∈ l → q x
⊢ filter p (l.attachWith q H) =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      (filter
        (fun x =>
          match x with
          | ⟨x, h⟩ => p ⟨x, ⋯⟩)
        l.attach)

Tactic:
induction l with
| nil => rfl
| cons x xs ih =>
  simp only [attachWith_cons, filter_cons]
  split <;> simp_all [Function.comp_def, filter_map]

Result:
no goals

Proof state:
case cons
α : Type u_1
q : α → Prop
p : { x // q x } → Bool
x : α
xs : List α
ih :
  ∀ (H : ∀ (x : α), x ∈ xs → q x),
    filter p (xs.attachWith q H) =
      map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        (filter
          (fun x =>
            match x with
            | ⟨x, h⟩ => p ⟨x, ⋯⟩)
          xs.attach)
H : ∀ (x_1 : α), x_1 ∈ x :: xs → q x_1
⊢ filter p ((x :: xs).attachWith q H) =
    map
      (fun x_1 =>
        match x_1 with
        | ⟨x_2, h⟩ => ⟨x_2, ⋯⟩)
      (filter
        (fun x_1 =>
          match x_1 with
          | ⟨x_2, h⟩ => p ⟨x_2, ⋯⟩)
        (x :: xs).attach)

Tactic:
simp only [attachWith_cons, filter_cons]

Result:
case cons
α : Type u_1
q : α → Prop
p : { x // q x } → Bool
x : α
xs : List α
ih :
  ∀ (H : ∀ (x : α), x ∈ xs → q x),
    filter p (xs.attachWith q H) =
      map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        (filter
          (fun x =>
            match x with
            | ⟨x, h⟩ => p ⟨x, ⋯⟩)
          xs.attach)
H : ∀ (x_1 : α), x_1 ∈ x :: xs → q x_1
⊢ (if p ⟨x, ⋯⟩ = true then ⟨x, ⋯⟩ :: filter p (xs.attachWith q ⋯) else filter p (xs.attachWith q ⋯)) =
    map (fun x_1 => ⟨x_1.val, ⋯⟩) (filter (fun x_1 => p ⟨x_1.val, ⋯⟩) (x :: xs).attach)

Proof state:
case cons
α : Type u_1
q : α → Prop
p : { x // q x } → Bool
x : α
xs : List α
ih :
  ∀ (H : ∀ (x : α), x ∈ xs → q x),
    filter p (xs.attachWith q H) =
      map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        (filter
          (fun x =>
            match x with
            | ⟨x, h⟩ => p ⟨x, ⋯⟩)
          xs.attach)
H : ∀ (x_1 : α), x_1 ∈ x :: xs → q x_1
⊢ (if p ⟨x, ⋯⟩ = true then ⟨x, ⋯⟩ :: filter p (xs.attachWith q ⋯) else filter p (xs.attachWith q ⋯)) =
    map (fun x_1 => ⟨x_1.val, ⋯⟩) (filter (fun x_1 => p ⟨x_1.val, ⋯⟩) (x :: xs).attach)

Tactic:
split <;> simp_all [Function.comp_def, filter_map]

Result:
no goals

Proof state:
case nil
α : Type u_1
q : α → Prop
p : { x // q x } → Bool
H : ∀ (x : α), x ∈ [] → q x
⊢ filter p ([].attachWith q H) =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      (filter
        (fun x =>
          match x with
          | ⟨x, h⟩ => p ⟨x, ⋯⟩)
        [].attach)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/MinMax.lean
theorem max_le_of_forall_le (l : List α) (a : α) (h : ∀ x ∈ l, x ≤ a) : l.foldr max ⊥ ≤ a

Proof state:
case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a y : α
l : List α
IH : (∀ (x : α), x ∈ l → x ≤ a) → foldr max ⊥ l ≤ a
h : ∀ (x : α), x ∈ y :: l → x ≤ a
⊢ foldr max ⊥ (y :: l) ≤ a

Tactic:
simpa [h y (mem_cons_self _ _)] using IH fun x hx => h x <| mem_cons_of_mem _ hx

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
a : α
h : ∀ (x : α), x ∈ l → x ≤ a
⊢ foldr max ⊥ l ≤ a

Tactic:
induction' l with y l IH

Result:
case nil
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a : α
h : ∀ (x : α), x ∈ [] → x ≤ a
⊢ foldr max ⊥ [] ≤ a

case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a y : α
l : List α
IH : (∀ (x : α), x ∈ l → x ≤ a) → foldr max ⊥ l ≤ a
h : ∀ (x : α), x ∈ y :: l → x ≤ a
⊢ foldr max ⊥ (y :: l) ≤ a

Proof state:
case nil
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a : α
h : ∀ (x : α), x ∈ [] → x ≤ a
⊢ foldr max ⊥ [] ≤ a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Permutation.lean
theorem permutations'Aux_eq_permutationsAux2 (t : α) (ts : List α) :
    permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).2

Proof state:
α : Type u_1
t : α
ts : List α
⊢ permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).2

Tactic:
induction' ts with a ts ih

Result:
case nil
α : Type u_1
t : α
⊢ permutations'Aux t [] = (permutationsAux2 t [] [[] ++ [t]] [] id).2

case cons
α : Type u_1
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).2
⊢ permutations'Aux t (a :: ts) = (permutationsAux2 t [] [a :: ts ++ [t]] (a :: ts) id).2

Proof state:
case cons
α : Type u_1
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).2
⊢ map (cons a) (permutationsAux2 t [] [ts ++ [t]] ts id).2 =
    (permutationsAux2 t [] [a :: (ts ++ [t])] ts fun x => a :: x).2

Tactic:
simp (config := { singlePass := true }) only [← permutationsAux2_append]

Result:
case cons
α : Type u_1
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).2
⊢ map (cons a) ((permutationsAux2 t [] [] ts id).2 ++ [ts ++ [t]]) =
    (permutationsAux2 t [] [] ts fun x => a :: x).2 ++ [a :: (ts ++ [t])]

Proof state:
case nil
α : Type u_1
t : α
⊢ permutations'Aux t [] = (permutationsAux2 t [] [[] ++ [t]] [] id).2

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).2
⊢ permutations'Aux t (a :: ts) = (permutationsAux2 t [] [a :: ts ++ [t]] (a :: ts) id).2

Tactic:
simp only [permutations'Aux, ih, cons_append, permutationsAux2_snd_cons, append_nil, id_eq,
  cons.injEq, true_and]

Result:
case cons
α : Type u_1
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).2
⊢ map (cons a) (permutationsAux2 t [] [ts ++ [t]] ts id).2 =
    (permutationsAux2 t [] [a :: (ts ++ [t])] ts fun x => a :: x).2

Proof state:
case cons
α : Type u_1
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).2
⊢ map (cons a) ((permutationsAux2 t [] [] ts id).2 ++ [ts ++ [t]]) =
    (permutationsAux2 t [] [] ts fun x => a :: x).2 ++ [a :: (ts ++ [t])]

Tactic:
simp [map_permutationsAux2]

Result:
no goals