harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Kleene.lean
theorem kstar_eq_one : a∗ = 1 ↔ a ≤ 1 :=
  ⟨le_kstar.trans_eq,
    fun h ↦ one_le_kstar.antisymm' <| kstar_le_of_mul_le_left le_rfl <| by rwa [one_mul]⟩

Proof state:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : a ≤ 1
⊢ 1 * a ≤ 1

Tactic:
rwa [one_mul]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem bind_ret (f : α → β) : ∀ s, bind s (ret ∘ f) = map f s
  | ⟨a, s⟩ => by
    dsimp [bind, map]
    -- Porting note: Was `rw [map_comp]; simp [Function.comp, ret]`
    rw [map_comp, ret]
    simp

Proof state:
α : Type u
β : Type v
f : α → β
a : α
s : Seq α
⊢ bind (a, s) (ret ∘ f) = map f (a, s)

Tactic:
dsimp [bind, map]

Result:
α : Type u
β : Type v
f : α → β
a : α
s : Seq α
⊢ join (ret (f a), Seq.map (ret ∘ f) s) = (f a, Seq.map f s)

Proof state:
α : Type u
β : Type v
f : α → β
a : α
s : Seq α
⊢ join (ret (f a), Seq.map (ret ∘ f) s) = (f a, Seq.map f s)

Tactic:
rw [map_comp, ret]

Result:
α : Type u
β : Type v
f : α → β
a : α
s : Seq α
⊢ join ((f a, nil), Seq.map ret (Seq.map f s)) = (f a, Seq.map f s)

Proof state:
α : Type u
β : Type v
f : α → β
a : α
s : Seq α
⊢ join ((f a, nil), Seq.map ret (Seq.map f s)) = (f a, Seq.map f s)

Tactic:
simp

Result:
no goals
-- Mathlib/Control/Monad/Cont.lean
theorem ExceptT.goto_mkLabel {α β ε : Type _} (x : Label (Except.{u, u} ε α) m β) (i : α) :
    goto (ExceptT.mkLabel x) i = ExceptT.mk (Except.ok <$> goto x (Except.ok i))

Proof state:
case mk
m : Type u → Type v
inst✝ : Monad m
α β ε : Type u
i : α
apply✝ : Except ε α → m β
⊢ goto (mkLabel { apply := apply✝ }) i = mk (Except.ok <$> goto { apply := apply✝ } (Except.ok i))

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u → Type v
inst✝ : Monad m
α β ε : Type u
x : Label (Except ε α) m β
i : α
⊢ goto (mkLabel x) i = mk (Except.ok <$> goto x (Except.ok i))

Tactic:
cases x

Result:
case mk
m : Type u → Type v
inst✝ : Monad m
α β ε : Type u
i : α
apply✝ : Except ε α → m β
⊢ goto (mkLabel { apply := apply✝ }) i = mk (Except.ok <$> goto { apply := apply✝ } (Except.ok i))
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma inr_mem_Icc_iff_norm_le {x : A} :
    (x : A⁺¹) ∈ Icc 0 1 ↔ 0 ≤ x ∧ ‖x‖ ≤ 1

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
⊢ 0 ≤ x → (↑x ≤ 1 ↔ ‖x‖ ≤ 1)

Tactic:
rw [← norm_inr (𝕜 := ℂ), ← inr_nonneg_iff, iff_comm]

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
⊢ 0 ≤ ↑x → (‖↑x‖ ≤ 1 ↔ ↑x ≤ 1)

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
⊢ ↑x ∈ Icc 0 1 ↔ 0 ≤ x ∧ ‖x‖ ≤ 1

Tactic:
simp only [mem_Icc, inr_nonneg_iff, and_congr_right_iff]

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
⊢ 0 ≤ x → (↑x ≤ 1 ↔ ‖x‖ ≤ 1)
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem mem_smul_span {s : Set M} {x : M} :
    x ∈ I • Submodule.span R s ↔ x ∈ Submodule.span R (⋃ (a ∈ I) (b ∈ s), ({a • b} : Set M))

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
s : Set M
x : M
⊢ x ∈ I • span R s ↔ x ∈ span R (⋃ a ∈ I, ⋃ b ∈ s, {a • b})

Tactic:
rw [← I.span_eq, Submodule.span_smul_span, I.span_eq]

Result:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
s : Set M
x : M
⊢ x ∈ span R (⋃ s_1 ∈ ↑I, ⋃ t ∈ s, {s_1 • t}) ↔ x ∈ span R (⋃ a ∈ I, ⋃ b ∈ s, {a • b})

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
s : Set M
x : M
⊢ x ∈ span R (⋃ s_1 ∈ ↑I, ⋃ t ∈ s, {s_1 • t}) ↔ x ∈ span R (⋃ a ∈ I, ⋃ b ∈ s, {a • b})

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem ciSup_mono {f g : ι → α} (B : BddAbove (range g)) (H : ∀ x, f x ≤ g x) :
    iSup f ≤ iSup g

Proof state:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : IsEmpty ι
⊢ iSup f ≤ iSup g

Tactic:
rw [iSup_of_empty', iSup_of_empty']

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
⊢ iSup f ≤ iSup g

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : IsEmpty ι
⊢ iSup f ≤ iSup g

case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : Nonempty ι
⊢ iSup f ≤ iSup g

Proof state:
case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : Nonempty ι
⊢ iSup f ≤ iSup g

Tactic:
exact ciSup_le fun x => le_ciSup_of_le B x (H x)

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma le_of_forall_lt_iff_le : (∀ z : α, x < z → y ≤ z) ↔ y ≤ x

Proof state:
α : Type u_1
inst✝² : LinearOrder α
x y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), x < ↑z → y ≤ ↑z) ↔ y ≤ x

Tactic:
cases x <;> cases y <;> simp [exists_lt, forall_gt_imp_ge_iff_le_of_dense]

Result:
no goals
-- Mathlib/Order/Hom/Set.lean
/-- Two order embeddings on a well-order are equal provided that their ranges are equal. -/
lemma OrderEmbedding.range_inj [LinearOrder α] [WellFoundedLT α] [Preorder β] {f g : α ↪o β} :
    Set.range f = Set.range g ↔ f = g

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ↪o β
⊢ range ⇑f = range ⇑g ↔ f = g

Tactic:
rw [f.strictMono.range_inj g.strictMono, DFunLike.coe_fn_eq]

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma comap_isBasis'_iff {I X : Set α} :
    (N.comap f).IsBasis' I X ↔ N.IsBasis' (f '' I) (f '' X) ∧ I.InjOn f ∧ I ⊆ X

Proof state:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
⊢ (N.comap f).IsBasis' I X ↔ N.IsBasis' (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X

Tactic:
simp only [isBasis'_iff_isBasis_inter_ground, comap_ground_eq, comap_isBasis_iff,
  image_inter_preimage, subset_inter_iff, ← and_assoc, and_congr_left_iff, and_iff_left_iff_imp,
  and_imp]

Result:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
⊢ N.IsBasis (f '' I) (f '' X ∩ N.E) → InjOn f I → I ⊆ X → I ⊆ f ⁻¹' N.E

Proof state:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
⊢ N.IsBasis (f '' I) (f '' X ∩ N.E) → InjOn f I → I ⊆ X → I ⊆ f ⁻¹' N.E

Tactic:
exact fun h _ _ ↦ (image_subset_iff.1 h.indep.subset_ground)

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem braiding_leftUnitor (X : C) : (β_ X (𝟙_ C)).hom ≫ (λ_ X).hom = (ρ_ X).hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ X (𝟙_ C)).hom ≫ (λ_ X).hom = (ρ_ X).hom

Tactic:
rw [← whiskerRight_iff, comp_whiskerRight, braiding_leftUnitor_aux₂]

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
theorem inter_eq_zero_iff_disjoint [DecidableEq α] {s t : Multiset α} :
    s ∩ t = 0 ↔ Disjoint s t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t ⊆ 0 ↔ _root_.Disjoint s t

Tactic:
simp [subset_iff, disjoint_left]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t = 0 ↔ _root_.Disjoint s t

Tactic:
rw [← subset_zero]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t ⊆ 0 ↔ _root_.Disjoint s t
-- Mathlib/Data/Nat/Digits.lean
theorem digits_add_two_add_one (b n : ℕ) :
    digits (b + 2) (n + 1) = ((n + 1) % (b + 2)) :: digits (b + 2) ((n + 1) / (b + 2))

Proof state:
b n : ℕ
⊢ (b + 2).digits (n + 1) = (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))

Tactic:
simp [digits, digitsAux_def]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sdiff_idem : (a \ b) \ b = a \ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a \ b) \ b = a \ b

Tactic:
rw [sdiff_sdiff_left, sup_idem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_alterKey {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} :
    (alterKey k f l).length =
      if h : containsKey k l then
        if f (some (getValue k l h)) |>.isSome then l.length else l.length - 1
      else
        if f none |>.isSome then l.length + 1 else l.length

Proof state:
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
⊢ (match f (getValue? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l).length =
    if h : containsKey k l = true then if (f (some (getValue k l h))).isSome = true then l.length else l.length - 1
    else if (f none).isSome = true then l.length + 1 else l.length

Tactic:
cases h : getValue? k l <;> split <;> simp_all [length_eraseKey, length_insertEntry,
  containsKey_eq_isSome_getValue?, ← getValue?_eq_some_getValue, -getValue?_eq_none]

Result:
no goals

Proof state:
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
⊢ (alterKey k f l).length =
    if h : containsKey k l = true then if (f (some (getValue k l h))).isSome = true then l.length else l.length - 1
    else if (f none).isSome = true then l.length + 1 else l.length

Tactic:
rw [alterKey]

Result:
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
⊢ (match f (getValue? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l).length =
    if h : containsKey k l = true then if (f (some (getValue k l h))).isSome = true then l.length else l.length - 1
    else if (f none).isSome = true then l.length + 1 else l.length
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
@[to_additive (attr := simp) existing cast_addConst_mul_card]
lemma cast_mulConst_mul_card (A B : Finset G) : (σₘ[A, B] * #A : 𝕜) = #(A * B)

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ σₘ[A, B] * ↑(#A) = ↑(#(A * B))

Tactic:
exact mulConst_mul_card _ _

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑σₘ[A, B] * ↑(#A) = ↑(#(A * B))

Tactic:
norm_cast

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ σₘ[A, B] * ↑(#A) = ↑(#(A * B))
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_nonneg_iff : 0 ≤ a / b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

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

Tactic:
simp [division_def, mul_nonneg_iff]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem veblen_zero : veblen 0 = fun a ↦ ω ^ a

Proof state:
⊢ veblen 0 = fun a => ω ^ a

Tactic:
rw [veblen, veblenWith_zero]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_add_of_le {n : ℕ} [NeZero n] {a b : ZMod n} (h : n ≤ a.val + b.val) :
    (a + b).val = a.val + b.val - n

Proof state:
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ (a + b).val = (a + b).val + n - n

Tactic:
exact eq_tsub_of_add_eq rfl

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ (a + b).val = a.val + b.val - n

Tactic:
rw [val_add_val_of_le h]

Result:
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ (a + b).val = (a + b).val + n - n
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem contractRight_mul_algebraMap (a : CliffordAlgebra Q) (r : R) :
    a * algebraMap _ _ r⌊d = a⌊d * algebraMap _ _ r

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
a : CliffordAlgebra Q
r : R
⊢ (contractRight (a * (algebraMap R (CliffordAlgebra Q)) r)) d =
    (contractRight a) d * (algebraMap R (CliffordAlgebra Q)) r

Tactic:
rw [← Algebra.commutes, contractRight_algebraMap_mul, Algebra.commutes]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem le_sum_card_inter (h : ∀ a ∈ s, n ≤ #{b ∈ B | a ∈ b}) : #s * n ≤ ∑ t ∈ B, #(s ∩ t)

Proof state:
α : Type u_2
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, n ≤ #(filter (fun b => a ∈ b) B)
⊢ (∑ x ∈ s, ∑ a ∈ B, if x ∈ a then 1 else 0) ≤ ∑ x ∈ B, ∑ a ∈ s, if a ∈ x then 1 else 0

Tactic:
exact sum_comm.le

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, n ≤ #(filter (fun b => a ∈ b) B)
⊢ #s * n ≤ ∑ t ∈ B, #(s ∩ t)

Tactic:
apply (s.card_nsmul_le_sum _ _ h).trans

Result:
α : Type u_2
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, n ≤ #(filter (fun b => a ∈ b) B)
⊢ ∑ x ∈ s, #(filter (fun b => x ∈ b) B) ≤ ∑ t ∈ B, #(s ∩ t)

Proof state:
α : Type u_2
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, n ≤ #(filter (fun b => a ∈ b) B)
⊢ ∑ x ∈ s, #(filter (fun b => x ∈ b) B) ≤ ∑ t ∈ B, #(s ∩ t)

Tactic:
simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]

Result:
α : Type u_2
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, n ≤ #(filter (fun b => a ∈ b) B)
⊢ (∑ x ∈ s, ∑ a ∈ B, if x ∈ a then 1 else 0) ≤ ∑ x ∈ B, ∑ a ∈ s, if a ∈ x then 1 else 0
-- Mathlib/Algebra/Lie/Submodule.lean
theorem isIdealMorphism_of_surjective (h : Function.Surjective f) : f.IsIdealMorphism

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : Function.Surjective ⇑f
⊢ f.IsIdealMorphism

Tactic:
rw [isIdealMorphism_def, f.idealRange_eq_top_of_surjective h, f.range_eq_top.mpr h,
  LieIdeal.top_toLieSubalgebra]

Result:
no goals
-- Mathlib/Algebra/Group/Invertible/Defs.lean
theorem mul_invOf_eq_iff_eq_mul_right : a * ⅟c = b ↔ a = b * c

Proof state:
α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ a * ⅟c = b ↔ a = b * c

Tactic:
rw [← mul_left_inj_of_invertible (c := c), invOf_mul_cancel_right]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem filter_ne [DecidableEq β] (s : Finset β) (b : β) :
    (s.filter fun a => b ≠ a) = s.erase b

Proof state:
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
⊢ filter (fun a => b ≠ a) s = s.erase b

Tactic:
ext

Result:
case h
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b a✝ : β
⊢ a✝ ∈ filter (fun a => b ≠ a) s ↔ a✝ ∈ s.erase b

Proof state:
case h
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b a✝ : β
⊢ a✝ ∈ s ∧ ¬b = a✝ ↔ ¬a✝ = b ∧ a✝ ∈ s

Tactic:
tauto

Result:
no goals

Proof state:
case h
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b a✝ : β
⊢ a✝ ∈ filter (fun a => b ≠ a) s ↔ a✝ ∈ s.erase b

Tactic:
simp only [mem_filter, mem_erase, Ne, decide_not, Bool.not_eq_true', decide_eq_false_iff_not]

Result:
case h
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b a✝ : β
⊢ a✝ ∈ s ∧ ¬b = a✝ ↔ ¬a✝ = b ∧ a✝ ∈ s
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem mk'_one (h : IsIntegral R (1 : B) := isIntegral_one) : mk' A 1 h = 1 :=
  algebraMap_injective A R B <| by rw [algebraMap_mk', RingHom.map_one]

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsIntegralClosure A R B
h : optParam (IsIntegral R 1) ⋯
⊢ (algebraMap A B) (mk' A 1 h) = (algebraMap A B) 1

Tactic:
rw [algebraMap_mk', RingHom.map_one]

Result:
no goals
-- Mathlib/Algebra/ZeroOne/Lemmas.lean
@[to_additive]
lemma dite_le_one [LE α] (ha : ∀ h, a h ≤ 1) (hb : ∀ h, b h ≤ 1) : dite p a b ≤ 1

Proof state:
case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LE α
ha : ∀ (h : p), a h ≤ 1
hb : ∀ (h : ¬p), b h ≤ 1
h✝ : p
⊢ a h✝ ≤ 1

case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LE α
ha : ∀ (h : p), a h ≤ 1
hb : ∀ (h : ¬p), b h ≤ 1
h✝ : ¬p
⊢ b h✝ ≤ 1

Tactic:
exacts [ha ‹_›, hb ‹_›]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LE α
ha : ∀ (h : p), a h ≤ 1
hb : ∀ (h : ¬p), b h ≤ 1
⊢ dite p a b ≤ 1

Tactic:
split

Result:
case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LE α
ha : ∀ (h : p), a h ≤ 1
hb : ∀ (h : ¬p), b h ≤ 1
h✝ : p
⊢ a h✝ ≤ 1

case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LE α
ha : ∀ (h : p), a h ≤ 1
hb : ∀ (h : ¬p), b h ≤ 1
h✝ : ¬p
⊢ b h✝ ≤ 1
-- Mathlib/CategoryTheory/NatIso.lean
@[reassoc (attr := simp)]
lemma inv_hom_id_app_app_app {F G : C ⥤ D ⥤ E ⥤ E'} (e : F ≅ G)
    (X₁ : C) (X₂ : D) (X₃ : E) :
    ((e.inv.app X₁).app X₂).app X₃ ≫ ((e.hom.app X₁).app X₂).app X₃ = 𝟙 _

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F G : C ⥤ D ⥤ E ⥤ E'
e : F ≅ G
X₁ : C
X₂ : D
X₃ : E
⊢ ((e.inv.app X₁).app X₂).app X₃ ≫ ((e.hom.app X₁).app X₂).app X₃ = 𝟙 (((G.obj X₁).obj X₂).obj X₃)

Tactic:
rw [← NatTrans.comp_app, ← NatTrans.comp_app, Iso.inv_hom_id_app,
  NatTrans.id_app, NatTrans.id_app]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma δ_ofHom_comp {n : ℤ} (f : F ⟶ G) (z : Cochain G K n) (m : ℤ) :
    δ n m ((Cochain.ofHom f).comp z (zero_add n)) =
      (Cochain.ofHom f).comp (δ n m z) (zero_add m)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n : ℤ
f : F ⟶ G
z : Cochain G K n
m : ℤ
⊢ δ n m ((Cochain.ofHom f).comp z ⋯) = (Cochain.ofHom f).comp (δ n m z) ⋯

Tactic:
rw [← Cocycle.ofHom_coe, δ_zero_cocycle_comp]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Over.lean
@[simp]
lemma overEquiv_symm_iff {X : C} {Y : Over X} (S : Sieve Y.left) {Z : Over X} (f : Z ⟶ Y) :
    (overEquiv Y).symm S f ↔ S f.left

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Sieve Y.left
Z : Over X
f : Z ⟶ Y
⊢ ((overEquiv Y).symm S).arrows f ↔ S.arrows f.left

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem OrderIso.map_sSup_eq_sSup_symm_preimage [CompleteLattice β] (f : α ≃o β) (s : Set α) :
    f (sSup s) = sSup (f.symm ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α ≃o β
s : Set α
⊢ f (sSup s) = sSup (⇑f.symm ⁻¹' s)

Tactic:
rw [map_sSup, ← sSup_image, f.image_eq_preimage]

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean
theorem congr_reverse_comp {X Y : Paths <| Quiver.Symmetrify V} (p : X ⟶ Y) :
    Quot.mk (@Quotient.CompClosure _ _ redStep _ _) (p.reverse ≫ p) =
      Quot.mk (@Quotient.CompClosure _ _ redStep _ _) (𝟙 Y)

Proof state:
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (Quotient.CompClosure redStep) (Quiver.Path.reverse p ≫ (Quiver.Path.reverse p).reverse) =
    Quot.mk (Quotient.CompClosure redStep) (𝟙 Y)

Tactic:
apply congr_comp_reverse

Result:
no goals

Proof state:
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (Quotient.CompClosure redStep) (Quiver.Path.reverse p ≫ p) = Quot.mk (Quotient.CompClosure redStep) (𝟙 Y)

Tactic:
nth_rw 2 [← Quiver.Path.reverse_reverse p]

Result:
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (Quotient.CompClosure redStep) (Quiver.Path.reverse p ≫ (Quiver.Path.reverse p).reverse) =
    Quot.mk (Quotient.CompClosure redStep) (𝟙 Y)
-- Mathlib/Algebra/Order/Monovary.lean
lemma monovaryOn_inv₀ (hf : ∀ i ∈ s, 0 < f i) (hg : ∀ i ∈ s, 0 < g i) :
    MonovaryOn f⁻¹ g⁻¹ s ↔ MonovaryOn f g s

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrderedSemifield α
inst✝ : LinearOrderedSemifield β
s : Set ι
f : ι → α
g : ι → β
hf : ∀ i ∈ s, 0 < f i
hg : ∀ i ∈ s, 0 < g i
⊢ MonovaryOn f⁻¹ g⁻¹ s ↔ MonovaryOn f g s

Tactic:
rw [monovaryOn_inv_left₀ hf, antivaryOn_inv_right₀ hg]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
lemma mem_image_support_coeff_finSuccEquiv {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {x} :
    x ∈ Finsupp.cons i '' ((finSuccEquiv R n f).coeff i).support ↔
      x ∈ f.support ∧ x 0 = i

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
x : Fin (n + 1) →₀ ℕ
⊢ x ∈ cons i '' ↑(((finSuccEquiv R n) f).coeff i).support ↔ x ∈ f.support ∧ x 0 = i

Tactic:
simpa using congr(x ∈ $image_support_finSuccEquiv)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldl_append {β : Type _} (f : β → α → β) (b) (l l' : List α) :
    (l ++ l').foldl f b = l'.foldl f (l.foldl f b)

Proof state:
α : Type u_1
β : Type u_2
f : β → α → β
b : β
l l' : List α
⊢ foldl f b (l ++ l') = foldl f (foldl f b l) l'

Tactic:
simp [foldl_eq_foldlM]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem sup_eq_right : a ⊔ b = b ↔ a ≤ b :=
  le_antisymm_iff.trans <| by simp [le_rfl]

Proof state:
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ⊔ b ≤ b ∧ b ≤ a ⊔ b ↔ a ≤ b

Tactic:
simp [le_rfl]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem le_log_iff_exp_le (hy : 0 < y) : x ≤ log y ↔ exp x ≤ y

Proof state:
x y : ℝ
hy : 0 < y
⊢ x ≤ log y ↔ rexp x ≤ y

Tactic:
rw [← exp_le_exp, exp_log hy]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mod_eq_sub_div_mul {x k : Nat} : x % k = x - (x / k) * k

Proof state:
x k : Nat
⊢ x % k = x - x / k * k

Tactic:
rw [mod_eq_sub_mul_div, Nat.mul_comm]

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma normEDS_one : normEDS b c d 1 = 1

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
⊢ normEDS b c d 1 = 1

Tactic:
erw [normEDS_ofNat, preNormEDS'_one, one_mul, if_neg Nat.not_even_one]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
@[simp] lemma closure_inter_ground (M : Matroid α) (X : Set α) :
    M.closure (X ∩ M.E) = M.closure X

Proof state:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.closure (X ∩ M.E) = M.closure X

Tactic:
simp_rw [closure_def, inter_assoc, inter_self]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem cpow_nat_inv_pow (x : ℂ) {n : ℕ} (hn : n ≠ 0) : (x ^ (n⁻¹ : ℂ)) ^ n = x

Proof state:
x : ℂ
n : ℕ
hn : n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x

Tactic:
rw [← cpow_nat_mul, mul_inv_cancel₀, cpow_one]

Result:
x : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

Proof state:
x : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
assumption_mod_cast

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem atLeastTwo_false_left  : atLeastTwo false b c = (b && c)

Proof state:
b c : Bool
⊢ false.atLeastTwo b c = (b && c)

Tactic:
simp [atLeastTwo]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Completion.lean
theorem extend_pureCauchy {f : α → β} (hf : UniformContinuous f) (a : α) :
    extend f (pureCauchy a) = f a

Proof state:
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
a : α
⊢ ⋯.extend f (pureCauchy a) = f a

Tactic:
exact uniformly_extend_of_ind isUniformInducing_pureCauchy denseRange_pureCauchy hf _

Result:
no goals

Proof state:
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
a : α
⊢ extend f (pureCauchy a) = f a

Tactic:
rw [extend, if_pos hf]

Result:
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
a : α
⊢ ⋯.extend f (pureCauchy a) = f a