harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean
@[reassoc]
lemma comp_homologySequenceδ :
    (F.shift n₀).map T.mor₂ ≫ F.homologySequenceδ T n₀ n₁ h = 0

Proof state:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_4, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (F.shift n₀).map T.mor₂ ≫ F.homologySequenceδ T n₀ n₁ h = 0

Tactic:
dsimp only [homologySequenceδ]

Result:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_4, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (F.shift n₀).map T.mor₂ ≫ F.shiftMap T.mor₃ n₀ n₁ ⋯ = 0

Proof state:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_4, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (F.shift n₀).map T.mor₂ ≫ F.shiftMap T.mor₃ n₀ n₁ ⋯ = 0

Tactic:
rw [← F.shiftMap_comp', comp_distTriang_mor_zero₂₃ _ hT, shiftMap_zero]

Result:
no goals
-- Mathlib/Geometry/Euclidean/PerpBisector.lean
theorem mem_perpBisector_iff_inner_pointReflection_vsub_eq_zero :
    c ∈ perpBisector p₁ p₂ ↔ ⟪Equiv.pointReflection c p₁ -ᵥ p₂, p₂ -ᵥ p₁⟫ = 0

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c p₁ p₂ : P
⊢ 2⁻¹ * inner (c -ᵥ p₁ + (c -ᵥ p₂)) (p₂ -ᵥ p₁) = 0 ↔ inner (c -ᵥ p₁ + (c -ᵥ p₂)) (p₂ -ᵥ p₁) = 0

Tactic:
simp

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c p₁ p₂ : P
⊢ c ∈ perpBisector p₁ p₂ ↔ inner ((Equiv.pointReflection c) p₁ -ᵥ p₂) (p₂ -ᵥ p₁) = 0

Tactic:
rw [mem_perpBisector_iff_inner_eq_zero, Equiv.pointReflection_apply,
  vsub_midpoint, invOf_eq_inv, ← smul_add, real_inner_smul_left, vadd_vsub_assoc]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c p₁ p₂ : P
⊢ 2⁻¹ * inner (c -ᵥ p₁ + (c -ᵥ p₂)) (p₂ -ᵥ p₁) = 0 ↔ inner (c -ᵥ p₁ + (c -ᵥ p₂)) (p₂ -ᵥ p₁) = 0
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean
theorem biprod.lift_mapBiprod (f : W ⟶ X) (g : W ⟶ Y) :
    biprod.lift (F.map f) (F.map g) ≫ (F.mapBiprod X Y).inv = F.map (biprod.lift f g)

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ lift (F.map f) (F.map g) ≫ (F.mapBiprod X Y).inv = F.map (lift f g)

Tactic:
rw [← biprod.map_lift_mapBiprod, Category.assoc, Iso.hom_inv_id, Category.comp_id]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycleOn.extendDomain {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p)
    (h : g.IsCycleOn s) : (g.extendDomain f).IsCycleOn ((↑) ∘ f '' s) :=
  ⟨h.1.extendDomain, by
    rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩
    exact (h.2 ha hb).extendDomain⟩

Proof state:
α : Type u_2
β : Type u_3
g : Perm α
s : Set α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
h : g.IsCycleOn s
⊢ ∀ ⦃x : β⦄, x ∈ Subtype.val ∘ ⇑f '' s → ∀ ⦃y : β⦄, y ∈ Subtype.val ∘ ⇑f '' s → (g.extendDomain f).SameCycle x y

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_2
β : Type u_3
g : Perm α
s : Set α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
h : g.IsCycleOn s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ (g.extendDomain f).SameCycle ((Subtype.val ∘ ⇑f) a) ((Subtype.val ∘ ⇑f) b)

Proof state:
case intro.intro.intro.intro
α : Type u_2
β : Type u_3
g : Perm α
s : Set α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
h : g.IsCycleOn s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ (g.extendDomain f).SameCycle ((Subtype.val ∘ ⇑f) a) ((Subtype.val ∘ ⇑f) b)

Tactic:
exact (h.2 ha hb).extendDomain

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurable_to_prop {f : α → Prop} (h : MeasurableSet (f ⁻¹' {True})) : Measurable f

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
⊢ MeasurableSet (f ⁻¹' {x})

Tactic:
by_cases hx : x

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
hx : x
⊢ MeasurableSet (f ⁻¹' {x})

case neg
α : Type u_1
inst✝ : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
hx : ¬x
⊢ MeasurableSet (f ⁻¹' {x})

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
⊢ Measurable f

Tactic:
refine measurable_to_countable' fun x => ?_

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
⊢ MeasurableSet (f ⁻¹' {x})

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
hx : x
⊢ MeasurableSet (f ⁻¹' {x})

Tactic:
simpa [hx] using h

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
hx : ¬x
⊢ MeasurableSet (f ⁻¹' {x})

Tactic:
simpa only [hx, ← preimage_compl, Prop.compl_singleton, not_true, preimage_singleton_false]
  using h.compl

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem range_coe : range (some : α → WithTop α) = Iio ⊤

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ range some = Iio ⊤

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝ : Preorder α
x : WithTop α
⊢ x ∈ range some ↔ x ∈ Iio ⊤

Proof state:
case h
α : Type u_1
inst✝ : Preorder α
x : WithTop α
⊢ x ∈ range some ↔ x ∈ Iio ⊤

Tactic:
rw [mem_Iio, WithTop.lt_top_iff_ne_top, mem_range, ne_top_iff_exists]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem le_mul_iff_one_le_right [MulOneClass α] [MulLeftMono α]
    {a b : α} (ha : MulLECancellable a) :
    a ≤ a * b ↔ 1 ≤ b :=
  Iff.trans (by rw [mul_one]) ha.mul_le_mul_iff_left

Proof state:
α : Type u_1
inst✝² : LE α
inst✝¹ : MulOneClass α
inst✝ : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ a ≤ a * b ↔ a * 1 ≤ a * b

Tactic:
rw [mul_one]

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem fromBlocks_one : fromBlocks (1 : Matrix l l α) 0 0 (1 : Matrix m m α) = 1

Proof state:
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
⊢ fromBlocks 1 0 0 1 = 1

Tactic:
ext i j

Result:
case a
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
i j : l ⊕ m
⊢ fromBlocks 1 0 0 1 i j = 1 i j

Proof state:
case a
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
i j : l ⊕ m
⊢ fromBlocks 1 0 0 1 i j = 1 i j

Tactic:
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [one_apply]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem two_zsmul_oangle_of_span_eq_of_span_eq {w x y z : V} (hwx : (ℝ ∙ w) = ℝ ∙ x)
    (hyz : (ℝ ∙ y) = ℝ ∙ z) : (2 : ℤ) • o.oangle w y = (2 : ℤ) • o.oangle x z

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
hwx : Submodule.span ℝ {w} = Submodule.span ℝ {x}
hyz : Submodule.span ℝ {y} = Submodule.span ℝ {z}
⊢ 2 • o.oangle w y = 2 • o.oangle x z

Tactic:
rw [o.two_zsmul_oangle_left_of_span_eq y hwx, o.two_zsmul_oangle_right_of_span_eq x hyz]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Prod.lean
@[simp] lemma fst_prod (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsMarkovKernel η] :
    fst (κ ×ₖ η) = κ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsMarkovKernel η
⊢ (κ ⊗ₖ (prodMkLeft β η).swapLeft).fst = κ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsMarkovKernel η
⊢ (κ ×ₖ η).fst = κ

Tactic:
rw [prod]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsMarkovKernel η
⊢ (κ ⊗ₖ (prodMkLeft β η).swapLeft).fst = κ
-- Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
theorem finite_approx_of_totallyBounded {s : Set α} (hs : TotallyBounded s) :
    ∀ ε > 0, ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ y ∈ t, ball y ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : TotallyBounded s
⊢ ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
intro ε ε_pos

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : TotallyBounded s
ε : ℝ
ε_pos : ε > 0
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : TotallyBounded s
ε : ℝ
ε_pos : ε > 0
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
rw [totallyBounded_iff_subset] at hs

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : ∀ d ∈ 𝓤 α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
ε : ℝ
ε_pos : ε > 0
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : ∀ d ∈ 𝓤 α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
ε : ℝ
ε_pos : ε > 0
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
exact hs _ (dist_mem_uniformity ε_pos)

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem LowerSet.iSup_Iic (s : Set α) : ⨆ a ∈ s, LowerSet.Iic a = lowerClosure s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ ⨆ a ∈ s, Iic a = lowerClosure s

Tactic:
ext

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
s : Set α
x✝ : α
⊢ x✝ ∈ ↑(⨆ a ∈ s, Iic a) ↔ x✝ ∈ ↑(lowerClosure s)

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
s : Set α
x✝ : α
⊢ x✝ ∈ ↑(⨆ a ∈ s, Iic a) ↔ x✝ ∈ ↑(lowerClosure s)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/QuadraticDiscriminant.lean
lemma discrim_le_zero_of_nonpos (h : ∀ x : K, a * (x * x) + b * x + c ≤ 0) : discrim a b c ≤ 0 :=
  discrim_neg a b c ▸ discrim_le_zero <| by simpa only [neg_mul, ← neg_add, neg_nonneg]

Proof state:
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), a * (x * x) + b * x + c ≤ 0
⊢ ∀ (x : K), 0 ≤ -a * (x * x) + -b * x + -c

Tactic:
simpa only [neg_mul, ← neg_add, neg_nonneg]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem rightDistributor_inv_comp_biproduct_π {J : Type} [Fintype J] (f : J → C) (X : C) (j : J) :
    (rightDistributor f X).inv ≫ (biproduct.π _ j ▷ X) = biproduct.π _ j

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j : J
⊢ (rightDistributor f X).inv ≫ biproduct.π f j ▷ X = biproduct.π (fun j => f j ⊗ X) j

Tactic:
simp [rightDistributor_inv, Preadditive.sum_comp, ← MonoidalCategory.comp_whiskerRight,
  biproduct.ι_π, dite_whiskerRight, comp_dite]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j : J
⊢ (rightDistributor f X).inv ≫ biproduct.π f j ▷ X = biproduct.π (fun j => f j ⊗ X) j

Tactic:
classical
simp [rightDistributor_inv, Preadditive.sum_comp, ← MonoidalCategory.comp_whiskerRight,
  biproduct.ι_π, dite_whiskerRight, comp_dite]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem validFor : ∀ {it}, Valid it → ∃ l r, ValidFor l r it
  | ⟨⟨_⟩, ⟨_⟩⟩, ⟨l, r, rfl, rfl⟩ =>
    ⟨l.reverse, r, by simpa [List.reverseAux_eq] using @ValidFor.mk l.reverse r⟩

Proof state:
l r : List Char
⊢ ValidFor l.reverse r { s := { data := l ++ r }, i := { byteIdx := utf8ByteSize.go l } }

Tactic:
simpa [List.reverseAux_eq] using @ValidFor.mk l.reverse r

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
lemma dist_le_pi_dist (f g : ∀ b, π b) (b : β) : dist (f b) (g b) ≤ dist f g

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
b : β
⊢ dist (f b) (g b) ≤ dist f g

Tactic:
simp only [dist_nndist, NNReal.coe_le_coe, nndist_le_pi_nndist f g b]

Result:
no goals
-- Mathlib/Topology/FiberBundle/Basic.lean
theorem localTrivAt_apply (p : Z.TotalSpace) : (Z.localTrivAt p.1) p = ⟨p.1, p.2⟩

Proof state:
case a
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
p : Z.TotalSpace
⊢ p.proj ∈ Z.baseSet (Z.indexAt p.proj)

Tactic:
exact Z.mem_baseSet_at p.1

Result:
no goals

Proof state:
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
p : Z.TotalSpace
⊢ ↑(Z.localTrivAt p.proj) p = (p.proj, p.snd)

Tactic:
rw [localTrivAt, localTriv_apply, coordChange_self]

Result:
case a
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
p : Z.TotalSpace
⊢ p.proj ∈ Z.baseSet (Z.indexAt p.proj)
-- Mathlib/SetTheory/Lists.lean
theorem of_toList : ∀ {l : Lists α}, IsList l → ofList (toList l) = l
  | ⟨true, l⟩, _ => by simp_all [ofList, of']

Proof state:
α : Type u_1
l : Lists' α true
x✝ : IsList ⟨true, l⟩
⊢ ofList (toList ⟨true, l⟩) = ⟨true, l⟩

Tactic:
simp_all [ofList, of']

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_permute (σ : Perm n) (M : Matrix n n R) :
    (M.submatrix σ id).det = Perm.sign σ * M.det :=
  ((detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_perm M σ).trans (by simp [Units.smul_def])

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
σ : Perm n
M : Matrix n n R
⊢ sign σ • detRowAlternating M = ↑↑(sign σ) * M.det

Tactic:
simp [Units.smul_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem keys_perm_keys_toListModel {m : Raw α β} :
    Perm m.keys (List.keys (toListModel m.buckets))

Proof state:
α : Type u
β : α → Type v
m : Raw α β
⊢ m.keys ~ List.keys (toListModel m.buckets)

Tactic:
simp [Raw.keys, foldRev_cons_key, keys_eq_map]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Tower.lean
theorem restrictScalars_top : restrictScalars R (⊤ : Subalgebra S A) = ⊤ :=
  SetLike.coe_injective <| by dsimp

Proof state:
R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
⊢ ↑(restrictScalars R ⊤) = ↑⊤

Tactic:
dsimp

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem all_balanceL {P l x r} (hl : Balanced l) (hr : Balanced r) (sl : Sized l) (sr : Sized r)
    (H :
      (∃ l', Raised l' (size l) ∧ BalancedSz l' (size r)) ∨
        ∃ r', Raised (size r) r' ∧ BalancedSz (size l) r') :
    All P (@balanceL α l x r) ↔ All P l ∧ P x ∧ All P r

Proof state:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ All P (l.balanceL x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
rw [balanceL_eq_balance' hl hr sl sr H, all_balance']

Result:
no goals
-- Mathlib/Geometry/Euclidean/Inversion/ImageHyperplane.lean
theorem inversion_mem_perpBisector_inversion_iff' (hR : R ≠ 0) (hy : y ≠ c) :
    inversion c R x ∈ perpBisector c (inversion c R y) ↔ dist x y = dist y c ∧ x ≠ c

Proof state:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ x
⊢ inversion x R x ∈ perpBisector x (inversion x R y) ↔ dist x y = dist y x ∧ x ≠ x

Tactic:
simp [*]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R x ∈ perpBisector c (inversion c R y) ↔ dist x y = dist y c ∧ x ≠ c

Tactic:
rcases eq_or_ne x c with rfl | hx

Result:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ x
⊢ inversion x R x ∈ perpBisector x (inversion x R y) ↔ dist x y = dist y x ∧ x ≠ x

case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
hx : x ≠ c
⊢ inversion c R x ∈ perpBisector c (inversion c R y) ↔ dist x y = dist y c ∧ x ≠ c

Proof state:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
hx : x ≠ c
⊢ inversion c R x ∈ perpBisector c (inversion c R y) ↔ dist x y = dist y c ∧ x ≠ c

Tactic:
simp [inversion_mem_perpBisector_inversion_iff hR hx hy, hx]

Result:
no goals
-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem uniqueDiffOn_Ico (a b : ℝ) : UniqueDiffOn ℝ (Ico a b) :=
  if hab : a < b then
    uniqueDiffOn_convex (convex_Ico a b) <| by simp only [interior_Ico, nonempty_Ioo, hab]
  else by simp only [Ico_eq_empty hab, uniqueDiffOn_empty]

Proof state:
a b : ℝ
hab : ¬a < b
⊢ UniqueDiffOn ℝ (Ico a b)

Tactic:
simp only [Ico_eq_empty hab, uniqueDiffOn_empty]

Result:
no goals

Proof state:
a b : ℝ
hab : a < b
⊢ (interior (Ico a b)).Nonempty

Tactic:
simp only [interior_Ico, nonempty_Ioo, hab]

Result:
no goals
-- Mathlib/Algebra/Lie/InvariantForm.lean
lemma orthogonal_isCompl (I : LieIdeal K L) (hI : IsAtom I) :
    IsCompl I (orthogonal Φ hΦ_inv I)

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ IsCompl I (orthogonal Φ hΦ_inv I)

Tactic:
rw [LieSubmodule.isCompl_iff_toSubmodule]

Result:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ IsCompl ↑I ↑(orthogonal Φ hΦ_inv I)

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ IsCompl ↑I ↑(orthogonal Φ hΦ_inv I)

Tactic:
exact orthogonal_isCompl_toSubmodule Φ hΦ_nondeg hΦ_inv hΦ_refl hL I hI

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Calculus.lean
theorem HasFDerivWithinAt.inner (hf : HasFDerivWithinAt f f' s x)
    (hg : HasFDerivWithinAt g g' s x) :
    HasFDerivWithinAt (fun t => ⟪f t, g t⟫) ((fderivInnerCLM 𝕜 (f x, g x)).comp <| f'.prod g') s
      x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt g g' s x
⊢ HasFDerivWithinAt (fun t => Inner.inner (f t) (g t)) ((fderivInnerCLM 𝕜 (f x, g x)).comp (f'.prod g')) s x

Tactic:
exact isBoundedBilinearMap_inner (𝕜 := 𝕜) (E := E)
  |>.hasFDerivAt (f x, g x) |>.comp_hasFDerivWithinAt x (hf.prod hg)

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Permanent.lean
theorem permanent_zero [Nonempty n] : permanent (0 : Matrix n n R) = 0

Proof state:
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nonempty n
⊢ permanent 0 = 0

Tactic:
simp [permanent]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Lemmas.lean
theorem getElem_insertIdx_eq (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) :
    (as.insertIdx i v)[i]'(by simp; omega) = v

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
⊢ (as.insertIdx i v h)[i] = v

Tactic:
simp [getElem_insertIdx, h]

Result:
no goals

Proof state:
α : Type ?u.131244
as : Array α
i : Nat
h : i ≤ as.size
v : α
⊢ i < (as.insertIdx i v h).size

Tactic:
simp

Result:
α : Type ?u.131244
as : Array α
i : Nat
h : i ≤ as.size
v : α
⊢ i < as.size + 1

Proof state:
α : Type ?u.131244
as : Array α
i : Nat
h : i ≤ as.size
v : α
⊢ i < as.size + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rtakeWhile_suffix : l.rtakeWhile p <:+ l

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p l <:+ l

Tactic:
rw [← reverse_prefix, rtakeWhile, reverse_reverse]

Result:
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l.reverse <+: l.reverse

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l.reverse <+: l.reverse

Tactic:
exact takeWhile_prefix _

Result:
no goals