harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem adc_spec (x y : BitVec w) (c : Bool) :
    adc x y c = (carry w x y c, x + y + setWidth w (ofBool c))

Proof state:
w : Nat
x y : BitVec w
c : Bool
⊢ carry 0 x y c = c

Tactic:
simp [carry, Nat.mod_one]

Result:
w : Nat
x y : BitVec w
c : Bool
⊢ decide (1 ≤ c.toNat) = c

Proof state:
w : Nat
x y : BitVec w
c : Bool
⊢ x.adc y c = (carry w x y c, x + y + setWidth w (ofBool c))

Tactic:
simp only [adc]

Result:
w : Nat
x y : BitVec w
c : Bool
⊢ iunfoldr (fun i c => adcb (x.getLsbD ↑i) (y.getLsbD ↑i) c) c = (carry w x y c, x + y + setWidth w (ofBool c))

Proof state:
w : Nat
x y : BitVec w
c : Bool
⊢ iunfoldr (fun i c => adcb (x.getLsbD ↑i) (y.getLsbD ↑i) c) c = (carry w x y c, x + y + setWidth w (ofBool c))

Tactic:
apply iunfoldr_replace
        (fun i => carry i x y c)
        (x + y + setWidth w (ofBool c))
        c

Result:
case init
w : Nat
x y : BitVec w
c : Bool
⊢ carry 0 x y c = c

case step
w : Nat
x y : BitVec w
c : Bool
⊢ ∀ (i : Fin w),
    adcb (x.getLsbD ↑i) (y.getLsbD ↑i) (carry (↑i) x y c) =
      (carry (↑i + 1) x y c, (x + y + setWidth w (ofBool c)).getLsbD ↑i)

Proof state:
w : Nat
x y : BitVec w
c : Bool
⊢ ∀ (i : Fin w),
    adcb (x.getLsbD ↑i) (y.getLsbD ↑i) (carry (↑i) x y c) =
      (carry (↑i + 1) x y c, (x + y + setWidth w (ofBool c)).getLsbD ↑i)

Tactic:
simp [adcb, Prod.mk.injEq, carry_succ, getLsbD_add_add_bool]

Result:
no goals

Proof state:
case step
w : Nat
x y : BitVec w
c : Bool
⊢ ∀ (i : Fin w),
    adcb (x.getLsbD ↑i) (y.getLsbD ↑i) (carry (↑i) x y c) =
      (carry (↑i + 1) x y c, (x + y + setWidth w (ofBool c)).getLsbD ↑i)

Tactic:
case step =>
  simp [adcb, Prod.mk.injEq, carry_succ, getLsbD_add_add_bool]

Result:
no goals

Proof state:
case init
w : Nat
x y : BitVec w
c : Bool
⊢ carry 0 x y c = c

case step
w : Nat
x y : BitVec w
c : Bool
⊢ ∀ (i : Fin w),
    adcb (x.getLsbD ↑i) (y.getLsbD ↑i) (carry (↑i) x y c) =
      (carry (↑i + 1) x y c, (x + y + setWidth w (ofBool c)).getLsbD ↑i)

Tactic:
case init =>
  simp [carry, Nat.mod_one]
  cases c <;> rfl

Result:
case step
w : Nat
x y : BitVec w
c : Bool
⊢ ∀ (i : Fin w),
    adcb (x.getLsbD ↑i) (y.getLsbD ↑i) (carry (↑i) x y c) =
      (carry (↑i + 1) x y c, (x + y + setWidth w (ofBool c)).getLsbD ↑i)

Proof state:
w : Nat
x y : BitVec w
c : Bool
⊢ decide (1 ≤ c.toNat) = c

Tactic:
cases c <;> rfl

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_eq_zero : ∀ {n : ℕ} (a : ZMod n), a.val = 0 ↔ a = 0
  | 0, _ => Int.natAbs_eq_zero
  | n + 1, a => by
    rw [Fin.ext_iff]
    exact Iff.rfl

Proof state:
n : ℕ
a : ZMod (n + 1)
⊢ a.val = 0 ↔ a = 0

Tactic:
rw [Fin.ext_iff]

Result:
n : ℕ
a : ZMod (n + 1)
⊢ a.val = 0 ↔ ↑a = ↑0

Proof state:
n : ℕ
a : ZMod (n + 1)
⊢ a.val = 0 ↔ ↑a = ↑0

Tactic:
exact Iff.rfl

Result:
no goals
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem lift_comp_inr : (lift fn fg h).comp inr = fg

Proof state:
case h
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
x✝ : G
⊢ ((lift fn fg h).comp inr) x✝ = fg x✝

Tactic:
simp

Result:
no goals

Proof state:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
⊢ (lift fn fg h).comp inr = fg

Tactic:
ext

Result:
case h
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
x✝ : G
⊢ ((lift fn fg h).comp inr) x✝ = fg x✝
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem image.ι_zero {X Y : C} [HasImage (0 : X ⟶ Y)] : image.ι (0 : X ⟶ Y) = 0

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X Y : C
inst✝ : HasImage 0
⊢ lift (monoFactorisationZero X Y) ≫ (monoFactorisationZero X Y).m = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X Y : C
inst✝ : HasImage 0
⊢ ι 0 = 0

Tactic:
rw [← image.lift_fac (monoFactorisationZero X Y)]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X Y : C
inst✝ : HasImage 0
⊢ lift (monoFactorisationZero X Y) ≫ (monoFactorisationZero X Y).m = 0
-- Mathlib/NumberTheory/LSeries/Injectivity.lean
lemma LSeries_eq_zero_of_abscissaOfAbsConv_eq_top {f : ℕ → ℂ} (h : abscissaOfAbsConv f = ⊤) :
    LSeries f = 0

Proof state:
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0

Tactic:
ext1 s

Result:
case h
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
s : ℂ
⊢ LSeries f s = 0 s

Proof state:
case h
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
s : ℂ
⊢ LSeries f s = 0 s

Tactic:
exact LSeries.eq_zero_of_not_LSeriesSummable f s <| mt LSeriesSummable.abscissaOfAbsConv_le <|
  h ▸ fun H ↦ (H.trans_lt <| EReal.coe_lt_top _).false

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem mul_left' (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD c * n]

Proof state:
case inr.inl
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ 0 * a ≡ 0 * b [ZMOD 0 * n]

Tactic:
simp only [Int.zero_mul, ModEq.rfl]

Result:
no goals

Proof state:
case inl
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ c * a ≡ c * b [ZMOD c * n]

Tactic:
rw [← neg_modEq_neg, ← modEq_neg, ← Int.neg_mul, ← Int.neg_mul, ← Int.neg_mul]

Result:
case inl
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ -c * a ≡ -c * b [ZMOD -c * n]

Proof state:
case inl
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ -c * a ≡ -c * b [ZMOD -c * n]

Tactic:
simp only [ModEq, mul_emod_mul_of_pos _ _ (neg_pos.2 hc), h.eq]

Result:
no goals

Proof state:
case inr.inr
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : 0 < c
⊢ c * a ≡ c * b [ZMOD c * n]

Tactic:
simp only [ModEq, mul_emod_mul_of_pos _ _ hc, h.eq]

Result:
no goals

Proof state:
n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ c * a ≡ c * b [ZMOD c * n]

Tactic:
obtain hc | rfl | hc := lt_trichotomy c 0

Result:
case inl
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ c * a ≡ c * b [ZMOD c * n]

case inr.inl
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ 0 * a ≡ 0 * b [ZMOD 0 * n]

case inr.inr
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : 0 < c
⊢ c * a ≡ c * b [ZMOD c * n]
-- Mathlib/Algebra/Homology/Embedding/Extend.lean
lemma d_eq {i j : Option ι} {a b : ι} (hi : i = some a) (hj : j = some b) :
    d K i j = (XIso K hi).hom ≫ K.d a b ≫ (XIso K hj).inv

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i j : Option ι
a b : ι
hi : i = some a
hj : j = some b
⊢ d K i j = (XIso K hi).hom ≫ K.d a b ≫ (XIso K hj).inv

Tactic:
subst hi hj

Result:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
a b : ι
⊢ d K (some a) (some b) = (XIso K ⋯).hom ≫ K.d a b ≫ (XIso K ⋯).inv

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
a b : ι
⊢ d K (some a) (some b) = (XIso K ⋯).hom ≫ K.d a b ≫ (XIso K ⋯).inv

Tactic:
dsimp [XIso, d]

Result:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
a b : ι
⊢ K.d a b = 𝟙 (X K (some a)) ≫ K.d a b ≫ 𝟙 (X K (some b))

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
a b : ι
⊢ K.d a b = 𝟙 (X K (some a)) ≫ K.d a b ≫ 𝟙 (X K (some b))

Tactic:
erw [id_comp, comp_id]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem offDiag_filter_lt_eq_filter_le {ι}
    [PartialOrder ι] [DecidableEq ι]
    [DecidableRel (LE.le (α := ι))] [DecidableRel (LT.lt (α := ι))]
    (s : Finset ι) :
    s.offDiag.filter (fun i => i.1 < i.2) = s.offDiag.filter (fun i => i.1 ≤ i.2)

Proof state:
ι : Type u_4
inst✝³ : PartialOrder ι
inst✝² : DecidableEq ι
inst✝¹ : DecidableRel LE.le
inst✝ : DecidableRel LT.lt
s : Finset ι
⊢ ∀ ⦃a : ι × ι⦄, a ∈ s.offDiag → (a.1 < a.2 ↔ a.1 ≤ a.2)

Tactic:
rintro ⟨i, j⟩

Result:
case mk
ι : Type u_4
inst✝³ : PartialOrder ι
inst✝² : DecidableEq ι
inst✝¹ : DecidableRel LE.le
inst✝ : DecidableRel LT.lt
s : Finset ι
i j : ι
⊢ (i, j) ∈ s.offDiag → ((i, j).1 < (i, j).2 ↔ (i, j).1 ≤ (i, j).2)

Proof state:
case mk
ι : Type u_4
inst✝³ : PartialOrder ι
inst✝² : DecidableEq ι
inst✝¹ : DecidableRel LE.le
inst✝ : DecidableRel LT.lt
s : Finset ι
i j : ι
⊢ i ∈ s → j ∈ s → i ≠ j → (i < j ↔ i ≤ j)

Tactic:
rintro _ _ h

Result:
case mk
ι : Type u_4
inst✝³ : PartialOrder ι
inst✝² : DecidableEq ι
inst✝¹ : DecidableRel LE.le
inst✝ : DecidableRel LT.lt
s : Finset ι
i j : ι
a✝¹ : i ∈ s
a✝ : j ∈ s
h : i ≠ j
⊢ i < j ↔ i ≤ j

Proof state:
case mk
ι : Type u_4
inst✝³ : PartialOrder ι
inst✝² : DecidableEq ι
inst✝¹ : DecidableRel LE.le
inst✝ : DecidableRel LT.lt
s : Finset ι
i j : ι
a✝¹ : i ∈ s
a✝ : j ∈ s
h : i ≠ j
⊢ i < j ↔ i ≤ j

Tactic:
rw [Ne.le_iff_lt h]

Result:
no goals

Proof state:
case mk
ι : Type u_4
inst✝³ : PartialOrder ι
inst✝² : DecidableEq ι
inst✝¹ : DecidableRel LE.le
inst✝ : DecidableRel LT.lt
s : Finset ι
i j : ι
⊢ (i, j) ∈ s.offDiag → ((i, j).1 < (i, j).2 ↔ (i, j).1 ≤ (i, j).2)

Tactic:
simp_rw [mem_offDiag, and_imp]

Result:
case mk
ι : Type u_4
inst✝³ : PartialOrder ι
inst✝² : DecidableEq ι
inst✝¹ : DecidableRel LE.le
inst✝ : DecidableRel LT.lt
s : Finset ι
i j : ι
⊢ i ∈ s → j ∈ s → i ≠ j → (i < j ↔ i ≤ j)

Proof state:
ι : Type u_4
inst✝³ : PartialOrder ι
inst✝² : DecidableEq ι
inst✝¹ : DecidableRel LE.le
inst✝ : DecidableRel LT.lt
s : Finset ι
⊢ filter (fun i => i.1 < i.2) s.offDiag = filter (fun i => i.1 ≤ i.2) s.offDiag

Tactic:
rw [Finset.filter_inj']

Result:
ι : Type u_4
inst✝³ : PartialOrder ι
inst✝² : DecidableEq ι
inst✝¹ : DecidableRel LE.le
inst✝ : DecidableRel LT.lt
s : Finset ι
⊢ ∀ ⦃a : ι × ι⦄, a ∈ s.offDiag → (a.1 < a.2 ↔ a.1 ≤ a.2)
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem ENNReal.tsum_geometric (r : ℝ≥0∞) : ∑' n : ℕ, r ^ n = (1 - r)⁻¹

Proof state:
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ⊤
n : ℕ
hn : a < ↑n
⊢ ↑n = ∑ i ∈ Finset.range n, 1

Tactic:
rw [sum_const, nsmul_one, card_range]

Result:
no goals

Proof state:
case inr
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∀ b < ⊤, ∃ i, b < ∑ a ∈ Finset.range i, r ^ a

Tactic:
refine fun a ha ↦
  (ENNReal.exists_nat_gt (lt_top_iff_ne_top.1 ha)).imp fun n hn ↦ lt_of_lt_of_le hn ?_

Result:
case inr
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ⊤
n : ℕ
hn : a < ↑n
⊢ ↑n ≤ ∑ a ∈ Finset.range n, r ^ a

Proof state:
r : ℝ≥0∞
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

Tactic:
rcases lt_or_le r 1 with hr | hr

Result:
case inl
r : ℝ≥0∞
hr : r < 1
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

case inr
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

Proof state:
case inr
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ⊤
n : ℕ
hn : a < ↑n
⊢ ↑n ≤ ∑ a ∈ Finset.range n, r ^ a

Tactic:
calc
  (n : ℝ≥0∞) = ∑ i ∈ range n, 1 := by rw [sum_const, nsmul_one, card_range]
  _ ≤ ∑ i ∈ range n, r ^ i := by gcongr; apply one_le_pow₀ hr

Result:
no goals

Proof state:
case inl.intro.intro
r : ℝ≥0
hr' hr : r < 1
⊢ ∑' (n : ℕ), ↑(r ^ n) = (↑(1 - r))⁻¹

Tactic:
convert ENNReal.tsum_coe_eq (NNReal.hasSum_geometric hr)

Result:
case h.e'_3
r : ℝ≥0
hr' hr : r < 1
⊢ (↑(1 - r))⁻¹ = ↑(1 - r)⁻¹

Proof state:
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ⊤
n : ℕ
hn : a < ↑n
⊢ ∑ i ∈ Finset.range n, 1 ≤ ∑ i ∈ Finset.range n, r ^ i

Tactic:
gcongr

Result:
case h
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ⊤
n : ℕ
hn : a < ↑n
i✝ : ℕ
a✝ : i✝ ∈ Finset.range n
⊢ 1 ≤ r ^ i✝

Proof state:
case h
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ⊤
n : ℕ
hn : a < ↑n
i✝ : ℕ
a✝ : i✝ ∈ Finset.range n
⊢ 1 ≤ r ^ i✝

Tactic:
apply one_le_pow₀ hr

Result:
no goals

Proof state:
case inl.intro.intro
r : ℝ≥0
hr' : ↑r < 1
hr : ↑r < 1
⊢ ∑' (n : ℕ), ↑r ^ n = (1 - ↑r)⁻¹

Tactic:
norm_cast at *

Result:
case inl.intro.intro
r : ℝ≥0
hr' hr : r < 1
⊢ ∑' (n : ℕ), ↑(r ^ n) = (↑(1 - r))⁻¹

Proof state:
case inl
r : ℝ≥0∞
hr : r < 1
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

Tactic:
rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩

Result:
case inl.intro.intro
r : ℝ≥0
hr' : ↑r < 1
hr : ↑r < 1
⊢ ∑' (n : ℕ), ↑r ^ n = (1 - ↑r)⁻¹

Proof state:
case inr
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

Tactic:
rw [tsub_eq_zero_iff_le.mpr hr, ENNReal.inv_zero, ENNReal.tsum_eq_iSup_nat, iSup_eq_top]

Result:
case inr
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∀ b < ⊤, ∃ i, b < ∑ a ∈ Finset.range i, r ^ a

Proof state:
case h.e'_3
r : ℝ≥0
hr' hr : r < 1
⊢ (↑(1 - r))⁻¹ = ↑(1 - r)⁻¹

Tactic:
rw [ENNReal.coe_inv <| ne_of_gt <| tsub_pos_iff_lt.2 hr, coe_sub, coe_one]

Result:
no goals
-- Mathlib/Order/Filter/CountableInter.lean
theorem EventuallyLE.countable_bUnion {ι : Type*} {S : Set ι} (hS : S.Countable)
    {s t : ∀ i ∈ S, Set α} (h : ∀ i hi, s i hi ≤ᶠ[l] t i hi) :
    ⋃ i ∈ S, s i ‹_› ≤ᶠ[l] ⋃ i ∈ S, t i ‹_›

Proof state:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
this : Encodable ↑S
⊢ ⋃ x, s ↑x ⋯ ≤ᶠ[l] ⋃ x, t ↑x ⋯

Tactic:
exact EventuallyLE.countable_iUnion fun i => h i i.2

Result:
no goals

Proof state:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋃ i, ⋃ (h : i ∈ S), s i h ≤ᶠ[l] ⋃ i, ⋃ (h : i ∈ S), t i h

Tactic:
simp only [biUnion_eq_iUnion]

Result:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋃ x, s ↑x ⋯ ≤ᶠ[l] ⋃ x, t ↑x ⋯

Proof state:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋃ x, s ↑x ⋯ ≤ᶠ[l] ⋃ x, t ↑x ⋯

Tactic:
haveI := hS.toEncodable

Result:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
this : Encodable ↑S
⊢ ⋃ x, s ↑x ⋯ ≤ᶠ[l] ⋃ x, t ↑x ⋯
-- Mathlib/Logic/IsEmpty.lean
theorem biTotal_iff_isEmpty_right [IsEmpty α] : BiTotal R ↔ IsEmpty β

Proof state:
α : Type u_4
β : Type u_5
R : α → β → Prop
inst✝ : IsEmpty α
⊢ BiTotal R ↔ IsEmpty β

Tactic:
simp only [BiTotal, leftTotal_empty, rightTotal_iff_isEmpty_right, true_and]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean
lemma exp_neg_llr' [SigmaFinite μ] [SigmaFinite ν] (hμν : ν ≪ μ) :
    (fun x ↦ exp (- llr μ ν x)) =ᵐ[ν] fun x ↦ (ν.rnDeriv μ x).toReal

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : ν ≪ μ
x : α
hx : llr ν μ x = -llr μ ν x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal

Tactic:
rw [← hx, hx_exp_log]

Result:
no goals

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : ν ≪ μ
x : α
hx : (-llr ν μ) x = llr μ ν x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal

Tactic:
rw [Pi.neg_apply, neg_eq_iff_eq_neg] at hx

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : ν ≪ μ
x : α
hx : llr ν μ x = -llr μ ν x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : ν ≪ μ
⊢ (fun x => rexp (-llr μ ν x)) =ᶠ[ae ν] fun x => (ν.rnDeriv μ x).toReal

Tactic:
filter_upwards [neg_llr hμν, exp_llr_of_ac ν μ hμν] with x hx hx_exp_log

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : ν ≪ μ
x : α
hx : (-llr ν μ) x = llr μ ν x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem isWeightedHomogeneous_X (w : σ → M) (i : σ) :
    IsWeightedHomogeneous w (X i : MvPolynomial σ R) (w i)

Proof state:
case hm
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
i : σ
⊢ (weight w) (Finsupp.single i 1) = w i

Tactic:
simp only [weight, LinearMap.toAddMonoidHom_coe, linearCombination_single, one_nsmul]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
i : σ
⊢ IsWeightedHomogeneous w (X i) (w i)

Tactic:
apply isWeightedHomogeneous_monomial

Result:
case hm
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
i : σ
⊢ (weight w) (Finsupp.single i 1) = w i
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem eq_of_norm_add_lt_left {z1 z2 : ℚ_[p]} (h : ‖z1 + z2‖ < ‖z1‖) : ‖z1‖ = ‖z2‖ :=
  _root_.by_contradiction fun hne ↦
    not_lt_of_ge (by rw [padicNormE.add_eq_max_of_ne hne]; apply le_max_left) h

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1 + z2‖ ≥ ‖z1‖

Tactic:
rw [padicNormE.add_eq_max_of_ne hne]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1‖ ⊔ ‖z2‖ ≥ ‖z1‖

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1‖ ⊔ ‖z2‖ ≥ ‖z1‖

Tactic:
apply le_max_left

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem alterKey_of_perm {a : α} {f : Option (β a) → Option (β a)} {l l' : List ((a : α) × β a)}
    (hl : DistinctKeys l) (hp : Perm l l') : Perm (alterKey a f l) (alterKey a f l')

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l l' : List ((a : α) × β a)
hl : DistinctKeys l
hp : l.Perm l'
⊢ (match f (getValueCast? a l') with
      | none => eraseKey a l
      | some v => insertEntry a v l).Perm
    (match f (getValueCast? a l') with
    | none => eraseKey a l'
    | some v => insertEntry a v l')

Tactic:
split

Result:
case h_1
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l l' : List ((a : α) × β a)
hl : DistinctKeys l
hp : l.Perm l'
x✝ : Option (β a)
heq✝ : f (getValueCast? a l') = none
⊢ (eraseKey a l).Perm (eraseKey a l')

case h_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l l' : List ((a : α) × β a)
hl : DistinctKeys l
hp : l.Perm l'
x✝ : Option (β a)
v✝ : β a
heq✝ : f (getValueCast? a l') = some v✝
⊢ (insertEntry a v✝ l).Perm (insertEntry a v✝ l')

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l l' : List ((a : α) × β a)
hl : DistinctKeys l
hp : l.Perm l'
⊢ (alterKey a f l).Perm (alterKey a f l')

Tactic:
simp only [alterKey, getValueCast?_of_perm hl hp]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l l' : List ((a : α) × β a)
hl : DistinctKeys l
hp : l.Perm l'
⊢ (match f (getValueCast? a l') with
      | none => eraseKey a l
      | some v => insertEntry a v l).Perm
    (match f (getValueCast? a l') with
    | none => eraseKey a l'
    | some v => insertEntry a v l')

Proof state:
case h_1
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l l' : List ((a : α) × β a)
hl : DistinctKeys l
hp : l.Perm l'
x✝ : Option (β a)
heq✝ : f (getValueCast? a l') = none
⊢ (eraseKey a l).Perm (eraseKey a l')

Tactic:
exact eraseKey_of_perm hl hp

Result:
no goals

Proof state:
case h_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l l' : List ((a : α) × β a)
hl : DistinctKeys l
hp : l.Perm l'
x✝ : Option (β a)
v✝ : β a
heq✝ : f (getValueCast? a l') = some v✝
⊢ (insertEntry a v✝ l).Perm (insertEntry a v✝ l')

Tactic:
exact insertEntry_of_perm hl hp

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Basic.lean
theorem MonoidHom.comp_id_commGrp {G : CommGrp.{u}} {H : Type u} [Monoid H] (f : G →* H) :
    f.comp (CommGrp.Hom.hom (𝟙 G)) = f

Proof state:
G : CommGrp
H : Type u
inst✝ : Monoid H
f : ↑G →* H
⊢ f.comp (CommGrp.Hom.hom (𝟙 G)) = f

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Fold.lean
theorem fold_min_le : s.fold min b f ≤ c ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c

Proof state:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ fold min b f s ≤ c ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c

Tactic:
show _ ≥ _ ↔ _

Result:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ c ≥ fold min b f s ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c

Proof state:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ c ≥ fold min b f s ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c

Tactic:
apply fold_op_rel_iff_or

Result:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x ≥ y ⊓ z ↔ x ≥ y ∨ x ≥ z

Proof state:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ y ⊓ z ≤ x ↔ x ≥ y ∨ x ≥ z

Tactic:
exact min_le_iff

Result:
no goals

Proof state:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x ≥ y ⊓ z ↔ x ≥ y ∨ x ≥ z

Tactic:
intro x y z

Result:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ x ≥ y ⊓ z ↔ x ≥ y ∨ x ≥ z

Proof state:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ x ≥ y ⊓ z ↔ x ≥ y ∨ x ≥ z

Tactic:
show _ ≤ _ ↔ _

Result:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ y ⊓ z ≤ x ↔ x ≥ y ∨ x ≥ z
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem prod_Ico_eq_mul_inv {δ : Type*} [CommGroup δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) :
    ∏ k ∈ Ico m n, f k = (∏ k ∈ range n, f k) * (∏ k ∈ range m, f k)⁻¹ :=
  eq_mul_inv_iff_mul_eq.2 <| by (rw [mul_comm]; exact prod_range_mul_prod_Ico f h)

Proof state:
δ : Type u_3
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k ∈ Ico m n, f k) * ∏ k ∈ range m, f k = ∏ k ∈ range n, f k

Tactic:
(rw [mul_comm]; exact prod_range_mul_prod_Ico f h)

Result:
no goals

Proof state:
δ : Type u_3
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k ∈ Ico m n, f k) * ∏ k ∈ range m, f k = ∏ k ∈ range n, f k

Tactic:
rw [mul_comm]

Result:
δ : Type u_3
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k ∈ range m, f k) * ∏ k ∈ Ico m n, f k = ∏ k ∈ range n, f k

Proof state:
δ : Type u_3
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k ∈ range m, f k) * ∏ k ∈ Ico m n, f k = ∏ k ∈ range n, f k

Tactic:
exact prod_range_mul_prod_Ico f h

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem eq_emptyOn [IsEmpty α] (M : Matroid α) : M = emptyOn α

Proof state:
α : Type u_1
inst✝ : IsEmpty α
M : Matroid α
⊢ M = emptyOn α

Tactic:
rw [← ground_eq_empty_iff]

Result:
α : Type u_1
inst✝ : IsEmpty α
M : Matroid α
⊢ M.E = ∅

Proof state:
α : Type u_1
inst✝ : IsEmpty α
M : Matroid α
⊢ M.E = ∅

Tactic:
exact M.E.eq_empty_of_isEmpty

Result:
no goals