harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem pairwise_lt_range (n : Nat) : Pairwise (· < ·) (range n)

Proof state:
n : Nat
⊢ Pairwise (fun x1 x2 => x1 < x2) (range n)

Tactic:
simp +decide only [range_eq_range', pairwise_lt_range']

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Finite.exists_finset {s : Set α} (h : s.Finite) :
    ∃ s' : Finset α, ∀ a : α, a ∈ s' ↔ a ∈ s

Proof state:
case intro
α : Type u
s : Set α
h : s.Finite
val✝ : Fintype ↑s
⊢ ∃ s', ∀ (a : α), a ∈ s' ↔ a ∈ s

Tactic:
exact ⟨s.toFinset, fun _ => mem_toFinset⟩

Result:
no goals

Proof state:
α : Type u
s : Set α
h : s.Finite
⊢ ∃ s', ∀ (a : α), a ∈ s' ↔ a ∈ s

Tactic:
cases h.nonempty_fintype

Result:
case intro
α : Type u
s : Set α
h : s.Finite
val✝ : Fintype ↑s
⊢ ∃ s', ∀ (a : α), a ∈ s' ↔ a ∈ s
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
theorem edist_eq_one_iff_adj : G.edist u v = 1 ↔ G.Adj u v

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v = 1 ↔ G.Adj u v

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
⊢ G.Adj u v

case refine_2
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ G.edist u v = 1

Proof state:
case refine_1
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
⊢ G.Adj u v

Tactic:
obtain ⟨w, hw⟩ := exists_walk_of_edist_ne_top <| by rw [h]; simp

Result:
case refine_1.intro
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
w : G.Walk u v
hw : ↑w.length = G.edist u v
⊢ G.Adj u v

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
⊢ 1 ≠ ⊤

Tactic:
simp

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
⊢ edist ?m.10924 ?m.10925 ?m.10926 ≠ ⊤

Tactic:
rw [h]

Result:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
⊢ 1 ≠ ⊤

Proof state:
case refine_2
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ G.edist u v = 1

Tactic:
exact le_antisymm (edist_le h.toWalk) (Order.one_le_iff_pos.mpr <| edist_pos_of_ne h.ne)

Result:
no goals

Proof state:
case refine_1.intro
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
w : G.Walk u v
hw : ↑w.length = G.edist u v
⊢ G.Adj u v

Tactic:
exact w.adj_of_length_eq_one <| Nat.cast_eq_one.mp <| h ▸ hw

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem isoPullback_inv_snd (h : IsPullback fst snd f g) [HasPullback f g] :
    h.isoPullback.inv ≫ snd = pullback.snd _ _

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ h.isoPullback.inv ≫ snd = pullback.snd f g

Tactic:
simp [Iso.inv_comp_eq]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem le_tsub_of_add_le_right (hb : AddLECancellable b) (h : a + b ≤ c) : a ≤ c - b :=
  hb.le_tsub_of_add_le_left <| by rwa [add_comm]

Proof state:
α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a + b ≤ c
⊢ b + a ≤ c

Tactic:
rwa [add_comm]

Result:
no goals
-- Mathlib/Data/Nat/WithBot.lean
theorem coe_nonneg {n : ℕ} : 0 ≤ (n : WithBot ℕ)

Proof state:
n : ℕ
⊢ 0 ≤ ↑n

Tactic:
rw [← WithBot.coe_zero, cast_withBot, WithBot.coe_le_coe]

Result:
n : ℕ
⊢ 0 ≤ n

Proof state:
n : ℕ
⊢ 0 ≤ n

Tactic:
exact n.zero_le

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem matrixOfPolynomials_blockTriangular {R} [Semiring R] {n : ℕ} (p : Fin n → R[X])
    (h_deg : ∀ i, (p i).natDegree ≤ i) :
    Matrix.BlockTriangular (Matrix.of (fun (i j : Fin n) => (p j).coeff i)) id :=
  fun _ j h => by
    exact coeff_eq_zero_of_natDegree_lt <| Nat.lt_of_le_of_lt (h_deg j) h

Proof state:
R : Type u_8
inst✝ : Semiring R
n : ℕ
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
x✝ j : Fin n
h : id j < id x✝
⊢ of (fun i j => (p j).coeff ↑i) x✝ j = 0

Tactic:
exact coeff_eq_zero_of_natDegree_lt <| Nat.lt_of_le_of_lt (h_deg j) h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Range/Lemmas.lean
theorem forIn'_eq_forIn'_range' [Monad m] (r : Std.Range)
    (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) :
    forIn' r init f =
      forIn' (List.range' r.start r.size r.step) init (fun a h => f a (mem_of_mem_range' h))

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
⊢ forIn'.loop r f init r.start ⋯ ⋯ = forIn' (List.range' r.start r.size r.step) init fun a h => f a ⋯

Tactic:
simp only [size]

Result:
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
⊢ forIn'.loop r f init r.start ⋯ ⋯ =
    forIn' (List.range' r.start ((r.stop - r.start + r.step - 1) / r.step) r.step) init fun a h => f a ⋯

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
⊢ forIn'.loop r f init r.start ⋯ ⋯ =
    forIn' (List.range' r.start ((r.stop - r.start + r.step - 1) / r.step) r.step) init fun a h => f a ⋯

Tactic:
rw [forIn'_loop_eq_forIn'_range']

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
⊢ forIn' r init f = forIn' (List.range' r.start r.size r.step) init fun a h => f a ⋯

Tactic:
conv => lhs; simp only [forIn', Range.forIn']

Result:
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
⊢ forIn'.loop r f init r.start ⋯ ⋯ = forIn' (List.range' r.start r.size r.step) init fun a h => f a ⋯
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem exists_lt_of_lt_ciSup' {f : ι → α} {a : α} (h : a < ⨆ i, f i) : ∃ i, a < f i

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
a : α
h : ∀ (i : ι), f i ≤ a
⊢ ⨆ i, f i ≤ a

Tactic:
exact ciSup_le' h

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
a : α
h : a < ⨆ i, f i
⊢ ∃ i, a < f i

Tactic:
contrapose! h

Result:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
a : α
h : ∀ (i : ι), f i ≤ a
⊢ ⨆ i, f i ≤ a
-- Mathlib/NumberTheory/LSeries/HurwitzZeta.lean
lemma cosZeta_eq (a : UnitAddCircle) (s : ℂ) :
    cosZeta a s = (expZeta a s + expZeta (-a) s) / 2

Proof state:
a : UnitAddCircle
s : ℂ
⊢ cosZeta a s = (cosZeta a s + I * sinZeta a s + (cosZeta a s + I * -sinZeta a s)) / 2

Tactic:
ring_nf

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
⊢ cosZeta a s = (expZeta a s + expZeta (-a) s) / 2

Tactic:
rw [expZeta, expZeta, cosZeta_neg, sinZeta_neg]

Result:
a : UnitAddCircle
s : ℂ
⊢ cosZeta a s = (cosZeta a s + I * sinZeta a s + (cosZeta a s + I * -sinZeta a s)) / 2
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem derivWithin_const_add_fun (c : F) :
    derivWithin (c + f ·) = derivWithin f

Proof state:
case h.h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
c : F
x✝¹ : Set 𝕜
x✝ : 𝕜
⊢ derivWithin (fun x => c + f x) x✝¹ x✝ = derivWithin f x✝¹ x✝

Tactic:
apply derivWithin_const_add

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
c : F
⊢ (derivWithin fun x => c + f x) = derivWithin f

Tactic:
ext

Result:
case h.h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
c : F
x✝¹ : Set 𝕜
x✝ : 𝕜
⊢ derivWithin (fun x => c + f x) x✝¹ x✝ = derivWithin f x✝¹ x✝
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem Monic.mul {f g : MvPolynomial σ R} (hf : m.Monic f) (hg : m.Monic g) :
    m.Monic (f * g)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ m.Monic (f * g)

Tactic:
rw [Monic, MonomialOrder.leadingCoeff,
  degree_mul_of_mul_leadingCoeff_ne_zero, coeff_mul_of_degree_add, this]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0

Tactic:
rw [this]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ 1 ≠ 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
⊢ m.Monic (f * g)

Tactic:
suffices m.leadingCoeff f * m.leadingCoeff g = 1 by
  rw [Monic, MonomialOrder.leadingCoeff,
    degree_mul_of_mul_leadingCoeff_ne_zero, coeff_mul_of_degree_add, this]
  rw [this]
  exact one_ne_zero

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
⊢ m.leadingCoeff f * m.leadingCoeff g = 1

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
⊢ m.leadingCoeff f * m.leadingCoeff g = 1

Tactic:
rw [hf.leadingCoeff_eq_one, hg.leadingCoeff_eq_one, one_mul]

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
⊢ m.Monic (f * g)

Tactic:
nontriviality R

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
⊢ m.Monic (f * g)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Instances.lean
theorem run_map [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α)
    : (f <$> x).run = Except.map f <$> x.run

Proof state:
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : ExceptT ε m α
⊢ (mk do
        let a ← x
        match a with
          | Except.ok a => pure (Except.ok (f a))
          | Except.error e => pure (Except.error e)).run =
    do
    let a ← x.run
    pure (Except.map f a)

Tactic:
apply bind_congr

Result:
case h
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : ExceptT ε m α
⊢ ∀ (a : Except ε α),
    (match a with
      | Except.ok a => pure (Except.ok (f a))
      | Except.error e => pure (Except.error e)) =
      pure (Except.map f a)

Proof state:
case h
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : ExceptT ε m α
⊢ ∀ (a : Except ε α),
    (match a with
      | Except.ok a => pure (Except.ok (f a))
      | Except.error e => pure (Except.error e)) =
      pure (Except.map f a)

Tactic:
intro a

Result:
case h
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : ExceptT ε m α
a : Except ε α
⊢ (match a with
    | Except.ok a => pure (Except.ok (f a))
    | Except.error e => pure (Except.error e)) =
    pure (Except.map f a)

Proof state:
case h
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : ExceptT ε m α
a : Except ε α
⊢ (match a with
    | Except.ok a => pure (Except.ok (f a))
    | Except.error e => pure (Except.error e)) =
    pure (Except.map f a)

Tactic:
cases a <;> simp [Except.map]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : ExceptT ε m α
⊢ (f <$> x).run = Except.map f <$> x.run

Tactic:
simp [Functor.map, ExceptT.map, ←bind_pure_comp]

Result:
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : ExceptT ε m α
⊢ (mk do
        let a ← x
        match a with
          | Except.ok a => pure (Except.ok (f a))
          | Except.error e => pure (Except.error e)).run =
    do
    let a ← x.run
    pure (Except.map f a)
-- Mathlib/GroupTheory/CommutingProbability.lean
private lemma div_four_lt : {n : ℕ} → (h0 : n ≠ 0) → (h1 : n ≠ 1) → n / 4 + 1 < n
  | 0 | 1 | 2 | 3 => by decide
  | n + 4 => by omega

Proof state:
n : ℕ
⊢ n + 4 ≠ 0 → n + 4 ≠ 1 → (n + 4) / 4 + 1 < n + 4

Tactic:
omega

Result:
no goals

Proof state:
⊢ 3 ≠ 0 → 3 ≠ 1 → 3 / 4 + 1 < 3

Tactic:
decide

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem toMeasure_bindOnSupport_apply [MeasurableSpace β] (hs : MeasurableSet s) :
    (p.bindOnSupport f).toMeasure s =
      ∑' a, p a * if h : p a = 0 then 0 else (f a h).toMeasure s

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
inst✝ : MeasurableSpace β
hs : MeasurableSet s
⊢ (p.bindOnSupport f).toMeasure s = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h).toMeasure s

Tactic:
simp only [toMeasure_apply_eq_toOuterMeasure_apply _ _ hs, toOuterMeasure_bindOnSupport_apply]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem expand_pow (f : R[X]) : expand R (p ^ q) f = (expand R p)^[q] f :=
  Nat.recOn q (by rw [pow_zero, expand_one, Function.iterate_zero, id]) fun n ih => by
    rw [Function.iterate_succ_apply', pow_succ', expand_mul, ih]

Proof state:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
⊢ (expand R (p ^ Nat.zero)) f = (⇑(expand R p))^[Nat.zero] f

Tactic:
rw [pow_zero, expand_one, Function.iterate_zero, id]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
ih : (expand R (p ^ n)) f = (⇑(expand R p))^[n] f
⊢ (expand R (p ^ n.succ)) f = (⇑(expand R p))^[n.succ] f

Tactic:
rw [Function.iterate_succ_apply', pow_succ', expand_mul, ih]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Finite.lean
lemma disjoint_closure_of_disjoint_support {S T : Set (Perm α)}
    (h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support) :
    _root_.Disjoint (closure S) (closure T)

Proof state:
case h.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
⊢ ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support

Tactic:
exact h

Result:
no goals

Proof state:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
⊢ ∀ a ∈ closure S, ∀ b ∈ closure T, _root_.Disjoint a.support b.support

Tactic:
apply disjoint_support_closure_of_disjoint_support

Result:
case h.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
⊢ ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
⊢ _root_.Disjoint (closure S) (closure T)

Tactic:
apply disjoint_of_disjoint_support

Result:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
⊢ ∀ a ∈ closure S, ∀ b ∈ closure T, _root_.Disjoint a.support b.support
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem neg_eq_zero_iff {x : BitVec w} : -x = 0#w ↔ x = 0#w

Proof state:
case mp
w : Nat
x : BitVec w
h : -x = 0#w
⊢ x = 0#w

Tactic:
have : - (- x) = - 0 := by simp [h]

Result:
case mp
w : Nat
x : BitVec w
h : -x = 0#w
this : - -x = -0
⊢ x = 0#w

Proof state:
w : Nat
x : BitVec w
h : -x = 0#w
⊢ - -x = -0

Tactic:
simp [h]

Result:
no goals

Proof state:
case mpr
w : Nat
x : BitVec w
h : x = 0#w
⊢ -x = 0#w

Tactic:
simp [h]

Result:
no goals

Proof state:
case mp
w : Nat
x : BitVec w
h : -x = 0#w
this : - -x = -0
⊢ x = 0#w

Tactic:
simpa using this

Result:
no goals

Proof state:
case mpr
w : Nat
x : BitVec w
⊢ x = 0#w → -x = 0#w

Tactic:
intro h

Result:
case mpr
w : Nat
x : BitVec w
h : x = 0#w
⊢ -x = 0#w

Proof state:
case mp
w : Nat
x : BitVec w
⊢ -x = 0#w → x = 0#w

Tactic:
intro h

Result:
case mp
w : Nat
x : BitVec w
h : -x = 0#w
⊢ x = 0#w

Proof state:
w : Nat
x : BitVec w
⊢ -x = 0#w ↔ x = 0#w

Tactic:
constructor

Result:
case mp
w : Nat
x : BitVec w
⊢ -x = 0#w → x = 0#w

case mpr
w : Nat
x : BitVec w
⊢ x = 0#w → -x = 0#w
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma eq_singularPart_measure (h : κ = η.withDensity f + ξ)
    (hf : Measurable (Function.uncurry f)) (a : α) (hξ : ξ a ⟂ₘ η a) :
    ξ a = (κ a).singularPart (η a)

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : ξ a ⟂ₘ η a
⊢ κ a = ξ a + (η a).withDensity (f a)

Tactic:
rw [h, coe_add, Pi.add_apply, η.withDensity_apply hf, add_comm]

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : ξ a ⟂ₘ η a
⊢ ξ a = (κ a).singularPart (η a)

Tactic:
have : κ a = ξ a + (η a).withDensity (f a) := by
  rw [h, coe_add, Pi.add_apply, η.withDensity_apply hf, add_comm]

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : ξ a ⟂ₘ η a
this : κ a = ξ a + (η a).withDensity (f a)
⊢ ξ a = (κ a).singularPart (η a)

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : ξ a ⟂ₘ η a
this : κ a = ξ a + (η a).withDensity (f a)
⊢ ξ a = (κ a).singularPart (η a)

Tactic:
exact (κ a).eq_singularPart (hf.comp measurable_prod_mk_left) hξ this

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem IsBlock.orbit_of_normal {N : Subgroup G} [N.Normal] (a : X) :
    IsBlock G (orbit N a)

Proof state:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
⊢ IsBlock G (orbit (↥N) a)

Tactic:
rw [isBlock_iff_smul_eq_or_disjoint]

Result:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
⊢ ∀ (g : G), g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)

Proof state:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
g : G
⊢ g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)

Tactic:
rw [smul_orbit_eq_orbit_smul]

Result:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
g : G
⊢ orbit (↥N) (g • a) = orbit (↥N) a ∨ Disjoint (orbit (↥N) (g • a)) (orbit (↥N) a)

Proof state:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
g : G
⊢ orbit (↥N) (g • a) = orbit (↥N) a ∨ Disjoint (orbit (↥N) (g • a)) (orbit (↥N) a)

Tactic:
apply orbit.eq_or_disjoint

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
⊢ ∀ (g : G), g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)

Tactic:
intro g

Result:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
g : G
⊢ g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)
-- Mathlib/Data/Set/NAry.lean
theorem image2_comm {g : β → α → γ} (h_comm : ∀ a b, f a b = g b a) : image2 f s t = image2 g t s :=
  (image2_swap _ _ _).trans <| by simp_rw [h_comm]

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
⊢ image2 (fun a b => f b a) t s = image2 g t s

Tactic:
simp_rw [h_comm]

Result:
no goals
-- Mathlib/Combinatorics/Additive/ErdosGinzburgZiv.lean
private lemma totalDegree_f₁_add_totalDegree_f₂ {a : ι → ZMod p} :
    (f₁ s a).totalDegree + (f₂ s a).totalDegree < 2 * p - 1

Proof state:
case h₂.hf
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
i : { x // x ∈ s }
a✝ : i ∈ univ
⊢ (a ↑i • X i ^ (p - 1)).totalDegree ≤ p - 1

Tactic:
exact (totalDegree_smul_le ..).trans (totalDegree_X_pow ..).le

Result:
no goals

Proof state:
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ (f₁ s a).totalDegree + (f₂ s a).totalDegree ≤ p - 1 + (p - 1)

Tactic:
gcongr <;> apply totalDegree_finsetSum_le <;> rintro i _

Result:
case h₁.hf
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
i : { x // x ∈ s }
a✝ : i ∈ univ
⊢ (X i ^ (p - 1)).totalDegree ≤ p - 1

case h₂.hf
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
i : { x // x ∈ s }
a✝ : i ∈ univ
⊢ (a ↑i • X i ^ (p - 1)).totalDegree ≤ p - 1

Proof state:
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
this : 2 ≤ p
⊢ p - 1 + (p - 1) < 2 * p - 1

Tactic:
omega

Result:
no goals

Proof state:
case h₁.hf
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
i : { x // x ∈ s }
a✝ : i ∈ univ
⊢ (X i ^ (p - 1)).totalDegree ≤ p - 1

Tactic:
exact (totalDegree_X_pow ..).le

Result:
no goals

Proof state:
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ p - 1 + (p - 1) < 2 * p - 1

Tactic:
have := (Fact.out : p.Prime).two_le

Result:
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
this : 2 ≤ p
⊢ p - 1 + (p - 1) < 2 * p - 1
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem measure_fundamentalDomain_ne_zero [Finite ι] [MeasurableSpace E] [BorelSpace E]
    {μ : Measure E} [Measure.IsAddHaarMeasure μ] :
    μ (fundamentalDomain b) ≠ 0

Proof state:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Finite ι
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
⊢ VAddInvariantMeasure (↥(span ℤ (Set.range ⇑b))) E μ

Tactic:
exact inferInstanceAs <| VAddInvariantMeasure (span ℤ (Set.range b)).toAddSubgroup E μ

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Finite ι
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
⊢ μ (fundamentalDomain b) ≠ 0

Tactic:
convert (ZSpan.isAddFundamentalDomain b μ).measure_ne_zero (NeZero.ne μ)

Result:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Finite ι
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
⊢ VAddInvariantMeasure (↥(span ℤ (Set.range ⇑b))) E μ