harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
theorem dart_edge_fiber_card [DecidableEq V] (e : Sym2 V) (h : e ∈ G.edgeSet) :
    #{d : G.Dart | d.edge = e} = 2

Proof state:
case h.e'_3
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { toProd := (v, w), adj := h }
⊢ 2 = #{d, d.symm}

Tactic:
rw [card_insert_of_not_mem, card_singleton]

Result:
case h.e'_3
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { toProd := (v, w), adj := h }
⊢ d ∉ {d.symm}

Proof state:
case mk.mk
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
⊢ #(filter (fun d => d.edge = Quot.mk (Sym2.Rel V) (v, w)) univ) = 2

Tactic:
let d : G.Dart := ⟨(v, w), h⟩

Result:
case mk.mk
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { toProd := (v, w), adj := h }
⊢ #(filter (fun d => d.edge = Quot.mk (Sym2.Rel V) (v, w)) univ) = 2

Proof state:
case h.e'_3
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { toProd := (v, w), adj := h }
⊢ ¬d = d.symm

Tactic:
exact d.symm_ne.symm

Result:
no goals

Proof state:
case h.e'_3
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { toProd := (v, w), adj := h }
⊢ d ∉ {d.symm}

Tactic:
rw [mem_singleton]

Result:
case h.e'_3
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { toProd := (v, w), adj := h }
⊢ ¬d = d.symm

Proof state:
case mk.mk
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { toProd := (v, w), adj := h }
⊢ #(filter (fun d => d.edge = Quot.mk (Sym2.Rel V) (v, w)) univ) = 2

Tactic:
convert congr_arg card d.edge_fiber

Result:
case h.e'_3
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { toProd := (v, w), adj := h }
⊢ 2 = #{d, d.symm}

Proof state:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
h : e ∈ G.edgeSet
⊢ #(filter (fun d => d.edge = e) univ) = 2

Tactic:
obtain ⟨v, w⟩ := e

Result:
case mk.mk
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
⊢ #(filter (fun d => d.edge = Quot.mk (Sym2.Rel V) (v, w)) univ) = 2
-- Mathlib/LinearAlgebra/Matrix/DotProduct.lean
theorem dotProduct_self_star_eq_zero {v : n → R} : dotProduct v (star v) = 0 ↔ v = 0 :=
  (Fintype.sum_eq_zero_iff_of_nonneg fun _ => mul_star_self_nonneg _).trans <|
    by simp [funext_iff, mul_eq_zero]

Proof state:
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
⊢ (fun i => v i * star v i) = 0 ↔ v = 0

Tactic:
simp [funext_iff, mul_eq_zero]

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem isAdjoinRoot_root_eq_root : (AdjoinRoot.isAdjoinRoot f).root = AdjoinRoot.root f

Proof state:
R : Type u
inst✝ : CommRing R
f : R[X]
⊢ (AdjoinRoot.isAdjoinRoot f).root = root f

Tactic:
simp only [IsAdjoinRoot.root, AdjoinRoot.root, AdjoinRoot.isAdjoinRoot_map_eq_mk]

Result:
no goals
-- Mathlib/Topology/Connected/LocPathConnected.lean
theorem IsOpen.pathComponentIn (x : X) (hF : IsOpen F) :
    IsOpen (pathComponentIn x F)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
F : Set X
inst✝ : LocPathConnectedSpace X
x : X
hF : IsOpen F
y : X
hy : y ∈ pathComponentIn x F
⊢ pathComponentIn x F ∈ 𝓝 y

Tactic:
let ⟨s, hs⟩ := (path_connected_basis y).mem_iff.mp (hF.mem_nhds (pathComponentIn_subset hy))

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
F : Set X
inst✝ : LocPathConnectedSpace X
x : X
hF : IsOpen F
y : X
hy : y ∈ pathComponentIn x F
s : Set X
hs : (s ∈ 𝓝 y ∧ IsPathConnected s) ∧ id s ⊆ F
⊢ pathComponentIn x F ∈ 𝓝 y

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
F : Set X
inst✝ : LocPathConnectedSpace X
x : X
hF : IsOpen F
⊢ IsOpen (pathComponentIn x F)

Tactic:
rw [isOpen_iff_mem_nhds]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
F : Set X
inst✝ : LocPathConnectedSpace X
x : X
hF : IsOpen F
⊢ ∀ x_1 ∈ pathComponentIn x F, pathComponentIn x F ∈ 𝓝 x_1

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
F : Set X
inst✝ : LocPathConnectedSpace X
x : X
hF : IsOpen F
y : X
hy : y ∈ pathComponentIn x F
s : Set X
hs : (s ∈ 𝓝 y ∧ IsPathConnected s) ∧ id s ⊆ F
⊢ pathComponentIn x F ∈ 𝓝 y

Tactic:
exact mem_of_superset hs.1.1 <| pathComponentIn_congr hy ▸
  hs.1.2.subset_pathComponentIn (mem_of_mem_nhds hs.1.1) hs.2

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
F : Set X
inst✝ : LocPathConnectedSpace X
x : X
hF : IsOpen F
⊢ ∀ x_1 ∈ pathComponentIn x F, pathComponentIn x F ∈ 𝓝 x_1

Tactic:
intro y hy

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
F : Set X
inst✝ : LocPathConnectedSpace X
x : X
hF : IsOpen F
y : X
hy : y ∈ pathComponentIn x F
⊢ pathComponentIn x F ∈ 𝓝 y
-- Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean
theorem mod_four_eq_three_of_nat_prime_of_prime (p : ℕ) [hp : Fact p.Prime]
    (hpi : Prime (p : ℤ[i])) : p % 4 = 3 :=
  hp.1.eq_two_or_odd.elim
    (fun hp2 => by
      have := hpi.irreducible.isUnit_or_isUnit (a := ⟨1, 1⟩) (b := ⟨1, -1⟩)
      simp [hp2, Zsqrtd.ext_iff, ← norm_eq_one_iff, norm_def] at this)
    fun hp1 =>
    by_contradiction fun hp3 : p % 4 ≠ 3 => by
      have hp41 : p % 4 = 1

Proof state:
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
⊢ False

Tactic:
have hpk : p ∣ k ^ 2 + 1 := by
  rw [pow_two, ← CharP.cast_eq_zero_iff (ZMod p) p, Nat.cast_add, Nat.cast_mul, Nat.cast_one,
    ← hk, neg_add_cancel]

Result:
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
⊢ False

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }
y : ℕ
hy : k ^ 2 + 1 = p * y
⊢ ↑k ^ 2 + 1 = ↑(k ^ 2 + 1)

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Integral.lean
theorem integral_piecewise (a : α) (g : β → E) :
    ∫ b, g b ∂piecewise hs κ η a = if a ∈ s then ∫ b, g b ∂κ a else ∫ b, g b ∂η a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → E
⊢ (∫ (b : β), g b ∂if a ∈ s then κ a else η a) = if a ∈ s then ∫ (b : β), g b ∂κ a else ∫ (b : β), g b ∂η a

Tactic:
split_ifs <;> rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → E
⊢ ∫ (b : β), g b ∂(piecewise hs κ η) a = if a ∈ s then ∫ (b : β), g b ∂κ a else ∫ (b : β), g b ∂η a

Tactic:
simp_rw [piecewise_apply]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → E
⊢ (∫ (b : β), g b ∂if a ∈ s then κ a else η a) = if a ∈ s then ∫ (b : β), g b ∂κ a else ∫ (b : β), g b ∂η a
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem absNorm_top : absNorm (⊤ : Ideal S) = 1

Proof state:
S : Type u_1
inst✝³ : CommRing S
inst✝² : Nontrivial S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
⊢ absNorm ⊤ = 1

Tactic:
rw [← Ideal.one_eq_top, map_one]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/QuasiIso.lean
lemma quasiIso_iff_comp_right (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [hφ' : QuasiIso φ'] :
    QuasiIso (φ ≫ φ') ↔ QuasiIso φ

Proof state:
case mpr
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : QuasiIso φ'
a✝ : QuasiIso φ
⊢ QuasiIso (φ ≫ φ')

Tactic:
exact quasiIso_comp φ φ'

Result:
no goals

Proof state:
case mp
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : QuasiIso φ'
a✝ : QuasiIso (φ ≫ φ')
⊢ QuasiIso φ

Tactic:
exact quasiIso_of_comp_right φ φ'

Result:
no goals

Proof state:
case mp
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : QuasiIso φ'
⊢ QuasiIso (φ ≫ φ') → QuasiIso φ

Tactic:
intro

Result:
case mp
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : QuasiIso φ'
a✝ : QuasiIso (φ ≫ φ')
⊢ QuasiIso φ

Proof state:
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : QuasiIso φ'
⊢ QuasiIso (φ ≫ φ') ↔ QuasiIso φ

Tactic:
constructor

Result:
case mp
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : QuasiIso φ'
⊢ QuasiIso (φ ≫ φ') → QuasiIso φ

case mpr
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : QuasiIso φ'
⊢ QuasiIso φ → QuasiIso (φ ≫ φ')

Proof state:
case mpr
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : QuasiIso φ'
⊢ QuasiIso φ → QuasiIso (φ ≫ φ')

Tactic:
intro

Result:
case mpr
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : QuasiIso φ'
a✝ : QuasiIso φ
⊢ QuasiIso (φ ≫ φ')
-- Mathlib/Data/Rat/Lemmas.lean
theorem isSquare_iff {q : ℚ} : IsSquare q ↔ IsSquare q.num ∧ IsSquare q.den

Proof state:
case mpr.intro.intro.intro
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ q = ↑nr / ↑dr * (↑nr / ↑dr)

Tactic:
rw [div_mul_div_comm, ← Int.cast_mul, ← Nat.cast_mul, ← hnr, ← hdr, num_div_den]

Result:
no goals

Proof state:
case mp
q : ℚ
⊢ IsSquare q → IsSquare q.num ∧ IsSquare q.den

Tactic:
rintro ⟨qr, rfl⟩

Result:
case mp.intro
qr : ℚ
⊢ IsSquare (qr * qr).num ∧ IsSquare (qr * qr).den

Proof state:
case mpr.intro.intro.intro
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ IsSquare q

Tactic:
refine ⟨nr / dr, ?_⟩

Result:
case mpr.intro.intro.intro
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ q = ↑nr / ↑dr * (↑nr / ↑dr)

Proof state:
case mpr
q : ℚ
⊢ IsSquare q.num ∧ IsSquare q.den → IsSquare q

Tactic:
rintro ⟨⟨nr, hnr⟩, ⟨dr, hdr⟩⟩

Result:
case mpr.intro.intro.intro
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ IsSquare q

Proof state:
q : ℚ
⊢ IsSquare q ↔ IsSquare q.num ∧ IsSquare q.den

Tactic:
constructor

Result:
case mp
q : ℚ
⊢ IsSquare q → IsSquare q.num ∧ IsSquare q.den

case mpr
q : ℚ
⊢ IsSquare q.num ∧ IsSquare q.den → IsSquare q

Proof state:
case mp.intro
qr : ℚ
⊢ IsSquare (qr.num * qr.num) ∧ IsSquare (qr.den * qr.den)

Tactic:
simp only [IsSquare.mul_self, and_self]

Result:
no goals

Proof state:
case mp.intro
qr : ℚ
⊢ IsSquare (qr * qr).num ∧ IsSquare (qr * qr).den

Tactic:
rw [Rat.mul_self_num, mul_self_den]

Result:
case mp.intro
qr : ℚ
⊢ IsSquare (qr.num * qr.num) ∧ IsSquare (qr.den * qr.den)
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem mono_of_cofan_isVanKampen [HasInitial C] {ι : Type*} {F : Discrete ι ⥤ C}
    {c : Cocone F} (hc : IsVanKampenColimit c) (i : Discrete ι) : Mono (c.ι.app i)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i : Discrete ι
f : ι → C := F.obj ∘ Discrete.mk
⊢ Mono (c.ι.app i)

Tactic:
have : F = Discrete.functor f :=
  Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i : Discrete ι
f : ι → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor f
⊢ Mono (c.ι.app i)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ Mono (c.ι.app i)

Tactic:
refine PullbackCone.mono_of_isLimitMkIdId _ (IsPullback.isLimit ?_)

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ IsPullback (𝟙 ((Discrete.functor f).obj i)) (𝟙 ((Discrete.functor f).obj i)) (c.ι.app i) (c.ι.app i)
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_iInf_ge_nat_add (f : ℕ → α) (k : ℕ) :
    ⨆ n, ⨅ i ≥ n, f (i + k) = ⨆ n, ⨅ i ≥ n, f i

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
⊢ ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f i

Tactic:
have hf : Monotone fun n => ⨅ i ≥ n, f i := fun n m h => biInf_mono fun i => h.trans

Result:
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
hf : Monotone fun n => ⨅ i, ⨅ (_ : i ≥ n), f i
⊢ ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f i

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
hf : Monotone fun n => ⨅ i, ⨅ (_ : i ≥ n), f i
⊢ ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n + k), f i

Tactic:
simp_rw [iInf_ge_eq_iInf_nat_add, ← Nat.add_assoc]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
hf : Monotone fun n => ⨅ i, ⨅ (_ : i ≥ n), f i
⊢ ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f i

Tactic:
rw [← Monotone.iSup_nat_add hf k]

Result:
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
hf : Monotone fun n => ⨅ i, ⨅ (_ : i ≥ n), f i
⊢ ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n + k), f i
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem zero_le : ∀ a : Cardinal, 0 ≤ a

Proof state:
⊢ ∀ (a : Cardinal.{u_1}), 0 ≤ a

Tactic:
rintro ⟨α⟩

Result:
case mk
a✝ : Cardinal.{u_1}
α : Type u_1
⊢ 0 ≤ Quot.mk (⇑isEquivalent) α

Proof state:
case mk
a✝ : Cardinal.{u_1}
α : Type u_1
⊢ 0 ≤ Quot.mk (⇑isEquivalent) α

Tactic:
exact ⟨Embedding.ofIsEmpty⟩

Result:
no goals
-- Mathlib/FieldTheory/KrullTopology.lean
@[simp] lemma IntermediateField.fixingSubgroup_bot (K L : Type*) [Field K] [Field L] [Algebra K L] :
    IntermediateField.fixingSubgroup (⊥ : IntermediateField K L) = ⊤

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ ⊥.fixingSubgroup = ⊤

Tactic:
ext

Result:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : L ≃ₐ[K] L
⊢ x✝ ∈ ⊥.fixingSubgroup ↔ x✝ ∈ ⊤

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : L ≃ₐ[K] L
⊢ x✝ ∈ ⊥.fixingSubgroup ↔ x✝ ∈ ⊤

Tactic:
simp [mem_fixingSubgroup_iff, mem_bot]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range_subset {m n : Nat} : range m ⊆ range n ↔ m ≤ n

Proof state:
m n : Nat
⊢ range m ⊆ range n ↔ m ≤ n

Tactic:
simp only [range_eq_range', range'_subset_right, lt_succ_self]

Result:
no goals
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upperCrossingTime_mono (hnm : n ≤ m) :
    upperCrossingTime a b f N n ω ≤ upperCrossingTime a b f N m ω

Proof state:
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
this : Monotone fun n => upperCrossingTime a b f N n ω
⊢ upperCrossingTime a b f N n ω ≤ upperCrossingTime a b f N m ω

Tactic:
exact this hnm

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
⊢ upperCrossingTime a b f N n ω ≤ upperCrossingTime a b f N m ω

Tactic:
suffices Monotone fun n => upperCrossingTime a b f N n ω by exact this hnm

Result:
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
⊢ Monotone fun n => upperCrossingTime a b f N n ω

Proof state:
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
⊢ Monotone fun n => upperCrossingTime a b f N n ω

Tactic:
exact monotone_nat_of_le_succ fun n =>
  le_trans upperCrossingTime_le_lowerCrossingTime lowerCrossingTime_le_upperCrossingTime_succ

Result:
no goals
-- Mathlib/Control/LawfulFix.lean
theorem approx_mono ⦃i j : ℕ⦄ (hij : i ≤ j) : approx f i ≤ approx f j

Proof state:
case succ.step
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
ih : i ≤ j → approx (⇑f) i ≤ approx (⇑f) j
a✝ : i.le j
⊢ approx (⇑f) i ≤ approx (⇑f) (j + 1)

Tactic:
exact le_trans (ih ‹_›) (approx_mono' f)

Result:
no goals

Proof state:
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
hij : i ≤ 0
⊢ approx (⇑f) i ≤ approx (⇑f) 0

Tactic:
cases hij

Result:
case zero.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ approx (⇑f) 0 ≤ approx (⇑f) 0

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
hij : i ≤ j
⊢ approx (⇑f) i ≤ approx (⇑f) j

Tactic:
induction' j with j ih

Result:
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
hij : i ≤ 0
⊢ approx (⇑f) i ≤ approx (⇑f) 0

case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
ih : i ≤ j → approx (⇑f) i ≤ approx (⇑f) j
hij : i ≤ j + 1
⊢ approx (⇑f) i ≤ approx (⇑f) (j + 1)

Proof state:
case zero.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ approx (⇑f) 0 ≤ approx (⇑f) 0

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case succ.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
j : ℕ
ih : j + 1 ≤ j → approx (⇑f) (j + 1) ≤ approx (⇑f) j
⊢ approx (⇑f) (j + 1) ≤ approx (⇑f) (j + 1)

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
ih : i ≤ j → approx (⇑f) i ≤ approx (⇑f) j
hij : i ≤ j + 1
⊢ approx (⇑f) i ≤ approx (⇑f) (j + 1)

Tactic:
cases hij

Result:
case succ.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
j : ℕ
ih : j + 1 ≤ j → approx (⇑f) (j + 1) ≤ approx (⇑f) j
⊢ approx (⇑f) (j + 1) ≤ approx (⇑f) (j + 1)

case succ.step
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
ih : i ≤ j → approx (⇑f) i ≤ approx (⇑f) j
a✝ : i.le j
⊢ approx (⇑f) i ≤ approx (⇑f) (j + 1)
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem existsUnique_mem_range : ∃! n : ℕ, n < p ∧ x - n ∈ maximalIdeal ℤ_[p]

Proof state:
case right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hn₁ : n < p
hn₂ : x - ↑n ∈ maximalIdeal ℤ_[p]
m : ℕ
x✝ : (fun n => n < p ∧ x - ↑n ∈ maximalIdeal ℤ_[p]) m
hm₁ : m < p
hm₂ : x - ↑m ∈ maximalIdeal ℤ_[p]
this : ↑m = ↑n
⊢ m = n

Tactic:
rwa [ZMod.natCast_eq_natCast_iff, ModEq, mod_eq_of_lt hn₁, mod_eq_of_lt hm₁] at this

Result:
no goals

Proof state:
case right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hn₁ : n < p
hn₂ : x - ↑n ∈ maximalIdeal ℤ_[p]
m : ℕ
x✝ : (fun n => n < p ∧ x - ↑n ∈ maximalIdeal ℤ_[p]) m
hm₁ : m < p
hm₂ : x - ↑m ∈ maximalIdeal ℤ_[p]
⊢ m = n

Tactic:
have := (zmod_congr_of_sub_mem_max_ideal x n m hn₂ hm₂).symm

Result:
case right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hn₁ : n < p
hn₂ : x - ↑n ∈ maximalIdeal ℤ_[p]
m : ℕ
x✝ : (fun n => n < p ∧ x - ↑n ∈ maximalIdeal ℤ_[p]) m
hm₁ : m < p
hm₂ : x - ↑m ∈ maximalIdeal ℤ_[p]
this : ↑m = ↑n
⊢ m = n

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∃! n, n < p ∧ x - ↑n ∈ maximalIdeal ℤ_[p]

Tactic:
obtain ⟨n, hn₁, hn₂⟩ := exists_mem_range x

Result:
case intro.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hn₁ : n < p
hn₂ : x - ↑n ∈ maximalIdeal ℤ_[p]
⊢ ∃! n, n < p ∧ x - ↑n ∈ maximalIdeal ℤ_[p]

Proof state:
case intro.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hn₁ : n < p
hn₂ : x - ↑n ∈ maximalIdeal ℤ_[p]
⊢ ∃! n, n < p ∧ x - ↑n ∈ maximalIdeal ℤ_[p]

Tactic:
use n, ⟨hn₁, hn₂⟩, fun m ⟨hm₁, hm₂⟩ ↦ ?_

Result:
case right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hn₁ : n < p
hn₂ : x - ↑n ∈ maximalIdeal ℤ_[p]
m : ℕ
x✝ : (fun n => n < p ∧ x - ↑n ∈ maximalIdeal ℤ_[p]) m
hm₁ : m < p
hm₂ : x - ↑m ∈ maximalIdeal ℤ_[p]
⊢ m = n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_shiftConcat_lt_of_lt {x : BitVec w} {b : Bool} {k : Nat}
    (hk : k < w) (hx : x.toNat < 2 ^ k) :
    (x.shiftConcat b).toNat < 2 ^ (k + 1)

Proof state:
w : Nat
x : BitVec w
b : Bool
k : Nat
hk : k < w
hx : x.toNat < 2 ^ k
⊢ (x.shiftConcat b).toNat < 2 ^ (k + 1)

Tactic:
rw [toNat_shiftConcat_eq_of_lt hk hx]

Result:
w : Nat
x : BitVec w
b : Bool
k : Nat
hk : k < w
hx : x.toNat < 2 ^ k
⊢ x.toNat * 2 + b.toNat < 2 ^ (k + 1)

Proof state:
w : Nat
x : BitVec w
b : Bool
k : Nat
hk : k < w
hx : x.toNat < 2 ^ k
⊢ x.toNat * 2 + b.toNat < 2 ^ (k + 1)

Tactic:
have := Bool.toNat_lt b

Result:
w : Nat
x : BitVec w
b : Bool
k : Nat
hk : k < w
hx : x.toNat < 2 ^ k
this : b.toNat < 2
⊢ x.toNat * 2 + b.toNat < 2 ^ (k + 1)

Proof state:
w : Nat
x : BitVec w
b : Bool
k : Nat
hk : k < w
hx : x.toNat < 2 ^ k
this : b.toNat < 2
⊢ x.toNat * 2 + b.toNat < 2 ^ (k + 1)

Tactic:
omega

Result:
no goals