harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem All.ins {x : α} {t : RBNode α}
  (h₁ : p x) (h₂ : t.All p) : (ins cmp x t).All p

Proof state:
α : Type u_1
p : α → Prop
cmp : α → α → Ordering
x : α
t : RBNode α
h₁ : p x
h₂ : All p t
⊢ All p (ins cmp x t)

Tactic:
induction t <;> unfold ins <;> try simp [*]

Result:
case node
α : Type u_1
p : α → Prop
cmp : α → α → Ordering
x : α
h₁ : p x
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : All p l✝ → All p (ins cmp x l✝)
r_ih✝ : All p r✝ → All p (ins cmp x r✝)
h₂ : All p (node c✝ l✝ v✝ r✝)
⊢ All p
    (match node c✝ l✝ v✝ r✝ with
    | nil => node red nil x nil
    | node red a y b =>
      match cmp x y with
      | Ordering.lt => node red (ins cmp x a) y b
      | Ordering.gt => node red a y (ins cmp x b)
      | Ordering.eq => node red a x b
    | node black a y b =>
      match cmp x y with
      | Ordering.lt => (ins cmp x a).balance1 y b
      | Ordering.gt => a.balance2 y (ins cmp x b)
      | Ordering.eq => node black a x b)

Proof state:
case node
α : Type u_1
p : α → Prop
cmp : α → α → Ordering
x : α
h₁ : p x
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : All p l✝ → All p (ins cmp x l✝)
r_ih✝ : All p r✝ → All p (ins cmp x r✝)
h₂ : All p (node c✝ l✝ v✝ r✝)
⊢ All p
    (match node c✝ l✝ v✝ r✝ with
    | nil => node red nil x nil
    | node red a y b =>
      match cmp x y with
      | Ordering.lt => node red (ins cmp x a) y b
      | Ordering.gt => node red a y (ins cmp x b)
      | Ordering.eq => node red a x b
    | node black a y b =>
      match cmp x y with
      | Ordering.lt => (ins cmp x a).balance1 y b
      | Ordering.gt => a.balance2 y (ins cmp x b)
      | Ordering.eq => node black a x b)

Tactic:
split <;> cases ‹_=_› <;> split <;> simp at h₂ <;> simp [*]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Prop
cmp : α → α → Ordering
x : α
h₁ : p x
h₂ : All p nil
⊢ All p (node red nil x nil)

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem single_apply_mem (x) : single a b x ∈ ({0, b} : Set M)

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
x : α
⊢ (single a b) x ∈ {0, b}

Tactic:
rcases em (a = x) with (rfl | hx) <;> [simp; simp [single_eq_of_ne hx]]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem himp_eq_top_iff : a ⇨ b = ⊤ ↔ a ≤ b

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⇨ b = ⊤ ↔ a ≤ b

Tactic:
rw [← top_le_iff, le_himp_iff, top_inf_eq]

Result:
no goals
-- Mathlib/Data/DFinsupp/WellFounded.lean
theorem Lex.acc_of_single_erase [DecidableEq ι] {x : Π₀ i, α i} (i : ι)
    (hs : Acc (DFinsupp.Lex r s) <| single i (x i)) (hu : Acc (DFinsupp.Lex r s) <| x.erase i) :
    Acc (DFinsupp.Lex r s) x

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (DFinsupp.Lex r s) (single i (x i))
hu : Acc (DFinsupp.Lex r s) (erase i x)
⊢ Acc (DFinsupp.Lex r s) x

Tactic:
convert ← @Acc.of_fibration _ _ _ _ _ (lex_fibration r s) ⟨{i}, _⟩
  (InvImage.accessible snd <| hs.prod_gameAdd hu)

Result:
case h.e'_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (DFinsupp.Lex r s) (single i (x i))
hu : Acc (DFinsupp.Lex r s) (erase i x)
⊢ ({i}, single i (x i), erase i x).2.1.piecewise ({i}, single i (x i), erase i x).2.2
      ({i}, single i (x i), erase i x).1 =
    x

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (DFinsupp.Lex r s) (single i (x i))
hu : Acc (DFinsupp.Lex r s) (erase i x)
⊢ Acc (DFinsupp.Lex r s) x

Tactic:
classical
  convert ← @Acc.of_fibration _ _ _ _ _ (lex_fibration r s) ⟨{i}, _⟩
    (InvImage.accessible snd <| hs.prod_gameAdd hu)
  convert piecewise_single_erase x i

Result:
no goals

Proof state:
case h.e'_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (DFinsupp.Lex r s) (single i (x i))
hu : Acc (DFinsupp.Lex r s) (erase i x)
⊢ ({i}, single i (x i), erase i x).2.1.piecewise ({i}, single i (x i), erase i x).2.2
      ({i}, single i (x i), erase i x).1 =
    x

Tactic:
convert piecewise_single_erase x i

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
/-- Embedding `i : Fin n` into `Fin (n + 1)` using a pivot `p` that is greater
results in a value that is less than `p`. -/
lemma succAbove_lt_iff_castSucc_lt (p : Fin (n + 1)) (i : Fin n) :
    p.succAbove i < p ↔ castSucc i < p

Proof state:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ ¬i.succ < p

Tactic:
exact Fin.not_lt.2 <| Fin.le_of_lt H

Result:
no goals

Proof state:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i < p ↔ i.castSucc < p

Tactic:
rcases castSucc_lt_or_lt_succ p i with H | H

Result:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ p.succAbove i < p ↔ i.castSucc < p

case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p.succAbove i < p ↔ i.castSucc < p

Proof state:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p.succAbove i < p ↔ i.castSucc < p

Tactic:
rw [castSucc_lt_iff_succ_le, iff_false_right (Fin.not_le.2 H), succAbove_of_lt_succ _ _ H]

Result:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ ¬i.succ < p

Proof state:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ p.succAbove i < p ↔ i.castSucc < p

Tactic:
rwa [iff_true_right H, succAbove_of_castSucc_lt _ _ H]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem mapRange_zero (f : ∀ i, β₁ i → β₂ i) (hf : ∀ i, f i 0 = 0) :
    mapRange f hf (0 : Π₀ i, β₁ i) = 0

Proof state:
case h
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
i✝ : ι
⊢ (mapRange f hf 0) i✝ = 0 i✝

Tactic:
simp only [mapRange_apply, coe_zero, Pi.zero_apply, hf]

Result:
no goals

Proof state:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
⊢ mapRange f hf 0 = 0

Tactic:
ext

Result:
case h
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
i✝ : ι
⊢ (mapRange f hf 0) i✝ = 0 i✝
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem tendsto_Ioi_atBot {f : β → Ioi a} :
    Tendsto f l atBot ↔ Tendsto (fun x => (f x : α)) l (𝓝[>] a)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
l : Filter β
f : β → ↑(Ioi a)
⊢ Tendsto (Subtype.val ∘ f) l (𝓝[>] a) ↔ Tendsto (fun x => ↑(f x)) l (𝓝[>] a)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
l : Filter β
f : β → ↑(Ioi a)
⊢ Tendsto f l atBot ↔ Tendsto (fun x => ↑(f x)) l (𝓝[>] a)

Tactic:
rw [← comap_coe_Ioi_nhdsGT, tendsto_comap_iff]

Result:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
l : Filter β
f : β → ↑(Ioi a)
⊢ Tendsto (Subtype.val ∘ f) l (𝓝[>] a) ↔ Tendsto (fun x => ↑(f x)) l (𝓝[>] a)
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_add_right (a b : α) : toIocMod hp a (b + p) = toIocMod hp a b

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

Tactic:
simpa only [one_zsmul] using toIocMod_add_zsmul hp a b 1

Result:
no goals
-- Mathlib/Algebra/Algebra/Tower.lean
theorem map_mem_span_algebraMap_image {S T : Type*} [CommSemiring S] [Semiring T] [Algebra R S]
    [Algebra R T] [Algebra S T] [IsScalarTower R S T] (x : S) (a : Set S)
    (hx : x ∈ Submodule.span R a) : algebraMap S T x ∈ Submodule.span R (algebraMap S T '' a)

Proof state:
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
T : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : S
a : Set S
hx : x ∈ span R a
⊢ (algebraMap S T) x ∈ span R (⇑(algebraMap S T) '' a)

Tactic:
rw [span_algebraMap_image_of_tower, mem_map]

Result:
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
T : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : S
a : Set S
hx : x ∈ span R a
⊢ ∃ y ∈ span R a, (↑R (Algebra.linearMap S T)) y = (algebraMap S T) x

Proof state:
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
T : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : S
a : Set S
hx : x ∈ span R a
⊢ ∃ y ∈ span R a, (↑R (Algebra.linearMap S T)) y = (algebraMap S T) x

Tactic:
exact ⟨x, hx, rfl⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem mem_enumFrom {x : α} {i j : Nat} {xs : List α} (h : (i, x) ∈ xs.enumFrom j) :
    j ≤ i ∧ i < j + xs.length ∧
      x = xs[i - j]'(by have := le_fst_of_mem_enumFrom h; have := fst_lt_add_of_mem_enumFrom h; omega) :=
  ⟨le_fst_of_mem_enumFrom h, fst_lt_add_of_mem_enumFrom h, snd_eq_of_mem_enumFrom h⟩

Proof state:
α : Type ?u.63802
x : α
i j : Nat
xs : List α
h : (i, x) ∈ enumFrom j xs
this : j ≤ (i, x).fst
⊢ i - j < xs.length

Tactic:
have := fst_lt_add_of_mem_enumFrom h

Result:
α : Type ?u.63802
x : α
i j : Nat
xs : List α
h : (i, x) ∈ enumFrom j xs
this✝ : j ≤ (i, x).fst
this : (i, x).fst < j + xs.length
⊢ i - j < xs.length

Proof state:
α : Type ?u.63802
x : α
i j : Nat
xs : List α
h : (i, x) ∈ enumFrom j xs
⊢ i - j < xs.length

Tactic:
have := le_fst_of_mem_enumFrom h

Result:
α : Type ?u.63802
x : α
i j : Nat
xs : List α
h : (i, x) ∈ enumFrom j xs
this : j ≤ (i, x).fst
⊢ i - j < xs.length

Proof state:
α : Type ?u.63802
x : α
i j : Nat
xs : List α
h : (i, x) ∈ enumFrom j xs
this✝ : j ≤ (i, x).fst
this : (i, x).fst < j + xs.length
⊢ i - j < xs.length

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Polynomial/RingDivision.lean
theorem rootMultiplicity_mul {p q : R[X]} {x : R} (hpq : p * q ≠ 0) :
    rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
have hq : q ≠ 0 := right_ne_zero_of_mul hpq

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
rw [rootMultiplicity_eq_multiplicity (p * q), if_neg hpq, rootMultiplicity_eq_multiplicity p,
  if_neg hp, rootMultiplicity_eq_multiplicity q, if_neg hq,
  multiplicity_mul (prime_X_sub_C x) (finiteMultiplicity_X_sub_C _ hpq)]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
have hp : p ≠ 0 := left_ne_zero_of_mul hpq

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
classical
have hp : p ≠ 0 := left_ne_zero_of_mul hpq
have hq : q ≠ 0 := right_ne_zero_of_mul hpq
rw [rootMultiplicity_eq_multiplicity (p * q), if_neg hpq, rootMultiplicity_eq_multiplicity p,
  if_neg hp, rootMultiplicity_eq_multiplicity q, if_neg hq,
  multiplicity_mul (prime_X_sub_C x) (finiteMultiplicity_X_sub_C _ hpq)]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioo_subset_Ioo_iff [DenselyOrdered α] (h₁ : a₁ < b₁) :
    Ioo a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ :=
  ⟨fun h => by
    rcases exists_between h₁ with ⟨x, xa, xb⟩
    constructor <;> refine le_of_not_lt fun h' => ?_
    · have ab := (h ⟨xa, xb⟩).1.trans xb
      exact lt_irrefl _ (h ⟨h', ab⟩).1
    · have ab := xa.trans (h ⟨xa, xb⟩).2
      exact lt_irrefl _ (h ⟨ab, h'⟩).2,
    fun ⟨h₁, h₂⟩ => Ioo_subset_Ioo h₁ h₂⟩

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
constructor <;> refine le_of_not_lt fun h' => ?_

Result:
case intro.intro.left
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
⊢ False

case intro.intro.right
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
⊢ False

Proof state:
case intro.intro.right
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
ab : a₁ < b₂
⊢ False

Tactic:
exact lt_irrefl _ (h ⟨ab, h'⟩).2

Result:
no goals

Proof state:
case intro.intro.left
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
⊢ False

Tactic:
have ab := (h ⟨xa, xb⟩).1.trans xb

Result:
case intro.intro.left
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
ab : a₂ < b₁
⊢ False

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
⊢ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
rcases exists_between h₁ with ⟨x, xa, xb⟩

Result:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Proof state:
case intro.intro.left
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
ab : a₂ < b₁
⊢ False

Tactic:
exact lt_irrefl _ (h ⟨h', ab⟩).1

Result:
no goals

Proof state:
case intro.intro.right
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
⊢ False

Tactic:
have ab := xa.trans (h ⟨xa, xb⟩).2

Result:
case intro.intro.right
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
ab : a₁ < b₂
⊢ False
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem of_nonpos_disjoint_union_eq_zero {s : SignedMeasure α} {A B : Set α} (h : Disjoint A B)
    (hA₁ : MeasurableSet A) (hB₁ : MeasurableSet B) (hA₂ : s A ≤ 0) (hB₂ : s B ≤ 0)
    (hAB : s (A ∪ B) = 0) : s A = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : ↑s A ≤ 0
hB₂ : ↑s B ≤ 0
hAB : ↑s (A ∪ B) = 0
⊢ ↑s A = 0

Tactic:
rw [of_union h hA₁ hB₁] at hAB

Result:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : ↑s A ≤ 0
hB₂ : ↑s B ≤ 0
hAB : ↑s A + ↑s B = 0
⊢ ↑s A = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : ↑s A ≤ 0
hB₂ : ↑s B ≤ 0
hAB : ↑s A + ↑s B = 0
⊢ ↑s A = 0

Tactic:
linarith

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
lemma factorial_le_pow : ∀ n, n ! ≤ n ^ n
  | 0 => le_refl _
  | n + 1 =>
    calc
      _ ≤ (n + 1) * n ^ n := Nat.mul_le_mul_left _ n.factorial_le_pow
      _ ≤ (n + 1) * (n + 1) ^ n := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left n.le_succ _)
      _ = _

Proof state:
n : ℕ
⊢ (n + 1) * (n + 1) ^ n = (n + 1) ^ (n + 1)

Tactic:
rw [pow_succ']

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem exists_coeff_ne_zero_and_order (h : f.order.toNat = f.order) :
    ∃ d : σ →₀ ℕ, coeff R d f ≠ 0 ∧ degree d = f.order

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
h : ↑f.order.toNat = f.order
⊢ ∃ d, (coeff R d) f ≠ 0 ∧ ↑((weight fun x => 1) d) = f.order

Tactic:
exact exists_coeff_ne_zero_and_weightedOrder _ h

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
h : ↑f.order.toNat = f.order
⊢ ∃ d, (coeff R d) f ≠ 0 ∧ ↑d.degree = f.order

Tactic:
simp_rw [degree_eq_weight_one]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
h : ↑f.order.toNat = f.order
⊢ ∃ d, (coeff R d) f ≠ 0 ∧ ↑((weight fun x => 1) d) = f.order
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lex/Lemmas.lean
theorem empty_lt_push [LT α] (l : Array α) (a : α) : #[] < l.push a

Proof state:
α : Type u_1
inst✝ : LT α
l : Array α
a : α
⊢ #[] < l.push a

Tactic:
rcases l with (_ | ⟨x, l⟩) <;> simp

Result:
no goals
-- Mathlib/GroupTheory/HNNExtension.lean
theorem lift_t (f : G →* H) (x : H) (hx : ∀ a : A, x * f ↑a = f (φ a : G) * x) :
    lift f x hx t = x

Proof state:
G : Type u_1
inst✝¹ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝ : Group H
f : G →* H
x : H
hx : ∀ (a : ↥A), x * f ↑a = f ↑(φ a) * x
⊢ (lift f x hx) t = x

Tactic:
simp [lift, t]

Result:
no goals
-- Mathlib/Order/Nucleus.lean
lemma map_himp_le : n (x ⇨ y) ≤ x ⇨ n y

Proof state:
X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ n (y ⊓ x) ≤ n y

Tactic:
gcongr

Result:
case hab
X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ y ⊓ x ≤ y

Proof state:
X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ n (x ⇨ y) ⊓ n x = n (y ⊓ x)

Tactic:
rw [← map_inf, himp_inf_self]

Result:
no goals

Proof state:
case hab
X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ y ⊓ x ≤ y

Tactic:
exact inf_le_left

Result:
no goals

Proof state:
X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ n (x ⇨ y) ⊓ x ≤ n (x ⇨ y) ⊓ n x

Tactic:
gcongr

Result:
case h
X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ x ≤ n x

Proof state:
case h
X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ x ≤ n x

Tactic:
exact n.le_apply

Result:
no goals

Proof state:
X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ n (x ⇨ y) ≤ x ⇨ n y

Tactic:
rw [le_himp_iff]

Result:
X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ n (x ⇨ y) ⊓ x ≤ n y

Proof state:
X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ n (x ⇨ y) ⊓ x ≤ n y

Tactic:
calc
  n (x ⇨ y) ⊓ x
  _ ≤ n (x ⇨ y) ⊓ n x := by gcongr; exact n.le_apply
  _ = n (y ⊓ x) := by rw [← map_inf, himp_inf_self]
  _ ≤ n y := by gcongr; exact inf_le_left

Result:
no goals
-- Mathlib/Geometry/Euclidean/Inversion/Basic.lean
theorem inversion_dist_center' (c x : P) : inversion c (dist c x) x = x

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
⊢ inversion c (dist c x) x = x

Tactic:
rw [dist_comm, inversion_dist_center]

Result:
no goals
-- Mathlib/Order/Interval/Set/SuccPred.lean
lemma Ioc_pred_right_eq_Ioo (a b : α) : Ioc a (pred b) = Ioo a b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
⊢ Ioc a (pred b) = Ioo a b

Tactic:
by_cases hb : IsMin b

Result:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : IsMin b
⊢ Ioc a (pred b) = Ioo a b

case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : ¬IsMin b
⊢ Ioc a (pred b) = Ioo a b

Proof state:
case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : ¬IsMin b
⊢ Ioc a (pred b) = Ioo a b

Tactic:
ext x

Result:
case neg.h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : ¬IsMin b
x : α
⊢ x ∈ Ioc a (pred b) ↔ x ∈ Ioo a b

Proof state:
case neg.h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : ¬IsMin b
x : α
⊢ x ∈ Ioc a (pred b) ↔ x ∈ Ioo a b

Tactic:
rw [mem_Ioc, mem_Ioo, le_pred_iff_of_not_isMin hb]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : IsMin b
⊢ Ioc a (pred b) = Ioo a b

Tactic:
rw [Ioc_eq_empty (hb.mono <| pred_le _).not_lt, Ioo_eq_empty hb.not_lt]

Result:
no goals
-- Mathlib/Topology/Category/CompHausLike/Limits.lean
lemma finiteCoproduct.ι_injective (a : α) : Function.Injective (finiteCoproduct.ι X a)

Proof state:
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
x y : ↑(X a).toTop
hxy : (ConcreteCategory.hom (ι X a)) x = (ConcreteCategory.hom (ι X a)) y
⊢ x = y

Tactic:
exact eq_of_heq (Sigma.ext_iff.mp hxy).2

Result:
no goals

Proof state:
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
⊢ Function.Injective ⇑(ConcreteCategory.hom (ι X a))

Tactic:
intro x y hxy

Result:
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
x y : ↑(X a).toTop
hxy : (ConcreteCategory.hom (ι X a)) x = (ConcreteCategory.hom (ι X a)) y
⊢ x = y
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
protected lemma comp_sub {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ z₂' : Cochain G K n₂)
    (h : n₁ + n₂ = n₁₂) : z₁.comp (z₂ - z₂') h = z₁.comp z₂ h - z₁.comp z₂' h

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ z₂' : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ (z₁.comp (z₂ - z₂') h).v p q hpq = (z₁.comp z₂ h - z₁.comp z₂' h).v p q hpq

Tactic:
simp only [comp_v _ _ h p _ q rfl (by omega), sub_v, comp_sub]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ z₂' : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ p + n₁ + n₂ = q

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ z₂' : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ z₁.comp (z₂ - z₂') h = z₁.comp z₂ h - z₁.comp z₂' h

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ z₂' : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ (z₁.comp (z₂ - z₂') h).v p q hpq = (z₁.comp z₂ h - z₁.comp z₂' h).v p q hpq
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem contains_def [DecidableEq α] {a : α} {as : Array α} : as.contains a ↔ a ∈ as

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
as : Array α
⊢ as.contains a = true ↔ a ∈ as

Tactic:
rw [mem_def, contains, ← any_toList, List.any_eq_true]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ x, x ∈ as.toList ∧ (a == x) = true) ↔ a ∈ as.toList

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ x, x ∈ as.toList ∧ (a == x) = true) ↔ a ∈ as.toList

Tactic:
simp [and_comm]

Result:
no goals