harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem EquicontinuousAt.closure' {A : Set Y} {u : Y → X → α} {x₀ : X}
    (hA : EquicontinuousAt (u ∘ (↑) : A → X → α) x₀) (hu : Continuous u) :
    EquicontinuousAt (u ∘ (↑) : closure A → X → α) x₀

Proof state:
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
x₀ : X
hA : EquicontinuousAt (u ∘ Subtype.val) x₀
hu : Continuous u
⊢ EquicontinuousAt (u ∘ Subtype.val) x₀

Tactic:
rw [← equicontinuousWithinAt_univ] at hA ⊢

Result:
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) univ x₀
hu : Continuous u
⊢ EquicontinuousWithinAt (u ∘ Subtype.val) univ x₀

Proof state:
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) univ x₀
hu : Continuous u
⊢ EquicontinuousWithinAt (u ∘ Subtype.val) univ x₀

Tactic:
exact hA.closure' (Pi.continuous_restrict _ |>.comp hu) (continuous_apply x₀ |>.comp hu)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean
theorem go_get (aig : AIG BVBit) (a : Nat) (curr : Nat) (hcurr : curr ≤ w)
    (s : AIG.RefVec aig curr) :
    ∀ (idx : Nat) (hidx : idx < curr),
        (go aig w a curr s hcurr).vec.get idx (by omega)
          =
        (s.get idx hidx).cast (by apply go_le_size)

Proof state:
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
⊢ aig.decls.size ≤ (go aig w a curr s hcurr).aig.decls.size

Tactic:
apply go_le_size

Result:
no goals

Proof state:
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx✝ : Nat
hidx✝ : idx✝ < curr
⊢ (go aig w a curr s hcurr).vec.get idx✝ ⋯ = (s.get idx✝ hidx✝).cast ⋯

Tactic:
apply go_get_aux

Result:
no goals

Proof state:
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
⊢ idx < w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
⊢ ∀ (idx : Nat) (hidx : idx < curr), (go aig w a curr s hcurr).vec.get idx ⋯ = (s.get idx hidx).cast ⋯

Tactic:
intros

Result:
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx✝ : Nat
hidx✝ : idx✝ < curr
⊢ (go aig w a curr s hcurr).vec.get idx✝ ⋯ = (s.get idx✝ hidx✝).cast ⋯
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem mul_nonsing_inv_cancel_right (B : Matrix m n α) (h : IsUnit A.det) : B * A * A⁻¹ = B

Proof state:
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
B : Matrix m n α
h : IsUnit A.det
⊢ B * A * A⁻¹ = B

Tactic:
simp [Matrix.mul_assoc, mul_nonsing_inv A h]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem nnnorm_neg (f : Lp E p μ) : ‖-f‖₊ = ‖f‖₊

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p μ)
⊢ ‖-f‖₊ = ‖f‖₊

Tactic:
rw [nnnorm_def, nnnorm_def, eLpNorm_congr_ae (coeFn_neg _), eLpNorm_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem set_tail (l : List α) (i : Nat) (a : α) :
    l.tail.set i a = (l.set (i + 1) a).tail

Proof state:
α : Type u_1
l : List α
i : Nat
a : α
⊢ l.tail.set i a = (l.set (i + 1) a).tail

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem Sorted.head!_le [Inhabited α] [Preorder α] {a : α} {l : List α} (h : Sorted (· < ·) l)
    (ha : a ∈ l) : l.head! ≤ a

Proof state:
case tail
α : Type u
inst✝¹ : Inhabited α
inst✝ : Preorder α
a : α
l : List α
h : Sorted (fun x1 x2 => x1 < x2) (l.head! :: l.tail)
a✝ : Mem a l.tail
⊢ l.head! ≤ a

Tactic:
exact le_of_lt (rel_of_sorted_cons h a (by assumption))

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Inhabited α
inst✝ : Preorder α
a : α
l : List α
h : Sorted (fun x1 x2 => x1 < x2) (l.head! :: l.tail)
a✝ : Mem a l.tail
⊢ a ∈ l.tail

Tactic:
assumption

Result:
no goals

Proof state:
case head
α : Type u
inst✝¹ : Inhabited α
inst✝ : Preorder α
l : List α
h : Sorted (fun x1 x2 => x1 < x2) (l.head! :: l.tail)
⊢ l.head! ≤ l.head!

Tactic:
exact le_rfl

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Inhabited α
inst✝ : Preorder α
a : α
l : List α
h : Sorted (fun x1 x2 => x1 < x2) l
ha : a ∈ l
⊢ l.head! ≤ a

Tactic:
rw [← List.cons_head!_tail (List.ne_nil_of_mem ha)] at h ha

Result:
α : Type u
inst✝¹ : Inhabited α
inst✝ : Preorder α
a : α
l : List α
h : Sorted (fun x1 x2 => x1 < x2) (l.head! :: l.tail)
ha : a ∈ l.head! :: l.tail
⊢ l.head! ≤ a

Proof state:
α : Type u
inst✝¹ : Inhabited α
inst✝ : Preorder α
a : α
l : List α
h : Sorted (fun x1 x2 => x1 < x2) (l.head! :: l.tail)
ha : a ∈ l.head! :: l.tail
⊢ l.head! ≤ a

Tactic:
cases ha

Result:
case head
α : Type u
inst✝¹ : Inhabited α
inst✝ : Preorder α
l : List α
h : Sorted (fun x1 x2 => x1 < x2) (l.head! :: l.tail)
⊢ l.head! ≤ l.head!

case tail
α : Type u
inst✝¹ : Inhabited α
inst✝ : Preorder α
a : α
l : List α
h : Sorted (fun x1 x2 => x1 < x2) (l.head! :: l.tail)
a✝ : Mem a l.tail
⊢ l.head! ≤ a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/DecidableEq.lean
theorem isEqv_self [DecidableEq α] (a : Vector α n) : Vector.isEqv a a (· = ·) = true

Proof state:
α : Type u_1
n : Nat
inst✝ : DecidableEq α
a : Vector α n
⊢ (a.isEqv a fun x1 x2 => decide (x1 = x2)) = true

Tactic:
rcases a with ⟨a, rfl⟩

Result:
case mk
α : Type u_1
inst✝ : DecidableEq α
a : Array α
⊢ ({ toArray := a, size_toArray := ⋯ }.isEqv { toArray := a, size_toArray := ⋯ } fun x1 x2 => decide (x1 = x2)) = true

Proof state:
case mk
α : Type u_1
inst✝ : DecidableEq α
a : Array α
⊢ ({ toArray := a, size_toArray := ⋯ }.isEqv { toArray := a, size_toArray := ⋯ } fun x1 x2 => decide (x1 = x2)) = true

Tactic:
simp [Array.isEqv_self]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma map_negY : (W'.map f).toAffine.negY (f x) (f y) = f (W'.negY x y)

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x y : R
⊢ (map W' f).toAffine.negY (f x) (f y) = f (W'.negY x y)

Tactic:
simp only [negY]

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x y : R
⊢ -f y - (map W' f).toAffine.a₁ * f x - (map W' f).toAffine.a₃ = f (-y - W'.a₁ * x - W'.a₃)

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x y : R
⊢ -f y - (map W' f).toAffine.a₁ * f x - (map W' f).toAffine.a₃ = f (-y - W'.a₁ * x - W'.a₃)

Tactic:
map_simp

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem Ico_succ_left_of_not_isMax (ha : ¬IsMax a) : Ico (succ a) b = Ioo a b

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ico (succ a) b = Ioo a b

Tactic:
rw [← Ici_inter_Iio, Ici_succ_of_not_isMax ha, Ioi_inter_Iio]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem mem_prod_iff_right {s : Set (α × β)} :
    s ∈ f ×ˢ g ↔ ∃ t ∈ g, ∀ᶠ x in f, ∀ y ∈ t, (x, y) ∈ s

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
⊢ s ∈ f ×ˢ g ↔ ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s

Tactic:
rw [prod_comm, mem_map, mem_prod_iff_left]

Result:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
⊢ (∃ t ∈ g, ∀ᶠ (y : α) in f, ∀ x ∈ t, (x, y) ∈ (fun p => (p.2, p.1)) ⁻¹' s) ↔
    ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
⊢ (∃ t ∈ g, ∀ᶠ (y : α) in f, ∀ x ∈ t, (x, y) ∈ (fun p => (p.2, p.1)) ⁻¹' s) ↔
    ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem castSucc_ne_zero_of_lt {p i : Fin n} (h : p < i) : castSucc i ≠ 0

Proof state:
case zero
p i : Fin 0
h : p < i
⊢ i.castSucc ≠ 0

Tactic:
exact i.elim0

Result:
no goals

Proof state:
case succ
n✝ : ℕ
p i : Fin (n✝ + 1)
h : p < i
⊢ ¬↑i = ↑0

Tactic:
exact ((zero_le _).trans_lt h).ne'

Result:
no goals

Proof state:
case succ
n✝ : ℕ
p i : Fin (n✝ + 1)
h : p < i
⊢ i.castSucc ≠ 0

Tactic:
rw [castSucc_ne_zero_iff', Ne, Fin.ext_iff]

Result:
case succ
n✝ : ℕ
p i : Fin (n✝ + 1)
h : p < i
⊢ ¬↑i = ↑0

Proof state:
n : ℕ
p i : Fin n
h : p < i
⊢ i.castSucc ≠ 0

Tactic:
cases n

Result:
case zero
p i : Fin 0
h : p < i
⊢ i.castSucc ≠ 0

case succ
n✝ : ℕ
p i : Fin (n✝ + 1)
h : p < i
⊢ i.castSucc ≠ 0
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma coe_basis : (CoordinateRing.basis W : Fin 2 → W.CoordinateRing) = ![1, mk W Y]

Proof state:
case h.«0»
R : Type u
inst✝ : CommRing R
W : Affine R
⊢ (CoordinateRing.basis W) ((fun i => i) ⟨0, ⋯⟩) = ![1, (mk W) Y] ((fun i => i) ⟨0, ⋯⟩)

case h.«1»
R : Type u
inst✝ : CommRing R
W : Affine R
⊢ (CoordinateRing.basis W) ((fun i => i) ⟨1, ⋯⟩) = ![1, (mk W) Y] ((fun i => i) ⟨1, ⋯⟩)

Tactic:
exacts [basis_zero W, basis_one W]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
⊢ ⇑(CoordinateRing.basis W) = ![1, (mk W) Y]

Tactic:
ext n

Result:
case h
R : Type u
inst✝ : CommRing R
W : Affine R
n : Fin 2
⊢ (CoordinateRing.basis W) n = ![1, (mk W) Y] n

Proof state:
case h
R : Type u
inst✝ : CommRing R
W : Affine R
n : Fin 2
⊢ (CoordinateRing.basis W) n = ![1, (mk W) Y] n

Tactic:
fin_cases n

Result:
case h.«0»
R : Type u
inst✝ : CommRing R
W : Affine R
⊢ (CoordinateRing.basis W) ((fun i => i) ⟨0, ⋯⟩) = ![1, (mk W) Y] ((fun i => i) ⟨0, ⋯⟩)

case h.«1»
R : Type u
inst✝ : CommRing R
W : Affine R
⊢ (CoordinateRing.basis W) ((fun i => i) ⟨1, ⋯⟩) = ![1, (mk W) Y] ((fun i => i) ⟨1, ⋯⟩)
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem mem_bot {x : A} : x ∈ (⊥ : NonUnitalSubalgebra R A) ↔ x = 0 :=
  show x ∈ Submodule.span R (NonUnitalSubsemiring.closure (∅ : Set A) : Set A) ↔ x = 0 by
    rw [NonUnitalSubsemiring.closure_empty, NonUnitalSubsemiring.coe_bot,
      Submodule.span_zero_singleton, Submodule.mem_bot]

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
⊢ x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure ∅) ↔ x = 0

Tactic:
rw [NonUnitalSubsemiring.closure_empty, NonUnitalSubsemiring.coe_bot,
  Submodule.span_zero_singleton, Submodule.mem_bot]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bdiv_add_bmod (x : Int) (m : Nat) : m * bdiv x m + bmod x m = x

Proof state:
x : Int
m : Nat
⊢ ↑m * x.bdiv m + x.bmod m = x

Tactic:
unfold bdiv bmod

Result:
x : Int
m : Nat
⊢ ((↑m *
        if m = 0 then 0
        else
          let q := x / ↑m;
          let r := x % ↑m;
          if r < (↑m + 1) / 2 then q else q + 1) +
      let r := x % ↑m;
      if r < (↑m + 1) / 2 then r else r - ↑m) =
    x

Proof state:
case isFalse.isFalse
x : Int
m : Nat
h✝¹ : ¬m = 0
h✝ : ¬x % ↑m < (↑m + 1) / 2
⊢ ↑m * (x / ↑m) + x % ↑m = x

Tactic:
exact ediv_add_emod x m

Result:
no goals

Proof state:
case isFalse.isTrue
x : Int
m : Nat
h✝¹ : ¬m = 0
h✝ : x % ↑m < (↑m + 1) / 2
⊢ ↑m * (x / ↑m) + x % ↑m = x

Tactic:
exact ediv_add_emod x m

Result:
no goals

Proof state:
case isFalse.isFalse
x : Int
m : Nat
h✝¹ : ¬m = 0
h✝ : ¬x % ↑m < (↑m + 1) / 2
⊢ ↑m * (x / ↑m + 1) + (x % ↑m - ↑m) = x

Tactic:
rw [Int.mul_add, Int.mul_one, Int.add_assoc, Int.add_comm m, Int.sub_add_cancel]

Result:
case isFalse.isFalse
x : Int
m : Nat
h✝¹ : ¬m = 0
h✝ : ¬x % ↑m < (↑m + 1) / 2
⊢ ↑m * (x / ↑m) + x % ↑m = x

Proof state:
case isFalse
x : Int
m : Nat
h✝ : ¬m = 0
⊢ ((↑m *
        let q := x / ↑m;
        let r := x % ↑m;
        if r < (↑m + 1) / 2 then q else q + 1) +
      let r := x % ↑m;
      if r < (↑m + 1) / 2 then r else r - ↑m) =
    x

Tactic:
dsimp only

Result:
case isFalse
x : Int
m : Nat
h✝ : ¬m = 0
⊢ ((↑m * if x % ↑m < (↑m + 1) / 2 then x / ↑m else x / ↑m + 1) +
      if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m) =
    x

Proof state:
case isFalse
x : Int
m : Nat
h✝ : ¬m = 0
⊢ ((↑m * if x % ↑m < (↑m + 1) / 2 then x / ↑m else x / ↑m + 1) +
      if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m) =
    x

Tactic:
split

Result:
case isFalse.isTrue
x : Int
m : Nat
h✝¹ : ¬m = 0
h✝ : x % ↑m < (↑m + 1) / 2
⊢ ↑m * (x / ↑m) + x % ↑m = x

case isFalse.isFalse
x : Int
m : Nat
h✝¹ : ¬m = 0
h✝ : ¬x % ↑m < (↑m + 1) / 2
⊢ ↑m * (x / ↑m + 1) + (x % ↑m - ↑m) = x

Proof state:
case isTrue
x : Int
m : Nat
h✝ : m = 0
⊢ (↑m * 0 +
      let r := x % ↑m;
      if r < (↑m + 1) / 2 then r else r - ↑m) =
    x

Tactic:
simp_all only [Nat.cast_ofNat_Int, Int.mul_zero, emod_zero, Int.zero_add, Int.sub_zero,
  ite_self]

Result:
no goals

Proof state:
x : Int
m : Nat
⊢ ((↑m *
        if m = 0 then 0
        else
          let q := x / ↑m;
          let r := x % ↑m;
          if r < (↑m + 1) / 2 then q else q + 1) +
      let r := x % ↑m;
      if r < (↑m + 1) / 2 then r else r - ↑m) =
    x

Tactic:
split

Result:
case isTrue
x : Int
m : Nat
h✝ : m = 0
⊢ (↑m * 0 +
      let r := x % ↑m;
      if r < (↑m + 1) / 2 then r else r - ↑m) =
    x

case isFalse
x : Int
m : Nat
h✝ : ¬m = 0
⊢ ((↑m *
        let q := x / ↑m;
        let r := x % ↑m;
        if r < (↑m + 1) / 2 then q else q + 1) +
      let r := x % ↑m;
      if r < (↑m + 1) / 2 then r else r - ↑m) =
    x
-- Mathlib/Order/Antichain.lean
/-- A set which is simultaneously a chain and antichain is subsingleton. -/
lemma subsingleton_of_isChain_of_isAntichain (hs : IsChain r s) (ht : IsAntichain r s) :
    s.Subsingleton

Proof state:
case inl
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hne : x ≠ y
h : r x y
⊢ False

Tactic:
exact ht hx hy hne h

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hne : x ≠ y
⊢ False

Tactic:
cases hs hx hy hne with
| inl h => exact ht hx hy hne h
| inr h => exact ht hy hx hne.symm h

Result:
no goals

Proof state:
case inr
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hne : x ≠ y
h : r y x
⊢ False

Tactic:
exact ht hy hx hne.symm h

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
⊢ s.Subsingleton

Tactic:
intro x hx y hy

Result:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ x = y

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ x = y

Tactic:
by_contra! hne

Result:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hne : x ≠ y
⊢ False
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeriesHasSum.add {f g : ℕ → ℂ} {s a b : ℂ} (hf : LSeriesHasSum f s a)
    (hg : LSeriesHasSum g s b) :
    LSeriesHasSum (f + g) s (a + b)

Proof state:
f g : ℕ → ℂ
s a b : ℂ
hf : LSeriesHasSum f s a
hg : LSeriesHasSum g s b
⊢ LSeriesHasSum (f + g) s (a + b)

Tactic:
simpa [LSeriesHasSum, term_add] using HasSum.add hf hg

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DoubleCounting.lean
theorem sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow [∀ a b, Decidable (r a b)] :
    (∑ a ∈ s, #(t.bipartiteAbove r a)) = ∑ b ∈ t, #(s.bipartiteBelow r b)

Proof state:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst✝ : (a : α) → (b : β) → Decidable (r a b)
⊢ ∑ a ∈ s, #(bipartiteAbove r t a) = ∑ b ∈ t, #(bipartiteBelow r s b)

Tactic:
simp_rw [card_eq_sum_ones, sum_sum_bipartiteAbove_eq_sum_sum_bipartiteBelow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem zero_concat_true : concat 0#w true = 1#(w + 1)

Proof state:
case pred
w i✝ : Nat
a✝ : i✝ < w + 1
⊢ ((0#w).concat true).getLsbD i✝ = (1#(w + 1)).getLsbD i✝

Tactic:
simp [getLsbD_concat]

Result:
no goals

Proof state:
w : Nat
⊢ (0#w).concat true = 1#(w + 1)

Tactic:
ext

Result:
case pred
w i✝ : Nat
a✝ : i✝ < w + 1
⊢ ((0#w).concat true).getLsbD i✝ = (1#(w + 1)).getLsbD i✝
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive]
lemma finEquivZPowers_symm_apply (x : G) (hx) (n : ℕ) :
    (finEquivZPowers x hx).symm ⟨x ^ n, ⟨n, by simp⟩⟩ =
    ⟨n % orderOf x, Nat.mod_lt _ hx.orderOf_pos⟩

Proof state:
G : Type u_1
inst✝ : Group G
x : G
hx : IsOfFinOrder x
n : ℕ
⊢ (finEquivPowers x hx).symm ((Equiv.Set.ofEq ⋯).symm ⟨x ^ n, ⋯⟩) = ⟨n % orderOf x, ⋯⟩

Tactic:
exact finEquivPowers_symm_apply x _ n

Result:
no goals

Proof state:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x✝ y : G
i : ℤ
x : G
hx : IsOfFinOrder x
n : ℕ
⊢ (fun x_1 => x ^ x_1) ↑n = x ^ n

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
x : G
hx : IsOfFinOrder x
n : ℕ
⊢ (finEquivZPowers x hx).symm ⟨x ^ n, ⋯⟩ = ⟨n % orderOf x, ⋯⟩

Tactic:
rw [finEquivZPowers, Equiv.symm_trans_apply]

Result:
G : Type u_1
inst✝ : Group G
x : G
hx : IsOfFinOrder x
n : ℕ
⊢ (finEquivPowers x hx).symm ((Equiv.Set.ofEq ⋯).symm ⟨x ^ n, ⋯⟩) = ⟨n % orderOf x, ⋯⟩
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
    m.1.keys.isEmpty = m.1.isEmpty

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
⊢ m.val.keys.isEmpty = m.val.isEmpty

Tactic:
simp_to_model using List.isEmpty_keys_eq_isEmpty

Result:
no goals
-- Mathlib/Topology/FiberBundle/Basic.lean
theorem mem_localTrivAsPartialEquiv_target (p : B × F) :
    p ∈ (Z.localTrivAsPartialEquiv i).target ↔ p.1 ∈ Z.baseSet i

Proof state:
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
p : B × F
⊢ p.1 ∈ Z.baseSet i ∧ p.2 ∈ univ ↔ p.1 ∈ Z.baseSet i

Tactic:
simp only [and_true, mem_univ]

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
i : ι
p : B × F
⊢ p ∈ (Z.localTrivAsPartialEquiv i).target ↔ p.1 ∈ Z.baseSet i

Tactic:
erw [mem_prod]

Result:
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
p : B × F
⊢ p.1 ∈ Z.baseSet i ∧ p.2 ∈ univ ↔ p.1 ∈ Z.baseSet i
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem neg_sub' {X Y : C} (a b : X ⟶ Y) : -(a - b) = -a + b

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ -(a - b) = -a + b

Tactic:
rw [neg_def, neg_def]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - (a - b) = 0 - a + b

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - 0 - (a - b) = 0 - a + b

Tactic:
rw [sub_sub_sub, add_def, neg_def]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - (a - b) = 0 - a + b

Tactic:
conv_lhs => rw [← sub_self (0 : X ⟶ Y)]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - 0 - (a - b) = 0 - a + b
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_at_ofNat {S : Type*} [Semiring S] (f : R →+* S) (n : ℕ) [n.AtLeastTwo] :
    p.eval₂ f ofNat(n) = f (p.eval (ofNat(n)))

Proof state:
R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
f : R →+* S
n : ℕ
inst✝ : n.AtLeastTwo
⊢ eval₂ f (OfNat.ofNat n) p = f (eval (OfNat.ofNat n) p)

Tactic:
simp [OfNat.ofNat]

Result:
no goals
-- Mathlib/Algebra/Order/Module/OrderedSMul.lean
lemma sup_eq_half_smul_add_add_abs_sub (x y : β) : x ⊔ y = (⅟2 : α) • (x + y + |y - x|)

Proof state:
α : Type u_6
β : Type u_7
inst✝⁵ : Semiring α
inst✝⁴ : Invertible 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : AddLeftMono β
x y : β
⊢ x ⊔ y = ⅟2 • (x + y + |y - x|)

Tactic:
rw [← two_nsmul_sup_eq_add_add_abs_sub x y, two_smul, ← two_smul α,
  smul_smul, invOf_mul_self, one_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/DecidableEq.lean
theorem eq_of_isEqv [DecidableEq α] (a b : Array α) (h : Array.isEqv a b (fun x y => x = y)) : a = b

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h : (a.isEqv b fun x y => decide (x = y)) = true
⊢ a = b

Tactic:
have ⟨h, h'⟩ := rel_of_isEqv h

Result:
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h✝ : (a.isEqv b fun x y => decide (x = y)) = true
h : a.size = b.size
h' : ∀ (i : Nat) (h' : i < a.size), decide (a[i] = b[i]) = true
⊢ a = b

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h✝ : (a.isEqv b fun x y => decide (x = y)) = true
h : a.size = b.size
h' : ∀ (i : Nat) (h' : i < a.size), decide (a[i] = b[i]) = true
i : Nat
lt : i < a.size
x✝ : i < b.size
⊢ a[i] = b[i]

Tactic:
simpa using h' i lt

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h✝ : (a.isEqv b fun x y => decide (x = y)) = true
h : a.size = b.size
h' : ∀ (i : Nat) (h' : i < a.size), decide (a[i] = b[i]) = true
⊢ a = b

Tactic:
exact ext _ _ h (fun i lt _ => by simpa using h' i lt)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem isEmpty_eq_true {l : List α} : l.isEmpty ↔ l = []

Proof state:
α : Type u_1
l : List α
⊢ l.isEmpty = true ↔ l = []

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem Function.Surjective.pathConnectedSpace [PathConnectedSpace X]
    {f : X → Y} (hf : Surjective f) (hf' : Continuous f) : PathConnectedSpace Y

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
hf : Surjective f
hf' : Continuous f
⊢ IsPathConnected (range f)

Tactic:
exact isPathConnected_range hf'

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
hf : Surjective f
hf' : Continuous f
⊢ PathConnectedSpace Y

Tactic:
rw [pathConnectedSpace_iff_univ, ← hf.range_eq]

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
hf : Surjective f
hf' : Continuous f
⊢ IsPathConnected (range f)
-- Mathlib/CategoryTheory/Localization/SmallHom.lean
lemma hasSmallLocalizedHom_of_isLocalization :
    HasSmallLocalizedHom.{v₂} W X Y

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
⊢ Small.{v₂, v₂} (L.obj X ⟶ L.obj Y)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
⊢ HasSmallLocalizedHom W X Y

Tactic:
rw [hasSmallLocalizedHom_iff W L]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
⊢ Small.{v₂, v₂} (L.obj X ⟶ L.obj Y)