harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem range_omega : range omega = {x | ω ≤ x ∧ IsInitial x}

Proof state:
case h.mpr
x : Ordinal.{u_1}
⊢ x ∈ {x | ω ≤ x ∧ x.IsInitial} → x ∈ range ⇑ω_

Tactic:
rintro ⟨ha', ha⟩

Result:
case h.mpr.intro
x : Ordinal.{u_1}
ha' : ω ≤ x
ha : x.IsInitial
⊢ x ∈ range ⇑ω_

Proof state:
case h.mpr.intro.intro
a : Ordinal.{u_1}
ha' : ω ≤ preOmega a
ha : (preOmega a).IsInitial
⊢ preOmega a ∈ range ⇑ω_

Tactic:
use a - ω

Result:
case h
a : Ordinal.{u_1}
ha' : ω ≤ preOmega a
ha : (preOmega a).IsInitial
⊢ ω_ (a - ω) = preOmega a

Proof state:
case h
a : Ordinal.{u_1}
ha' : ω ≤ preOmega a
ha : (preOmega a).IsInitial
⊢ ω_ (a - ω) = preOmega a

Tactic:
rw [omega0_le_preOmega_iff] at ha'

Result:
case h
a : Ordinal.{u_1}
ha' : ω ≤ a
ha : (preOmega a).IsInitial
⊢ ω_ (a - ω) = preOmega a

Proof state:
⊢ range ⇑ω_ = {x | ω ≤ x ∧ x.IsInitial}

Tactic:
ext x

Result:
case h
x : Ordinal.{u_1}
⊢ x ∈ range ⇑ω_ ↔ x ∈ {x | ω ≤ x ∧ x.IsInitial}

Proof state:
case h.mp
x : Ordinal.{u_1}
⊢ x ∈ range ⇑ω_ → x ∈ {x | ω ≤ x ∧ x.IsInitial}

Tactic:
rintro ⟨a, rfl⟩

Result:
case h.mp.intro
a : Ordinal.{u_1}
⊢ ω_ a ∈ {x | ω ≤ x ∧ x.IsInitial}

Proof state:
case h.mp.intro
a : Ordinal.{u_1}
⊢ ω_ a ∈ {x | ω ≤ x ∧ x.IsInitial}

Tactic:
exact ⟨omega0_le_omega a, isInitial_omega a⟩

Result:
no goals

Proof state:
case h
a : Ordinal.{u_1}
ha' : ω ≤ a
ha : (preOmega a).IsInitial
⊢ ω_ (a - ω) = preOmega a

Tactic:
rw [omega_eq_preOmega, Ordinal.add_sub_cancel_of_le ha']

Result:
no goals

Proof state:
case h
x : Ordinal.{u_1}
⊢ x ∈ range ⇑ω_ ↔ x ∈ {x | ω ≤ x ∧ x.IsInitial}

Tactic:
constructor

Result:
case h.mp
x : Ordinal.{u_1}
⊢ x ∈ range ⇑ω_ → x ∈ {x | ω ≤ x ∧ x.IsInitial}

case h.mpr
x : Ordinal.{u_1}
⊢ x ∈ {x | ω ≤ x ∧ x.IsInitial} → x ∈ range ⇑ω_

Proof state:
case h.mpr.intro
x : Ordinal.{u_1}
ha' : ω ≤ x
ha : x.IsInitial
⊢ x ∈ range ⇑ω_

Tactic:
obtain ⟨a, rfl⟩ := ha.mem_range_preOmega

Result:
case h.mpr.intro.intro
a : Ordinal.{u_1}
ha' : ω ≤ preOmega a
ha : (preOmega a).IsInitial
⊢ preOmega a ∈ range ⇑ω_
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
/-- If `f` is `ℝ`-valued and integrable, then for any `c < 0` the set `{x | f x ≤ c}` has finite
measure. -/
lemma Integrable.measure_le_lt_top {f : α → ℝ} (hf : Integrable f μ) {c : ℝ} (c_neg : c < 0) :
    μ {a : α | f a ≤ c} < ∞

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
c : ℝ
c_neg : c < 0
⊢ {a | f a ≤ c} ⊆ {x | -c ≤ ‖f x‖}

Tactic:
intro x hx

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
c : ℝ
c_neg : c < 0
x : α
hx : x ∈ {a | f a ≤ c}
⊢ x ∈ {x | -c ≤ ‖f x‖}

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
c : ℝ
c_neg : c < 0
x : α
hx : f x ≤ c
⊢ -c ≤ |f x|

Tactic:
exact (show -c ≤ - f x by linarith).trans (neg_le_abs _)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
c : ℝ
c_neg : c < 0
x : α
hx : x ∈ {a | f a ≤ c}
⊢ x ∈ {x | -c ≤ ‖f x‖}

Tactic:
simp only [Real.norm_eq_abs, Set.mem_setOf_eq] at hx ⊢

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
c : ℝ
c_neg : c < 0
x : α
hx : f x ≤ c
⊢ -c ≤ |f x|

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
c : ℝ
c_neg : c < 0
⊢ μ {a | f a ≤ c} < ⊤

Tactic:
refine lt_of_le_of_lt (measure_mono ?_) (hf.measure_norm_ge_lt_top (show 0 < -c by linarith))

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
c : ℝ
c_neg : c < 0
⊢ {a | f a ≤ c} ⊆ {x | -c ≤ ‖f x‖}

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
c : ℝ
c_neg : c < 0
x : α
hx : f x ≤ c
⊢ -c ≤ -f x

Tactic:
linarith

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
c : ℝ
c_neg : c < 0
⊢ 0 < -c

Tactic:
linarith

Result:
no goals
-- Mathlib/Data/List/Lemmas.lean
theorem injOn_insertIdx_index_of_not_mem (l : List α) (x : α) (hx : x ∉ l) :
    Set.InjOn (fun k => insertIdx k x l) { n | n ≤ l.length }

Proof state:
case cons.succ.succ
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : ¬x = hd ∧ x ∉ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : hd :: insertIdx n✝¹ x tl = hd :: insertIdx n✝ x tl
⊢ n✝¹ = n✝

Tactic:
refine IH hx.right ?_ ?_ (by injection h)

Result:
case cons.succ.succ.refine_1
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : ¬x = hd ∧ x ∉ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : hd :: insertIdx n✝¹ x tl = hd :: insertIdx n✝ x tl
⊢ n✝¹ ∈ {n | n ≤ tl.length}

case cons.succ.succ.refine_2
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : ¬x = hd ∧ x ∉ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : hd :: insertIdx n✝¹ x tl = hd :: insertIdx n✝ x tl
⊢ n✝ ∈ {n | n ≤ tl.length}

Proof state:
case cons
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : x ∉ hd :: tl
n : ℕ
hn : n ≤ tl.length + 1
m : ℕ
hm : m ≤ tl.length + 1
h : (fun k => insertIdx k x (hd :: tl)) n = (fun k => insertIdx k x (hd :: tl)) m
⊢ n = m

Tactic:
simp only [mem_cons, not_or] at hx

Result:
case cons
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
n : ℕ
hn : n ≤ tl.length + 1
m : ℕ
hm : m ≤ tl.length + 1
h : (fun k => insertIdx k x (hd :: tl)) n = (fun k => insertIdx k x (hd :: tl)) m
hx : ¬x = hd ∧ x ∉ tl
⊢ n = m

Proof state:
case cons.zero.zero
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : ¬x = hd ∧ x ∉ tl
hn hm : 0 ≤ tl.length + 1
h : (fun k => insertIdx k x (hd :: tl)) 0 = (fun k => insertIdx k x (hd :: tl)) 0
⊢ 0 = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem _root_.IsPrimitiveRoot.lcm_totient_le_finrank [FiniteDimensional K L] {p q : ℕ} {x y : L}
    (hx : IsPrimitiveRoot x p) (hy : IsPrimitiveRoot y q)
    (hirr : Irreducible (cyclotomic (Nat.lcm p q) K)) :
    (Nat.lcm p q).totient ≤ Module.finrank K L

Proof state:
case inr.inr
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (cyclotomic (p.lcm q) K)
hppos : p > 0
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm ⟨p, hppos⟩ ⟨q, hqpos⟩
this : IsPrimitiveRoot z ↑k
⊢ φ (p.lcm q) ≤ Module.finrank K L

Tactic:
haveI := IsPrimitiveRoot.adjoin_isCyclotomicExtension K this

Result:
case inr.inr
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (cyclotomic (p.lcm q) K)
hppos : p > 0
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm ⟨p, hppos⟩ ⟨q, hqpos⟩
this✝ : IsPrimitiveRoot z ↑k
this : IsCyclotomicExtension {k} K ↥(adjoin K {z})
⊢ φ (p.lcm q) ≤ Module.finrank K L

Proof state:
case inr.inr
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (cyclotomic (p.lcm q) K)
hppos : p > 0
hqpos : q > 0
⊢ φ (p.lcm q) ≤ Module.finrank K L

Tactic:
let z := x ^ (p / factorizationLCMLeft p q) * y ^ (q / factorizationLCMRight p q)

Result:
case inr.inr
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (cyclotomic (p.lcm q) K)
hppos : p > 0
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
⊢ φ (p.lcm q) ≤ Module.finrank K L

Proof state:
case inr.inr
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (cyclotomic (p.lcm q) K)
hppos : p > 0
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
⊢ φ (p.lcm q) ≤ Module.finrank K L

Tactic:
let k := PNat.lcm ⟨p, hppos⟩ ⟨q, hqpos⟩

Result:
case inr.inr
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (cyclotomic (p.lcm q) K)
hppos : p > 0
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm ⟨p, hppos⟩ ⟨q, hqpos⟩
⊢ φ (p.lcm q) ≤ Module.finrank K L
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem AddValuation.map_one : addValuationDef (1 : ℚ_[p]) = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ addValuationDef 1 = 0

Tactic:
rw [addValuationDef, if_neg one_ne_zero, valuation_one, WithTop.coe_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean
lemma isRightDerivedFunctor_iff_of_iso (α' : F ⟶ L ⋙ RF') (W : MorphismProperty C)
    [L.IsLocalization W] (e : RF ≅ RF') (comm : α ≫ whiskerLeft L e.hom = α') :
    RF.IsRightDerivedFunctor α W ↔ RF'.IsRightDerivedFunctor α' W

Proof state:
C : Type u_1
D : Type u_6
H : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_6} D
inst✝¹ : Category.{u_2, u_3} H
RF RF' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
α' : F ⟶ L ⋙ RF'
W : MorphismProperty C
inst✝ : L.IsLocalization W
e : RF ≅ RF'
comm : α ≫ whiskerLeft L e.hom = α'
⊢ RF.IsLeftKanExtension α ↔ RF'.IsLeftKanExtension α'

Tactic:
exact isLeftKanExtension_iff_of_iso e _ _ comm

Result:
no goals

Proof state:
C : Type u_1
D : Type u_6
H : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_6} D
inst✝¹ : Category.{u_2, u_3} H
RF RF' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
α' : F ⟶ L ⋙ RF'
W : MorphismProperty C
inst✝ : L.IsLocalization W
e : RF ≅ RF'
comm : α ≫ whiskerLeft L e.hom = α'
⊢ RF.IsRightDerivedFunctor α W ↔ RF'.IsRightDerivedFunctor α' W

Tactic:
simp only [isRightDerivedFunctor_iff_isLeftKanExtension]

Result:
C : Type u_1
D : Type u_6
H : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_6} D
inst✝¹ : Category.{u_2, u_3} H
RF RF' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
α' : F ⟶ L ⋙ RF'
W : MorphismProperty C
inst✝ : L.IsLocalization W
e : RF ≅ RF'
comm : α ≫ whiskerLeft L e.hom = α'
⊢ RF.IsLeftKanExtension α ↔ RF'.IsLeftKanExtension α'
-- Mathlib/Algebra/Polynomial/PartialFractions.lean
theorem div_eq_quo_add_sum_rem_div (f : R[X]) {ι : Type*} {g : ι → R[X]} {s : Finset ι}
    (hg : ∀ i ∈ s, (g i).Monic) (hcop : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)) :
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧
        ((↑f : K) / ∏ i ∈ s, ↑(g i)) = ↑q + ∑ i ∈ s, (r i : K) / (g i : K)

Proof state:
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
ι : Type u_1
g : ι → R[X]
a : ι
b : Finset ι
hab : a ∉ b
Hind :
  ∀ (f : R[X]),
    (∀ i ∈ b, (g i).Monic) →
      ((↑b).Pairwise fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ i ∈ b, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ b, ↑(g i) = ↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ i ∈ insert a b, (g i).Monic
hcop : (↑(insert a b)).Pairwise fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : r₁.degree < (g a).degree
left✝ : r₂.degree < (∏ i ∈ b, g i).degree
hf✝ : ↑f / (↑(g a) * ↑(∏ i ∈ b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i ∈ b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ i ∈ b, (r i).degree < (g i).degree
hf : ↑f / ↑(g a * ∏ i ∈ b, g i) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i ∈ b, g i)
IH : ↑r₂ / ↑(∏ i ∈ b, g i) = ↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)
⊢ ↑q₀ + ↑r₁ / ↑(g a) + (↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)) = ↑(q₀ + q) + (↑r₁ / ↑(g a) + ∑ i ∈ b, ↑(r i) / ↑(g i))

Tactic:
push_cast

Result:
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
ι : Type u_1
g : ι → R[X]
a : ι
b : Finset ι
hab : a ∉ b
Hind :
  ∀ (f : R[X]),
    (∀ i ∈ b, (g i).Monic) →
      ((↑b).Pairwise fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ i ∈ b, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ b, ↑(g i) = ↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ i ∈ insert a b, (g i).Monic
hcop : (↑(insert a b)).Pairwise fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : r₁.degree < (g a).degree
left✝ : r₂.degree < (∏ i ∈ b, g i).degree
hf✝ : ↑f / (↑(g a) * ↑(∏ i ∈ b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i ∈ b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ i ∈ b, (r i).degree < (g i).degree
hf : ↑f / ↑(g a * ∏ i ∈ b, g i) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i ∈ b, g i)
IH : ↑r₂ / ↑(∏ i ∈ b, g i) = ↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)
⊢ ↑q₀ + ↑r₁ / ↑(g a) + (↑q + ∑ i ∈ b, ↑(r i) / ↑(g i)) = ↑q₀ + ↑q + (↑r₁ / ↑(g a) + ∑ i ∈ b, ↑(r i) / ↑(g i))
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive (attr := simp)]
lemma zpow_iterate (k : ℤ) : ∀ n : ℕ, (fun x : G ↦ x ^ k)^[n] = (· ^ k ^ n)
  | 0 => by ext; simp [Int.pow_zero]
  | n + 1 => by ext; simp [zpow_iterate, Int.pow_succ', zpow_mul]

Proof state:
G : Type u_3
inst✝ : Group G
k : ℤ
⊢ (fun x => x ^ k)^[0] = fun x => x ^ k ^ 0

Tactic:
ext

Result:
case h
G : Type u_3
inst✝ : Group G
k : ℤ
x✝ : G
⊢ (fun x => x ^ k)^[0] x✝ = x✝ ^ k ^ 0

Proof state:
case h
G : Type u_3
inst✝ : Group G
k : ℤ
n : ℕ
x✝ : G
⊢ (fun x => x ^ k)^[n + 1] x✝ = x✝ ^ k ^ (n + 1)

Tactic:
simp [zpow_iterate, Int.pow_succ', zpow_mul]

Result:
no goals

Proof state:
case h
G : Type u_3
inst✝ : Group G
k : ℤ
x✝ : G
⊢ (fun x => x ^ k)^[0] x✝ = x✝ ^ k ^ 0

Tactic:
simp [Int.pow_zero]

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
k : ℤ
n : ℕ
⊢ (fun x => x ^ k)^[n + 1] = fun x => x ^ k ^ (n + 1)

Tactic:
ext

Result:
case h
G : Type u_3
inst✝ : Group G
k : ℤ
n : ℕ
x✝ : G
⊢ (fun x => x ^ k)^[n + 1] x✝ = x✝ ^ k ^ (n + 1)
-- Mathlib/NumberTheory/LegendreSymbol/Basic.lean
theorem mul (a b : ℤ) : legendreSym p (a * b) = legendreSym p a * legendreSym p b

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a b : ℤ
⊢ legendreSym p (a * b) = legendreSym p a * legendreSym p b

Tactic:
simp [legendreSym, Int.cast_mul, map_mul, quadraticCharFun_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem iota_inj : iota n = iota n' ↔ n = n'

Proof state:
case mp
n n' : Nat
h : iota n = iota n'
h' : n = n'
⊢ n = n'

Tactic:
exact h'

Result:
no goals

Proof state:
n n' : Nat
⊢ iota n = iota n' ↔ n = n'

Tactic:
constructor

Result:
case mp
n n' : Nat
⊢ iota n = iota n' → n = n'

case mpr
n n' : Nat
⊢ n = n' → iota n = iota n'

Proof state:
case mp
n n' : Nat
⊢ iota n = iota n' → n = n'

Tactic:
intro h

Result:
case mp
n n' : Nat
h : iota n = iota n'
⊢ n = n'

Proof state:
case mpr
n n' : Nat
⊢ n = n' → iota n = iota n'

Tactic:
rintro rfl

Result:
case mpr
n : Nat
⊢ iota n = iota n

Proof state:
case mp
n n' : Nat
h : iota n = iota n'
h' : (iota n).length = (iota n').length
⊢ n = n'

Tactic:
simp at h'

Result:
case mp
n n' : Nat
h : iota n = iota n'
h' : n = n'
⊢ n = n'

Proof state:
case mpr
n : Nat
⊢ iota n = iota n

Tactic:
simp

Result:
no goals

Proof state:
case mp
n n' : Nat
h : iota n = iota n'
⊢ n = n'

Tactic:
have h' := congrArg List.length h

Result:
case mp
n n' : Nat
h : iota n = iota n'
h' : (iota n).length = (iota n').length
⊢ n = n'
-- Mathlib/Data/Vector/Defs.lean
theorem toList_append {n m : ℕ} (v : Vector α n) (w : Vector α m) :
    toList (append v w) = toList v ++ toList w

Proof state:
case mk
α : Type u_1
n m : ℕ
w : Vector α m
val✝ : List α
property✝ : val✝.length = n
⊢ (append ⟨val✝, property✝⟩ w).toList = toList ⟨val✝, property✝⟩ ++ w.toList

Tactic:
cases w

Result:
case mk.mk
α : Type u_1
n m : ℕ
val✝¹ : List α
property✝¹ : val✝¹.length = n
val✝ : List α
property✝ : val✝.length = m
⊢ (append ⟨val✝¹, property✝¹⟩ ⟨val✝, property✝⟩).toList = toList ⟨val✝¹, property✝¹⟩ ++ toList ⟨val✝, property✝⟩

Proof state:
case mk.mk
α : Type u_1
n m : ℕ
val✝¹ : List α
property✝¹ : val✝¹.length = n
val✝ : List α
property✝ : val✝.length = m
⊢ (append ⟨val✝¹, property✝¹⟩ ⟨val✝, property✝⟩).toList = toList ⟨val✝¹, property✝¹⟩ ++ toList ⟨val✝, property✝⟩

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
n m : ℕ
v : Vector α n
w : Vector α m
⊢ (v.append w).toList = v.toList ++ w.toList

Tactic:
cases v

Result:
case mk
α : Type u_1
n m : ℕ
w : Vector α m
val✝ : List α
property✝ : val✝.length = n
⊢ (append ⟨val✝, property✝⟩ w).toList = toList ⟨val✝, property✝⟩ ++ w.toList
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
lemma image_exp_Ioc_eq_sphere : (fun θ : ℝ ↦ exp (θ * I)) '' Set.Ioc (-π) π = sphere 0 1

Proof state:
case h
x✝ : ℂ
⊢ x✝ ∈ (fun θ => cexp (↑θ * I)) '' Ioc (-π) π ↔ x✝ ∈ sphere 0 1

Tactic:
simpa using norm_eq_one_iff'.symm

Result:
no goals

Proof state:
⊢ (fun θ => cexp (↑θ * I)) '' Ioc (-π) π = sphere 0 1

Tactic:
ext

Result:
case h
x✝ : ℂ
⊢ x✝ ∈ (fun θ => cexp (↑θ * I)) '' Ioc (-π) π ↔ x✝ ∈ sphere 0 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_natAbs {a : Int} : a ≤ natAbs a :=
  match Int.le_total 0 a with
  | .inl h => by rw [eq_natAbs_of_zero_le h]; apply Int.le_refl
  | .inr h => Int.le_trans h (ofNat_zero_le _)

Proof state:
a : Int
h : 0 ≤ a
⊢ ↑a.natAbs ≤ ↑(↑a.natAbs).natAbs

Tactic:
apply Int.le_refl

Result:
no goals

Proof state:
a : Int
h : 0 ≤ a
⊢ a ≤ ↑a.natAbs

Tactic:
rw [eq_natAbs_of_zero_le h]

Result:
a : Int
h : 0 ≤ a
⊢ ↑a.natAbs ≤ ↑(↑a.natAbs).natAbs
-- Mathlib/Analysis/Convex/Jensen.lean
/-- Canonical form of the **equality case of Jensen's equality**.

For a strictly convex function `f` and positive weights `w`, we have
`f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)` if and only if the points `p` are all equal
(and in fact all equal to their center of mass wrt `w`). -/
lemma StrictConvexOn.map_sum_eq_iff {w : ι → 𝕜} {p : ι → E} (hf : StrictConvexOn 𝕜 s f)
    (h₀ : ∀ i ∈ t, 0 < w i) (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) :
    f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) → ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i

Tactic:
obtain rfl | ⟨i₀, hi₀⟩ := t.eq_empty_or_nonempty

Result:
case mp.inl
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ ∅, 0 < w i
h₁ : ∑ i ∈ ∅, w i = 1
hmem : ∀ i ∈ ∅, p i ∈ s
⊢ f (∑ i ∈ ∅, w i • p i) = ∑ i ∈ ∅, w i • f (p i) → ∀ j ∈ ∅, p j = ∑ i ∈ ∅, w i • p i

case mp.inr.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
i₀ : ι
hi₀ : i₀ ∈ t
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) → ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
h : ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i
H : ∀ j ∈ t, w j • f (p j) = w j • f (∑ i ∈ t, w i • p i)
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)

Tactic:
rw [sum_congr rfl H, ← sum_smul, h₁, one_smul]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem pullbackDiagonalMapIdIso_inv_snd_snd :
    (pullbackDiagonalMapIdIso f g i).inv ≫ pullback.snd _ _ ≫ pullback.snd _ _ =
      pullback.snd _ _

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).inv ≫
      snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ snd (f ≫ i) (g ≫ i) =
    snd f g

Tactic:
rw [Iso.inv_comp_eq]

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ snd (f ≫ i) (g ≫ i) =
    (pullbackDiagonalMapIdIso f g i).hom ≫ snd f g

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ snd (f ≫ i) (g ≫ i) =
    (pullbackDiagonalMapIdIso f g i).hom ≫ snd f g

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Denumerable.lean
theorem ofNat_surjective : Surjective (ofNat s)
  | ⟨x, hx⟩ => by
    set t : List s :=
      ((List.range x).filter fun y => y ∈ s).pmap
        (fun (y : ℕ) (hy : y ∈ s) => ⟨y, hy⟩)
        (by intros a ha; simpa using (List.mem_filter.mp ha).2) with ht
    have hmt : ∀ {y : s}, y ∈ t ↔ y < ⟨x, hx⟩

Proof state:
case bot
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
hmax : t.maximum = ⊥
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Tactic:
refine ⟨0, le_antisymm bot_le (le_of_not_gt fun h => List.not_mem_nil (⊥ : s) ?_)⟩

Result:
case bot
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
hmax : t.maximum = ⊥
h : ⟨x, hx⟩ > ofNat s 0
⊢ ⊥ ∈ []

Proof state:
case bot
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
hmax : t.maximum = ⊥
h : ⟨x, hx⟩ > ofNat s 0
⊢ ⊥ ∈ []

Tactic:
rwa [← List.maximum_eq_bot.1 hmax, hmt]

Result:
no goals