harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/NatAntidiagonal.lean
theorem mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} : x ∈ antidiagonal n ↔ x.1 + x.2 = n

Proof state:
x : ℕ × ℕ
⊢ (x.1, x.1 + x.2 - x.1).2 = x.2

Tactic:
simp only [Nat.add_sub_cancel_left]

Result:
no goals

Proof state:
case mp
n : ℕ
x : ℕ × ℕ
⊢ (∃ a ∈ range (n + 1), (a, n - a) = x) → x.1 + x.2 = n

Tactic:
rintro ⟨i, hi, rfl⟩

Result:
case mp.intro.intro
n i : ℕ
hi : i ∈ range (n + 1)
⊢ (i, n - i).1 + (i, n - i).2 = n

Proof state:
case mp.intro.intro
n i : ℕ
hi : i ≤ n
⊢ (i, n - i).1 + (i, n - i).2 = n

Tactic:
exact Nat.add_sub_cancel' hi

Result:
no goals

Proof state:
case mpr
x : ℕ × ℕ
⊢ ∃ a ∈ range (x.1 + x.2 + 1), (a, x.1 + x.2 - a) = x

Tactic:
refine ⟨x.fst, ?_, ?_⟩

Result:
case mpr.refine_1
x : ℕ × ℕ
⊢ x.1 ∈ range (x.1 + x.2 + 1)

case mpr.refine_2
x : ℕ × ℕ
⊢ (x.1, x.1 + x.2 - x.1) = x

Proof state:
case mpr
n : ℕ
x : ℕ × ℕ
⊢ x.1 + x.2 = n → ∃ a ∈ range (n + 1), (a, n - a) = x

Tactic:
rintro rfl

Result:
case mpr
x : ℕ × ℕ
⊢ ∃ a ∈ range (x.1 + x.2 + 1), (a, x.1 + x.2 - a) = x

Proof state:
n : ℕ
x : ℕ × ℕ
⊢ (∃ a ∈ range (n + 1), (a, n - a) = x) ↔ x.1 + x.2 = n

Tactic:
constructor

Result:
case mp
n : ℕ
x : ℕ × ℕ
⊢ (∃ a ∈ range (n + 1), (a, n - a) = x) → x.1 + x.2 = n

case mpr
n : ℕ
x : ℕ × ℕ
⊢ x.1 + x.2 = n → ∃ a ∈ range (n + 1), (a, n - a) = x

Proof state:
case mpr.refine_1
x : ℕ × ℕ
⊢ x.1 < x.1 + x.2 + 1

Tactic:
omega

Result:
no goals

Proof state:
case mpr.refine_2
x : ℕ × ℕ
⊢ (x.1, x.1 + x.2 - x.1) = x

Tactic:
exact Prod.ext rfl (by simp only [Nat.add_sub_cancel_left])

Result:
no goals

Proof state:
case mp.intro.intro
n i : ℕ
hi : i ∈ range (n + 1)
⊢ (i, n - i).1 + (i, n - i).2 = n

Tactic:
rw [mem_range, Nat.lt_succ_iff] at hi

Result:
case mp.intro.intro
n i : ℕ
hi : i ≤ n
⊢ (i, n - i).1 + (i, n - i).2 = n

Proof state:
n : ℕ
x : ℕ × ℕ
⊢ x ∈ antidiagonal n ↔ x.1 + x.2 = n

Tactic:
rw [antidiagonal, mem_map]

Result:
n : ℕ
x : ℕ × ℕ
⊢ (∃ a ∈ range (n + 1), (a, n - a) = x) ↔ x.1 + x.2 = n

Proof state:
case mpr.refine_1
x : ℕ × ℕ
⊢ x.1 ∈ range (x.1 + x.2 + 1)

Tactic:
rw [mem_range]

Result:
case mpr.refine_1
x : ℕ × ℕ
⊢ x.1 < x.1 + x.2 + 1
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem norm_rpow_of_nonneg {x y : ℝ} (hx_nonneg : 0 ≤ x) : ‖x ^ y‖ = ‖x‖ ^ y

Proof state:
x y : ℝ
hx_nonneg : 0 ≤ x
⊢ |x ^ y| = |x| ^ y

Tactic:
exact abs_rpow_of_nonneg hx_nonneg

Result:
no goals

Proof state:
x y : ℝ
hx_nonneg : 0 ≤ x
⊢ ‖x ^ y‖ = ‖x‖ ^ y

Tactic:
simp_rw [Real.norm_eq_abs]

Result:
x y : ℝ
hx_nonneg : 0 ≤ x
⊢ |x ^ y| = |x| ^ y
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem map_eq_of_eq {f : G →g G'} (f' : G →g G') (h : f = f') :
    p.map f = (p.map f').copy (h ▸ rfl) (h ▸ rfl)

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : G.Walk u v
f' : G →g G'
⊢ Walk.map f' p = (Walk.map f' p).copy ⋯ ⋯

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : G.Walk u v
f f' : G →g G'
h : f = f'
⊢ Walk.map f p = (Walk.map f' p).copy ⋯ ⋯

Tactic:
subst_vars

Result:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : G.Walk u v
f' : G →g G'
⊢ Walk.map f' p = (Walk.map f' p).copy ⋯ ⋯
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem maybeNormalize_eq {num den g} (den_nz reduced) :
    maybeNormalize num den g den_nz reduced =
    { num := num.tdiv g, den := den / g, den_nz, reduced }

Proof state:
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)
⊢ maybeNormalize num den g den_nz reduced = { num := num.tdiv ↑g, den := den / g, den_nz := den_nz, reduced := reduced }

Tactic:
unfold maybeNormalize

Result:
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)
⊢ (if hg : g = 1 then { num := num, den := den, den_nz := ⋯, reduced := ⋯ }
    else { num := num.tdiv ↑g, den := den / g, den_nz := den_nz, reduced := reduced }) =
    { num := num.tdiv ↑g, den := den / g, den_nz := den_nz, reduced := reduced }

Proof state:
case isFalse
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)
h✝ : ¬g = 1
⊢ { num := num.tdiv ↑g, den := den / g, den_nz := den_nz, reduced := reduced } =
    { num := num.tdiv ↑g, den := den / g, den_nz := den_nz, reduced := reduced }

Tactic:
rfl

Result:
no goals

Proof state:
case isTrue
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)
h✝ : g = 1
⊢ { num := num, den := den, den_nz := ⋯, reduced := ⋯ } =
    { num := num.tdiv ↑g, den := den / g, den_nz := den_nz, reduced := reduced }

Tactic:
subst g

Result:
case isTrue
num : Int
den : Nat
den_nz : den / 1 ≠ 0
reduced : (num.tdiv ↑1).natAbs.Coprime (den / 1)
⊢ { num := num, den := den, den_nz := ⋯, reduced := ⋯ } =
    { num := num.tdiv ↑1, den := den / 1, den_nz := den_nz, reduced := reduced }

Proof state:
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)
⊢ (if hg : g = 1 then { num := num, den := den, den_nz := ⋯, reduced := ⋯ }
    else { num := num.tdiv ↑g, den := den / g, den_nz := den_nz, reduced := reduced }) =
    { num := num.tdiv ↑g, den := den / g, den_nz := den_nz, reduced := reduced }

Tactic:
split

Result:
case isTrue
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)
h✝ : g = 1
⊢ { num := num, den := den, den_nz := ⋯, reduced := ⋯ } =
    { num := num.tdiv ↑g, den := den / g, den_nz := den_nz, reduced := reduced }

case isFalse
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)
h✝ : ¬g = 1
⊢ { num := num.tdiv ↑g, den := den / g, den_nz := den_nz, reduced := reduced } =
    { num := num.tdiv ↑g, den := den / g, den_nz := den_nz, reduced := reduced }

Proof state:
case isTrue
num : Int
den : Nat
den_nz : den / 1 ≠ 0
reduced : (num.tdiv ↑1).natAbs.Coprime (den / 1)
⊢ { num := num, den := den, den_nz := ⋯, reduced := ⋯ } =
    { num := num.tdiv ↑1, den := den / 1, den_nz := den_nz, reduced := reduced }

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
    m.size ≤ (m.erase k).size + 1

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
⊢ m.size ≤ (m.erase k).size + 1

Tactic:
simp_to_raw using Raw₀.size_le_size_erase ⟨m, _⟩

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
lemma ModularGroup_T_pow_mem_Gamma (N M : ℤ) (hNM : N ∣ M) :
    (ModularGroup.T ^ M) ∈ Gamma (Int.natAbs N)

Proof state:
N M : ℤ
hNM : N ∣ M
⊢ ↑N.natAbs ∣ M

Tactic:
simp only [Int.natCast_natAbs, abs_dvd, hNM]

Result:
no goals

Proof state:
N M : ℤ
hNM : N ∣ M
⊢ ModularGroup.T ^ M ∈ Γ(N.natAbs)

Tactic:
simp only [Gamma_mem, Fin.isValue, ModularGroup.coe_T_zpow, of_apply, cons_val', cons_val_zero,
  empty_val', cons_val_fin_one, Int.cast_one, cons_val_one, head_cons, head_fin_const,
  Int.cast_zero, and_self, and_true, true_and]

Result:
N M : ℤ
hNM : N ∣ M
⊢ ↑M = 0

Proof state:
N M : ℤ
hNM : N ∣ M
⊢ ↑M = 0

Tactic:
refine Iff.mpr (ZMod.intCast_zmod_eq_zero_iff_dvd M (Int.natAbs N)) ?_

Result:
N M : ℤ
hNM : N ∣ M
⊢ ↑N.natAbs ∣ M
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem concat_beq_concat [BEq α] {a b : α} {l₁ l₂ : List α} :
    (l₁ ++ [a] == l₂ ++ [b]) = (l₁ == l₂ && a == b)

Proof state:
case cons.cons
α : Type u_1
inst✝ : BEq α
a b x : α
l₁ : List α
ih : ∀ {l₂ : List α}, (l₁ ++ [a] == l₂ ++ [b]) = (l₁ == l₂ && a == b)
y : α
l₂ : List α
⊢ (x :: l₁ ++ [a] == y :: l₂ ++ [b]) = (x :: l₁ == y :: l₂ && a == b)

Tactic:
simp [ih, Bool.and_assoc]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : BEq α
a b : α
l₂ : List α
⊢ ([] ++ [a] == l₂ ++ [b]) = ([] == l₂ && a == b)

Tactic:
cases l₂ <;> simp

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
inst✝ : BEq α
a b x : α
l₁ : List α
ih : ∀ {l₂ : List α}, (l₁ ++ [a] == l₂ ++ [b]) = (l₁ == l₂ && a == b)
⊢ (x :: l₁ ++ [a] == [] ++ [b]) = (x :: l₁ == [] && a == b)

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : BEq α
a b x : α
l₁ : List α
ih : ∀ {l₂ : List α}, (l₁ ++ [a] == l₂ ++ [b]) = (l₁ == l₂ && a == b)
l₂ : List α
⊢ (x :: l₁ ++ [a] == l₂ ++ [b]) = (x :: l₁ == l₂ && a == b)

Tactic:
cases l₂ with
| nil => simp
| cons y l₂ => simp [ih, Bool.and_assoc]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
l₁ l₂ : List α
⊢ (l₁ ++ [a] == l₂ ++ [b]) = (l₁ == l₂ && a == b)

Tactic:
induction l₁ generalizing l₂ with
| nil => cases l₂ <;> simp
| cons x l₁ ih =>
  cases l₂ with
  | nil => simp
  | cons y l₂ => simp [ih, Bool.and_assoc]

Result:
no goals
-- Mathlib/Data/Set/Card/Arithmetic.lean
theorem exists_union_disjoint_ncard_eq_of_even (he : Even s.ncard) :
    ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard

Proof state:
case intro.intro.intro.intro
α : Type u_1
s : Set α
he : Even s.ncard
t u : Set α
hutu : t ∪ u = s
hdtu : Disjoint t u
hctu : #↑t = #↑u
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard

Tactic:
exact ⟨t, u, hutu, hdtu, congrArg Cardinal.toNat hctu⟩

Result:
no goals

Proof state:
α : Type u_1
s : Set α
he : Even s.ncard
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard

Tactic:
obtain ⟨t, u, hutu, hdtu, hctu⟩ := exists_union_disjoint_cardinal_eq_of_even he

Result:
case intro.intro.intro.intro
α : Type u_1
s : Set α
he : Even s.ncard
t u : Set α
hutu : t ∪ u = s
hdtu : Disjoint t u
hctu : #↑t = #↑u
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard
-- Mathlib/Data/Finset/Insert.lean
theorem insert_val' (a : α) (s : Finset α) : (insert a s).1 = dedup (a ::ₘ s.1)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).val = (a ::ₘ s.val).dedup

Tactic:
rw [dedup_cons, dedup_eq_self]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).val = ndinsert a s.val

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).val = ndinsert a s.val

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
lemma natDegree_eraseLead (h : f.nextCoeff ≠ 0) : f.eraseLead.natDegree = f.natDegree - 1

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.natDegree = f.natDegree - 1

Tactic:
refine f.eraseLead_natDegree_le.antisymm <| le_natDegree_of_ne_zero ?_

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.coeff (f.natDegree - 1) ≠ 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < 1

Tactic:
all_goals positivity

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ f.eraseLead.natDegree = f.natDegree - 1

Tactic:
have := natDegree_pos_of_nextCoeff_ne_zero h

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.natDegree = f.natDegree - 1

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.coeff (f.natDegree - 1) ≠ 0

Tactic:
rwa [eraseLead_coeff_of_ne _ (tsub_lt_self _ _).ne, ← nextCoeff_of_natDegree_pos]

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < 1

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < 1

Tactic:
positivity

Result:
no goals
-- Mathlib/CategoryTheory/Limits/EpiMono.lean
lemma mono_iff_isPullback : Mono f ↔ IsPullback (𝟙 X) (𝟙 X) f f

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
⊢ IsPullback (𝟙 X) (𝟙 X) f f → Mono f

Tactic:
intro hf

Result:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
hf : IsPullback (𝟙 X) (𝟙 X) f f
⊢ Mono f

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
a✝ : Mono f
⊢ IsPullback (𝟙 X) (𝟙 X) f f

Tactic:
exact IsPullback.of_isLimit (PullbackCone.isLimitMkIdId f)

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
⊢ Mono f ↔ IsPullback (𝟙 X) (𝟙 X) f f

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
⊢ Mono f → IsPullback (𝟙 X) (𝟙 X) f f

case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
⊢ IsPullback (𝟙 X) (𝟙 X) f f → Mono f

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
hf : IsPullback (𝟙 X) (𝟙 X) f f
⊢ Mono f

Tactic:
exact (mono_iff_fst_eq_snd hf.isLimit).2 rfl

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
⊢ Mono f → IsPullback (𝟙 X) (𝟙 X) f f

Tactic:
intro

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
a✝ : Mono f
⊢ IsPullback (𝟙 X) (𝟙 X) f f
-- Mathlib/MeasureTheory/Order/UpperLower.lean
theorem IsLowerSet.null_frontier (hs : IsLowerSet s) : volume (frontier s) = 0

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
⊢ x ∈
    {x |
        (fun x =>
            Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0)
              (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ

Tactic:
by_cases h : x ∈ closure s <;>
  simp only [mem_compl_iff, mem_setOf, h, not_false_eq_true, indicator_of_not_mem,
    indicator_of_mem, Pi.one_apply]

Result:
case pos
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
⊢ ¬Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)

case neg
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∉ closure s
⊢ ¬Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)

Proof state:
case pos
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
x✝ : ℝ
⊢ x ∈ frontier sᶜ

Tactic:
rwa [frontier_compl]

Result:
no goals

Proof state:
case pos
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
⊢ ¬Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)

Tactic:
refine aux₁ fun _ ↦ hs.compl.exists_subset_ball <| frontier_subset_closure ?_

Result:
case pos
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
x✝ : ℝ
⊢ x ∈ frontier sᶜ

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
⊢ volume (frontier s) = 0

Tactic:
refine measure_mono_null (fun x hx ↦ ?_)
  (Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet _
    (isClosed_closure (s := s)).measurableSet)

Result:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
⊢ x ∈
    {x |
        (fun x =>
            Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0)
              (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ

Proof state:
case neg
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∉ closure s
⊢ ¬Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)

Tactic:
exact aux₀ fun _ ↦ hs.exists_subset_ball <| frontier_subset_closure hx

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
nonrec lemma is3Clique_iff [NoAccidental t] {s : Finset (α ⊕ β ⊕ γ)} :
    (graph t).IsNClique 3 s ↔ ∃ x, x ∈ t ∧ toTriangle x = s

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
x y z : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
hxz : (graph t).Adj x z
hyz : (graph t).Adj y z
⊢ ∃ x_1 ∈ t, toTriangle x_1 = {x, y, z}

Tactic:
obtain ⟨a, b, c, habc, hab, hac, hbc⟩ := graph_triple hxy hxz hyz

Result:
case refine_1.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
x y z : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
hxz : (graph t).Adj x z
hyz : (graph t).Adj y z
a : α
b : β
c : γ
habc : {in₀ a, in₁ b, in₂ c} = {x, y, z}
hab : (graph t).Adj (in₀ a) (in₁ b)
hac : (graph t).Adj (in₀ a) (in₂ c)
hbc : (graph t).Adj (in₁ b) (in₂ c)
⊢ ∃ x_1 ∈ t, toTriangle x_1 = {x, y, z}

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
x y z : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
hxz : (graph t).Adj x z
hyz : (graph t).Adj y z
a : α
b : β
c : γ
habc : {in₀ a, in₁ b, in₂ c} = {x, y, z}
hab : (graph t).Adj (in₀ a) (in₁ b)
hac : (graph t).Adj (in₀ a) (in₂ c)
hbc : (graph t).Adj (in₁ b) (in₂ c)
c' : γ
hc' : (a, b, c') ∈ t
b' : β
hb' : (a, b', c) ∈ t
a' : α
ha' : (a', b, c) ∈ t
⊢ (a, b, c) ∈ t

Tactic:
obtain rfl | rfl | rfl := NoAccidental.eq_or_eq_or_eq ha' hb' hc' <;> assumption

Result:
no goals
-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem map_congr_perm [DecidableEq ι] [Fintype ι] (σ : Equiv.Perm ι) :
    g v = Equiv.Perm.sign σ • g (v ∘ σ)

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
g : M [⋀^ι]→ₗ[R] N'
v : ι → M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
σ : Equiv.Perm ι
⊢ g v = (Equiv.Perm.sign σ * Equiv.Perm.sign σ) • g v

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
g : M [⋀^ι]→ₗ[R] N'
v : ι → M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
σ : Equiv.Perm ι
⊢ g v = Equiv.Perm.sign σ • g (v ∘ ⇑σ)

Tactic:
rw [g.map_perm, smul_smul]

Result:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
g : M [⋀^ι]→ₗ[R] N'
v : ι → M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
σ : Equiv.Perm ι
⊢ g v = (Equiv.Perm.sign σ * Equiv.Perm.sign σ) • g v
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem map_subtype {p : α → Prop} {l : Vector { x // p x } n}
    {f : { x // p x } → β} {g : α → β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.map f = l.unattach.map g

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β
g : α → β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
l : Array { x // p x }
⊢ map f { toArray := l, size_toArray := ⋯ } = map g { toArray := l, size_toArray := ⋯ }.unattach

Tactic:
simp [Array.map_subtype hf]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
p : α → Prop
l : Vector { x // p x } n
f : { x // p x } → β
g : α → β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ map f l = map g l.unattach

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β
g : α → β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
l : Array { x // p x }
⊢ map f { toArray := l, size_toArray := ⋯ } = map g { toArray := l, size_toArray := ⋯ }.unattach
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_insertEntryIfNew [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
    (insertEntryIfNew k v l).isEmpty = false

Proof state:
case true
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l = true
⊢ l.isEmpty = false

Tactic:
exact isEmpty_eq_false_of_containsKey h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ (insertEntryIfNew k v l).isEmpty = false

Tactic:
cases h : containsKey k l

Result:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l = false
⊢ (insertEntryIfNew k v l).isEmpty = false

case true
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l = true
⊢ (insertEntryIfNew k v l).isEmpty = false

Proof state:
case true
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l = true
⊢ (insertEntryIfNew k v l).isEmpty = false

Tactic:
rw [insertEntryIfNew_of_containsKey h]

Result:
case true
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l = true
⊢ l.isEmpty = false

Proof state:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l = false
⊢ (insertEntryIfNew k v l).isEmpty = false

Tactic:
simp [insertEntryIfNew_of_containsKey_eq_false h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β}
    (h : m.WF) : (Const.alter m k f).getKey? k' =
      if k == k' then
        if (f (Const.get? m k)).isSome then some k else none
      else
        m.getKey? k'

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : Option β → Option β
h : m.WF
⊢ (alter m k f).getKey? k' =
    if (k == k') = true then if (f (get? m k)).isSome = true then some k else none else m.getKey? k'

Tactic:
simp_to_raw using Raw₀.Const.getKey?_alter

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem map_comp_map (f : M →ₗ[R'] N) (g : N →ₗ[R'] P) :
    map (g.comp f) = (map g).comp (map f)

Proof state:
case h
R' : Type u
M : Type v
inst✝¹² : CommSemiring R'
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R' M
inst✝⁹ : Module R'ᵐᵒᵖ M
inst✝⁸ : IsCentralScalar R' M
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R' N
inst✝⁵ : Module R'ᵐᵒᵖ N
inst✝⁴ : IsCentralScalar R' N
inst✝³ : AddCommMonoid P
inst✝² : Module R' P
inst✝¹ : Module R'ᵐᵒᵖ P
inst✝ : IsCentralScalar R' P
f : M →ₗ[R'] N
g : N →ₗ[R'] P
⊢ ∀ (m : M), (map (g ∘ₗ f)) (inr m) = ((map g).comp (map f)) (inr m)

Tactic:
simp only [map_inr, LinearMap.coe_comp, Function.comp_apply, AlgHom.coe_comp, forall_const]

Result:
no goals

Proof state:
R' : Type u
M : Type v
inst✝¹² : CommSemiring R'
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R' M
inst✝⁹ : Module R'ᵐᵒᵖ M
inst✝⁸ : IsCentralScalar R' M
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R' N
inst✝⁵ : Module R'ᵐᵒᵖ N
inst✝⁴ : IsCentralScalar R' N
inst✝³ : AddCommMonoid P
inst✝² : Module R' P
inst✝¹ : Module R'ᵐᵒᵖ P
inst✝ : IsCentralScalar R' P
f : M →ₗ[R'] N
g : N →ₗ[R'] P
⊢ map (g ∘ₗ f) = (map g).comp (map f)

Tactic:
apply algHom_ext

Result:
case h
R' : Type u
M : Type v
inst✝¹² : CommSemiring R'
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R' M
inst✝⁹ : Module R'ᵐᵒᵖ M
inst✝⁸ : IsCentralScalar R' M
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R' N
inst✝⁵ : Module R'ᵐᵒᵖ N
inst✝⁴ : IsCentralScalar R' N
inst✝³ : AddCommMonoid P
inst✝² : Module R' P
inst✝¹ : Module R'ᵐᵒᵖ P
inst✝ : IsCentralScalar R' P
f : M →ₗ[R'] N
g : N →ₗ[R'] P
⊢ ∀ (m : M), (map (g ∘ₗ f)) (inr m) = ((map g).comp (map f)) (inr m)
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem zpow_eq_one (h : IsPrimitiveRoot ζ k) : ζ ^ (k : ℤ) = 1

Proof state:
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
⊢ ζ ^ ↑k = 1

Tactic:
exact_mod_cast h.pow_eq_one

Result:
no goals