harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Logic/Equiv/List.lean
theorem list_ofNat_succ (v : ℕ) :
    ofNat (List α) (succ v) = ofNat α v.unpair.1 :: ofNat (List α) v.unpair.2 :=
  ofNat_of_decode <|
    show decodeList (succ v) = _ by
      rcases e : unpair v with ⟨v₁, v₂⟩
      simp [decodeList, e]
      rw [show decodeList v₂ = decode (α := List α) v₂ from rfl, decode_eq_ofNat, Option.seq_some]

Proof state:
case mk
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ decodeList v.succ = some (ofNat α (v₁, v₂).1 :: ofNat (List α) (v₁, v₂).2)

Tactic:
simp [decodeList, e]

Result:
case mk
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ (some fun x2 => ofNat α v₁ :: x2) <*> decodeList v₂ = some (ofNat α v₁ :: ofNat (List α) v₂)

Proof state:
α : Type u_1
inst✝ : Denumerable α
v : ℕ
⊢ decodeList v.succ = some (ofNat α (unpair v).1 :: ofNat (List α) (unpair v).2)

Tactic:
rcases e : unpair v with ⟨v₁, v₂⟩

Result:
case mk
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ decodeList v.succ = some (ofNat α (v₁, v₂).1 :: ofNat (List α) (v₁, v₂).2)

Proof state:
case mk
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ (some fun x2 => ofNat α v₁ :: x2) <*> decodeList v₂ = some (ofNat α v₁ :: ofNat (List α) v₂)

Tactic:
rw [show decodeList v₂ = decode (α := List α) v₂ from rfl, decode_eq_ofNat, Option.seq_some]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
lemma differentiableOn_negMulLog : DifferentiableOn ℝ negMulLog {0}ᶜ

Proof state:
⊢ DifferentiableOn ℝ negMulLog {0}ᶜ

Tactic:
simpa only [negMulLog_eq_neg] using differentiableOn_mul_log.neg

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/Measure.lean
theorem volume_setOf_liouville : volume { x : ℝ | Liouville x } = 0

Proof state:
⊢ volume {x | Liouville x} = 0

Tactic:
simpa only [ae_iff, Classical.not_not] using ae_not_liouville

Result:
no goals
-- Mathlib/Data/Set/Countable.lean
theorem Countable.setOf_finite [Countable α] : {s : Set α | s.Finite}.Countable

Proof state:
α : Type u
inst✝ : Countable α
⊢ {s | s.Finite}.Countable

Tactic:
simpa using countable_setOf_finite_subset countable_univ

Result:
no goals
-- Mathlib/Computability/PartrecCode.lean
theorem eval_prec_succ (cf cg : Code) (a k : ℕ) :
    eval (prec cf cg) (Nat.pair a (Nat.succ k)) =
      do {let ih ← eval (prec cf cg) (Nat.pair a k); eval cg (Nat.pair a (Nat.pair k ih))}

Proof state:
cf cg : Code
a k : ℕ
⊢ Nat.rec (cf.eval (a, k.succ).1)
      (fun y IH => do
        let i ← IH
        cg.eval (Nat.pair (a, k.succ).1 (Nat.pair y i)))
      (a, k.succ).2 =
    (unpaired
          (fun a n =>
            Nat.rec (cf.eval a)
              (fun y IH => do
                let i ← IH
                cg.eval (Nat.pair a (Nat.pair y i)))
              n)
          (Nat.pair a k)).bind
      fun ih => cg.eval (Nat.pair a (Nat.pair k ih))

Tactic:
simp

Result:
no goals

Proof state:
cf cg : Code
a k : ℕ
⊢ (cf.prec cg).eval (Nat.pair a k.succ) = do
    let ih ← (cf.prec cg).eval (Nat.pair a k)
    cg.eval (Nat.pair a (Nat.pair k ih))

Tactic:
rw [eval, Nat.unpaired, Part.bind_eq_bind, Nat.unpair_pair]

Result:
cf cg : Code
a k : ℕ
⊢ Nat.rec (cf.eval (a, k.succ).1)
      (fun y IH => do
        let i ← IH
        cg.eval (Nat.pair (a, k.succ).1 (Nat.pair y i)))
      (a, k.succ).2 =
    (unpaired
          (fun a n =>
            Nat.rec (cf.eval a)
              (fun y IH => do
                let i ← IH
                cg.eval (Nat.pair a (Nat.pair y i)))
              n)
          (Nat.pair a k)).bind
      fun ih => cg.eval (Nat.pair a (Nat.pair k ih))
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem Minpoly.toAdjoin.apply_X :
    Minpoly.toAdjoin R x (mk (minpoly R x) X) = ⟨x, self_mem_adjoin_singleton R x⟩

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ (toAdjoin R x) ((mk (minpoly R x)) X) = ⟨x, ⋯⟩

Tactic:
simp [toAdjoin]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion₂_inter (s : ∀ i, κ i → Set α) (t : Set α) :
    (⋃ (i) (j), s i j) ∩ t = ⋃ (i) (j), s i j ∩ t

Proof state:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋃ i, ⋃ j, s i j) ∩ t = ⋃ i, ⋃ j, s i j ∩ t

Tactic:
simp_rw [iUnion_inter]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_rotateLeft {x : BitVec w} {r : Nat} :
    (x.rotateLeft r).toNat = (x.toNat <<< (r % w)) % (2^w) ||| x.toNat >>> (w - r % w)

Proof state:
w : Nat
x : BitVec w
r : Nat
⊢ (x.rotateLeft r).toNat = x.toNat <<< (r % w) % 2 ^ w ||| x.toNat >>> (w - r % w)

Tactic:
simp only [rotateLeft_def, toNat_shiftLeft, toNat_ushiftRight, toNat_or]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma nilRank_eq_polyCharpoly_natTrailingDegree (b : Basis ι R L) :
    nilRank φ = (polyCharpoly φ b).natTrailingDegree

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : Nontrivial R
b : Basis ι R L
⊢ φ.nilRank = (φ.polyCharpoly b).natTrailingDegree

Tactic:
apply nilRankAux_basis_indep

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Set/Basic.lean
lemma Nonempty.mul_zero (hs : s.Nonempty) : s * 0 = 0 :=
  s.mul_zero_subset.antisymm <| by simpa [mem_mul] using hs

Proof state:
α : Type u_1
inst✝ : MulZeroClass α
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ s * 0

Tactic:
simpa [mem_mul] using hs

Result:
no goals
-- Mathlib/Logic/Equiv/Set.lean
theorem ofInjective_symm_apply {α β} {f : α → β} (hf : Injective f) (a : α) :
    (ofInjective f hf).symm ⟨f a, ⟨a, rfl⟩⟩ = a

Proof state:
α : Sort u_1
β : Type u_2
f : α → β
hf : Injective f
a : α
⊢ (ofInjective f hf).symm ⟨f a, ⋯⟩ = a

Tactic:
apply (ofInjective f hf).injective

Result:
case a
α : Sort u_1
β : Type u_2
f : α → β
hf : Injective f
a : α
⊢ (ofInjective f hf) ((ofInjective f hf).symm ⟨f a, ⋯⟩) = (ofInjective f hf) a

Proof state:
case a
α : Sort u_1
β : Type u_2
f : α → β
hf : Injective f
a : α
⊢ (ofInjective f hf) ((ofInjective f hf).symm ⟨f a, ⋯⟩) = (ofInjective f hf) a

Tactic:
simp [apply_ofInjective_symm hf]

Result:
no goals
-- Mathlib/GroupTheory/DoubleCoset.lean
theorem eq_of_not_disjoint {H K : Subgroup G} {a b : G}
    (h : ¬Disjoint (doset a H K) (doset b H K)) : doset a H K = doset b H K

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset b ↑H ↑K) (doset a ↑H ↑K)
ha : a ∈ doset b ↑H ↑K
⊢ doset a ↑H ↑K = doset b ↑H ↑K

Tactic:
apply doset_eq_of_mem ha

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset b ↑H ↑K) (doset a ↑H ↑K)
⊢ doset a ↑H ↑K = doset b ↑H ↑K

Tactic:
have ha : a ∈ doset b H K := mem_doset_of_not_disjoint h

Result:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset b ↑H ↑K) (doset a ↑H ↑K)
ha : a ∈ doset b ↑H ↑K
⊢ doset a ↑H ↑K = doset b ↑H ↑K

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset a ↑H ↑K) (doset b ↑H ↑K)
⊢ doset a ↑H ↑K = doset b ↑H ↑K

Tactic:
rw [disjoint_comm] at h

Result:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset b ↑H ↑K) (doset a ↑H ↑K)
⊢ doset a ↑H ↑K = doset b ↑H ↑K
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem le_mul_inv_iff_mul_le : c ≤ a * b⁻¹ ↔ c * b ≤ a :=
  (mul_le_mul_iff_right b).symm.trans <| by rw [inv_mul_cancel_right]

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ c * b ≤ a * b⁻¹ * b ↔ c * b ≤ a

Tactic:
rw [inv_mul_cancel_right]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma one_le_ofENat {n : ℕ∞} : 1 ≤ (n : Cardinal) ↔ 1 ≤ n

Proof state:
n : ℕ∞
⊢ 1 ≤ ↑n ↔ 1 ≤ n

Tactic:
norm_cast

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Basic.lean
@[reassoc (attr := simp)]
lemma _root_.CategoryTheory.Iso.inv_hom_id_triangle_hom₂ {A B : Triangle C} (e : A ≅ B) :
    e.inv.hom₂ ≫ e.hom.hom₂ = 𝟙 _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ e.inv.hom₂ ≫ e.hom.hom₂ = 𝟙 B.obj₂

Tactic:
rw [← comp_hom₂, e.inv_hom_id, id_hom₂]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem Filter.HasBasis.equicontinuousAt_iff_left {p : κ → Prop} {s : κ → Set X}
    {F : ι → X → α} {x₀ : X} (hX : (𝓝 x₀).HasBasis p s) :
    EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ i, (F i x₀, F i x) ∈ U

Proof state:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set X
F : ι → X → α
x₀ : X
hX : (𝓝 x₀).HasBasis p s
⊢ (∀ ib ∈ 𝓤 α, ∃ ia, p ia ∧ ∀ x ∈ s ia, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α ib}) ↔
    ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set X
F : ι → X → α
x₀ : X
hX : (𝓝 x₀).HasBasis p s
⊢ EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U

Tactic:
rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
  hX.tendsto_iff (UniformFun.hasBasis_nhds ι α _)]

Result:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set X
F : ι → X → α
x₀ : X
hX : (𝓝 x₀).HasBasis p s
⊢ (∀ ib ∈ 𝓤 α, ∃ ia, p ia ∧ ∀ x ∈ s ia, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α ib}) ↔
    ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Ioi_sub_one_eq_Ici (a : α) : Ioi (a - 1) = Ici a

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a : α
⊢ Ioi (a - 1) = Ici a

Tactic:
simpa [pred_eq_sub_one] using Ioi_pred_eq_Ici a

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean
lemma toCircle_natCast (j : ℕ) :
    toCircle (j : ZMod N) = exp (2 * π * I * j / N)

Proof state:
N : ℕ
inst✝ : NeZero N
j : ℕ
⊢ ↑(toCircle ↑j) = cexp (2 * ↑π * I * ↑j / ↑N)

Tactic:
simpa using toCircle_intCast (N := N) j

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem cons_injective2 : Function.Injective2 (cons : α → Stream' α → Stream' α) := fun x y s t h =>
  ⟨by rw [← get_zero_cons x s, h, get_zero_cons],
    Stream'.ext fun n => by rw [← get_succ_cons n _ x, h, get_succ_cons]⟩

Proof state:
α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
n : ℕ
⊢ s.get n = t.get n

Tactic:
rw [← get_succ_cons n _ x, h, get_succ_cons]

Result:
no goals

Proof state:
α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
⊢ x = y

Tactic:
rw [← get_zero_cons x s, h, get_zero_cons]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem exists_lt_of_prod_lt' (Hlt : ∏ i ∈ s, f i < ∏ i ∈ s, g i) : ∃ i ∈ s, f i < g i

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : LinearOrderedCancelCommMonoid M
f g : ι → M
s : Finset ι
Hle : ∀ i ∈ s, g i ≤ f i
⊢ ∏ i ∈ s, g i ≤ ∏ i ∈ s, f i

Tactic:
exact prod_le_prod' Hle

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : LinearOrderedCancelCommMonoid M
f g : ι → M
s : Finset ι
Hlt : ∏ i ∈ s, f i < ∏ i ∈ s, g i
⊢ ∃ i ∈ s, f i < g i

Tactic:
contrapose! Hlt with Hle

Result:
ι : Type u_1
M : Type u_4
inst✝ : LinearOrderedCancelCommMonoid M
f g : ι → M
s : Finset ι
Hle : ∀ i ∈ s, g i ≤ f i
⊢ ∏ i ∈ s, g i ≤ ∏ i ∈ s, f i
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem mul_inv_cancel (φ : MvPowerSeries σ k) (h : constantCoeff σ k φ ≠ 0) :
    φ * φ⁻¹ = 1

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : (constantCoeff σ k) φ ≠ 0
⊢ φ * φ⁻¹ = 1

Tactic:
rw [← invOfUnit_eq φ h, mul_invOfUnit φ (Units.mk0 _ h) rfl]

Result:
no goals
-- Mathlib/Data/Multiset/Sym.lean
theorem mk_mem_sym2_iff {m : Multiset α} {a b : α} :
    s(a, b) ∈ m.sym2 ↔ a ∈ m ∧ b ∈ m :=
  m.inductionOn fun xs => by simp [List.mk_mem_sym2_iff]

Proof state:
α : Type u_1
m : Multiset α
a b : α
xs : List α
⊢ s(a, b) ∈ Multiset.sym2 ⟦xs⟧ ↔ a ∈ ⟦xs⟧ ∧ b ∈ ⟦xs⟧

Tactic:
simp [List.mk_mem_sym2_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKey?_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} :
    (m.alter k f).getKey? k = if (f (m.get? k)).isSome then some k else none

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
⊢ (m.alter k f).getKey? k = if (f (m.get? k)).isSome = true then some k else none

Tactic:
simp only [getKey?_alter, beq_self_eq_true, ↓reduceIte]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/ByteArray.lean
theorem ofFn_succ (f : Fin (n+1) → UInt8) :
    ofFn f = (ofFn fun i => f i.castSucc).push (f (Fin.last n))

Proof state:
n : Nat
f : Fin (n + 1) → UInt8
⊢ ofFn f = (ofFn fun i => f i.castSucc).push (f (Fin.last n))

Tactic:
simp [ofFn, Fin.foldl_succ_last, mkEmpty]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Ioc_sub_one_left_eq_Icc (a b : α) : Ioc (a - 1) b = Icc a b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Ioc (a - 1) b = Icc a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_left_eq_Icc a b

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.lo_ro_2 (u w v k₁ k₂ : Nat) : u + k₁ ≤ w → w ≤ v + k₂ → u ≤ v + (k₂ - k₁)

Proof state:
u w v k₁ k₂ : Nat
⊢ u + k₁ ≤ w → w ≤ v + k₂ → u ≤ v + (k₂ - k₁)

Tactic:
omega

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
theorem map_apply (κ : Kernel α β) (hf : Measurable f) (a : α) : map κ f a = (κ a).map f

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
κ : Kernel α β
hf : Measurable f
a : α
⊢ (κ.map f) a = Measure.map f (κ a)

Tactic:
simp only [map, hf, ↓reduceDIte, mapOfMeasurable, coe_mk]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
theorem limitConstTerminal_inv_π {J : Type*} [Category J] {C : Type*} [Category C] [HasTerminal C]
    {j : J} :
    limitConstTerminal.inv ≫ limit.π ((CategoryTheory.Functor.const J).obj (⊤_ C)) j =
      terminal.from _

Proof state:
J : Type u_1
inst✝² : Category.{u_3, u_1} J
C : Type u_2
inst✝¹ : Category.{u_4, u_2} C
inst✝ : HasTerminal C
j : J
⊢ limitConstTerminal.inv ≫ limit.π ((Functor.const J).obj (⊤_ C)) j = terminal.from (⊤_ C)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
@[simp]
lemma evalEval_polynomial_zero : W'.polynomial.evalEval 0 0 = -W'.a₆

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ evalEval 0 0 W'.polynomial = -W'.a₆

Tactic:
simp only [evalEval_polynomial, zero_add, zero_sub, mul_zero, zero_pow <| Nat.succ_ne_zero _]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
    (m.alter k f).get? k = f (m.get? k)

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ (m.alter k f).get? k = f (m.get? k)

Tactic:
simp [get?_alter h]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioc_subset_Iic_self : Ioc a b ⊆ Iic b

Proof state:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
⊢ Ioc a b ⊆ Iic b

Tactic:
simpa [← coe_subset] using Set.Ioc_subset_Iic_self

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Basic.lean
theorem dist_algebraMap' [NormOneClass 𝕜'] (x y : 𝕜) :
    (dist (algebraMap 𝕜 𝕜' x) (algebraMap 𝕜 𝕜' y)) = dist x y

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x y : 𝕜
⊢ dist ((algebraMap 𝕜 𝕜') x) ((algebraMap 𝕜 𝕜') y) = dist x y

Tactic:
simp only [dist_eq_norm, ← map_sub, norm_algebraMap']

Result:
no goals
-- Mathlib/Computability/Halting.lean
theorem cond {c : α → Bool} {f : α →. σ} {g : α →. σ} (hc : Computable c) (hf : Partrec f)
    (hg : Partrec g) : Partrec fun a => cond (c a) (f a) (g a) :=
  let ⟨cf, ef⟩ := exists_code.1 hf
  let ⟨cg, eg⟩ := exists_code.1 hg
  ((eval_part.comp (Computable.cond hc (const cf) (const cg)) Computable.encode).bind
    ((@Computable.decode σ _).comp snd).ofOption.to₂).of_eq
    fun a => by cases c a <;> simp [ef, eg, encodek]

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Bool
f g : α →. σ
hc : Computable c
hf : Partrec f
hg : Partrec g
cf : Code
ef : cf.eval = fun n => (↑(decode n)).bind fun a => Part.map encode (f a)
cg : Code
eg : cg.eval = fun n => (↑(decode n)).bind fun a => Part.map encode (g a)
a : α
⊢ (((bif c a then cf else cg).eval (encode a)).bind fun b => ↑(decode (a, b).2)) = bif c a then f a else g a

Tactic:
cases c a <;> simp [ef, eg, encodek]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/IsDiag.lean
theorem IsDiag.map [Zero α] [Zero β] {A : Matrix n n α} (ha : A.IsDiag) {f : α → β} (hf : f 0 = 0) :
    (A.map f).IsDiag

Proof state:
α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Zero α
inst✝ : Zero β
A : Matrix n n α
ha : A.IsDiag
f : α → β
hf : f 0 = 0
i j : n
h : i ≠ j
⊢ A.map f i j = 0

Tactic:
simp [ha h, hf]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Zero α
inst✝ : Zero β
A : Matrix n n α
ha : A.IsDiag
f : α → β
hf : f 0 = 0
⊢ (A.map f).IsDiag

Tactic:
intro i j h

Result:
α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Zero α
inst✝ : Zero β
A : Matrix n n α
ha : A.IsDiag
f : α → β
hf : f 0 = 0
i j : n
h : i ≠ j
⊢ A.map f i j = 0
-- Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean
theorem range_ι_le_evenOdd_one : LinearMap.range (ι Q) ≤ evenOdd Q 1

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ LinearMap.range (ι Q) ≤ evenOdd Q 1

Tactic:
refine le_trans ?_ (le_iSup _ ⟨1, Nat.cast_one⟩)

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ LinearMap.range (ι Q) ≤ LinearMap.range (ι Q) ^ ↑⟨1, ⋯⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ LinearMap.range (ι Q) ≤ LinearMap.range (ι Q) ^ ↑⟨1, ⋯⟩

Tactic:
exact (pow_one _).ge

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiff.prod_map {f : E → F} {g : E' → F'} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
    ContDiff 𝕜 n (Prod.map f g)

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : WithTop ℕ∞
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
F' : Type u_4
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
hf : ContDiff 𝕜 n f
hg : ContDiff 𝕜 n g
⊢ ContDiff 𝕜 n (Prod.map f g)

Tactic:
rw [contDiff_iff_contDiffAt] at *

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : WithTop ℕ∞
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
F' : Type u_4
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
hf : ∀ (x : E), ContDiffAt 𝕜 n f x
hg : ∀ (x : E'), ContDiffAt 𝕜 n g x
⊢ ∀ (x : E × E'), ContDiffAt 𝕜 n (Prod.map f g) x

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : WithTop ℕ∞
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
F' : Type u_4
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
hf : ∀ (x : E), ContDiffAt 𝕜 n f x
hg : ∀ (x : E'), ContDiffAt 𝕜 n g x
⊢ ∀ (x : E × E'), ContDiffAt 𝕜 n (Prod.map f g) x

Tactic:
exact fun ⟨x, y⟩ => (hf x).prod_map (hg y)

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma sub_one_lt_iff : m - 1 < n ↔ m ≤ n

Proof state:
m n : ℤ
⊢ m - 1 < n ↔ m ≤ n

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Nat/Factorial/DoubleFactorial.lean
theorem doubleFactorial_eq_prod_even : ∀ n : ℕ, (2 * n)‼ = ∏ i ∈ Finset.range n, 2 * (i + 1)
  | 0 => rfl
  | n + 1 => by
    rw [Finset.prod_range_succ, ← doubleFactorial_eq_prod_even _, mul_comm (2 * n)‼,
      (by ring : 2 * (n + 1) = 2 * n + 2)]
    rfl

Proof state:
n : ℕ
⊢ (2 * n + 2)‼ = (2 * n + 2) * (2 * n)‼

Tactic:
rfl

Result:
no goals

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

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
⊢ (2 * (n + 1))‼ = ∏ i ∈ Finset.range (n + 1), 2 * (i + 1)

Tactic:
rw [Finset.prod_range_succ, ← doubleFactorial_eq_prod_even _, mul_comm (2 * n)‼,
  (by ring : 2 * (n + 1) = 2 * n + 2)]

Result:
n : ℕ
⊢ (2 * n + 2)‼ = (2 * n + 2) * (2 * n)‼
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tdiv_mul_cancel_of_tmod_eq_zero {a b : Int} (H : a.tmod b = 0) : a.tdiv b * b = a

Proof state:
a b : Int
H : a.tmod b = 0
⊢ a.tdiv b * b = a

Tactic:
rw [Int.mul_comm, mul_tdiv_cancel_of_tmod_eq_zero H]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
lemma nndist_le_pi_nndist (f g : ∀ b, π b) (b : β) : nndist (f b) (g b) ≤ nndist f g

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
b : β
⊢ nndist (f b) (g b) ≤ nndist f g

Tactic:
rw [← ENNReal.coe_le_coe, ← edist_nndist, ← edist_nndist]

Result:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
b : β
⊢ edist (f b) (g b) ≤ edist f g

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
b : β
⊢ edist (f b) (g b) ≤ edist f g

Tactic:
exact edist_le_pi_edist f g b

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem affineIndependent_iff_not_finrank_vectorSpan_le [Fintype ι] (p : ι → P) {n : ℕ}
    (hc : Fintype.card ι = n + 2) :
    AffineIndependent k p ↔ ¬finrank k (vectorSpan k (Set.range p)) ≤ n

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 2
⊢ AffineIndependent k p ↔ ¬finrank k ↥(vectorSpan k (Set.range p)) ≤ n

Tactic:
rw [affineIndependent_iff_le_finrank_vectorSpan k p hc, ← Nat.lt_iff_add_one_le, lt_iff_not_ge]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
theorem nondegenerate_toBilin'_iff_det_ne_zero {M : Matrix ι ι A} :
    M.toBilin'.Nondegenerate ↔ M.det ≠ 0

Proof state:
A : Type u_5
inst✝³ : CommRing A
inst✝² : IsDomain A
ι : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
M : Matrix ι ι A
⊢ (toBilin' M).Nondegenerate ↔ M.det ≠ 0

Tactic:
rw [Matrix.nondegenerate_toBilin'_iff, Matrix.nondegenerate_iff_det_ne_zero]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem apply_eq_zero_iff (p : PMF α) (a : α) : p a = 0 ↔ a ∉ p.support

Proof state:
α : Type u_1
p : PMF α
a : α
⊢ p a = 0 ↔ a ∉ p.support

Tactic:
rw [mem_support_iff, Classical.not_not]

Result:
no goals