harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem toSubalgebra_iSup_of_directed (dir : Directed (· ≤ ·) t) :
    (iSup t).toSubalgebra = ⨆ i, (t i).toSubalgebra

Proof state:
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
dir : Directed (fun x1 x2 => x1 ≤ x2) t
⊢ (iSup t).toSubalgebra = ⨆ i, (t i).toSubalgebra

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
dir : Directed (fun x1 x2 => x1 ≤ x2) t
h✝ : IsEmpty ι
⊢ (iSup t).toSubalgebra = ⨆ i, (t i).toSubalgebra

case inr
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
dir : Directed (fun x1 x2 => x1 ≤ x2) t
h✝ : Nonempty ι
⊢ (iSup t).toSubalgebra = ⨆ i, (t i).toSubalgebra

Proof state:
case inr
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
dir : Directed (fun x1 x2 => x1 ≤ x2) t
h✝ : Nonempty ι
⊢ (iSup t).toSubalgebra = ⨆ i, (t i).toSubalgebra

Tactic:
exact SetLike.ext' ((coe_iSup_of_directed dir).trans (Subalgebra.coe_iSup_of_directed dir).symm)

Result:
no goals

Proof state:
case inl
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
dir : Directed (fun x1 x2 => x1 ≤ x2) t
h✝ : IsEmpty ι
⊢ (iSup t).toSubalgebra = ⨆ i, (t i).toSubalgebra

Tactic:
simp_rw [iSup_of_empty, bot_toSubalgebra]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.not_mem_closure_iff_of_not_mem (hI : M.Indep I) (heI : e ∉ I)
    (he : e ∈ M.E

Proof state:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
he : autoParam (e ∈ M.E) _auto✝
⊢ e ∉ M.closure I ↔ M.Indep (insert e I)

Tactic:
rw [hI.not_mem_closure_iff, and_iff_left heI]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthInf_le_of_eventually_le {u v : ℕ → ℝ≥0∞} {C : ℝ≥0∞} (hC : C ≠ ∞)
    (h : ∀ᶠ n in atTop, u n ≤ C * v n) :
    expGrowthInf u ≤ expGrowthInf v

Proof state:
u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
C_pos : 0 < C
⊢ 0 ≠ ⊥ ∨ expGrowthInf v ≠ ⊤

Tactic:
exact Or.inl EReal.zero_ne_bot

Result:
no goals

Proof state:
u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
⊢ (expGrowthInf fun x => C * v x) ≤ expGrowthInf v

Tactic:
rcases eq_zero_or_pos C with rfl | C_pos

Result:
case inl
u v : ℕ → ℝ≥0∞
hC : 0 ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0 * v n
⊢ (expGrowthInf fun x => 0 * v x) ≤ expGrowthInf v

case inr
u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
C_pos : 0 < C
⊢ (expGrowthInf fun x => C * v x) ≤ expGrowthInf v

Proof state:
case inr
u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
C_pos : 0 < C
⊢ 0 + expGrowthInf v = expGrowthInf v

Tactic:
exact zero_add (expGrowthInf v)

Result:
no goals

Proof state:
u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
C_pos : 0 < C
⊢ 0 ≠ ⊤ ∨ expGrowthInf v ≠ ⊥

Tactic:
exact Or.inl EReal.zero_ne_top

Result:
no goals

Proof state:
case inr
u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
C_pos : 0 < C
⊢ (expGrowthInf fun x => C * v x) ≤ expGrowthInf v

Tactic:
apply (expGrowthInf_mul_le _ _).trans_eq <;> rw [expGrowthSup_const C_pos.ne' hC]

Result:
case inr
u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
C_pos : 0 < C
⊢ 0 + expGrowthInf v = expGrowthInf v

u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
C_pos : 0 < C
⊢ 0 ≠ ⊥ ∨ expGrowthInf v ≠ ⊤

u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
C_pos : 0 < C
⊢ 0 ≠ ⊤ ∨ expGrowthInf v ≠ ⊥

Proof state:
u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
⊢ expGrowthInf u ≤ expGrowthInf v

Tactic:
apply (expGrowthInf_eventually_monotone h).trans

Result:
u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
⊢ (expGrowthInf fun x => C * v x) ≤ expGrowthInf v

Proof state:
case inl
u v : ℕ → ℝ≥0∞
hC : 0 ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0 * v n
⊢ (expGrowthInf fun x => 0 * v x) ≤ expGrowthInf v

Tactic:
simp only [zero_mul, ← Pi.zero_def, expGrowthInf_zero, bot_le]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem continuous_of_bound (f : MultilinearMap 𝕜 E G) (C : ℝ) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) :
    Continuous f

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
D : ℝ := C ⊔ 1
D_pos : 0 ≤ D
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ D * ∏ i : ι, ‖m i‖
m m' : (i : ι) → E i
h' : dist m' m < 1
this : ‖m'‖ ⊔ ‖m‖ ≤ ‖m‖ + 1
⊢ ‖f m' - f m‖ ≤ D * ↑(Fintype.card ι) * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖

Tactic:
calc
  ‖f m' - f m‖ ≤ D * Fintype.card ι * max ‖m'‖ ‖m‖ ^ (Fintype.card ι - 1) * ‖m' - m‖ :=
    f.norm_image_sub_le_of_bound D_pos H m' m
  _ ≤ D * Fintype.card ι * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖ := by gcongr

Result:
no goals

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
D : ℝ := C ⊔ 1
⊢ Continuous ⇑f

Tactic:
have D_pos : 0 ≤ D := le_trans zero_le_one (le_max_right _ _)

Result:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
D : ℝ := C ⊔ 1
D_pos : 0 ≤ D
⊢ Continuous ⇑f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem reverse_eq_push_iff {xs : Vector α (n + 1)} {ys : Vector α n} {a : α} :
    xs.reverse = ys.push a ↔ xs = (#v[a] ++ ys.reverse).cast (by omega)

Proof state:
α : Type ?u.359142
n : Nat
xs : Vector α (n + 1)
ys : Vector α n
a : α
⊢ 1 + n = n + 1

Tactic:
omega

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
a : α
xs ys : Array α
h : xs.size = ys.size + 1
⊢ { toArray := xs, size_toArray := h }.reverse = { toArray := ys, size_toArray := ⋯ }.push a ↔
    { toArray := xs, size_toArray := h } =
      Vector.cast ⋯ ({ toArray := #[a], size_toArray := ⋯ } ++ { toArray := ys, size_toArray := ⋯ }.reverse)

Tactic:
simp [Array.reverse_eq_push_iff]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
xs : Vector α (n + 1)
ys : Vector α n
a : α
⊢ xs.reverse = ys.push a ↔ xs = Vector.cast ⋯ ({ toArray := #[a], size_toArray := ⋯ } ++ ys.reverse)

Tactic:
rcases xs with ⟨xs, h⟩

Result:
case mk
α : Type u_1
n : Nat
ys : Vector α n
a : α
xs : Array α
h : xs.size = n + 1
⊢ { toArray := xs, size_toArray := h }.reverse = ys.push a ↔
    { toArray := xs, size_toArray := h } = Vector.cast ⋯ ({ toArray := #[a], size_toArray := ⋯ } ++ ys.reverse)

Proof state:
case mk
α : Type u_1
n : Nat
ys : Vector α n
a : α
xs : Array α
h : xs.size = n + 1
⊢ { toArray := xs, size_toArray := h }.reverse = ys.push a ↔
    { toArray := xs, size_toArray := h } = Vector.cast ⋯ ({ toArray := #[a], size_toArray := ⋯ } ++ ys.reverse)

Tactic:
rcases ys with ⟨ys, rfl⟩

Result:
case mk.mk
α : Type u_1
a : α
xs ys : Array α
h : xs.size = ys.size + 1
⊢ { toArray := xs, size_toArray := h }.reverse = { toArray := ys, size_toArray := ⋯ }.push a ↔
    { toArray := xs, size_toArray := h } =
      Vector.cast ⋯ ({ toArray := #[a], size_toArray := ⋯ } ++ { toArray := ys, size_toArray := ⋯ }.reverse)
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem alternatingProd_eq_finset_prod {G : Type*} [CommGroup G] :
    ∀ (L : List G), alternatingProd L = ∏ i : Fin L.length, L[i] ^ (-1 : ℤ) ^ (i : ℕ)
  | [] => by
    rw [alternatingProd, Finset.prod_eq_one]
    rintro ⟨i, ⟨⟩⟩
  | g::[] => by
    show g = ∏ i : Fin 1, [g][i] ^ (-1 : ℤ) ^ (i : ℕ)
    rw [Fin.prod_univ_succ]; simp
  | g::h::L =>
    calc g * h⁻¹ * L.alternatingProd
      = g * h⁻¹ * ∏ i : Fin L.length, L[i] ^ (-1 : ℤ) ^ (i : ℕ) :=
        congr_arg _ (alternatingProd_eq_finset_prod _)
    _ = ∏ i : Fin (L.length + 2), (g::h::L)[i] ^ (-1 : ℤ) ^ (i : ℕ)

Proof state:
G : Type u_3
inst✝ : CommGroup G
g : G
⊢ g = [g][0] ^ (-1) ^ ↑0 * ∏ i : Fin 0, [g][i.succ] ^ (-1) ^ ↑i.succ

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_3
inst✝ : CommGroup G
g : G
⊢ [g].alternatingProd = ∏ i : Fin [g].length, [g][i] ^ (-1) ^ ↑i

Tactic:
show g = ∏ i : Fin 1, [g][i] ^ (-1 : ℤ) ^ (i : ℕ)

Result:
G : Type u_3
inst✝ : CommGroup G
g : G
⊢ g = ∏ i : Fin 1, [g][i] ^ (-1) ^ ↑i

Proof state:
G : Type u_3
inst✝ : CommGroup G
g : G
⊢ g = ∏ i : Fin 1, [g][i] ^ (-1) ^ ↑i

Tactic:
rw [Fin.prod_univ_succ]

Result:
G : Type u_3
inst✝ : CommGroup G
g : G
⊢ g = [g][0] ^ (-1) ^ ↑0 * ∏ i : Fin 0, [g][i.succ] ^ (-1) ^ ↑i.succ

Proof state:
G : Type u_3
inst✝ : CommGroup G
⊢ ∀ x ∈ univ, [][x] ^ (-1) ^ ↑x = 1

Tactic:
rintro ⟨i, ⟨⟩⟩

Result:
no goals

Proof state:
G : Type u_3
inst✝ : CommGroup G
⊢ [].alternatingProd = ∏ i : Fin [].length, [][i] ^ (-1) ^ ↑i

Tactic:
rw [alternatingProd, Finset.prod_eq_one]

Result:
G : Type u_3
inst✝ : CommGroup G
⊢ ∀ x ∈ univ, [][x] ^ (-1) ^ ↑x = 1

Proof state:
G : Type u_3
inst✝ : CommGroup G
g h : G
L : List G
⊢ g * h⁻¹ * ∏ i : Fin L.length, L[i] ^ (-1) ^ ↑i = ∏ i : Fin (L.length + 2), (g :: h :: L)[i] ^ (-1) ^ ↑i

Tactic:
rw [Fin.prod_univ_succ, Fin.prod_univ_succ, mul_assoc]

Result:
G : Type u_3
inst✝ : CommGroup G
g h : G
L : List G
⊢ g * (h⁻¹ * ∏ i : Fin L.length, L[i] ^ (-1) ^ ↑i) =
    (g :: h :: L)[0] ^ (-1) ^ ↑0 *
      ((g :: h :: L)[Fin.succ 0] ^ (-1) ^ ↑(Fin.succ 0) *
        ∏ i : Fin L.length, (g :: h :: L)[i.succ.succ] ^ (-1) ^ ↑i.succ.succ)

Proof state:
G : Type u_3
inst✝ : CommGroup G
g h : G
L : List G
⊢ g * (h⁻¹ * ∏ i : Fin L.length, L[i] ^ (-1) ^ ↑i) =
    (g :: h :: L)[0] ^ (-1) ^ ↑0 *
      ((g :: h :: L)[Fin.succ 0] ^ (-1) ^ ↑(Fin.succ 0) *
        ∏ i : Fin L.length, (g :: h :: L)[i.succ.succ] ^ (-1) ^ ↑i.succ.succ)

Tactic:
simp [pow_add]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem ite_tmul (x₁ : M) (x₂ : N) (P : Prop) [Decidable P] :
    (if P then x₁ else 0) ⊗ₜ[R] x₂ = if P then x₁ ⊗ₜ x₂ else 0

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
x₁ : M
x₂ : N
P : Prop
inst✝ : Decidable P
⊢ (if P then x₁ else 0) ⊗ₜ[R] x₂ = if P then x₁ ⊗ₜ[R] x₂ else 0

Tactic:
split_ifs <;> simp

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem segment_subset_Icc (h : x ≤ y) : [x -[𝕜] y] ⊆ Icc x y

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ Icc x y

Tactic:
constructor

Result:
case intro.intro.intro.intro.intro.left
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ x ≤ a • x + b • y

case intro.intro.intro.intro.intro.right
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ≤ y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • x ≤ a • x + b • y

Tactic:
gcongr

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.right
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ≤ y

Tactic:
calc
  a • x + b • y ≤ a • y + b • y := by gcongr
  _ = y := Convex.combo_self hab _

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.left
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ x ≤ a • x + b • y

Tactic:
calc
  x = a • x + b • x := (Convex.combo_self hab _).symm
  _ ≤ a • x + b • y := by gcongr

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ≤ a • y + b • y

Tactic:
gcongr

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
⊢ [x-[𝕜]y] ⊆ Icc x y

Tactic:
rintro z ⟨a, b, ha, hb, hab, rfl⟩

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ Icc x y
-- Mathlib/Analysis/SpecialFunctions/Stirling.lean
theorem stirlingSeq_zero : stirlingSeq 0 = 0

Proof state:
⊢ stirlingSeq 0 = 0

Tactic:
rw [stirlingSeq, cast_zero, mul_zero, Real.sqrt_zero, zero_mul, div_zero]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem fromEdgeSet_mono {s t : Set (Sym2 V)} (h : s ⊆ t) : fromEdgeSet s ≤ fromEdgeSet t

Proof state:
V : Type u
s t : Set (Sym2 V)
h : s ⊆ t
v w : V
⊢ (fromEdgeSet s).Adj v w → (fromEdgeSet t).Adj v w

Tactic:
simp +contextual only [fromEdgeSet_adj, Ne, not_false_iff,
  and_true, and_imp]

Result:
V : Type u
s t : Set (Sym2 V)
h : s ⊆ t
v w : V
⊢ s(v, w) ∈ s → ¬v = w → s(v, w) ∈ t

Proof state:
V : Type u
s t : Set (Sym2 V)
h : s ⊆ t
⊢ fromEdgeSet s ≤ fromEdgeSet t

Tactic:
rintro v w

Result:
V : Type u
s t : Set (Sym2 V)
h : s ⊆ t
v w : V
⊢ (fromEdgeSet s).Adj v w → (fromEdgeSet t).Adj v w

Proof state:
V : Type u
s t : Set (Sym2 V)
h : s ⊆ t
v w : V
⊢ s(v, w) ∈ s → ¬v = w → s(v, w) ∈ t

Tactic:
exact fun vws _ => h vws

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem coe_splitUpper : (splitUpper I i x : Set (ι → ℝ)) = ↑I ∩ { y | x < y i }

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ ↑(I.splitUpper i x) = ↑I ∩ {y | x < y i}

Tactic:
classical
rw [splitUpper, coe_mk']
ext y
simp only [mem_univ_pi, mem_Ioc, mem_inter_iff, mem_coe, mem_setOf_eq, forall_and,
  forall_update_iff I.lower fun j z => z < y j, max_lt_iff, and_assoc (a := x < y i),
  and_forall_ne (p := fun j => lower I j < y j) i, mem_def]
exact and_comm

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ ↑(I.splitUpper i x) = ↑I ∩ {y | x < y i}

Tactic:
rw [splitUpper, coe_mk']

Result:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (univ.pi fun i_1 => Ioc (update I.lower i (x ⊔ I.lower i) i_1) (I.upper i_1)) = ↑I ∩ {y | x < y i}

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (univ.pi fun i_1 => Ioc (update I.lower i (x ⊔ I.lower i) i_1) (I.upper i_1)) = ↑I ∩ {y | x < y i}

Tactic:
ext y

Result:
case h
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ (y ∈ univ.pi fun i_1 => Ioc (update I.lower i (x ⊔ I.lower i) i_1) (I.upper i_1)) ↔ y ∈ ↑I ∩ {y | x < y i}

Proof state:
case h
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ (x < y i ∧ (∀ (b : ι), I.lower b < y b) ∧ ∀ (x : ι), y x ≤ I.upper x) ↔
    ((∀ (x : ι), I.lower x < y x) ∧ ∀ (x : ι), y x ≤ I.upper x) ∧ x < y i

Tactic:
exact and_comm

Result:
no goals

Proof state:
case h
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ (y ∈ univ.pi fun i_1 => Ioc (update I.lower i (x ⊔ I.lower i) i_1) (I.upper i_1)) ↔ y ∈ ↑I ∩ {y | x < y i}

Tactic:
simp only [mem_univ_pi, mem_Ioc, mem_inter_iff, mem_coe, mem_setOf_eq, forall_and,
  forall_update_iff I.lower fun j z => z < y j, max_lt_iff, and_assoc (a := x < y i),
  and_forall_ne (p := fun j => lower I j < y j) i, mem_def]

Result:
case h
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ (x < y i ∧ (∀ (b : ι), I.lower b < y b) ∧ ∀ (x : ι), y x ≤ I.upper x) ↔
    ((∀ (x : ι), I.lower x < y x) ∧ ∀ (x : ι), y x ≤ I.upper x) ∧ x < y i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem unattach_reverse {p : α → Prop} {l : Array { x // p x }} :
    l.reverse.unattach = l.unattach.reverse

Proof state:
α : Type u_1
p : α → Prop
l : Array { x // p x }
⊢ l.reverse.unattach = l.unattach.reverse

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Prop
toList✝ : List { x // p x }
⊢ { toList := toList✝ }.reverse.unattach = { toList := toList✝ }.unattach.reverse

Proof state:
case mk
α : Type u_1
p : α → Prop
toList✝ : List { x // p x }
⊢ { toList := toList✝ }.reverse.unattach = { toList := toList✝ }.unattach.reverse

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/CharP/Algebra.lean
theorem Algebra.ringChar_eq : ringChar K = ringChar L

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommSemiring L
inst✝¹ : Nontrivial L
inst✝ : Algebra K L
⊢ ringChar K = ringChar L

Tactic:
rw [ringChar.eq_iff, Algebra.charP_iff K L]

Result:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommSemiring L
inst✝¹ : Nontrivial L
inst✝ : Algebra K L
⊢ CharP L (ringChar L)

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommSemiring L
inst✝¹ : Nontrivial L
inst✝ : Algebra K L
⊢ CharP L (ringChar L)

Tactic:
apply ringChar.charP

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem getKey!ₘ_eq_getKey! [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α]
    {m : Raw₀ α β} (hm : Raw.WFImp m.1) {a : α} :
    m.getKey!ₘ a = List.getKey! a (toListModel m.1.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
⊢ m.getKey!ₘ a = List.getKey! a (toListModel m.val.buckets)

Tactic:
rw [getKey!ₘ, getKey?ₘ_eq_getKey? hm, List.getKey!_eq_getKey?]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat

Proof state:
w : Nat
x : BitVec w
⊢ (if x.msb = true then -x else x).toNat = if x.msb = true then 2 ^ w - x.toNat else x.toNat

Tactic:
by_cases h : x.msb = true

Result:
case pos
w : Nat
x : BitVec w
h : x.msb = true
⊢ (if x.msb = true then -x else x).toNat = if x.msb = true then 2 ^ w - x.toNat else x.toNat

case neg
w : Nat
x : BitVec w
h : ¬x.msb = true
⊢ (if x.msb = true then -x else x).toNat = if x.msb = true then 2 ^ w - x.toNat else x.toNat

Proof state:
case pos
w : Nat
x : BitVec w
h : x.msb = true
⊢ (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat

Tactic:
have : 2 * x.toNat ≥ 2 ^ w := BitVec.msb_eq_true_iff_two_mul_ge.mp h

Result:
case pos
w : Nat
x : BitVec w
h : x.msb = true
this : 2 * x.toNat ≥ 2 ^ w
⊢ (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat

Proof state:
w : Nat
x : BitVec w
h : x.msb = true
this : 2 * x.toNat ≥ 2 ^ w
⊢ 2 ^ w - x.toNat < 2 ^ w

Tactic:
omega

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
h : ¬x.msb = true
⊢ (if x.msb = true then -x else x).toNat = if x.msb = true then 2 ^ w - x.toNat else x.toNat

Tactic:
simp [h]

Result:
no goals

Proof state:
case pos
w : Nat
x : BitVec w
h : x.msb = true
⊢ (if x.msb = true then -x else x).toNat = if x.msb = true then 2 ^ w - x.toNat else x.toNat

Tactic:
simp only [h, ↓reduceIte, toNat_neg]

Result:
case pos
w : Nat
x : BitVec w
h : x.msb = true
⊢ (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat

Proof state:
w : Nat
x : BitVec w
⊢ x.abs.toNat = if x.msb = true then 2 ^ w - x.toNat else x.toNat

Tactic:
simp only [BitVec.abs, neg_eq]

Result:
w : Nat
x : BitVec w
⊢ (if x.msb = true then -x else x).toNat = if x.msb = true then 2 ^ w - x.toNat else x.toNat

Proof state:
case pos
w : Nat
x : BitVec w
h : x.msb = true
this : 2 * x.toNat ≥ 2 ^ w
⊢ (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat

Tactic:
rw [Nat.mod_eq_of_lt (by omega)]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
lemma isZero₃_iff_isIso₁ : IsZero T.obj₃ ↔ IsIso T.mor₁

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ IsZero T.obj₃ ↔ IsIso T.mor₁

Tactic:
refine Iff.trans ?_ (Triangle.isZero₁_iff_isIso₂ _ (inv_rot_of_distTriang _ hT))

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ IsZero T.obj₃ ↔ IsZero T.invRotate.obj₁

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ IsZero T.obj₃ ↔ IsZero ((CategoryTheory.shiftFunctor C (-1)).obj T.obj₃)

Tactic:
simp only [IsZero.iff_id_eq_zero, ← Functor.map_id, Functor.map_eq_zero_iff]

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ IsZero T.obj₃ ↔ IsZero T.invRotate.obj₁

Tactic:
dsimp

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ IsZero T.obj₃ ↔ IsZero ((CategoryTheory.shiftFunctor C (-1)).obj T.obj₃)
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem next_nat_zero : (ComplexShape.down ℕ).next 0 = 0

Proof state:
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
classical
  refine dif_neg ?_
  push_neg
  intro
  apply Nat.noConfusion

Result:
no goals

Proof state:
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
refine dif_neg ?_

Result:
⊢ ¬∃ j, (ComplexShape.down ℕ).Rel 0 j

Proof state:
⊢ ∀ (j : ℕ), ¬(ComplexShape.down ℕ).Rel 0 j

Tactic:
intro

Result:
j✝ : ℕ
⊢ ¬(ComplexShape.down ℕ).Rel 0 j✝

Proof state:
j✝ : ℕ
⊢ ¬(ComplexShape.down ℕ).Rel 0 j✝

Tactic:
apply Nat.noConfusion

Result:
no goals

Proof state:
⊢ ¬∃ j, (ComplexShape.down ℕ).Rel 0 j

Tactic:
push_neg

Result:
⊢ ∀ (j : ℕ), ¬(ComplexShape.down ℕ).Rel 0 j