harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem addNat_last (n : Nat) :
    addNat (last n) m = (last (n + m)).cast (by omega)

Proof state:
case h
m n : Nat
⊢ ↑((last n).addNat m) = ↑(Fin.cast ⋯ (last (n + m)))

Tactic:
simp

Result:
no goals

Proof state:
m n : Nat
⊢ n + m + 1 = n + 1 + m

Tactic:
omega

Result:
no goals

Proof state:
m n : Nat
⊢ (last n).addNat m = Fin.cast ⋯ (last (n + m))

Tactic:
ext

Result:
case h
m n : Nat
⊢ ↑((last n).addNat m) = ↑(Fin.cast ⋯ (last (n + m)))
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem front_eq (s : String) : front s = s.1.headD default

Proof state:
s : String
⊢ s.get 0 = s.data.headD default

Tactic:
exact get_of_valid [] s.1

Result:
no goals

Proof state:
s : String
⊢ s.front = s.data.headD default

Tactic:
unfold front

Result:
s : String
⊢ s.get 0 = s.data.headD default
-- Mathlib/Data/Complex/FiniteDimensional.lean
theorem rank_real_complex : Module.rank ℝ ℂ = 2

Proof state:
⊢ Module.rank ℝ ℂ = 2

Tactic:
simp [← finrank_eq_rank, finrank_real_complex]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/CommShift.lean
lemma commShiftIso_zero' (a : A) (h : a = 0) :
    F.commShiftIso a = CommShift.isoZero' F A a h

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_7, u_1} C
inst✝⁴ : Category.{u_6, u_2} D
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a : A
h : a = 0
⊢ F.commShiftIso a = CommShift.isoZero' F A a h

Tactic:
subst h

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_7, u_1} C
inst✝⁴ : Category.{u_6, u_2} D
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
⊢ F.commShiftIso 0 = CommShift.isoZero' F A 0 ⋯

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_7, u_1} C
inst✝⁴ : Category.{u_6, u_2} D
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
⊢ F.commShiftIso 0 = CommShift.isoZero' F A 0 ⋯

Tactic:
rw [CommShift.isoZero'_eq_isoZero, commShiftIso_zero]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean
/-- If `P` is a morphism property affine locally defined by `affineAnd Q`, `P` is stable under
composition if `Q` is. -/
lemma HasAffineProperty.affineAnd_isStableUnderComposition {P : MorphismProperty Scheme.{u}}
    (hA : HasAffineProperty P (affineAnd Q)) (hQ : RingHom.StableUnderComposition Q) :
    P.IsStableUnderComposition where
  comp_mem {X Y Z} f g hf hg

Proof state:
case intro.intro
Q✝ Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hZ : IsAffine Z
hY : IsAffine Y
hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ P (f ≫ g)

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))]

Result:
case intro.intro
Q✝ Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hZ : IsAffine Z
hY : IsAffine Y
hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) (f ≫ g)
-- Mathlib/RingTheory/Ideal/Prod.lean
theorem map_fst_prod (I : Ideal R) (J : Ideal S) : map (RingHom.fst R S) (prod I J) = I

Proof state:
case intro.intro
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : R × S
h : x ∈ I.prod J
⊢ (RingHom.fst R S) x ∈ I

Tactic:
exact h.1

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ map (RingHom.fst R S) (I.prod J) = I

Tactic:
ext x

Result:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : R
⊢ x ∈ map (RingHom.fst R S) (I.prod J) ↔ x ∈ I

Proof state:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : R
⊢ (∃ x_1 ∈ I.prod J, (RingHom.fst R S) x_1 = x) ↔ x ∈ I

Tactic:
exact
  ⟨by
    rintro ⟨x, ⟨h, rfl⟩⟩
    exact h.1, fun h => ⟨⟨x, 0⟩, ⟨⟨h, Ideal.zero_mem _⟩, rfl⟩⟩⟩

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : R
⊢ (∃ x_1 ∈ I.prod J, (RingHom.fst R S) x_1 = x) → x ∈ I

Tactic:
rintro ⟨x, ⟨h, rfl⟩⟩

Result:
case intro.intro
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : R × S
h : x ∈ I.prod J
⊢ (RingHom.fst R S) x ∈ I

Proof state:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : R
⊢ x ∈ map (RingHom.fst R S) (I.prod J) ↔ x ∈ I

Tactic:
rw [mem_map_iff_of_surjective (RingHom.fst R S) Prod.fst_surjective]

Result:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : R
⊢ (∃ x_1 ∈ I.prod J, (RingHom.fst R S) x_1 = x) ↔ x ∈ I
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem mul_le_mul_of_nonneg_right {a b c : Int}
    (h₁ : a ≤ b) (h₂ : 0 ≤ c) : a * c ≤ b * c

Proof state:
a b c : Int
h₁ : a ≤ b
h₂ : 0 ≤ c
⊢ a * c ≤ b * c

Tactic:
rw [Int.mul_comm, Int.mul_comm b]

Result:
a b c : Int
h₁ : a ≤ b
h₂ : 0 ≤ c
⊢ c * a ≤ c * b

Proof state:
a b c : Int
h₁ : a ≤ b
h₂ : 0 ≤ c
⊢ c * a ≤ c * b

Tactic:
exact Int.mul_le_mul_of_nonneg_left h₁ h₂

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_mul_right_add_left (m n k : ℕ) : Coprime (k * n + m) n ↔ Coprime m n

Proof state:
m n k : ℕ
⊢ (k * n + m).Coprime n ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_mul_right_add_left]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Trim.lean
theorem sigmaFinite_trim_bot_iff : SigmaFinite (μ.trim bot_le) ↔ IsFiniteMeasure μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ IsFiniteMeasure (μ.trim ⋯) ↔ IsFiniteMeasure μ

Tactic:
refine ⟨fun h => ⟨?_⟩, fun h => ⟨?_⟩⟩ <;> have h_univ := h.measure_univ_lt_top

Result:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure (μ.trim ⋯)
h_univ : (μ.trim ⋯) Set.univ < ⊤
⊢ μ Set.univ < ⊤

case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure μ
h_univ : μ Set.univ < ⊤
⊢ (μ.trim ⋯) Set.univ < ⊤

Proof state:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure μ
h_univ : μ Set.univ < ⊤
⊢ (μ.trim ⋯) Set.univ < ⊤

Tactic:
rwa [trim_measurableSet_eq bot_le MeasurableSet.univ]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ SigmaFinite (μ.trim ⋯) ↔ IsFiniteMeasure μ

Tactic:
rw [sigmaFinite_bot_iff]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ IsFiniteMeasure (μ.trim ⋯) ↔ IsFiniteMeasure μ

Proof state:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure (μ.trim ⋯)
h_univ : (μ.trim ⋯) Set.univ < ⊤
⊢ μ Set.univ < ⊤

Tactic:
rwa [trim_measurableSet_eq bot_le MeasurableSet.univ] at h_univ

Result:
no goals
-- Mathlib/SetTheory/Lists.lean
theorem subset_def {l₁ l₂ : Lists' α true} : l₁ ⊆ l₂ ↔ ∀ a ∈ l₁.toList, a ∈ l₂ :=
  ⟨fun H _ => mem_of_subset' H, fun H => by
    rw [← of_toList l₁]
    revert H; induction' toList l₁ with h t t_ih <;> intro H
    · exact Subset.nil
    · simp only [ofList, List.find?, List.mem_cons, forall_eq_or_imp] at *
      exact cons_subset.2 ⟨H.1, t_ih H.2⟩⟩

Proof state:
case nil
α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ a ∈ [], a ∈ l₂
⊢ ofList [] ⊆ l₂

Tactic:
exact Subset.nil

Result:
no goals

Proof state:
case cons
α : Type u_1
l₁ l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : (∀ a ∈ t, a ∈ l₂) → ofList t ⊆ l₂
H : ∀ a ∈ h :: t, a ∈ l₂
⊢ ofList (h :: t) ⊆ l₂

Tactic:
simp only [ofList, List.find?, List.mem_cons, forall_eq_or_imp] at *

Result:
case cons
α : Type u_1
l₁ l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : (∀ a ∈ t, a ∈ l₂) → ofList t ⊆ l₂
H : h ∈ l₂ ∧ ∀ a ∈ t, a ∈ l₂
⊢ cons h (ofList t) ⊆ l₂

Proof state:
α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ a ∈ l₁.toList, a ∈ l₂
⊢ l₁ ⊆ l₂

Tactic:
rw [← of_toList l₁]

Result:
α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ a ∈ l₁.toList, a ∈ l₂
⊢ ofList l₁.toList ⊆ l₂

Proof state:
case cons
α : Type u_1
l₁ l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : (∀ a ∈ t, a ∈ l₂) → ofList t ⊆ l₂
H : h ∈ l₂ ∧ ∀ a ∈ t, a ∈ l₂
⊢ cons h (ofList t) ⊆ l₂

Tactic:
exact cons_subset.2 ⟨H.1, t_ih H.2⟩

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ a ∈ l₁.toList, a ∈ l₂
⊢ ofList l₁.toList ⊆ l₂

Tactic:
revert H

Result:
α : Type u_1
l₁ l₂ : Lists' α true
⊢ (∀ a ∈ l₁.toList, a ∈ l₂) → ofList l₁.toList ⊆ l₂

Proof state:
α : Type u_1
l₁ l₂ : Lists' α true
⊢ (∀ a ∈ l₁.toList, a ∈ l₂) → ofList l₁.toList ⊆ l₂

Tactic:
induction' toList l₁ with h t t_ih <;> intro H

Result:
case nil
α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ a ∈ [], a ∈ l₂
⊢ ofList [] ⊆ l₂

case cons
α : Type u_1
l₁ l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : (∀ a ∈ t, a ∈ l₂) → ofList t ⊆ l₂
H : ∀ a ∈ h :: t, a ∈ l₂
⊢ ofList (h :: t) ⊆ l₂
-- Mathlib/Data/Finset/Image.lean
theorem coe_fin (n : ℕ) (s : Finset ℕ) : (s.fin n : Set (Fin n)) = Fin.val ⁻¹' s

Proof state:
case h
n : ℕ
s : Finset ℕ
x✝ : Fin n
⊢ x✝ ∈ ↑(Finset.fin n s) ↔ x✝ ∈ Fin.val ⁻¹' ↑s

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
s : Finset ℕ
⊢ ↑(Finset.fin n s) = Fin.val ⁻¹' ↑s

Tactic:
ext

Result:
case h
n : ℕ
s : Finset ℕ
x✝ : Fin n
⊢ x✝ ∈ ↑(Finset.fin n s) ↔ x✝ ∈ Fin.val ⁻¹' ↑s
-- Mathlib/Topology/MetricSpace/Perfect.lean
theorem Perfect.small_diam_splitting (hC : Perfect C) (hnonempty : C.Nonempty) (ε_pos : 0 < ε) :
    ∃ C₀ C₁ : Set α, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧
    (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
sub1 : D₁ ⊆ C
x₀ : α
hx₀ : x₀ ∈ D₀
x₁ : α
hx₁ : x₁ ∈ D₁
⊢ ∃ C₀ C₁,
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧
      (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁

Tactic:
rcases perf0.small_diam_aux ε_pos hx₀ with ⟨perf0', non0', sub0', diam0⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
sub1 : D₁ ⊆ C
x₀ : α
hx₀ : x₀ ∈ D₀
x₁ : α
hx₁ : x₁ ∈ D₁
perf0' : Perfect (closure (EMetric.ball x₀ (ε / 2) ∩ D₀))
non0' : (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)).Nonempty
sub0' : closure (EMetric.ball x₀ (ε / 2) ∩ D₀) ⊆ D₀
diam0 : EMetric.diam (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)) ≤ ε
⊢ ∃ C₀ C₁,
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧
      (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
non1 : D₁.Nonempty
sub1 : D₁ ⊆ C
x₀ : α
hx₀ : x₀ ∈ D₀
⊢ ∃ C₀ C₁,
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧
      (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁

Tactic:
obtain ⟨x₁, hx₁⟩ := non1

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
sub1 : D₁ ⊆ C
x₀ : α
hx₀ : x₀ ∈ D₀
x₁ : α
hx₁ : x₁ ∈ D₁
⊢ ∃ C₀ C₁,
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧
      (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁
-- Mathlib/GroupTheory/FreeAbelianGroup.lean
theorem lift_comp {α} {β} {γ} [AddCommGroup γ] (f : α → β) (g : β → γ) (x : FreeAbelianGroup α) :
    lift (g ∘ f) x = lift g (map f x)

Proof state:
case Cn
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x✝ : α
h : (lift (g ∘ f)) (of x✝) = (lift g) ((map f) (of x✝))
⊢ (lift (g ∘ f)) (-of x✝) = (lift g) ((map f) (-of x✝))

Tactic:
simp only [h, AddMonoidHom.map_neg]

Result:
no goals

Proof state:
case C1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x✝ : α
⊢ (lift (g ∘ f)) (of x✝) = (lift g) ((map f) (of x✝))

Tactic:
simp only [lift.of, map, Function.comp]

Result:
no goals

Proof state:
case Cp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x✝ y✝ : FreeAbelianGroup α
h₁ : (lift (g ∘ f)) x✝ = (lift g) ((map f) x✝)
h₂ : (lift (g ∘ f)) y✝ = (lift g) ((map f) y✝)
⊢ (lift (g ∘ f)) (x✝ + y✝) = (lift g) ((map f) (x✝ + y✝))

Tactic:
simp only [h₁, h₂, AddMonoidHom.map_add]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ (lift (g ∘ f)) x = (lift g) ((map f) x)

Tactic:
induction x using FreeAbelianGroup.induction_on with
| C0 => simp only [map_zero]
| C1 => simp only [lift.of, map, Function.comp]
| Cn _ h => simp only [h, AddMonoidHom.map_neg]
| Cp _ _ h₁ h₂ => simp only [h₁, h₂, AddMonoidHom.map_add]

Result:
no goals

Proof state:
case C0
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
⊢ (lift (g ∘ f)) 0 = (lift g) ((map f) 0)

Tactic:
simp only [map_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem chaar_nonneg (K₀ : PositiveCompacts G) (K : Compacts G) : 0 ≤ chaar K₀ K

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
this : chaar K₀ K ∈ (fun K => Icc 0 ↑(index ↑K ↑K₀)) K
⊢ 0 ≤ chaar K₀ K

Tactic:
rw [mem_Icc] at this

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
this : 0 ≤ chaar K₀ K ∧ chaar K₀ K ≤ ↑(index ↑K ↑K₀)
⊢ 0 ≤ chaar K₀ K

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
⊢ 0 ≤ chaar K₀ K

Tactic:
have := chaar_mem_haarProduct K₀ K (mem_univ _)

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
this : chaar K₀ K ∈ (fun K => Icc 0 ↑(index ↑K ↑K₀)) K
⊢ 0 ≤ chaar K₀ K

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
this : 0 ≤ chaar K₀ K ∧ chaar K₀ K ≤ ↑(index ↑K ↑K₀)
⊢ 0 ≤ chaar K₀ K

Tactic:
exact this.1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat ≥ 2^(n-1)

Proof state:
n✝ n : Nat
x : BitVec (n + 1)
p : 2 ^ n ≤ x.toNat
⊢ x.toNat ≥ 2 ^ (n + 1 - 1)

Tactic:
simp only [Nat.add_sub_cancel]

Result:
n✝ n : Nat
x : BitVec (n + 1)
p : 2 ^ n ≤ x.toNat
⊢ x.toNat ≥ 2 ^ n

Proof state:
n : Nat
x : BitVec 0
p : x.msb = true
⊢ x.toNat ≥ 2 ^ (0 - 1)

Tactic:
simp [BitVec.msb, BitVec.getMsbD] at p

Result:
no goals

Proof state:
n : Nat
x : BitVec n
p : x.msb = true
⊢ x.toNat ≥ 2 ^ (n - 1)

Tactic:
match n with
| 0 =>
  simp [BitVec.msb, BitVec.getMsbD] at p
| n + 1 =>
  simp only [msb_eq_decide, Nat.add_one_sub_one, decide_eq_true_eq] at p
  simp only [Nat.add_sub_cancel]
  exact p

Result:
no goals

Proof state:
n✝ n : Nat
x : BitVec (n + 1)
p : 2 ^ n ≤ x.toNat
⊢ x.toNat ≥ 2 ^ n

Tactic:
exact p

Result:
no goals

Proof state:
n✝ n : Nat
x : BitVec (n + 1)
p : x.msb = true
⊢ x.toNat ≥ 2 ^ (n + 1 - 1)

Tactic:
simp only [msb_eq_decide, Nat.add_one_sub_one, decide_eq_true_eq] at p

Result:
n✝ n : Nat
x : BitVec (n + 1)
p : 2 ^ n ≤ x.toNat
⊢ x.toNat ≥ 2 ^ (n + 1 - 1)
-- Mathlib/Order/Monotone/Basic.lean
theorem Monotone.eq_of_le_of_le {a₁ a₂ : α} (h_mon : Monotone f) (h_fa : f a₁ = f a₂) {i : α}
    (h₁ : a₁ ≤ i) (h₂ : i ≤ a₂) : f i = f a₁

Proof state:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₁

Tactic:
rw [h_fa]

Result:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₂

Proof state:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₂

Tactic:
exact h_mon h₂

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i = f a₁

Tactic:
apply le_antisymm

Result:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₁

case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i

Proof state:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i

Tactic:
exact h_mon h₁

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem periodicOrbit_chain (r : α → α → Prop) {f : α → α} {x : α} :
    (periodicOrbit f x).Chain r ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)

Proof state:
case pos.refine_1.intro.inl
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n = minimalPeriod f x - succ 0
⊢ r (f^[n] x) (f^[n + 1] x)

Tactic:
rwa [hM', hM, iterate_minimalPeriod]

Result:
no goals

Proof state:
case pos
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)

Tactic:
rw [periodicOrbit, ← Cycle.map_coe, Cycle.chain_map, ← hM, Cycle.chain_range_succ]

Result:
case pos
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ (r (f^[minimalPeriod f x - succ 0] x) (f^[0] x) ∧ ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)) ↔
    ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)

Proof state:
case pos.refine_2
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) x

Tactic:
nth_rw 3 [← @iterate_minimalPeriod α f x]

Result:
case pos.refine_2
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x] x)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem getElem?_enum (l : List α) (n : Nat) : (enum l)[n]? = l[n]?.map fun a => (n, a)

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ l.enum[n]? = Option.map (fun a => (n, a)) l[n]?

Tactic:
rw [enum, getElem?_enumFrom, Nat.zero_add]

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma eventually_deriv_one_add_smoothingFn :
    deriv (fun x => 1 + ε x) =ᶠ[atTop] fun x => -x⁻¹ / (log x ^ 2) := calc
  deriv (fun x => 1 + ε x) =ᶠ[atTop] deriv ε

Proof state:
case h
x : ℝ
hx : 1 < x
⊢ deriv (fun x => 1 + ε x) x = deriv ε x

Tactic:
rw [deriv_add] <;> aesop

Result:
no goals

Proof state:
case h
x : ℝ
hx : 1 < x
⊢ deriv ε x = -x⁻¹ / log x ^ 2

Tactic:
simp [deriv_smoothingFn hx]

Result:
no goals

Proof state:
⊢ deriv ε =ᶠ[atTop] fun x => -x⁻¹ / log x ^ 2

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Result:
case h
x : ℝ
hx : 1 < x
⊢ deriv ε x = -x⁻¹ / log x ^ 2

Proof state:
⊢ (deriv fun x => 1 + ε x) =ᶠ[atTop] deriv ε

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Result:
case h
x : ℝ
hx : 1 < x
⊢ deriv (fun x => 1 + ε x) x = deriv ε x
-- Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean
lemma ker_rootForm_eq_dualAnnihilator :
    LinearMap.ker P.RootForm = P.corootSpan.dualAnnihilator.map P.toDualLeft.symm

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
_iM : IsReflexive R M
_iN : IsReflexive R N
aux0 : finrank R ↥P.corootSpan + finrank R ↥P.corootSpan.dualAnnihilator = finrank R N
⊢ finrank R ↥(LinearMap.ker P.RootForm) = finrank R ↥P.corootSpan.dualAnnihilator

Tactic:
have aux1 := Submodule.finrank_add_eq_of_isCompl P.isCompl_rootSpan_ker_rootForm

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
_iM : IsReflexive R M
_iN : IsReflexive R N
aux0 : finrank R ↥P.corootSpan + finrank R ↥P.corootSpan.dualAnnihilator = finrank R N
aux1 : finrank R ↥P.rootSpan + finrank R ↥(LinearMap.ker P.RootForm) = finrank R M
⊢ finrank R ↥(LinearMap.ker P.RootForm) = finrank R ↥P.corootSpan.dualAnnihilator

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
_iM : IsReflexive R M
_iN : IsReflexive R N
aux0 : finrank R ↥P.corootSpan + finrank R ↥P.corootSpan.dualAnnihilator = finrank R N
aux1 : finrank R ↥P.corootSpan + finrank R ↥(LinearMap.ker P.RootForm) = finrank R N
⊢ finrank R ↥(LinearMap.ker P.RootForm) = finrank R ↥P.corootSpan.dualAnnihilator

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Nat/Count.lean
theorem count_succ_eq_count_iff {n : ℕ} : count p (n + 1) = count p n ↔ ¬p n

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count p n ↔ ¬p n

Tactic:
by_cases h : p n <;> simp [h, count_succ]

Result:
no goals