harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
theorem lt_of_mul_lt_mul_of_le₀ (h : a * b < c * d) (hc : 0 < c) (hh : c ≤ a) : b < d

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : c ≤ a
ha : a ≠ 0
⊢ b < d

Tactic:
rw [← inv_le_inv₀ (zero_lt_iff.2 ha) hc] at hh

Result:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : a⁻¹ ≤ c⁻¹
ha : a ≠ 0
⊢ b < d

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : c ≤ a
⊢ b < d

Tactic:
have ha : a ≠ 0 := ne_of_gt (lt_of_lt_of_le hc hh)

Result:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : c ≤ a
ha : a ≠ 0
⊢ b < d

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : a⁻¹ ≤ c⁻¹
ha : a ≠ 0
⊢ b < d

Tactic:
simpa [inv_mul_cancel_left₀ ha, inv_mul_cancel_left₀ hc.ne']
  using mul_lt_mul_of_le_of_lt_of_nonneg_of_pos hh  h zero_le' (inv_pos.2 hc)

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem toFinset_nonempty : s.toFinset.Nonempty ↔ s ≠ 0

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ s.toFinset.Nonempty ↔ s ≠ 0

Tactic:
simp only [toFinset_eq_empty, Ne, Finset.nonempty_iff_ne_empty]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc]
lemma homologyι_descOpcycles_eq_zero_of_boundary [S.HasHomology]
    (k : S.X₂ ⟶ A) (x : S.X₃ ⟶ A) (hx : k = S.g ≫ x) :
    S.homologyι ≫ S.descOpcycles k (by rw [hx, S.zero_assoc, zero_comp]) = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst✝ : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.f ≫ k = 0

Tactic:
rw [hx, S.zero_assoc, zero_comp]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
A : C
inst✝ : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.homologyι ≫ S.descOpcycles k ⋯ = 0

Tactic:
dsimp only [homologyι]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
A : C
inst✝ : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ (S.rightHomologyIso.inv ≫ S.rightHomologyι) ≫ S.descOpcycles k ⋯ = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
A : C
inst✝ : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ (S.rightHomologyIso.inv ≫ S.rightHomologyι) ≫ S.descOpcycles k ⋯ = 0

Tactic:
rw [assoc, S.rightHomologyι_descOpcycles_π_eq_zero_of_boundary k x hx, comp_zero]

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
/-- **No wrap-around principle**.

The first `k` elements of `Fin (n + 1)` are `m`-Freiman isomorphic to the first `k` elements of `ℕ`
assuming there is no wrap-around. -/
lemma isAddFreimanIso_Iio (hm : m ≠ 0) (hkmn : m * k ≤ n) :
    IsAddFreimanIso m (Iio (k : Fin (n + 1))) (Iio k) val

Proof state:
case h.e'_6.h
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : Fin (n + 1)
⊢ ↑x < ↑(↑k + 1) ↔ ↑x ≤ k

Tactic:
simp_rw [← Nat.cast_add_one]

Result:
case h.e'_6.h
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : Fin (n + 1)
⊢ ↑x < ↑↑(k + 1) ↔ ↑x ≤ k

Proof state:
case h.e'_7.h
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : ℕ
⊢ x ∈ Iio (k + 1) ↔ x ∈ Iic k

Tactic:
simp [Nat.lt_succ_iff]

Result:
no goals

Proof state:
case succ
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
⊢ IsAddFreimanIso m (Iio ↑(k + 1)) (Iio (k + 1)) val

Tactic:
convert isAddFreimanIso_Iic hm hkmn' using 1 <;> ext x

Result:
case h.e'_6.h
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : Fin (n + 1)
⊢ x ∈ Iio ↑(k + 1) ↔ x ∈ Iic ↑k

case h.e'_7.h
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : ℕ
⊢ x ∈ Iio (k + 1) ↔ x ∈ Iic k

Proof state:
case zero
m n : ℕ
hm : m ≠ 0
hkmn : m * 0 ≤ n
⊢ IsAddFreimanIso m ∅ (Iio 0) val

Tactic:
simp [← _root_.bot_eq_zero, -Nat.bot_eq_zero, -bot_eq_zero']

Result:
no goals

Proof state:
case succ
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
⊢ IsAddFreimanIso m (Iio ↑(k + 1)) (Iio (k + 1)) val

Tactic:
have hkmn' : m * k ≤ n := (Nat.mul_le_mul_left _ k.le_succ).trans hkmn

Result:
case succ
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
⊢ IsAddFreimanIso m (Iio ↑(k + 1)) (Iio (k + 1)) val

Proof state:
k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
⊢ IsAddFreimanIso m (Iio ↑k) (Iio k) val

Tactic:
obtain _ | k := k

Result:
case zero
m n : ℕ
hm : m ≠ 0
hkmn : m * 0 ≤ n
⊢ IsAddFreimanIso m (Iio ↑0) (Iio 0) val

case succ
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
⊢ IsAddFreimanIso m (Iio ↑(k + 1)) (Iio (k + 1)) val

Proof state:
case h.e'_6.h
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : Fin (n + 1)
⊢ x ∈ Iio ↑(k + 1) ↔ x ∈ Iic ↑k

Tactic:
simp [lt_iff_val_lt_val, le_iff_val_le_val, -val_fin_le, -val_fin_lt, Nat.mod_eq_of_lt,
  aux hm hkmn']

Result:
case h.e'_6.h
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : Fin (n + 1)
⊢ ↑x < ↑(↑k + 1) ↔ ↑x ≤ k

Proof state:
case h.e'_6.h
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : Fin (n + 1)
⊢ ↑x < ↑↑(k + 1) ↔ ↑x ≤ k

Tactic:
rw [Fin.val_cast_of_lt (aux hm hkmn), Nat.lt_succ_iff]

Result:
no goals

Proof state:
case zero
m n : ℕ
hm : m ≠ 0
hkmn : m * 0 ≤ n
⊢ IsAddFreimanIso m (Iio ↑0) (Iio 0) val

Tactic:
simp [← bot_eq_zero]

Result:
case zero
m n : ℕ
hm : m ≠ 0
hkmn : m * 0 ≤ n
⊢ IsAddFreimanIso m ∅ (Iio 0) val
-- Mathlib/Combinatorics/Colex.lean
lemma lt_iff_max'_mem {s t : Colex α} :
    s < t ↔ ∃ h : s ≠ t, (ofColex s ∆ ofColex t).max' (max_mem_aux h) ∈ ofColex t

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Colex α
⊢ (∀ (h : s ≠ t), (s.ofColex ∆ t.ofColex).max' ⋯ ∈ t.ofColex) ∧ s ≠ t ↔
    ∃ (h : s ≠ t), (s.ofColex ∆ t.ofColex).max' ⋯ ∈ t.ofColex

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Colex α
⊢ s < t ↔ ∃ (h : s ≠ t), (s.ofColex ∆ t.ofColex).max' ⋯ ∈ t.ofColex

Tactic:
rw [lt_iff_le_and_ne, le_iff_max'_mem]

Result:
α : Type u_1
inst✝ : LinearOrder α
s t : Colex α
⊢ (∀ (h : s ≠ t), (s.ofColex ∆ t.ofColex).max' ⋯ ∈ t.ofColex) ∧ s ≠ t ↔
    ∃ (h : s ≠ t), (s.ofColex ∆ t.ofColex).max' ⋯ ∈ t.ofColex
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem all_bne' [BEq α] [PartialEquivBEq α] {xs : Vector α n} :
    (xs.all fun x => x != a) = !xs.contains a

Proof state:
α : Type u_1
n : Nat
a : α
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
xs : Vector α n
⊢ (xs.all fun x => x != a) = !xs.contains a

Tactic:
simp only [bne_comm, all_bne]

Result:
no goals
-- Mathlib/Probability/Kernel/Condexp.lean
lemma condExpKernel_singleton_ae_eq_cond [StandardBorelSpace Ω] (hs : MeasurableSet s)
    (ht : MeasurableSet t) :
    ∀ᵐ ω ∂μ.restrict s,
      condExpKernel μ (generateFrom {s}) ω t = μ[t|s]

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
s t : Set Ω
inst✝ : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ᵐ (ω : Ω) ∂μ.restrict s, ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]

Tactic:
have : (fun ω ↦ (condExpKernel μ (generateFrom {s}) ω t).toReal) =ᵐ[μ.restrict s]
    μ⟦t | generateFrom {s}⟧ :=
  ae_restrict_le <| condExpKernel_ae_eq_condExp
    (generateFrom_singleton_le hs) ht

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
s t : Set Ω
inst✝ : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (fun ω => (((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t).toReal) =ᶠ[ae (μ.restrict s)]
    μ[t.indicator fun ω => 1|MeasurableSpace.generateFrom {s}]
⊢ ∀ᵐ (ω : Ω) ∂μ.restrict s, ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]

Proof state:
case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
s t : Set Ω
inst✝ : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (fun ω => (((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t).toReal) =ᶠ[ae (μ.restrict s)]
    μ[t.indicator fun ω => 1|MeasurableSpace.generateFrom {s}]
ω : Ω
hω₁ : (μ[t.indicator fun ω => 1|MeasurableSpace.generateFrom {s}]) ω = μ[t | s].toReal
hω₂ :
  (((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t).toReal =
    (μ[t.indicator fun ω => 1|MeasurableSpace.generateFrom {s}]) ω
⊢ ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]

Tactic:
rwa [hω₁, ENNReal.toReal_eq_toReal (measure_ne_top _ t) (measure_ne_top _ t)] at hω₂

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
s t : Set Ω
inst✝ : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (fun ω => (((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t).toReal) =ᶠ[ae (μ.restrict s)]
    μ[t.indicator fun ω => 1|MeasurableSpace.generateFrom {s}]
⊢ ∀ᵐ (ω : Ω) ∂μ.restrict s, ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]

Tactic:
filter_upwards [condExp_set_generateFrom_singleton hs ht, this] with ω hω₁ hω₂

Result:
case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
s t : Set Ω
inst✝ : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (fun ω => (((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t).toReal) =ᶠ[ae (μ.restrict s)]
    μ[t.indicator fun ω => 1|MeasurableSpace.generateFrom {s}]
ω : Ω
hω₁ : (μ[t.indicator fun ω => 1|MeasurableSpace.generateFrom {s}]) ω = μ[t | s].toReal
hω₂ :
  (((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t).toReal =
    (μ[t.indicator fun ω => 1|MeasurableSpace.generateFrom {s}]) ω
⊢ ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem nsmul_lt_aleph0_iff {n : ℕ} {a : Cardinal} : n • a < ℵ₀ ↔ n = 0 ∨ a < ℵ₀

Proof state:
case succ
a : Cardinal.{u_1}
n : ℕ
⊢ (n + 1) • a < ℵ₀ ↔ a < ℵ₀

Tactic:
induction' n with n ih

Result:
case succ.zero
a : Cardinal.{u_1}
⊢ (0 + 1) • a < ℵ₀ ↔ a < ℵ₀

case succ.succ
a : Cardinal.{u_1}
n : ℕ
ih : (n + 1) • a < ℵ₀ ↔ a < ℵ₀
⊢ (n + 1 + 1) • a < ℵ₀ ↔ a < ℵ₀

Proof state:
case succ.zero
a : Cardinal.{u_1}
⊢ (0 + 1) • a < ℵ₀ ↔ a < ℵ₀

Tactic:
simp

Result:
no goals

Proof state:
case succ
a : Cardinal.{u_1}
n : ℕ
⊢ (n + 1) • a < ℵ₀ ↔ n + 1 = 0 ∨ a < ℵ₀

Tactic:
simp only [Nat.succ_ne_zero, false_or]

Result:
case succ
a : Cardinal.{u_1}
n : ℕ
⊢ (n + 1) • a < ℵ₀ ↔ a < ℵ₀

Proof state:
case zero
a : Cardinal.{u_1}
⊢ 0 • a < ℵ₀ ↔ 0 = 0 ∨ a < ℵ₀

Tactic:
simpa using nat_lt_aleph0 0

Result:
no goals

Proof state:
case succ.succ
a : Cardinal.{u_1}
n : ℕ
ih : (n + 1) • a < ℵ₀ ↔ a < ℵ₀
⊢ (n + 1 + 1) • a < ℵ₀ ↔ a < ℵ₀

Tactic:
rw [succ_nsmul, add_lt_aleph0_iff, ih, and_self_iff]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_sq_add_sin_sq : cos x ^ 2 + sin x ^ 2 = 1

Proof state:
x : ℝ
⊢ cos x ^ 2 + sin x ^ 2 = 1

Tactic:
rw [add_comm, sin_sq_add_cos_sq]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem factorThruKernelSubobject_comp_arrow {W : C} (h : W ⟶ X) (w : h ≫ f = 0) :
    factorThruKernelSubobject f h w ≫ (kernelSubobject f).arrow = h

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : h ≫ f = 0
⊢ (kernelSubobject f).factorThru h ⋯ ≫ (kernelSubobject f).arrow = h

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : h ≫ f = 0
⊢ factorThruKernelSubobject f h w ≫ (kernelSubobject f).arrow = h

Tactic:
dsimp [factorThruKernelSubobject]

Result:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : h ≫ f = 0
⊢ (kernelSubobject f).factorThru h ⋯ ≫ (kernelSubobject f).arrow = h
-- Mathlib/RingTheory/MvPolynomial/Basic.lean
theorem mem_restrictDegree (p : MvPolynomial σ R) (n : ℕ) :
    p ∈ restrictDegree σ R n ↔ ∀ s ∈ p.support, ∀ i, (s : σ →₀ ℕ) i ≤ n

Proof state:
σ : Type u
R : Type v
inst✝ : CommSemiring R
p : MvPolynomial σ R
n : ℕ
⊢ ↑p.support ⊆ {n_1 | ∀ (i : σ), n_1 i ≤ n} ↔ ∀ s ∈ p.support, ∀ (i : σ), s i ≤ n

Tactic:
rfl

Result:
no goals

Proof state:
σ : Type u
R : Type v
inst✝ : CommSemiring R
p : MvPolynomial σ R
n : ℕ
⊢ p ∈ restrictDegree σ R n ↔ ∀ s ∈ p.support, ∀ (i : σ), s i ≤ n

Tactic:
rw [restrictDegree, restrictSupport, Finsupp.mem_supported]

Result:
σ : Type u
R : Type v
inst✝ : CommSemiring R
p : MvPolynomial σ R
n : ℕ
⊢ ↑p.support ⊆ {n_1 | ∀ (i : σ), n_1 i ≤ n} ↔ ∀ s ∈ p.support, ∀ (i : σ), s i ≤ n
-- Mathlib/Data/Rat/Defs.lean
protected lemma add_zero : a + 0 = a

Proof state:
a : ℚ
⊢ a + 0 = a

Tactic:
simp [add_def, normalize_eq_mkRat]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldr_map (f : α₁ → α₂) (g : α₂ → β → β) (l : Vector α₁ n) (init : β) :
    (l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init

Proof state:
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
n : Nat
f : α₁ → α₂
g : α₂ → β → β
l : Vector α₁ n
init : β
⊢ foldr g init (map f l) = foldr (fun x y => g (f x) y) init l

Tactic:
cases l

Result:
case mk
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
n : Nat
f : α₁ → α₂
g : α₂ → β → β
init : β
toArray✝ : Array α₁
size_toArray✝ : toArray✝.size = n
⊢ foldr g init (map f { toArray := toArray✝, size_toArray := size_toArray✝ }) =
    foldr (fun x y => g (f x) y) init { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
n : Nat
f : α₁ → α₂
g : α₂ → β → β
init : β
toArray✝ : Array α₁
size_toArray✝ : toArray✝.size = n
⊢ foldr g init (map f { toArray := toArray✝, size_toArray := size_toArray✝ }) =
    foldr (fun x y => g (f x) y) init { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp [Array.foldr_map']

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma normEDS_ofNat (n : ℕ) :
    normEDS b c d n = preNormEDS' (b ^ 4) c d n * if Even n then b else 1

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
n : ℕ
⊢ normEDS b c d ↑n = preNormEDS' (b ^ 4) c d n * if Even n then b else 1

Tactic:
simp only [normEDS, preNormEDS_ofNat, Int.even_coe_nat]

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem Ioo_disjoint_Ioo [DenselyOrdered α] :
    Disjoint (Set.Ioo a₁ a₂) (Set.Ioo b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Proof state:
α : Type v
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
⊢ Disjoint (Ioo a₁ a₂) (Ioo b₁ b₂) ↔ a₂ ⊓ b₂ ≤ a₁ ⊔ b₁

Tactic:
simp_rw [Set.disjoint_iff_inter_eq_empty, Ioo_inter_Ioo, Ioo_eq_empty_iff, not_lt]

Result:
no goals
-- Mathlib/Analysis/Complex/Isometry.lean
theorem rotationOf_rotation (a : Circle) : rotationOf (rotation a) = a :=
  Subtype.ext <| by simp

Proof state:
a : Circle
⊢ ↑(rotationOf (rotation a)) = ↑a

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/CountableSeparatingOn.lean
theorem of_eventually_mem_of_forall_separating_mem_iff (p : Set β → Prop) {s : Set β}
    [h' : HasCountableSeparatingOn β p s] (hf : ∀ᶠ x in l, f x ∈ s) (hg : ∀ᶠ x in l, g x ∈ s)
    (h : ∀ U : Set β, p U → ∀ᶠ x in l, f x ∈ U ↔ g x ∈ U) : f =ᶠ[l] g

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
⊢ f =ᶠ[l] g

Tactic:
rcases h'.1 with ⟨S, hSc, hSp, hS⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
S : Set (Set β)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ f =ᶠ[l] g

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
S : Set (Set β)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
H : ∀ᶠ (x : α) in l, ∀ s ∈ S, f x ∈ s ↔ g x ∈ s
⊢ f =ᶠ[l] g

Tactic:
filter_upwards [H, hf, hg] with x hx hxf hxg using hS _ hxf _ hxg hx

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
S : Set (Set β)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ f =ᶠ[l] g

Tactic:
have H : ∀ᶠ x in l, ∀ s ∈ S, f x ∈ s ↔ g x ∈ s :=
  (eventually_countable_ball hSc).2 fun s hs ↦ (h _ (hSp _ hs))

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
S : Set (Set β)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
H : ∀ᶠ (x : α) in l, ∀ s ∈ S, f x ∈ s ↔ g x ∈ s
⊢ f =ᶠ[l] g
-- Mathlib/ModelTheory/Semantics.lean
theorem LHom.setOf_realize_onFormula [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M]
    (ψ : L.Formula α) : (setOf (φ.onFormula ψ).Realize : Set (α → M)) = setOf ψ.Realize

Proof state:
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L.Formula α
⊢ setOf (φ.onFormula ψ).Realize = setOf ψ.Realize

Tactic:
ext

Result:
case h
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L.Formula α
x✝ : α → M
⊢ x✝ ∈ setOf (φ.onFormula ψ).Realize ↔ x✝ ∈ setOf ψ.Realize

Proof state:
case h
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L.Formula α
x✝ : α → M
⊢ x✝ ∈ setOf (φ.onFormula ψ).Realize ↔ x✝ ∈ setOf ψ.Realize

Tactic:
simp

Result:
no goals
-- Mathlib/Control/Bitraversable/Lemmas.lean
theorem tfst_eq_fst_id {α α' β} (f : α → α') (x : t α β) :
    tfst (F := Id) (pure ∘ f) x = pure (fst f x)

Proof state:
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
inst✝ : LawfulBitraversable t
α α' β : Type u
f : α → α'
x : t α β
⊢ tfst (pure ∘ f) x = pure (fst f x)

Tactic:
apply bitraverse_eq_bimap_id

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
@[reassoc]
lemma extendToSuccObjIso_hom_naturality (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) :
    (extendToSucc hj F τ).map (homOfLE hi :
      ⟨i₁, hi.trans (hi₂.trans (Order.le_succ j))⟩ ⟶ ⟨i₂, hi₂.trans (Order.le_succ j)⟩) ≫
    (extendToSuccObjIso hj F τ i₂ hi₂).hom =
      (extendToSuccObjIso hj F τ i₁ (hi.trans hi₂)).hom ≫ F.map (homOfLE hi)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
⊢ extendToSucc.map hj F τ i₁ i₂ ⋯ ⋯ ≫ (extendToSucc.objIso F X ⟨i₂, hi₂⟩).hom =
    (extendToSucc.objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE hi)

Tactic:
rw [extendToSucc.map_eq _ _ _ _ _ _ hi₂, assoc, assoc, Iso.inv_hom_id, comp_id]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
⊢ (extendToSucc hj F τ).map (homOfLE hi) ≫ (extendToSuccObjIso hj F τ i₂ hi₂).hom =
    (extendToSuccObjIso hj F τ i₁ ⋯).hom ≫ F.map (homOfLE hi)

Tactic:
dsimp [extendToSucc, extendToSuccObjIso]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
⊢ extendToSucc.map hj F τ i₁ i₂ ⋯ ⋯ ≫ (extendToSucc.objIso F X ⟨i₂, hi₂⟩).hom =
    (extendToSucc.objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE hi)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sdiv_one {x : BitVec w} : x.sdiv 1#w = x

Proof state:
case neg
w : Nat
x : BitVec w
h : ¬w = 1
⊢ (match x.msb, (1#w).msb with
    | false, false => x.udiv 1#w
    | false, true => -x.udiv (-1#w)
    | true, false => -(-x).udiv 1#w
    | true, true => (-x).udiv (-1#w)) =
    x

Tactic:
rcases x.msb with msb | msb <;> simp [h]

Result:
no goals

Proof state:
case pos
w : Nat
x : BitVec w
h : w = 1
⊢ (match x.msb, (1#w).msb with
    | false, false => x.udiv 1#w
    | false, true => -x.udiv (-1#w)
    | true, false => -(-x).udiv 1#w
    | true, true => (-x).udiv (-1#w)) =
    x

Tactic:
subst h

Result:
case pos
x : BitVec 1
⊢ (match x.msb, (1#1).msb with
    | false, false => x.udiv 1#1
    | false, true => -x.udiv (-1#1)
    | true, false => -(-x).udiv 1#1
    | true, true => (-x).udiv (-1#1)) =
    x

Proof state:
case pos
x : BitVec 1
⊢ (match x.msb, (1#1).msb with
    | false, false => x.udiv 1#1
    | false, true => -x.udiv (-1#1)
    | true, false => -(-x).udiv 1#1
    | true, true => (-x).udiv (-1#1)) =
    x

Tactic:
rcases x.msb with msb | msb <;> simp

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ x.sdiv 1#w = x

Tactic:
simp only [sdiv_eq]

Result:
w : Nat
x : BitVec w
⊢ (match x.msb, (1#w).msb with
    | false, false => x.udiv 1#w
    | false, true => -x.udiv (-1#w)
    | true, false => -(-x).udiv 1#w
    | true, true => (-x).udiv (-1#w)) =
    x

Proof state:
w : Nat
x : BitVec w
⊢ (match x.msb, (1#w).msb with
    | false, false => x.udiv 1#w
    | false, true => -x.udiv (-1#w)
    | true, false => -(-x).udiv 1#w
    | true, true => (-x).udiv (-1#w)) =
    x

Tactic:
by_cases h : w = 1

Result:
case pos
w : Nat
x : BitVec w
h : w = 1
⊢ (match x.msb, (1#w).msb with
    | false, false => x.udiv 1#w
    | false, true => -x.udiv (-1#w)
    | true, false => -(-x).udiv 1#w
    | true, true => (-x).udiv (-1#w)) =
    x

case neg
w : Nat
x : BitVec w
h : ¬w = 1
⊢ (match x.msb, (1#w).msb with
    | false, false => x.udiv 1#w
    | false, true => -x.udiv (-1#w)
    | true, false => -(-x).udiv 1#w
    | true, true => (-x).udiv (-1#w)) =
    x
-- Mathlib/Data/List/ChainOfFn.lean
lemma chain'_ofFn {α : Type*} {n : ℕ} {f : Fin n → α} {r : α → α → Prop} :
    (ofFn f).Chain' r ↔ ∀ (i) (hi : i + 1 < n), r (f ⟨i, lt_of_succ_lt hi⟩) (f ⟨i + 1, hi⟩)

Proof state:
α : Type u_1
n : ℕ
f : Fin n → α
r : α → α → Prop
h : ∀ (i : ℕ) (h : i < n - 1), r (f (Fin.cast ⋯ ⟨i, ⋯⟩)) (f (Fin.cast ⋯ ⟨i + 1, ⋯⟩))
i : ℕ
hi : i + 1 < n
⊢ i < n - 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
f : Fin n → α
r : α → α → Prop
⊢ (∀ (i : ℕ) (h : i < n - 1), r (f (Fin.cast ⋯ ⟨i, ⋯⟩)) (f (Fin.cast ⋯ ⟨i + 1, ⋯⟩))) ↔
    ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)

Tactic:
exact ⟨fun h i hi ↦ h i (by omega), fun h i hi ↦ h i (by omega)⟩

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
f : Fin n → α
r : α → α → Prop
h : ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)
i : ℕ
hi : i < n - 1
⊢ i + 1 < n

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
f : Fin n → α
r : α → α → Prop
⊢ Chain' r (ofFn f) ↔ ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)

Tactic:
simp_rw [chain'_iff_get, get_ofFn, length_ofFn]

Result:
α : Type u_1
n : ℕ
f : Fin n → α
r : α → α → Prop
⊢ (∀ (i : ℕ) (h : i < n - 1), r (f (Fin.cast ⋯ ⟨i, ⋯⟩)) (f (Fin.cast ⋯ ⟨i + 1, ⋯⟩))) ↔
    ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)