harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/TakeDrop.lean
@[simp] lemma left_eq_take_iff {x y : List α} {n : ℕ} :
    x.take n = (x ++ y).take n ↔ y = [] ∨ n ≤ x.length

Proof state:
α : Type u
x y : List α
n : ℕ
⊢ take n x = take n (x ++ y) ↔ y = [] ∨ n ≤ x.length

Tactic:
rw [Eq.comm]

Result:
α : Type u
x y : List α
n : ℕ
⊢ take n (x ++ y) = take n x ↔ y = [] ∨ n ≤ x.length

Proof state:
α : Type u
x y : List α
n : ℕ
⊢ take n (x ++ y) = take n x ↔ y = [] ∨ n ≤ x.length

Tactic:
apply take_eq_left_iff

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem cofinite.blimsup_set_eq :
    blimsup s cofinite p = { x | { n | p n ∧ x ∈ s n }.Infinite }

Proof state:
case h
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
⊢ x ∈ ⋂₀ {a | {x | p x ∧ ¬s x ⊆ a}.Finite} ↔ x ∈ {x | {n | p n ∧ x ∈ s n}.Infinite}

Tactic:
refine ⟨fun h => ?_, fun hx t h => ?_⟩ <;> contrapose! h

Result:
case h.refine_1
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∉ {x | {n | p n ∧ x ∈ s n}.Infinite}
⊢ x ∉ ⋂₀ {a | {x | p x ∧ ¬s x ⊆ a}.Finite}

case h.refine_2
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
hx : x ∈ {x | {n | p n ∧ x ∈ s n}.Infinite}
t : Set α
h : x ∉ t
⊢ t ∉ {a | {x | p x ∧ ¬s x ⊆ a}.Finite}

Proof state:
case h.refine_1
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∉ {x | {n | p n ∧ x ∈ s n}.Infinite}
⊢ x ∉ ⋂₀ {a | {x | p x ∧ ¬s x ⊆ a}.Finite}

Tactic:
simp only [mem_sInter, mem_setOf_eq, not_forall, exists_prop]

Result:
case h.refine_1
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∉ {x | {n | p n ∧ x ∈ s n}.Infinite}
⊢ ∃ x_1, {x | p x ∧ ¬s x ⊆ x_1}.Finite ∧ x ∉ x_1

Proof state:
case h.refine_2
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
hx : x ∈ {x | {n | p n ∧ x ∈ s n}.Infinite}
t : Set α
h : x ∉ t
⊢ t ∉ {a | {x | p x ∧ ¬s x ⊆ a}.Finite}

Tactic:
exact hx.mono fun i hi => ⟨hi.1, fun hit => h (hit hi.2)⟩

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∉ {x | {n | p n ∧ x ∈ s n}.Infinite}
⊢ x ∉ {x}ᶜ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ ⋂₀ {a | {x | p x ∧ ¬s x ⊆ a}.Finite} = {x | {n | p n ∧ x ∈ s n}.Infinite}

Tactic:
ext x

Result:
case h
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
⊢ x ∈ ⋂₀ {a | {x | p x ∧ ¬s x ⊆ a}.Finite} ↔ x ∈ {x | {n | p n ∧ x ∈ s n}.Infinite}

Proof state:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ blimsup s cofinite p = {x | {n | p n ∧ x ∈ s n}.Infinite}

Tactic:
simp only [blimsup_eq, le_eq_subset, eventually_cofinite, not_forall, sInf_eq_sInter, exists_prop]

Result:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ ⋂₀ {a | {x | p x ∧ ¬s x ⊆ a}.Finite} = {x | {n | p n ∧ x ∈ s n}.Infinite}

Proof state:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∉ {x | {n | p n ∧ x ∈ s n}.Infinite}
⊢ {x_1 | p x_1 ∧ ¬s x_1 ⊆ {x}ᶜ}.Finite

Tactic:
simpa using h

Result:
no goals

Proof state:
case h.refine_1
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∉ {x | {n | p n ∧ x ∈ s n}.Infinite}
⊢ ∃ x_1, {x | p x ∧ ¬s x ⊆ x_1}.Finite ∧ x ∉ x_1

Tactic:
exact ⟨{x}ᶜ, by simpa using h, by simp⟩

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
lemma mk'_mul_mk' (n₁ n₂ : ℤ) (d₁ d₂ : ℕ) (hd₁ hd₂ hnd₁ hnd₂) (h₁₂ : n₁.natAbs.Coprime d₂)
    (h₂₁ : n₂.natAbs.Coprime d₁) :
    mk' n₁ d₁ hd₁ hnd₁ * mk' n₂ d₂ hd₂ hnd₂ = mk' (n₁ * n₂) (d₁ * d₂) (Nat.mul_ne_zero hd₁ hd₂) (by
      rw [Int.natAbs_mul]; exact (hnd₁.mul h₂₁).mul_right (h₁₂.mul hnd₂))

Proof state:
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ { num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ } * { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ } =
    { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }

Tactic:
rw [mul_def]

Result:
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ normalize
      ({ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ }.num *
        { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ }.num)
      ({ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ }.den *
        { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ }.den)
      ⋯ =
    { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }

Proof state:
q : ℚ
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ (n₁.natAbs * n₂.natAbs).Coprime (d₁ * d₂)

Tactic:
exact (hnd₁.mul h₂₁).mul_right (h₁₂.mul hnd₂)

Result:
no goals

Proof state:
q : ℚ
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ (n₁ * n₂).natAbs.Coprime (d₁ * d₂)

Tactic:
rw [Int.natAbs_mul]

Result:
q : ℚ
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ (n₁.natAbs * n₂.natAbs).Coprime (d₁ * d₂)

Proof state:
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ normalize
      ({ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ }.num *
        { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ }.num)
      ({ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ }.den *
        { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ }.den)
      ⋯ =
    { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }

Tactic:
dsimp

Result:
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ normalize (n₁ * n₂) (d₁ * d₂) ⋯ = { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }

Proof state:
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ normalize (n₁ * n₂) (d₁ * d₂) ⋯ = { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }

Tactic:
simp [mk_eq_normalize]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem schur_complement_eq₁₁ [Fintype m] [DecidableEq m] [Fintype n] {A : Matrix m m 𝕜}
    (B : Matrix m n 𝕜) (D : Matrix n n 𝕜) (x : m → 𝕜) (y : n → 𝕜) [Invertible A]
    (hA : A.IsHermitian) :
    (star (x ⊕ᵥ y)) ᵥ* (fromBlocks A B Bᴴ D) ⬝ᵥ (x ⊕ᵥ y) =
      (star (x + (A⁻¹ * B) *ᵥ y)) ᵥ* A ⬝ᵥ (x + (A⁻¹ * B) *ᵥ y) +
        (star y) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ y

Proof state:
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁵ : CommRing 𝕜
inst✝⁴ : StarRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible A
hA : A.IsHermitian
⊢ star (x ⊕ᵥ y) ᵥ* fromBlocks A B Bᴴ D ⬝ᵥ (x ⊕ᵥ y) =
    star (x + (A⁻¹ * B) *ᵥ y) ᵥ* A ⬝ᵥ (x + (A⁻¹ * B) *ᵥ y) + star y ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ y

Tactic:
simp [Function.star_sumElim, fromBlocks_mulVec, vecMul_fromBlocks, add_vecMul,
  dotProduct_mulVec, vecMul_sub, Matrix.mul_assoc, vecMul_mulVec, hA.eq,
  conjTranspose_nonsing_inv, star_mulVec]

Result:
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁵ : CommRing 𝕜
inst✝⁴ : StarRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible A
hA : A.IsHermitian
⊢ star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) =
    star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* (Bᴴ * (A⁻¹ * B)) ⬝ᵥ y) +
      (star y ᵥ* D ⬝ᵥ y - star y ᵥ* (Bᴴ * (A⁻¹ * B)) ⬝ᵥ y)

Proof state:
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁵ : CommRing 𝕜
inst✝⁴ : StarRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible A
hA : A.IsHermitian
⊢ star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) =
    star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* (Bᴴ * (A⁻¹ * B)) ⬝ᵥ y) +
      (star y ᵥ* D ⬝ᵥ y - star y ᵥ* (Bᴴ * (A⁻¹ * B)) ⬝ᵥ y)

Tactic:
abel

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Trace.lean
lemma trace_diagonal {o} [Fintype o] [DecidableEq o] (d : o → R) :
    trace (diagonal d) = ∑ i, d i

Proof state:
R : Type u_6
inst✝² : AddCommMonoid R
o : Type u_8
inst✝¹ : Fintype o
inst✝ : DecidableEq o
d : o → R
⊢ (diagonal d).trace = ∑ i : o, d i

Tactic:
simp only [trace, diag_apply, diagonal_apply_eq]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem mem_frange {f : α →₀ M} {y : M} : y ∈ f.frange ↔ y ≠ 0 ∧ ∃ x, f x = y

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
y : M
⊢ y ∈ f.frange ↔ y ≠ 0 ∧ ∃ x, f x = y

Tactic:
rw [frange, @Finset.mem_image _ _ (Classical.decEq _) _ f.support]

Result:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
y : M
⊢ (∃ a ∈ f.support, f a = y) ↔ y ≠ 0 ∧ ∃ x, f x = y

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
y : M
⊢ (∃ a ∈ f.support, f a = y) ↔ y ≠ 0 ∧ ∃ x, f x = y

Tactic:
exact ⟨fun ⟨x, hx1, hx2⟩ => ⟨hx2 ▸ mem_support_iff.1 hx1, x, hx2⟩, fun ⟨hy, x, hx⟩ =>
  ⟨x, mem_support_iff.2 (hx.symm ▸ hy), hx⟩⟩

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean
theorem IsHenstock.card_filter_tag_eq_le [Fintype ι] (h : π.IsHenstock) (x : ι → ℝ) :
    #{J ∈ π.boxes | π.tag J = x} ≤ 2 ^ Fintype.card ι

Proof state:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
h : π.IsHenstock
x : ι → ℝ
J : Box ι
hJ : J ∈ π.boxes ∧ π.tag J = x
⊢ J ∈ π.boxes ∧ x ∈ Box.Icc J

Tactic:
rcases hJ with ⟨hJ, rfl⟩

Result:
case intro
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
h : π.IsHenstock
J : Box ι
hJ : J ∈ π.boxes
⊢ J ∈ π.boxes ∧ π.tag J ∈ Box.Icc J

Proof state:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
h : π.IsHenstock
x : ι → ℝ
⊢ #(Finset.filter (fun J => π.tag J = x) π.boxes) ≤ 2 ^ Fintype.card ι

Tactic:
calc
  #{J ∈ π.boxes | π.tag J = x} ≤ #{J ∈ π.boxes | x ∈ Box.Icc J} := by
    refine Finset.card_le_card fun J hJ => ?_
    rw [Finset.mem_filter] at hJ ⊢; rcases hJ with ⟨hJ, rfl⟩
    exact ⟨hJ, h J hJ⟩
  _ ≤ 2 ^ Fintype.card ι := π.toPrepartition.card_filter_mem_Icc_le x

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
h : π.IsHenstock
x : ι → ℝ
J : Box ι
hJ : J ∈ Finset.filter (fun J => π.tag J = x) π.boxes
⊢ J ∈ Finset.filter (fun J => x ∈ Box.Icc J) π.boxes

Tactic:
rw [Finset.mem_filter] at hJ ⊢

Result:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
h : π.IsHenstock
x : ι → ℝ
J : Box ι
hJ : J ∈ π.boxes ∧ π.tag J = x
⊢ J ∈ π.boxes ∧ x ∈ Box.Icc J

Proof state:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
h : π.IsHenstock
x : ι → ℝ
⊢ #(Finset.filter (fun J => π.tag J = x) π.boxes) ≤ 2 ^ Fintype.card ι

Tactic:
classical
calc
  #{J ∈ π.boxes | π.tag J = x} ≤ #{J ∈ π.boxes | x ∈ Box.Icc J} := by
    refine Finset.card_le_card fun J hJ => ?_
    rw [Finset.mem_filter] at hJ ⊢; rcases hJ with ⟨hJ, rfl⟩
    exact ⟨hJ, h J hJ⟩
  _ ≤ 2 ^ Fintype.card ι := π.toPrepartition.card_filter_mem_Icc_le x

Result:
no goals

Proof state:
case intro
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
h : π.IsHenstock
J : Box ι
hJ : J ∈ π.boxes
⊢ J ∈ π.boxes ∧ π.tag J ∈ Box.Icc J

Tactic:
exact ⟨hJ, h J hJ⟩

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
h : π.IsHenstock
x : ι → ℝ
⊢ #(Finset.filter (fun J => π.tag J = x) π.boxes) ≤ #(Finset.filter (fun J => x ∈ Box.Icc J) π.boxes)

Tactic:
refine Finset.card_le_card fun J hJ => ?_

Result:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
h : π.IsHenstock
x : ι → ℝ
J : Box ι
hJ : J ∈ Finset.filter (fun J => π.tag J = x) π.boxes
⊢ J ∈ Finset.filter (fun J => x ∈ Box.Icc J) π.boxes
-- Mathlib/LinearAlgebra/UnitaryGroup.lean
theorem det_of_mem_unitary {A : Matrix n n α} (hA : A ∈ Matrix.unitaryGroup n α) :
    A.det ∈ unitary α

Proof state:
case left
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ star A.det * A.det = 1

Tactic:
simpa [star, det_transpose] using congr_arg det hA.1

Result:
no goals

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ A.det ∈ unitary α

Tactic:
constructor

Result:
case left
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ star A.det * A.det = 1

case right
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ A.det * star A.det = 1

Proof state:
case right
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ A.det * star A.det = 1

Tactic:
simpa [star, det_transpose] using congr_arg det hA.2

Result:
no goals
-- Mathlib/Topology/Instances/AddCircle.lean
lemma toAddCircle_injective : Function.Injective (toAddCircle : ZMod N → _)

Proof state:
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : toAddCircle x = toAddCircle y
⊢ x = y

Tactic:
have : (0 : ℝ) < N := Nat.cast_pos.mpr (NeZero.pos _)

Result:
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : toAddCircle x = toAddCircle y
this : 0 < ↑N
⊢ x = y

Proof state:
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ 0 ≤ ↑y.val / ↑N

Tactic:
positivity

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : toAddCircle x = toAddCircle y
this : 0 < ↑N
⊢ x = y

Tactic:
rwa [toAddCircle_apply, toAddCircle_apply, AddCircle.coe_eq_coe_iff_of_mem_Ico
  (hp := Real.fact_zero_lt_one) (a := 0), div_left_inj' this.ne', Nat.cast_inj,
  (val_injective N).eq_iff] at hxy <;>
exact ⟨by positivity, by simpa only [zero_add, div_lt_one this, Nat.cast_lt] using val_lt _⟩

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
⊢ Injective ⇑toAddCircle

Tactic:
intro x y hxy

Result:
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : toAddCircle x = toAddCircle y
⊢ x = y

Proof state:
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑y.val / ↑N < 0 + 1

Tactic:
simpa only [zero_add, div_lt_one this, Nat.cast_lt] using val_lt _

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem colimit.pre_desc (c : Cocone F) :
    colimit.pre F E ≫ colimit.desc F c = colimit.desc (E ⋙ F) (c.whisker E)

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
c : Cocone F
⊢ pre F E ≫ desc F c = desc (E ⋙ F) (Cocone.whisker E c)

Tactic:
ext

Result:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
c : Cocone F
j✝ : K
⊢ ι (E ⋙ F) j✝ ≫ pre F E ≫ desc F c = ι (E ⋙ F) j✝ ≫ desc (E ⋙ F) (Cocone.whisker E c)

Proof state:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
c : Cocone F
j✝ : K
⊢ ι F (E.obj j✝) ≫ desc F c = ι (E ⋙ F) j✝ ≫ desc (E ⋙ F) (Cocone.whisker E c)

Tactic:
simp

Result:
no goals

Proof state:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
c : Cocone F
j✝ : K
⊢ ι (E ⋙ F) j✝ ≫ pre F E ≫ desc F c = ι (E ⋙ F) j✝ ≫ desc (E ⋙ F) (Cocone.whisker E c)

Tactic:
rw [← assoc, colimit.ι_pre]

Result:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
c : Cocone F
j✝ : K
⊢ ι F (E.obj j✝) ≫ desc F c = ι (E ⋙ F) j✝ ≫ desc (E ⋙ F) (Cocone.whisker E c)
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem midpoint_add_sub (x y : V) : midpoint R (x + y) (x - y) = x

Proof state:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R (x - y) (x + y) = x

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R (x + y) (x - y) = x

Tactic:
rw [midpoint_comm]

Result:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R (x - y) (x + y) = x
-- Mathlib/Topology/MetricSpace/Holder.lean
theorem nndist_le_of_le (hf : HolderOnWith C r f s) (hx : x ∈ s) (hy : y ∈ s)
    {d : ℝ≥0} (hd : nndist x y ≤ d) : nndist (f x) (f y) ≤ C * d ^ (r : ℝ)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : nndist x y ≤ d
⊢ edist (f x) (f y) ≤ ↑C * ↑d ^ ↑r

Tactic:
apply hf.edist_le_of_le hx hy

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : nndist x y ≤ d
⊢ edist x y ≤ ↑d

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : nndist x y ≤ d
⊢ nndist (f x) (f y) ≤ C * d ^ ↑r

Tactic:
rw [← ENNReal.coe_le_coe, ← edist_nndist, ENNReal.coe_mul,
  ENNReal.coe_rpow_of_nonneg _ r.coe_nonneg]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : nndist x y ≤ d
⊢ edist (f x) (f y) ≤ ↑C * ↑d ^ ↑r

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : nndist x y ≤ d
⊢ edist x y ≤ ↑d

Tactic:
rwa [edist_nndist, ENNReal.coe_le_coe]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem eq_mul_inv_iff_mul_eq : a = b * c⁻¹ ↔ a * c = b :=
  ⟨fun h ↦ by rw [h, inv_mul_cancel_right], fun h ↦ by rw [← h, mul_inv_cancel_right]⟩

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : a = b * c⁻¹
⊢ a * c = b

Tactic:
rw [h, inv_mul_cancel_right]

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : a * c = b
⊢ a = b * c⁻¹

Tactic:
rw [← h, mul_inv_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem coe_bot : ((⊥ : NonUnitalSubalgebra R A) : Set A) = {0}

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
⊢ ↑⊥ = {0}

Tactic:
simp [Set.ext_iff, NonUnitalAlgebra.mem_bot]

Result:
no goals
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem _root_.IsOpen.isOpen_inter_preimage_of_deriv_eq_zero
    (hs : IsOpen s) (hf : DifferentiableOn 𝕜 f s)
    (hf' : s.EqOn (deriv f) 0) (t : Set G) : IsOpen (s ∩ f ⁻¹' t) :=
  hs.isOpen_inter_preimage_of_fderiv_eq_zero hf
    (fun x hx ↦ by ext; simp [← deriv_fderiv, hf' hx]) t

Proof state:
case h
𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
hs : IsOpen s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (deriv f) 0 s
t : Set G
x : 𝕜
hx : x ∈ s
⊢ (fderiv 𝕜 f x) 1 = (0 x) 1

Tactic:
simp [← deriv_fderiv, hf' hx]

Result:
no goals

Proof state:
𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
hs : IsOpen s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (deriv f) 0 s
t : Set G
x : 𝕜
hx : x ∈ s
⊢ fderiv 𝕜 f x = 0 x

Tactic:
ext

Result:
case h
𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
hs : IsOpen s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (deriv f) 0 s
t : Set G
x : 𝕜
hx : x ∈ s
⊢ (fderiv 𝕜 f x) 1 = (0 x) 1
-- Mathlib/Algebra/DirectSum/Module.lean
theorem IsInternal.submodule_iSup_eq_top (h : IsInternal A) : iSup A = ⊤

Proof state:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
⊢ Function.Surjective ⇑((DFinsupp.lsum ℕ) fun i => (A i).subtype)

Tactic:
exact Function.Bijective.surjective h

Result:
no goals

Proof state:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
⊢ iSup A = ⊤

Tactic:
rw [Submodule.iSup_eq_range_dfinsupp_lsum, LinearMap.range_eq_top]

Result:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
⊢ Function.Surjective ⇑((DFinsupp.lsum ℕ) fun i => (A i).subtype)
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem norm_integral_le (f : α →₁[μ] E) : ‖integral f‖ ≤ ‖f‖ :=
  calc
    ‖integral f‖ = ‖integralCLM f‖

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ ‖integral f‖ = ‖integralCLM f‖

Tactic:
simp only [integral]

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubring/Basic.lean
theorem mem_bot {x : R} : x ∈ (⊥ : NonUnitalSubring R) ↔ x = 0 :=
  show x ∈ ((⊥ : NonUnitalSubring R) : Set R) ↔ x = 0 by rw [coe_bot, Set.mem_singleton_iff]

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
x : R
⊢ x ∈ ↑⊥ ↔ x = 0

Tactic:
rw [coe_bot, Set.mem_singleton_iff]

Result:
no goals