harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Ordering/Lemmas.lean
theorem cmpUsing_eq_eq (a b : α) : cmpUsing lt a b = Ordering.eq ↔ ¬lt a b ∧ ¬lt b a

Proof state:
α : Type u
lt : α → α → Prop
inst✝ : DecidableRel lt
a b : α
⊢ cmpUsing lt a b = Ordering.eq ↔ ¬lt a b ∧ ¬lt b a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem lt_one_iff {x : BitVec w} (h : 0 < w) : x < 1#w ↔ x = 0#w

Proof state:
w : Nat
x : BitVec w
h : 0 < w
h₂ : ↑x.toNat < 1 % 2 ^ w
⊢ 1 < 2 ^ w

Tactic:
omega

Result:
no goals

Proof state:
case mp
w : Nat
x : BitVec w
h : 0 < w
h₂ : x < 1#w
⊢ x = 0#w

Tactic:
rw [lt_def, toNat_ofNat, ← Int.ofNat_lt, Int.ofNat_emod, Int.ofNat_one, Int.natCast_pow,
  Int.ofNat_two, @Int.emod_eq_of_lt 1 (2^w) (by omega) (by omega)] at h₂

Result:
case mp
w : Nat
x : BitVec w
h : 0 < w
h₂ : ↑x.toNat < 1
⊢ x = 0#w

Proof state:
case mpr
w : Nat
x : BitVec w
h : 0 < w
⊢ x = 0#w → x < 1#w

Tactic:
simp_all

Result:
no goals

Proof state:
w : Nat
x : BitVec w
h : 0 < w
h₂ : ↑x.toNat < 1
⊢ x.toNat = 0

Tactic:
omega

Result:
no goals

Proof state:
case mp
w : Nat
x : BitVec w
h : 0 < w
⊢ x < 1#w → x = 0#w

Tactic:
intro h₂

Result:
case mp
w : Nat
x : BitVec w
h : 0 < w
h₂ : x < 1#w
⊢ x = 0#w

Proof state:
w : Nat
x : BitVec w
h : 0 < w
⊢ x < 1#w ↔ x = 0#w

Tactic:
constructor

Result:
case mp
w : Nat
x : BitVec w
h : 0 < w
⊢ x < 1#w → x = 0#w

case mpr
w : Nat
x : BitVec w
h : 0 < w
⊢ x = 0#w → x < 1#w

Proof state:
case mp
w : Nat
x : BitVec w
h : 0 < w
h₂ : ↑x.toNat < 1
⊢ x = 0#w

Tactic:
simp [toNat_eq, show x.toNat = 0 by omega]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
h : 0 < w
h₂ : ↑x.toNat < 1 % 2 ^ w
⊢ 0 ≤ 1

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
lemma isGE_of_ge (p q : ℤ) (hpq : p ≤ q) [K.IsGE q] :
    K.IsGE p

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsGE q
i : ℤ
hi : i < p
⊢ ExactAt K i

Tactic:
apply K.exactAt_of_isGE q

Result:
case hi
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsGE q
i : ℤ
hi : i < p
⊢ i < q

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsGE q
⊢ K.IsGE p

Tactic:
rw [isGE_iff]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsGE q
⊢ ∀ i < p, ExactAt K i

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsGE q
⊢ ∀ i < p, ExactAt K i

Tactic:
intro i hi

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsGE q
i : ℤ
hi : i < p
⊢ ExactAt K i

Proof state:
case hi
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsGE q
i : ℤ
hi : i < p
⊢ i < q

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem insertIdx_comm (a b : α) :
    ∀ (i j : Nat) (l : List α) (_ : i ≤ j) (_ : j ≤ length l),
      (l.insertIdx i a).insertIdx (j + 1) b = (l.insertIdx j b).insertIdx i a
  | 0, j, l => by simp [insertIdx]
  | _ + 1, 0, _ => fun h => (Nat.not_lt_zero _ h).elim
  | i + 1, j + 1, [] => by simp
  | i + 1, j + 1, c :: l => fun h₀ h₁ => by
    simp only [insertIdx_succ_cons, cons.injEq, true_and]
    exact insertIdx_comm a b i j l (Nat.le_of_succ_le_succ h₀) (Nat.le_of_succ_le_succ h₁)

Proof state:
α : Type u
a b : α
i j : Nat
⊢ i + 1 ≤ j + 1 →
    j + 1 ≤ [].length → insertIdx (j + 1 + 1) b (insertIdx (i + 1) a []) = insertIdx (i + 1) a (insertIdx (j + 1) b [])

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
a b : α
i j : Nat
c : α
l : List α
h₀ : i + 1 ≤ j + 1
h₁ : j + 1 ≤ (c :: l).length
⊢ insertIdx (j + 1) b (insertIdx i a l) = insertIdx i a (insertIdx j b l)

Tactic:
exact insertIdx_comm a b i j l (Nat.le_of_succ_le_succ h₀) (Nat.le_of_succ_le_succ h₁)

Result:
no goals

Proof state:
α : Type u
a b : α
j : Nat
l : List α
⊢ 0 ≤ j → j ≤ l.length → insertIdx (j + 1) b (insertIdx 0 a l) = insertIdx 0 a (insertIdx j b l)

Tactic:
simp [insertIdx]

Result:
no goals

Proof state:
α : Type u
a b : α
i j : Nat
c : α
l : List α
h₀ : i + 1 ≤ j + 1
h₁ : j + 1 ≤ (c :: l).length
⊢ insertIdx (j + 1 + 1) b (insertIdx (i + 1) a (c :: l)) = insertIdx (i + 1) a (insertIdx (j + 1) b (c :: l))

Tactic:
simp only [insertIdx_succ_cons, cons.injEq, true_and]

Result:
α : Type u
a b : α
i j : Nat
c : α
l : List α
h₀ : i + 1 ≤ j + 1
h₁ : j + 1 ≤ (c :: l).length
⊢ insertIdx (j + 1) b (insertIdx i a l) = insertIdx i a (insertIdx j b l)
-- Mathlib/Data/ENNReal/Inv.lean
theorem exists_inv_two_pow_lt (ha : a ≠ 0) : ∃ n : ℕ, 2⁻¹ ^ n < a

Proof state:
case intro
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n)⁻¹ < a
⊢ 2⁻¹ ^ n < (↑n)⁻¹

Tactic:
rw [← ENNReal.inv_pow, ENNReal.inv_lt_inv]

Result:
case intro
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n)⁻¹ < a
⊢ ↑n < 2 ^ n

Proof state:
case intro
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n)⁻¹ < a
⊢ ∃ n, 2⁻¹ ^ n < a

Tactic:
refine ⟨n, lt_trans ?_ hn⟩

Result:
case intro
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n)⁻¹ < a
⊢ 2⁻¹ ^ n < (↑n)⁻¹

Proof state:
case intro
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n)⁻¹ < a
⊢ ↑n < 2 ^ n

Tactic:
norm_cast

Result:
case intro
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n)⁻¹ < a
⊢ n < 2 ^ n

Proof state:
a : ℝ≥0∞
ha : a ≠ 0
⊢ ∃ n, 2⁻¹ ^ n < a

Tactic:
rcases exists_inv_nat_lt ha with ⟨n, hn⟩

Result:
case intro
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n)⁻¹ < a
⊢ ∃ n, 2⁻¹ ^ n < a

Proof state:
case intro
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n)⁻¹ < a
⊢ n < 2 ^ n

Tactic:
exact n.lt_two_pow_self

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_zsmul_add' (a b : α) (m : ℤ) :
    toIocMod hp (m • p + a) b = m • p + toIocMod hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp (m • p + a) b = m • p + toIocMod hp a b

Tactic:
rw [add_comm, toIocMod_add_zsmul', add_comm]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Card.lean
theorem self_subset_generateMeasurableRec (s : Set (Set α)) (i : Ordinal) :
    s ⊆ generateMeasurableRec s i

Proof state:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ s ⊆
    let S := ⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ n, ↑(f n)

Tactic:
apply_rules [subset_union_of_subset_left]

Result:
case h.h.h
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ s ⊆ s

Proof state:
case h.h.h
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ s ⊆ s

Tactic:
exact subset_rfl

Result:
no goals

Proof state:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ s ⊆ generateMeasurableRec s i

Tactic:
unfold generateMeasurableRec

Result:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ s ⊆
    let S := ⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ n, ↑(f n)
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_succ_right (n k : ℕ) (hn : 0 < n) :
    choose n (k + 1) = choose (n - 1) k + choose (n - 1) (k + 1)

Proof state:
n k : ℕ
hn : 0 < n
⊢ n.choose (k + 1) = (n - 1).choose k + (n - 1).choose (k + 1)

Tactic:
obtain ⟨l, rfl⟩ : ∃ l, n = l + 1 := Nat.exists_eq_add_of_le' hn

Result:
case intro
k l : ℕ
hn : 0 < l + 1
⊢ (l + 1).choose (k + 1) = (l + 1 - 1).choose k + (l + 1 - 1).choose (k + 1)

Proof state:
case intro
k l : ℕ
hn : 0 < l + 1
⊢ (l + 1).choose (k + 1) = (l + 1 - 1).choose k + (l + 1 - 1).choose (k + 1)

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
theorem quadraticChar_sq_one {a : F} (ha : a ≠ 0) : quadraticChar F a ^ 2 = 1

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ (quadraticChar F) a ^ 2 = 1

Tactic:
rwa [pow_two, ← map_mul, ← pow_two, quadraticChar_sq_one']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_intMax : (intMax w).toNat = 2 ^ (w - 1) - 1

Proof state:
case neg
w : Nat
h : ¬w = 0
⊢ (twoPow w (w - 1) - 1).toNat = 2 ^ (w - 1) - 1

Tactic:
have h' : 0 < w := by omega

Result:
case neg
w : Nat
h : ¬w = 0
h' : 0 < w
⊢ (twoPow w (w - 1) - 1).toNat = 2 ^ (w - 1) - 1

Proof state:
case neg
w : Nat
h : ¬w = 0
h' : 0 < w
⊢ (twoPow w (w - 1) - 1).toNat = 2 ^ (w - 1) - 1

Tactic:
rw [toNat_sub, toNat_twoPow, ← Nat.sub_add_comm (by simpa [h'] using Nat.one_le_two_pow),
  Nat.add_sub_assoc (by simpa [h'] using Nat.one_le_two_pow),
  Nat.two_pow_pred_mod_two_pow h', ofNat_eq_ofNat, toNat_ofNat, Nat.one_mod_two_pow h',
  Nat.add_mod_left, Nat.mod_eq_of_lt]

Result:
case neg
w : Nat
h : ¬w = 0
h' : 0 < w
⊢ 2 ^ (w - 1) - 1 < 2 ^ w

Proof state:
w : Nat
⊢ (intMax w).toNat = 2 ^ (w - 1) - 1

Tactic:
simp only [intMax]

Result:
w : Nat
⊢ (twoPow w (w - 1) - 1).toNat = 2 ^ (w - 1) - 1

Proof state:
case neg
w : Nat
h : ¬w = 0
h' : 0 < w
this✝ : 2 ^ (w - 1) < 2 ^ w
this : 0 < 2 ^ w
⊢ 2 ^ (w - 1) - 1 < 2 ^ w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
⊢ (twoPow w (w - 1) - 1).toNat = 2 ^ (w - 1) - 1

Tactic:
by_cases h : w = 0

Result:
case pos
w : Nat
h : w = 0
⊢ (twoPow w (w - 1) - 1).toNat = 2 ^ (w - 1) - 1

case neg
w : Nat
h : ¬w = 0
⊢ (twoPow w (w - 1) - 1).toNat = 2 ^ (w - 1) - 1

Proof state:
case pos
w : Nat
h : w = 0
⊢ (twoPow w (w - 1) - 1).toNat = 2 ^ (w - 1) - 1

Tactic:
simp [h]

Result:
no goals

Proof state:
w : Nat
h : ¬w = 0
h' : 0 < w
⊢ BitVec.toNat 1 ≤ 2 ^ (w - 1) % 2 ^ w

Tactic:
simpa [h'] using Nat.one_le_two_pow

Result:
no goals

Proof state:
w : Nat
h : ¬w = 0
h' : 0 < w
⊢ BitVec.toNat 1 ≤ 2 ^ w

Tactic:
simpa [h'] using Nat.one_le_two_pow

Result:
no goals

Proof state:
w : Nat
h : ¬w = 0
⊢ 0 < w

Tactic:
omega

Result:
no goals

Proof state:
case neg
w : Nat
h : ¬w = 0
h' : 0 < w
⊢ 2 ^ (w - 1) - 1 < 2 ^ w

Tactic:
have := Nat.two_pow_pred_lt_two_pow h'

Result:
case neg
w : Nat
h : ¬w = 0
h' : 0 < w
this : 2 ^ (w - 1) < 2 ^ w
⊢ 2 ^ (w - 1) - 1 < 2 ^ w

Proof state:
case neg
w : Nat
h : ¬w = 0
h' : 0 < w
this : 2 ^ (w - 1) < 2 ^ w
⊢ 2 ^ (w - 1) - 1 < 2 ^ w

Tactic:
have := Nat.two_pow_pos w

Result:
case neg
w : Nat
h : ¬w = 0
h' : 0 < w
this✝ : 2 ^ (w - 1) < 2 ^ w
this : 0 < 2 ^ w
⊢ 2 ^ (w - 1) - 1 < 2 ^ w
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem denote_idx_const {aig : AIG α} {hstart} (h : aig.decls[start]'hstart = .const b) :
    ⟦aig, ⟨start, hstart⟩, assign⟧ = b

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
b : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.const b
⊢ (match elem :
      { aig := aig,
              ref :=
                { gate := start,
                  hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)) =
    b

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
b : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.const b
⊢ ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = b

Tactic:
unfold denote denote.go

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
b : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.const b
⊢ (match elem :
      { aig := aig,
              ref :=
                { gate := start,
                  hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)) =
    b
-- Mathlib/Data/Sym/Basic.lean
theorem exists_cons_of_mem {s : Sym α (n + 1)} {a : α} (h : a ∈ s) : ∃ t, s = a ::ₛ t

Proof state:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : (↑s).card = (a ::ₘ m).card
⊢ m.card = n

Tactic:
rw [s.2, Multiset.card_cons, add_left_inj] at h

Result:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : n = m.card
⊢ m.card = n

Proof state:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h : a ∈ s
⊢ ∃ t, s = a ::ₛ t

Tactic:
obtain ⟨m, h⟩ := Multiset.exists_cons_of_mem h

Result:
case intro
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : ↑s = a ::ₘ m
⊢ ∃ t, s = a ::ₛ t

Proof state:
case h.a
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : ↑s = a ::ₘ m
this : m.card = n
⊢ ↑s = ↑(a ::ₛ ⟨m, this⟩)

Tactic:
exact h

Result:
no goals

Proof state:
case intro
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : ↑s = a ::ₘ m
this : m.card = n
⊢ ∃ t, s = a ::ₛ t

Tactic:
use ⟨m, this⟩

Result:
case h
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : ↑s = a ::ₘ m
this : m.card = n
⊢ s = a ::ₛ ⟨m, this⟩

Proof state:
case intro
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : ↑s = a ::ₘ m
⊢ ∃ t, s = a ::ₛ t

Tactic:
have : Multiset.card m = n := by
  apply_fun Multiset.card at h
  rw [s.2, Multiset.card_cons, add_left_inj] at h
  exact h.symm

Result:
case intro
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : ↑s = a ::ₘ m
this : m.card = n
⊢ ∃ t, s = a ::ₛ t

Proof state:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : ↑s = a ::ₘ m
⊢ m.card = n

Tactic:
apply_fun Multiset.card at h

Result:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : (↑s).card = (a ::ₘ m).card
⊢ m.card = n

Proof state:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : n = m.card
⊢ m.card = n

Tactic:
exact h.symm

Result:
no goals

Proof state:
case h
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : ↑s = a ::ₘ m
this : m.card = n
⊢ s = a ::ₛ ⟨m, this⟩

Tactic:
apply Subtype.ext

Result:
case h.a
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : ↑s = a ::ₘ m
this : m.card = n
⊢ ↑s = ↑(a ::ₛ ⟨m, this⟩)
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem mem_sSup_of_directedOn {K : Set (Subgroup G)} (Kne : K.Nonempty) (hK : DirectedOn (· ≤ ·) K)
    {x : G} : x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s

Proof state:
G : Type u_1
inst✝ : Group G
K : Set (Subgroup G)
Kne : K.Nonempty
hK : DirectedOn (fun x1 x2 => x1 ≤ x2) K
x : G
⊢ x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s

Tactic:
haveI : Nonempty K := Kne.to_subtype

Result:
G : Type u_1
inst✝ : Group G
K : Set (Subgroup G)
Kne : K.Nonempty
hK : DirectedOn (fun x1 x2 => x1 ≤ x2) K
x : G
this : Nonempty ↑K
⊢ x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s

Proof state:
G : Type u_1
inst✝ : Group G
K : Set (Subgroup G)
Kne : K.Nonempty
hK : DirectedOn (fun x1 x2 => x1 ≤ x2) K
x : G
this : Nonempty ↑K
⊢ x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed hK.directed_val, SetCoe.exists, Subtype.coe_mk,
  exists_prop]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem Ico_succ_right : Ico a b.succ = Icc a b

Proof state:
case h
a b x : ℕ
⊢ x ∈ Ico a b.succ ↔ x ∈ Icc a b

Tactic:
rw [mem_Ico, mem_Icc, Nat.lt_succ_iff]

Result:
no goals

Proof state:
a b : ℕ
⊢ Ico a b.succ = Icc a b

Tactic:
ext x

Result:
case h
a b x : ℕ
⊢ x ∈ Ico a b.succ ↔ x ∈ Icc a b
-- Mathlib/Algebra/Module/Equiv/Defs.lean
lemma coe_toAddEquiv_symm : (e₁₂.symm : M₂ ≃+ M₁) = (e₁₂ : M₁ ≃+ M₂).symm

Proof state:
R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_7
M₂ : Type u_8
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₁
inst✝ : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
⊢ ↑e₁₂.symm = (↑e₁₂).symm

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem IsUniformInducing.uniformContinuous_iff {f : α → β} {g : β → γ} (hg : IsUniformInducing g) :
    UniformContinuous f ↔ UniformContinuous (g ∘ f)

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hg : IsUniformInducing g
⊢ map (fun x => (f x.1, f x.2)) (𝓤 α) ≤ 𝓤 β ↔ map (fun x => ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α) ≤ 𝓤 γ

Tactic:
simp only [← hg.comap_uniformity, ← map_le_iff_le_comap, Filter.map_map, Function.comp_def]

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hg : IsUniformInducing g
⊢ UniformContinuous f ↔ UniformContinuous (g ∘ f)

Tactic:
dsimp only [UniformContinuous, Tendsto]

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hg : IsUniformInducing g
⊢ map (fun x => (f x.1, f x.2)) (𝓤 α) ≤ 𝓤 β ↔ map (fun x => ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α) ≤ 𝓤 γ
-- Mathlib/Analysis/Normed/Field/Lemmas.lean
@[simp]
lemma inv_nhdsWithin_ne_zero : (𝓝[≠] (0 : α))⁻¹ = cobounded α

Proof state:
α : Type u_1
inst✝ : NormedDivisionRing α
⊢ (𝓝[≠] 0)⁻¹ = cobounded α

Tactic:
rw [← inv_cobounded₀, inv_inv]

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Lemmas.lean
theorem nilpotent_iff_mem_prime : IsNilpotent x ↔ ∀ J : Ideal R, J.IsPrime → x ∈ J

Proof state:
R : Type u_1
inst✝ : CommSemiring R
x : R
⊢ IsNilpotent x ↔ ∀ (J : Ideal R), J.IsPrime → x ∈ J

Tactic:
rw [← mem_nilradical, nilradical_eq_sInf, Submodule.mem_sInf]

Result:
R : Type u_1
inst✝ : CommSemiring R
x : R
⊢ (∀ p ∈ {J | J.IsPrime}, x ∈ p) ↔ ∀ (J : Ideal R), J.IsPrime → x ∈ J

Proof state:
R : Type u_1
inst✝ : CommSemiring R
x : R
⊢ (∀ p ∈ {J | J.IsPrime}, x ∈ p) ↔ ∀ (J : Ideal R), J.IsPrime → x ∈ J

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem card_units_lt (w : 1 < q) : Fintype.card (X q)ˣ < q ^ 2

Proof state:
q : ℕ+
w : 1 < q
⊢ Fintype.card (X q)ˣ < ↑q ^ 2

Tactic:
have : Fact (1 < (q : ℕ)) := ⟨w⟩

Result:
q : ℕ+
w : 1 < q
this : Fact (1 < ↑q)
⊢ Fintype.card (X q)ˣ < ↑q ^ 2

Proof state:
case h.e'_4
q : ℕ+
w : 1 < q
this : Fact (1 < ↑q)
⊢ ↑q ^ 2 = Fintype.card (X q)

Tactic:
rw [card_eq]

Result:
no goals

Proof state:
q : ℕ+
w : 1 < q
this : Fact (1 < ↑q)
⊢ Fintype.card (X q)ˣ < ↑q ^ 2

Tactic:
convert card_units_lt (X q)

Result:
case h.e'_4
q : ℕ+
w : 1 < q
this : Fact (1 < ↑q)
⊢ ↑q ^ 2 = Fintype.card (X q)
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem neg (hf : IsBoundedLinearMap 𝕜 f) : IsBoundedLinearMap 𝕜 fun e => -f e

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
hf : IsBoundedLinearMap 𝕜 f
⊢ IsBoundedLinearMap 𝕜 fun e => -f e

Tactic:
rw [show (fun e => -f e) = fun e => (-1 : 𝕜) • f e by funext; simp]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
hf : IsBoundedLinearMap 𝕜 f
⊢ IsBoundedLinearMap 𝕜 fun e => -1 • f e

Proof state:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
hf : IsBoundedLinearMap 𝕜 f
x✝ : E
⊢ -f x✝ = -1 • f x✝

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
hf : IsBoundedLinearMap 𝕜 f
⊢ (fun e => -f e) = fun e => -1 • f e

Tactic:
funext

Result:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
hf : IsBoundedLinearMap 𝕜 f
x✝ : E
⊢ -f x✝ = -1 • f x✝

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
hf : IsBoundedLinearMap 𝕜 f
⊢ IsBoundedLinearMap 𝕜 fun e => -1 • f e

Tactic:
exact smul (-1) hf

Result:
no goals
-- Mathlib/Data/Nat/Fib/Basic.lean
lemma fib_lt_fib {m : ℕ} (hm : 2 ≤ m) : ∀ {n}, fib m < fib n ↔ m < n
  | 0 => by simp [hm]
  | 1 => by simp [hm]
  | n + 2 => fib_strictMonoOn.lt_iff_lt hm <| by simp

Proof state:
m : ℕ
hm : 2 ≤ m
⊢ fib m < fib 1 ↔ m < 1

Tactic:
simp [hm]

Result:
no goals

Proof state:
m : ℕ
hm : 2 ≤ m
⊢ fib m < fib 0 ↔ m < 0

Tactic:
simp [hm]

Result:
no goals

Proof state:
m : ℕ
hm : 2 ≤ m
n : ℕ
⊢ n + 2 ∈ Set.Ici 2

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem ball_zero : ball x 0 = ∅

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
⊢ ball x 0 = ∅

Tactic:
rw [EMetric.ball_eq_empty_iff]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem nontrivial_of_infsep_pos (hs : 0 < s.infsep) : s.Nontrivial

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
hs : 0 < s.infsep
⊢ s.Nontrivial

Tactic:
contrapose hs

Result:
α : Type u_1
inst✝ : EDist α
s : Set α
hs : ¬s.Nontrivial
⊢ ¬0 < s.infsep

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
hs : ¬s.Nontrivial
⊢ ¬0 < s.infsep

Tactic:
rw [not_nontrivial_iff] at hs

Result:
α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Subsingleton
⊢ ¬0 < s.infsep

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Subsingleton
⊢ ¬0 < s.infsep

Tactic:
exact hs.infsep_zero ▸ lt_irrefl _

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem mapRange_def [∀ (i) (x : β₁ i), Decidable (x ≠ 0)] {f : ∀ i, β₁ i → β₂ i}
    {hf : ∀ i, f i 0 = 0} {g : Π₀ i, β₁ i} :
    mapRange f hf g = mk g.support fun i => f i.1 (g i.1)

Proof state:
case h
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β₁ i)
inst✝¹ : (i : ι) → Zero (β₂ i)
inst✝ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
i : ι
⊢ (mapRange f hf g) i = (mk g.support fun i => f (↑i) (g ↑i)) i

Tactic:
by_cases h : g i ≠ 0 <;> simp at h <;> simp [h, hf]

Result:
no goals

Proof state:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β₁ i)
inst✝¹ : (i : ι) → Zero (β₂ i)
inst✝ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
⊢ mapRange f hf g = mk g.support fun i => f (↑i) (g ↑i)

Tactic:
ext i

Result:
case h
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β₁ i)
inst✝¹ : (i : ι) → Zero (β₂ i)
inst✝ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
i : ι
⊢ (mapRange f hf g) i = (mk g.support fun i => f (↑i) (g ↑i)) i
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem factors_zero [HasZeroMorphisms C] {X Y : C} {P : Subobject Y} : P.Factors (0 : X ⟶ Y) :=
  (factors_iff _ _).mpr ⟨0, by simp⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
⊢ 0 ≫ (representative.obj P).arrow = 0

Tactic:
simp

Result:
no goals