harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem contract_expand {f : R[X]} (hp : p ≠ 0) : contract p (expand R p f) = f

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p ≠ 0
⊢ contract p ((expand R p) f) = f

Tactic:
ext

Result:
case a
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p ≠ 0
n✝ : ℕ
⊢ (contract p ((expand R p) f)).coeff n✝ = f.coeff n✝

Proof state:
case a
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p ≠ 0
n✝ : ℕ
⊢ (contract p ((expand R p) f)).coeff n✝ = f.coeff n✝

Tactic:
simp [coeff_contract hp, coeff_expand hp.bot_lt, Nat.mul_div_cancel _ hp.bot_lt]

Result:
no goals
-- Mathlib/Computability/Halting.lean
theorem merge' {f g : α →. σ} (hf : Partrec f) (hg : Partrec g) :
    ∃ k : α →. σ,
      Partrec k ∧ ∀ a, (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk✝ : Nat.Partrec k
k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a ∈ f a_2, encode a = x) ∨
          ∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a ∈ g a_2, encode a = x) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)
⊢ (↑(decode ((k (encode a)).get hk))).Dom

Tactic:
obtain ⟨a', _, y, _, e⟩ | ⟨a', _, y, _, e⟩ := (H _).1 _ ⟨hk, rfl⟩ <;>
  simp only [e.symm, encodek, coe_some, some_dom]

Result:
no goals

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)
a : α
⊢ ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a

Tactic:
intro x h'

Result:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)
a : α
x : σ
h' : x ∈ k' a
⊢ x ∈ f a ∨ x ∈ g a
-- Mathlib/Data/Set/Countable.lean
theorem countable_setOf_nonempty_of_disjoint {f : β → Set α}
    (hf : Pairwise (Disjoint on f)) {s : Set α} (h'f : ∀ t, f t ⊆ s) (hs : s.Countable) :
    Set.Countable {t | (f t).Nonempty}

Proof state:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
⊢ (f t ∩ f t').Nonempty

Tactic:
refine ⟨F ⟨t, ht⟩, hF ⟨t, _⟩, ?_⟩

Result:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
⊢ ↑(F ⟨t, ht⟩) ∈ f t'
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma biUnion_mem {ι : Type*} (hC : IsSetRing C) {s : ι → Set α}
    (S : Finset ι) (hs : ∀ n ∈ S, s n ∈ C) :
    ⋃ i ∈ S, s i ∈ C

Proof state:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
⊢ ⋃ i ∈ S, s i ∈ C

Tactic:
induction S using Finset.induction with
| empty => simp [hC.empty_mem]
| @insert i S _ h =>
  simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
  refine hC.union_mem (hs i (mem_insert_self i S)) ?_
  exact h (fun n hnS ↦ hs n (mem_insert_of_mem hnS))

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
⊢ ⋃ i ∈ S, s i ∈ C

Tactic:
classical
induction S using Finset.induction with
| empty => simp [hC.empty_mem]
| @insert i S _ h =>
  simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
  refine hC.union_mem (hs i (mem_insert_self i S)) ?_
  exact h (fun n hnS ↦ hs n (mem_insert_of_mem hnS))

Result:
no goals

Proof state:
case insert
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
a✝ : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → ⋃ i ∈ S, s i ∈ C
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ ⋃ x ∈ ↑S, s x ∈ C

Tactic:
exact h (fun n hnS ↦ hs n (mem_insert_of_mem hnS))

Result:
no goals

Proof state:
case insert
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
a✝ : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → ⋃ i ∈ S, s i ∈ C
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ s i ∪ ⋃ x ∈ ↑S, s x ∈ C

Tactic:
refine hC.union_mem (hs i (mem_insert_self i S)) ?_

Result:
case insert
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
a✝ : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → ⋃ i ∈ S, s i ∈ C
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ ⋃ x ∈ ↑S, s x ∈ C

Proof state:
case empty
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
hs : ∀ n ∈ ∅, s n ∈ C
⊢ ⋃ i ∈ ∅, s i ∈ C

Tactic:
simp [hC.empty_mem]

Result:
no goals

Proof state:
case insert
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
a✝ : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → ⋃ i ∈ S, s i ∈ C
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ ⋃ i_1 ∈ insert i S, s i_1 ∈ C

Tactic:
simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]

Result:
case insert
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
a✝ : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → ⋃ i ∈ S, s i ∈ C
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ s i ∪ ⋃ x ∈ ↑S, s x ∈ C
-- Mathlib/Order/Hom/Basic.lean
theorem map_inv_lt_iff (f : F) {a : α} {b : β} : EquivLike.inv f b < a ↔ b < f a

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ EquivLike.inv f b < a ↔ b < f a

Tactic:
rw [← map_lt_map_iff f]

Result:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ f (EquivLike.inv f b) < f a ↔ b < f a

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ f (EquivLike.inv f b) < f a ↔ b < f a

Tactic:
simp only [EquivLike.apply_inv_apply]

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem image_mem_nhds {f : X → Y} (hf : IsOpenEmbedding f) {s : Set X} {x : X} :
    f '' s ∈ 𝓝 (f x) ↔ s ∈ 𝓝 x

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
s : Set X
x : X
⊢ f '' s ∈ 𝓝 (f x) ↔ s ∈ 𝓝 x

Tactic:
rw [← hf.map_nhds_eq, mem_map, preimage_image_eq _ hf.injective]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Defs.lean
theorem two_add_one_eq_three [AddMonoidWithOne R] : 2 + 1 = (3 : R)

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1 + 1) = 3

Tactic:
apply congrArg

Result:
case h
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 1 + 1 + 1 = 3

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 2 + 1 = 3

Tactic:
rw [← one_add_one_eq_two, ← Nat.cast_one, ← Nat.cast_add, ← Nat.cast_add]

Result:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1 + 1) = 3

Proof state:
case h
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 1 + 1 + 1 = 3

Tactic:
decide

Result:
no goals
-- Mathlib/SetTheory/Nimber/Basic.lean
theorem add_comm (a b : Nimber) : a + b = b + a

Proof state:
case h.e'_3.h.e'_3.h.e'_2.h.h.e'_2.h.e'_2.h.a
a b x✝¹ x✝ : Nimber
a✝ : x✝ < b
⊢ a + x✝ = x✝¹ ↔ x✝ + a = x✝¹

Tactic:
rw [Nimber.add_comm]

Result:
no goals

Proof state:
a b : Nimber
⊢ sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ = sInf {x | (∃ b' < a, b + b' = x) ∨ ∃ a' < b, a' + a = x}ᶜ

Tactic:
congr! 7 <;>
  (rw [and_congr_right_iff]; intro; rw [Nimber.add_comm])

Result:
no goals

Proof state:
a b : Nimber
⊢ a + b = b + a

Tactic:
rw [add_def, add_def]

Result:
a b : Nimber
⊢ sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ = sInf {x | (∃ a' < b, a' + a = x) ∨ ∃ b' < a, b + b' = x}ᶜ

Proof state:
a b : Nimber
⊢ sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ = sInf {x | (∃ a' < b, a' + a = x) ∨ ∃ b' < a, b + b' = x}ᶜ

Tactic:
simp_rw [or_comm]

Result:
a b : Nimber
⊢ sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ = sInf {x | (∃ b' < a, b + b' = x) ∨ ∃ a' < b, a' + a = x}ᶜ

Proof state:
case h.e'_3.h.e'_3.h.e'_2.h.h.e'_2.h.e'_2.h.a
a b x✝¹ x✝ : Nimber
⊢ x✝ < b ∧ a + x✝ = x✝¹ ↔ x✝ < b ∧ x✝ + a = x✝¹

Tactic:
rw [and_congr_right_iff]

Result:
case h.e'_3.h.e'_3.h.e'_2.h.h.e'_2.h.e'_2.h.a
a b x✝¹ x✝ : Nimber
⊢ x✝ < b → (a + x✝ = x✝¹ ↔ x✝ + a = x✝¹)

Proof state:
case h.e'_3.h.e'_3.h.e'_2.h.h.e'_2.h.e'_2.h.a
a b x✝¹ x✝ : Nimber
⊢ x✝ < b → (a + x✝ = x✝¹ ↔ x✝ + a = x✝¹)

Tactic:
intro

Result:
case h.e'_3.h.e'_3.h.e'_2.h.h.e'_2.h.e'_2.h.a
a b x✝¹ x✝ : Nimber
a✝ : x✝ < b
⊢ a + x✝ = x✝¹ ↔ x✝ + a = x✝¹
-- Mathlib/Algebra/Ring/Basic.lean
theorem vieta_formula_quadratic {b c x : α} (h : x * x - b * x + c = 0) :
    ∃ y : α, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c

Proof state:
α : Type u_2
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
⊢ -(x * x - b * x) = x * (b - x)

Tactic:
simp [mul_sub, mul_comm]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ (b - x) * (b - x) - b * (b - x) + c = 0

Tactic:
rw [this, sub_add, ← sub_mul, sub_self]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ x * (b - x) = c

Tactic:
rw [this]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ ∃ y, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c

Tactic:
refine ⟨b - x, ?_, by simp, by rw [this]⟩

Result:
α : Type u_2
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ (b - x) * (b - x) - b * (b - x) + c = 0

Proof state:
α : Type u_2
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ x + (b - x) = b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
⊢ ∃ y, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c

Tactic:
have : c = x * (b - x) := (eq_neg_of_add_eq_zero_right h).trans (by simp [mul_sub, mul_comm])

Result:
α : Type u_2
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ ∃ y, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c
-- Mathlib/MeasureTheory/Measure/OpenPos.lean
theorem dense_of_ae {p : X → Prop} (hp : ∀ᵐ x ∂μ, p x) : Dense {x | p x}

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
p : X → Prop
hp : ∀ᵐ (x : X) ∂μ, p x
⊢ interior {x | p x}ᶜ = ∅

Tactic:
exact μ.interior_eq_empty_of_null hp

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
p : X → Prop
hp : ∀ᵐ (x : X) ∂μ, p x
⊢ Dense {x | p x}

Tactic:
rw [dense_iff_closure_eq, closure_eq_compl_interior_compl, compl_univ_iff]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
p : X → Prop
hp : ∀ᵐ (x : X) ∂μ, p x
⊢ interior {x | p x}ᶜ = ∅
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem ofNat_shiftLeft_eq {x y : Nat} : (x <<< y : Int) = (x : Int) * (2 ^ y : Nat)

Proof state:
x y : Nat
⊢ ↑(x <<< y) = ↑x * ↑(2 ^ y)

Tactic:
simp [Nat.shiftLeft_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tmod_add_tdiv : ∀ a b : Int, tmod a b + b * (a.tdiv b) = a
  | ofNat _, ofNat _ => congrArg ofNat (Nat.mod_add_div ..)
  | ofNat m, -[n+1] => by
    show (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
    rw [Int.neg_mul_neg]; exact congrArg ofNat (Nat.mod_add_div ..)
  | -[m+1], 0 => by
    show -(↑((succ m) % 0) : Int) + 0 * -↑(succ m / 0) = -↑(succ m)
    rw [Nat.mod_zero, Int.zero_mul, Int.add_zero]
  | -[m+1], ofNat n => by
    show -(↑((succ m) % n) : Int) + ↑n * -↑(succ m / n) = -↑(succ m)
    rw [Int.mul_neg, ← Int.neg_add]
    exact congrArg (-ofNat ·) (Nat.mod_add_div ..)
  | -[m+1], -[n+1] => by
    show -(↑(succ m % succ n) : Int) + -↑(succ n) * ↑(succ m / succ n) = -↑(succ m)
    rw [Int.neg_mul, ← Int.neg_add]
    exact congrArg (-ofNat ·) (Nat.mod_add_div ..)

Proof state:
m n : Nat
⊢ -↑(m.succ % n) + ↑n * -↑(m.succ / n) = -↑m.succ

Tactic:
rw [Int.mul_neg, ← Int.neg_add]

Result:
m n : Nat
⊢ -(↑(m.succ % n) + ↑n * ↑(m.succ / n)) = -↑m.succ

Proof state:
m : Nat
⊢ -↑(m.succ % 0) + 0 * -↑(m.succ / 0) = -↑m.succ

Tactic:
rw [Nat.mod_zero, Int.zero_mul, Int.add_zero]

Result:
no goals

Proof state:
m n : Nat
⊢ -[m+1].tmod -[n+1] + -[n+1] * -[m+1].tdiv -[n+1] = -[m+1]

Tactic:
show -(↑(succ m % succ n) : Int) + -↑(succ n) * ↑(succ m / succ n) = -↑(succ m)

Result:
m n : Nat
⊢ -↑(m.succ % n.succ) + -↑n.succ * ↑(m.succ / n.succ) = -↑m.succ

Proof state:
m n : Nat
⊢ ↑m % ↑n.succ + ↑n.succ * ↑(m / n.succ) = ↑m

Tactic:
exact congrArg ofNat (Nat.mod_add_div ..)

Result:
no goals

Proof state:
m n : Nat
⊢ -↑(m.succ % n.succ) + -↑n.succ * ↑(m.succ / n.succ) = -↑m.succ

Tactic:
rw [Int.neg_mul, ← Int.neg_add]

Result:
m n : Nat
⊢ -(↑(m.succ % n.succ) + ↑n.succ * ↑(m.succ / n.succ)) = -↑m.succ

Proof state:
m n : Nat
⊢ ↑m % ↑n.succ + -↑n.succ * -↑(m / n.succ) = ↑m

Tactic:
rw [Int.neg_mul_neg]

Result:
m n : Nat
⊢ ↑m % ↑n.succ + ↑n.succ * ↑(m / n.succ) = ↑m

Proof state:
m n : Nat
⊢ (ofNat m).tmod -[n+1] + -[n+1] * (ofNat m).tdiv -[n+1] = ofNat m

Tactic:
show (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m

Result:
m n : Nat
⊢ ↑m % ↑n.succ + -↑n.succ * -↑(m / n.succ) = ↑m

Proof state:
m : Nat
⊢ -[m+1].tmod 0 + 0 * -[m+1].tdiv 0 = -[m+1]

Tactic:
show -(↑((succ m) % 0) : Int) + 0 * -↑(succ m / 0) = -↑(succ m)

Result:
m : Nat
⊢ -↑(m.succ % 0) + 0 * -↑(m.succ / 0) = -↑m.succ

Proof state:
m n : Nat
⊢ -[m+1].tmod (ofNat n) + ofNat n * -[m+1].tdiv (ofNat n) = -[m+1]

Tactic:
show -(↑((succ m) % n) : Int) + ↑n * -↑(succ m / n) = -↑(succ m)

Result:
m n : Nat
⊢ -↑(m.succ % n) + ↑n * -↑(m.succ / n) = -↑m.succ
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem isRightInversion_inv_iff {w t : W} :
    cs.IsRightInversion w⁻¹ t ↔ cs.IsLeftInversion w t

Proof state:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
ht : cs.IsReflection t
⊢ cs.length (w⁻¹ * t) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w

Tactic:
rw [← length_inv, mul_inv_rev, inv_inv, ht.inv, cs.length_inv w]

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ cs.IsRightInversion w⁻¹ t ↔ cs.IsLeftInversion w t

Tactic:
apply and_congr_right

Result:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ cs.IsReflection t → (cs.length (w⁻¹ * t) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w)

Proof state:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ cs.IsReflection t → (cs.length (w⁻¹ * t) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w)

Tactic:
intro ht

Result:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
ht : cs.IsReflection t
⊢ cs.length (w⁻¹ * t) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
-- Mathlib/Order/Category/PartOrd.lean
lemma inv_hom_apply {X Y : PartOrd} (e : X ≅ Y) (x : X) : e.inv (e.hom x) = x

Proof state:
X Y : PartOrd
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mul_lt_aleph0_iff_of_ne_zero {a b : Cardinal} (ha : a ≠ 0) (hb : b ≠ 0) :
    a * b < ℵ₀ ↔ a < ℵ₀ ∧ b < ℵ₀

Proof state:
a b : Cardinal.{u_1}
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b < ℵ₀ ↔ a < ℵ₀ ∧ b < ℵ₀

Tactic:
simp [mul_lt_aleph0_iff, ha, hb]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem isRegular_X_pow (n : ℕ) : IsRegular (X ^ n : R[X])

Proof state:
case a
R : Type u
inst✝ : Semiring R
n : ℕ
P Q : R[X]
hPQ : X ^ n * P = X ^ n * Q
i : ℕ
⊢ P.coeff i = Q.coeff i

Tactic:
rw [← coeff_X_pow_mul P n i, hPQ, coeff_X_pow_mul Q n i]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ IsRegular (X ^ n)

Tactic:
suffices IsLeftRegular (X^n : R[X]) from
  ⟨this, this.right_of_commute (fun p => commute_X_pow p n)⟩

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ IsLeftRegular (X ^ n)

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
P Q : R[X]
hPQ : X ^ n * P = X ^ n * Q
⊢ P = Q

Tactic:
ext i

Result:
case a
R : Type u
inst✝ : Semiring R
n : ℕ
P Q : R[X]
hPQ : X ^ n * P = X ^ n * Q
i : ℕ
⊢ P.coeff i = Q.coeff i

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ IsLeftRegular (X ^ n)

Tactic:
intro P Q (hPQ : X^n * P = X^n * Q)

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
P Q : R[X]
hPQ : X ^ n * P = X ^ n * Q
⊢ P = Q
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem frontier_Ioi' {a : α} (ha : (Ioi a).Nonempty) : frontier (Ioi a) = {a}

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
ha : (Ioi a).Nonempty
⊢ frontier (Ioi a) = {a}

Tactic:
simp [frontier, closure_Ioi' ha, Iic_diff_Iio, Icc_self]

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem openSegment_subset_union (x y : E) {z : E} (hz : z ∈ range (lineMap x y : 𝕜 → E)) :
    openSegment 𝕜 x y ⊆ insert z (openSegment 𝕜 x z ∪ openSegment 𝕜 z y)

Proof state:
case intro.intro.inr.inr.h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
hc : 0 < 1 - c
⊢ (lineMap y x) (1 - a) ∈ (fun a => (lineMap y ((lineMap y x) (1 - c))) (1 - a)) '' Ioo 0 1

Tactic:
refine
  ⟨(a - c) / (1 - c), ⟨div_pos (sub_pos.2 hca) hc, (div_lt_one hc).2 <| sub_lt_sub_right h₁ _⟩,
    ?_⟩

Result:
case intro.intro.inr.inr.h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
hc : 0 < 1 - c
⊢ (fun a => (lineMap y ((lineMap y x) (1 - c))) (1 - a)) ((a - c) / (1 - c)) = (lineMap y x) (1 - a)

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c : 𝕜
⊢ MapsTo (⇑(lineMap x y)) (Ioo 0 1)
    (insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1))

Tactic:
rintro a ⟨h₀, h₁⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1)

Proof state:
case intro.intro.inr.inr.h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
hc : 0 < 1 - c
⊢ (fun a => (lineMap y ((lineMap y x) (1 - c))) (1 - a)) ((a - c) / (1 - c)) = (lineMap y x) (1 - a)

Tactic:
simp only [← homothety_eq_lineMap, ← homothety_mul_apply, sub_mul, one_mul,
  div_mul_cancel₀ _ hc.ne', sub_sub_sub_cancel_right]

Result:
no goals

Proof state:
case intro.intro.inr.inr.h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
⊢ (lineMap x y) a ∈ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1

Tactic:
have hc : 0 < 1 - c := sub_pos.2 (hca.trans h₁)

Result:
case intro.intro.inr.inr.h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
hc : 0 < 1 - c
⊢ (lineMap x y) a ∈ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1
-- Mathlib/Analysis/Normed/Order/UpperLower.lean
lemma dist_inf_sup_pi (x y : ι → ℝ) : dist (x ⊓ y) (x ⊔ y) = dist x y

Proof state:
ι : Type u_2
inst✝ : Fintype ι
x y : ι → ℝ
⊢ dist (x ⊓ y) (x ⊔ y) = dist x y

Tactic:
refine congr_arg NNReal.toReal (Finset.sup_congr rfl fun i _ ↦ ?_)

Result:
ι : Type u_2
inst✝ : Fintype ι
x y : ι → ℝ
i : ι
x✝ : i ∈ Finset.univ
⊢ nndist ((x ⊓ y) i) ((x ⊔ y) i) = nndist (x i) (y i)

Proof state:
ι : Type u_2
inst✝ : Fintype ι
x y : ι → ℝ
i : ι
x✝ : i ∈ Finset.univ
⊢ nndist ((x ⊓ y) i) ((x ⊔ y) i) = nndist (x i) (y i)

Tactic:
simp only [Real.nndist_eq', max_sub_min_eq_abs, Pi.inf_apply,
  Pi.sup_apply, Real.nnabs_of_nonneg, abs_nonneg, Real.toNNReal_abs]

Result:
no goals
-- Mathlib/Order/Partition/Basic.lean
@[simp]
lemma iSup_eq (P : Partition s) : ⨆ x ∈ P, x = s

Proof state:
α : Type u_1
s : α
inst✝ : CompleteLattice α
P : Partition s
⊢ ⨆ x ∈ P, x = s

Tactic:
simp_rw [← P.sSup_eq, sSup_eq_iSup]

Result:
α : Type u_1
s : α
inst✝ : CompleteLattice α
P : Partition s
⊢ ⨆ x ∈ P, x = ⨆ a ∈ ↑P, a

Proof state:
α : Type u_1
s : α
inst✝ : CompleteLattice α
P : Partition s
⊢ ⨆ x ∈ P, x = ⨆ a ∈ ↑P, a

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem mul_ofDigits (n : ℕ) {b : ℕ} {l : List ℕ} :
    n * ofDigits b l = ofDigits b (l.map (n * ·))

Proof state:
case cons
n b hd : ℕ
tl : List ℕ
ih : n * ofDigits b tl = ofDigits b (List.map (fun x => n * x) tl)
⊢ n * ofDigits b (hd :: tl) = ofDigits b (List.map (fun x => n * x) (hd :: tl))

Tactic:
rw [List.map_cons, ofDigits_cons, ofDigits_cons, ← ih]

Result:
case cons
n b hd : ℕ
tl : List ℕ
ih : n * ofDigits b tl = ofDigits b (List.map (fun x => n * x) tl)
⊢ n * (hd + b * ofDigits b tl) = n * hd + b * (n * ofDigits b tl)

Proof state:
case nil
n b : ℕ
⊢ n * ofDigits b [] = ofDigits b (List.map (fun x => n * x) [])

Tactic:
rfl

Result:
no goals

Proof state:
n b : ℕ
l : List ℕ
⊢ n * ofDigits b l = ofDigits b (List.map (fun x => n * x) l)

Tactic:
induction l with
| nil => rfl
| cons hd tl ih =>
  rw [List.map_cons, ofDigits_cons, ofDigits_cons, ← ih]
  ring

Result:
no goals

Proof state:
case cons
n b hd : ℕ
tl : List ℕ
ih : n * ofDigits b tl = ofDigits b (List.map (fun x => n * x) tl)
⊢ n * (hd + b * ofDigits b tl) = n * hd + b * (n * ofDigits b tl)

Tactic:
ring

Result:
no goals