harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem leftInvSeq_take (ω : List B) (j : ℕ) :
    lis (ω.take j) = (lis ω).take j

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
⊢ (cs.rightInvSeq (take j ω).reverse).reverse = take j (cs.rightInvSeq ω.reverse).reverse

Tactic:
rw [List.take_reverse]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
⊢ (cs.rightInvSeq (take j ω).reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
⊢ (cs.rightInvSeq (take j ω.reverse.reverse).reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse

Tactic:
rw [List.take_reverse]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
⊢ (cs.rightInvSeq (drop (ω.reverse.length - j) ω.reverse).reverse.reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
⊢ cs.leftInvSeq (take j ω) = take j (cs.leftInvSeq ω)

Tactic:
simp only [leftInvSeq_eq_reverse_rightInvSeq_reverse]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
⊢ (cs.rightInvSeq (take j ω).reverse).reverse = take j (cs.rightInvSeq ω.reverse).reverse

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
⊢ (cs.rightInvSeq (take j ω).reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse

Tactic:
nth_rw 1 [← List.reverse_reverse ω]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
⊢ (cs.rightInvSeq (take j ω.reverse.reverse).reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
⊢ (cs.rightInvSeq (drop (ω.reverse.length - j) ω.reverse).reverse.reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse

Tactic:
simp [rightInvSeq_drop]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
lemma rightHomologyMap_eq [S₁.HasRightHomology] [S₂.HasRightHomology] :
    rightHomologyMap φ = h₁.rightHomologyIso.hom ≫ γ.φH ≫ h₂.rightHomologyIso.inv

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ rightHomologyMap φ = rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ rightHomologyMap φ = h₁.rightHomologyIso.hom ≫ γ.φH ≫ h₂.rightHomologyIso.inv

Tactic:
dsimp [RightHomologyData.rightHomologyIso, rightHomologyMapIso']

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ rightHomologyMap φ =
    rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁ ≫ γ.φH ≫ rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ rightHomologyMap φ =
    rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁ ≫ γ.φH ≫ rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData

Tactic:
rw [← γ.rightHomologyMap'_eq, ← rightHomologyMap'_comp,
  ← rightHomologyMap'_comp, id_comp, comp_id]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ rightHomologyMap φ = rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem zipIdx_eq_zipIdxTR : @zipIdx = @zipIdxTR

Proof state:
case h.h.h
α : Type u_1
l : List α
n : optParam Nat 0
⊢ l.zipIdx n = (Array.foldr (fun a x => (x.fst - 1, (a, x.fst - 1) :: x.snd)) (n + l.toArray.size, []) l.toArray).snd

Tactic:
let f := fun (a : α) (n, acc) => (n-1, (a, n-1) :: acc)

Result:
case h.h.h
α : Type u_1
l : List α
n : optParam Nat 0
f : α → Nat × List (α × Nat) → Nat × List (α × Nat) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (a, n - 1) :: acc)
⊢ l.zipIdx n = (Array.foldr (fun a x => (x.fst - 1, (a, x.fst - 1) :: x.snd)) (n + l.toArray.size, []) l.toArray).snd

Proof state:
α : Type u_1
l : List α
n✝ : optParam Nat 0
f : α → Nat × List (α × Nat) → Nat × List (α × Nat) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (a, n - 1) :: acc)
a : α
as : List α
n : Nat
⊢ foldr f (n + (a :: as).length, []) (a :: as) = (n, (a :: as).zipIdx n)

Tactic:
rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]

Result:
α : Type u_1
l : List α
n✝ : optParam Nat 0
f : α → Nat × List (α × Nat) → Nat × List (α × Nat) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (a, n - 1) :: acc)
a : α
as : List α
n : Nat
⊢ f a (n.succ, as.zipIdx n.succ) = (n, (a :: as).zipIdx n)

Proof state:
α : Type u_1
l : List α
n✝ : optParam Nat 0
f : α → Nat × List (α × Nat) → Nat × List (α × Nat) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (a, n - 1) :: acc)
a : α
as : List α
n : Nat
⊢ f a (n.succ, as.zipIdx n.succ) = (n, (a :: as).zipIdx n)

Tactic:
simp [zipIdx, f]

Result:
no goals

Proof state:
case h.h.h
α : Type u_1
l : List α
n : optParam Nat 0
⊢ l.zipIdx n = l.zipIdxTR n

Tactic:
simp [zipIdxTR, -Array.size_toArray]

Result:
case h.h.h
α : Type u_1
l : List α
n : optParam Nat 0
⊢ l.zipIdx n = (Array.foldr (fun a x => (x.fst - 1, (a, x.fst - 1) :: x.snd)) (n + l.toArray.size, []) l.toArray).snd

Proof state:
⊢ @zipIdx = @zipIdxTR

Tactic:
funext α l n

Result:
case h.h.h
α : Type u_1
l : List α
n : optParam Nat 0
⊢ l.zipIdx n = l.zipIdxTR n

Proof state:
case h.h.h
α : Type u_1
l : List α
n : optParam Nat 0
f : α → Nat × List (α × Nat) → Nat × List (α × Nat) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (a, n - 1) :: acc)
⊢ l.zipIdx n = (Array.foldr (fun a x => (x.fst - 1, (a, x.fst - 1) :: x.snd)) (n + l.toArray.size, []) l.toArray).snd

Tactic:
rw [← Array.foldr_toList]

Result:
case h.h.h
α : Type u_1
l : List α
n : optParam Nat 0
f : α → Nat × List (α × Nat) → Nat × List (α × Nat) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (a, n - 1) :: acc)
⊢ l.zipIdx n = (foldr (fun a x => (x.fst - 1, (a, x.fst - 1) :: x.snd)) (n + l.toArray.size, []) l.toArray.toList).snd

Proof state:
case h.h.h
α : Type u_1
l : List α
n : optParam Nat 0
f : α → Nat × List (α × Nat) → Nat × List (α × Nat) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (a, n - 1) :: acc)
⊢ l.zipIdx n = (foldr (fun a x => (x.fst - 1, (a, x.fst - 1) :: x.snd)) (n + l.toArray.size, []) l.toArray.toList).snd

Tactic:
simp +zetaDelta [go]

Result:
no goals
-- Mathlib/Data/Nat/Pairing.lean
theorem add_le_pair (m n : ℕ) : m + n ≤ pair m n

Proof state:
m n : ℕ
⊢ m + n ≤ if m < n then n * n + m else m * m + (m + n)

Tactic:
split_ifs

Result:
case pos
m n : ℕ
h✝ : m < n
⊢ m + n ≤ n * n + m

case neg
m n : ℕ
h✝ : ¬m < n
⊢ m + n ≤ m * m + (m + n)

Proof state:
case pos
m n : ℕ
h✝ : m < n
⊢ m + n ≤ n * n + m

Tactic:
have := le_mul_self n

Result:
case pos
m n : ℕ
h✝ : m < n
this : n ≤ n * n
⊢ m + n ≤ n * n + m

Proof state:
case pos
m n : ℕ
h✝ : m < n
this : n ≤ n * n
⊢ m + n ≤ n * n + m

Tactic:
omega

Result:
no goals

Proof state:
m n : ℕ
⊢ m + n ≤ pair m n

Tactic:
simp only [pair, Nat.add_assoc]

Result:
m n : ℕ
⊢ m + n ≤ if m < n then n * n + m else m * m + (m + n)

Proof state:
case neg
m n : ℕ
h✝ : ¬m < n
⊢ m + n ≤ m * m + (m + n)

Tactic:
exact Nat.le_add_left _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem drop_length_cons {l : List α} (h : l ≠ []) (a : α) :
    (a :: l).drop l.length = [l.getLast h]

Proof state:
case nil
α : Type u_1
h : [] ≠ []
a : α
⊢ drop [].length [a] = [[].getLast h]

Tactic:
cases h rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop l.length (a :: l) = [l.getLast h]
h : y :: l ≠ []
a : α
⊢ drop l.length (y :: l) = [(y :: l).getLast h]

Tactic:
by_cases h₁ : l = []

Result:
case pos
α : Type u_1
y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop l.length (a :: l) = [l.getLast h]
h : y :: l ≠ []
a : α
h₁ : l = []
⊢ drop l.length (y :: l) = [(y :: l).getLast h]

case neg
α : Type u_1
y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop l.length (a :: l) = [l.getLast h]
h : y :: l ≠ []
a : α
h₁ : ¬l = []
⊢ drop l.length (y :: l) = [(y :: l).getLast h]

Proof state:
case neg
α : Type u_1
y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop l.length (a :: l) = [l.getLast h]
h : y :: l ≠ []
a : α
h₁ : ¬l = []
⊢ drop l.length (y :: l) = [l.getLast h₁]

Tactic:
exact ih h₁ y

Result:
no goals

Proof state:
case cons
α : Type u_1
y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop l.length (a :: l) = [l.getLast h]
h : y :: l ≠ []
a : α
⊢ drop (y :: l).length (a :: y :: l) = [(y :: l).getLast h]

Tactic:
simp only [drop, length]

Result:
case cons
α : Type u_1
y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop l.length (a :: l) = [l.getLast h]
h : y :: l ≠ []
a : α
⊢ drop l.length (y :: l) = [(y :: l).getLast h]

Proof state:
case neg
α : Type u_1
y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop l.length (a :: l) = [l.getLast h]
h : y :: l ≠ []
a : α
h₁ : ¬l = []
⊢ drop l.length (y :: l) = [(y :: l).getLast h]

Tactic:
rw [getLast_cons h₁]

Result:
case neg
α : Type u_1
y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop l.length (a :: l) = [l.getLast h]
h : y :: l ≠ []
a : α
h₁ : ¬l = []
⊢ drop l.length (y :: l) = [l.getLast h₁]

Proof state:
case pos
α : Type u_1
y : α
l : List α
ih : ∀ (h : l ≠ []) (a : α), drop l.length (a :: l) = [l.getLast h]
h : y :: l ≠ []
a : α
h₁ : l = []
⊢ drop l.length (y :: l) = [(y :: l).getLast h]

Tactic:
simp [h₁]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem monomial_mul_X_pow (n : ℕ) (r : R) (k : ℕ) :
    monomial n r * X ^ k = monomial (n + k) r

Proof state:
case succ
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
k : ℕ
ih : (monomial n) r * X ^ k = (monomial (n + k)) r
⊢ (monomial n) r * X ^ (k + 1) = (monomial (n + (k + 1))) r

Tactic:
simp [ih, pow_succ, ← mul_assoc, add_assoc]

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ (monomial n) r * X ^ 0 = (monomial (n + 0)) r

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
k : ℕ
⊢ (monomial n) r * X ^ k = (monomial (n + k)) r

Tactic:
induction k with
| zero => simp
| succ k ih => simp [ih, pow_succ, ← mul_assoc, add_assoc]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem norm_mul_pow_le_mul_pow_of_lt_radius (h : ↑r < p.radius) :
    ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ n, ‖p n‖ * (r : ℝ) ^ n ≤ C * a ^ n

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < p.radius
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : C > 0
H : ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
⊢ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n

Tactic:
exact ⟨a, ha, C, hC, fun n => (le_abs_self _).trans (H n)⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < p.radius
⊢ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n

Tactic:
have := ((TFAE_exists_lt_isLittleO_pow (fun n => ‖p n‖ * (r : ℝ) ^ n) 1).out 1 5).mp
  (p.isLittleO_of_lt_radius h)

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < p.radius
this : ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
⊢ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < p.radius
this : ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
⊢ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n

Tactic:
rcases this with ⟨a, ha, C, hC, H⟩

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < p.radius
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : C > 0
H : ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
⊢ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n
-- Mathlib/CategoryTheory/Opposites.lean
theorem isIso_of_op {X Y : C} (f : X ⟶ Y) [IsIso f.op] : IsIso f :=
  ⟨⟨(inv f.op).unop, ⟨Quiver.Hom.op_inj (by simp), Quiver.Hom.op_inj (by simp)⟩⟩⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f.op
⊢ (f ≫ (inv f.op).unop).op = (𝟙 X).op

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f.op
⊢ ((inv f.op).unop ≫ f).op = (𝟙 Y).op

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem incidenceSet_inter_incidenceSet_of_adj (h : G.Adj a b) :
    G.incidenceSet a ∩ G.incidenceSet b = {s(a, b)}

Proof state:
V : Type u
G : SimpleGraph V
a b : V
h : G.Adj a b
⊢ {s(a, b)} ⊆ G.incidenceSet a ∩ G.incidenceSet b

Tactic:
rintro _ (rfl : _ = s(a, b))

Result:
V : Type u
G : SimpleGraph V
a b : V
h : G.Adj a b
⊢ s(a, b) ∈ G.incidenceSet a ∩ G.incidenceSet b

Proof state:
V : Type u
G : SimpleGraph V
a b : V
h : G.Adj a b
⊢ G.incidenceSet a ∩ G.incidenceSet b = {s(a, b)}

Tactic:
refine (G.incidenceSet_inter_incidenceSet_subset <| h.ne).antisymm ?_

Result:
V : Type u
G : SimpleGraph V
a b : V
h : G.Adj a b
⊢ {s(a, b)} ⊆ G.incidenceSet a ∩ G.incidenceSet b

Proof state:
V : Type u
G : SimpleGraph V
a b : V
h : G.Adj a b
⊢ s(a, b) ∈ G.incidenceSet a ∩ G.incidenceSet b

Tactic:
exact ⟨G.mk'_mem_incidenceSet_left_iff.2 h, G.mk'_mem_incidenceSet_right_iff.2 h⟩

Result:
no goals
-- Mathlib/NumberTheory/Modular.lean
/-- For every `τ : ℍ` there is some `γ ∈ SL(2, ℤ)` that sends it to an element whose
imaginary part is at least `1/2` and such that `denom γ τ` has norm at most 1. -/
lemma exists_one_half_le_im_smul_and_norm_denom_le (τ : ℍ) :
    ∃ γ : SL(2, ℤ), 1 / 2 ≤ im (γ • τ) ∧ ‖denom γ τ‖ ≤ 1

Proof state:
τ : ℍ
h : 1 / 2 ≤ τ.im
⊢ ‖denom (↑1) τ‖ ≤ 1

Tactic:
simp only [coe_one, denom_one, norm_one, le_refl]

Result:
no goals

Proof state:
case inr
τ : ℍ
h : τ.im ≤ 1 / 2
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
⊢ ‖denom (↑γ) τ‖ ≤ 1

Tactic:
have h1 : τ.im ≤ (γ • τ).im := h.trans hγ

Result:
case inr
τ : ℍ
h : τ.im ≤ 1 / 2
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
h1 : τ.im ≤ (γ • τ).im
⊢ ‖denom (↑γ) τ‖ ≤ 1

Proof state:
case inr
τ : ℍ
h : τ.im ≤ 1 / 2
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
h1 : τ.im ≤ (γ • τ).im
⊢ ‖denom (↑γ) τ‖ ≤ 1

Tactic:
rw [im_smul_eq_div_normSq, le_div_iff₀ (normSq_denom_pos (↑γ) τ), normSq_eq_norm_sq] at h1

Result:
case inr
τ : ℍ
h : τ.im ≤ 1 / 2
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
h1 : τ.im * ‖denom (↑γ) τ‖ ^ 2 ≤ τ.im
⊢ ‖denom (↑γ) τ‖ ≤ 1

Proof state:
case inr
τ : ℍ
h : τ.im ≤ 1 / 2
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
h1 : τ.im * ‖denom (↑γ) τ‖ ^ 2 ≤ τ.im
⊢ ‖denom (↑γ) τ‖ ≤ 1

Tactic:
simpa only [sq_le_one_iff_abs_le_one, abs_norm] using
  (mul_le_iff_le_one_right τ.2).mp h1

Result:
no goals

Proof state:
case inl
τ : ℍ
h : 1 / 2 ≤ τ.im
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im ∧ ‖denom (↑γ) τ‖ ≤ 1

Tactic:
exact ⟨1, (one_smul SL(2, ℤ) τ).symm ▸ h, by simp only [coe_one, denom_one, norm_one, le_refl]⟩

Result:
no goals

Proof state:
τ : ℍ
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im ∧ ‖denom (↑γ) τ‖ ≤ 1

Tactic:
rcases le_total (1 / 2) τ.im with h | h

Result:
case inl
τ : ℍ
h : 1 / 2 ≤ τ.im
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im ∧ ‖denom (↑γ) τ‖ ≤ 1

case inr
τ : ℍ
h : τ.im ≤ 1 / 2
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im ∧ ‖denom (↑γ) τ‖ ≤ 1

Proof state:
case inr
τ : ℍ
h : τ.im ≤ 1 / 2
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im ∧ ‖denom (↑γ) τ‖ ≤ 1

Tactic:
refine (exists_one_half_le_im_smul τ).imp (fun γ hγ ↦ ⟨hγ, ?_⟩)

Result:
case inr
τ : ℍ
h : τ.im ≤ 1 / 2
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
⊢ ‖denom (↑γ) τ‖ ≤ 1
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_eq_iff (hn : n ≠ 0) : ⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ n

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
hn : n ≠ 0
⊢ ⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ ↑n

Tactic:
rw [← ceil_le, ← not_le, ← ceil_le, not_le,
  tsub_lt_iff_right (Nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)), Nat.lt_add_one_iff,
  le_antisymm_iff, and_comm]

Result:
no goals
-- Mathlib/RepresentationTheory/Invariants.lean
theorem mul_average_right (g : G) : average k G * ↑(Finsupp.single g 1) = average k G

Proof state:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x : G, single (x * g) 1 = ⅟↑(Fintype.card G) • Finset.univ.sum f

Tactic:
show ⅟ (Fintype.card G : k) • ∑ x : G, f (x * g) = ⅟ (Fintype.card G : k) • ∑ x : G, f x

Result:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x : G, f (x * g) = ⅟↑(Fintype.card G) • ∑ x : G, f x

Proof state:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
⊢ ⅟↑(Fintype.card G) • ∑ x : G, single (x * g) 1 = ⅟↑(Fintype.card G) • ∑ x : G, single x 1

Tactic:
set f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1

Result:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x : G, single (x * g) 1 = ⅟↑(Fintype.card G) • Finset.univ.sum f

Proof state:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
⊢ average k G * Finsupp.single g 1 = average k G

Tactic:
simp only [mul_one, Finset.sum_mul, Algebra.smul_mul_assoc, average, MonoidAlgebra.of_apply,
  Finset.sum_congr, MonoidAlgebra.single_mul_single]

Result:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
⊢ ⅟↑(Fintype.card G) • ∑ x : G, single (x * g) 1 = ⅟↑(Fintype.card G) • ∑ x : G, single x 1

Proof state:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x : G, f (x * g) = ⅟↑(Fintype.card G) • ∑ x : G, f x

Tactic:
rw [Function.Bijective.sum_comp (Group.mulRight_bijective g) _]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Finsupp.lean
theorem exists_of_mem_closure_range [Fintype ι] (hx : x ∈ closure (Set.range f)) :
    ∃ a : ι → ℕ, x = ∏ i, f i ^ a i

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
hx : x ∈ closure (Set.range f)
⊢ ∃ a, x = ∏ i : ι, f i ^ a i

Tactic:
obtain ⟨a, rfl⟩ := exists_finsupp_of_mem_closure_range f x hx

Result:
case intro
M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
inst✝ : Fintype ι
a : ι →₀ ℕ
hx : (a.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
⊢ ∃ a_1, (a.prod fun x1 x2 => f x1 ^ x2) = ∏ i : ι, f i ^ a_1 i

Proof state:
case intro
M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
inst✝ : Fintype ι
a : ι →₀ ℕ
hx : (a.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
⊢ ∃ a_1, (a.prod fun x1 x2 => f x1 ^ x2) = ∏ i : ι, f i ^ a_1 i

Tactic:
exact ⟨a, by simp⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
inst✝ : Fintype ι
a : ι →₀ ℕ
hx : (a.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
⊢ (a.prod fun x1 x2 => f x1 ^ x2) = ∏ i : ι, f i ^ a i

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
theorem algebraMap' (k : K) : (algebraMap K (K_hat R K) k).IsFiniteAdele

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this✝ : {v | (valuation K v) ↑d < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ {v | 1 < (valuation K v) k}
hk : (valuation K v) k * v.intValuation d = v.intValuation n
this : v.intValuationDef n ≤ 1
⊢ v.intValuation d < 1

Tactic:
contrapose! this

Result:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this✝ : {v | (valuation K v) ↑d < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ {v | 1 < (valuation K v) k}
hk : (valuation K v) k * v.intValuation d = v.intValuation n
this : 1 ≤ v.intValuation d
⊢ 1 < v.intValuationDef n