harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Fin/Tuple/Take.lean
theorem take_update_of_ge (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) (i : Fin n) (hi : i ≥ m)
    (x : α i) : take m h (update v i x) = take m h v

Proof state:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
j : Fin m
⊢ ↑j ≠ ↑i

Tactic:
exact Nat.ne_of_lt (lt_of_lt_of_le j.isLt hi)

Result:
no goals

Proof state:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
j : Fin m
⊢ ↑(castLE h j) ≠ ↑i

Tactic:
simp only [coe_castLE]

Result:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
j : Fin m
⊢ ↑j ≠ ↑i

Proof state:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
j : Fin m
⊢ castLE h j ≠ i

Tactic:
refine ne_of_val_ne ?_

Result:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
j : Fin m
⊢ ↑(castLE h j) ≠ ↑i

Proof state:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
⊢ take m h (update v i x) = take m h v

Tactic:
ext j

Result:
case h
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
j : Fin m
⊢ take m h (update v i x) j = take m h v j

Proof state:
case h
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
j : Fin m
this : castLE h j ≠ i
⊢ take m h (update v i x) j = take m h v j

Tactic:
simp only [take, update_of_ne this]

Result:
no goals

Proof state:
case h
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
j : Fin m
⊢ take m h (update v i x) j = take m h v j

Tactic:
have : castLE h j ≠ i := by
  refine ne_of_val_ne ?_
  simp only [coe_castLE]
  exact Nat.ne_of_lt (lt_of_lt_of_le j.isLt hi)

Result:
case h
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
j : Fin m
this : castLE h j ≠ i
⊢ take m h (update v i x) j = take m h v j
-- Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
theorem hasInitialChangeDiagram (h : HasColimit F₁) : HasColimit F₂ :=
  ⟨⟨⟨⟨colimit F₁, by aesop_cat, by simp⟩,
    isColimitChangeEmptyCocone C (colimit.isColimit F₁) _ (eqToIso rfl)⟩⟩⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
h : HasColimit F₁
⊢ ∀ ⦃X Y : Discrete PEmpty.{w' + 1}⦄ (f : X ⟶ Y),
    F₂.map f ≫ id (Discrete.casesOn Y fun as => ⋯.elim) =
      id (Discrete.casesOn X fun as => ⋯.elim) ≫ ((Functor.const (Discrete PEmpty.{w' + 1})).obj (colimit F₁)).map f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
h : HasColimit F₁
⊢ (X : Discrete PEmpty.{w' + 1}) → F₂.obj X ⟶ ((Functor.const (Discrete PEmpty.{w' + 1})).obj (colimit F₁)).obj X

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem LinearOrderedRing.orderOf_le_two : orderOf x ≤ 2

Proof state:
case inr
G : Type u_1
inst✝ : LinearOrderedRing G
x : G
h : |x| = 1
⊢ orderOf x ≤ 2

Tactic:
rcases eq_or_eq_neg_of_abs_eq h with (rfl | rfl)

Result:
case inr.inl
G : Type u_1
inst✝ : LinearOrderedRing G
h : |1| = 1
⊢ orderOf 1 ≤ 2

case inr.inr
G : Type u_1
inst✝ : LinearOrderedRing G
h : |(-1)| = 1
⊢ orderOf (-1) ≤ 2

Proof state:
case inr.inl
G : Type u_1
inst✝ : LinearOrderedRing G
h : |1| = 1
⊢ orderOf 1 ≤ 2

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝ : LinearOrderedRing G
x : G
⊢ orderOf x ≤ 2

Tactic:
rcases ne_or_eq |x| 1 with h | h

Result:
case inl
G : Type u_1
inst✝ : LinearOrderedRing G
x : G
h : |x| ≠ 1
⊢ orderOf x ≤ 2

case inr
G : Type u_1
inst✝ : LinearOrderedRing G
x : G
h : |x| = 1
⊢ orderOf x ≤ 2

Proof state:
G : Type u_1
inst✝ : LinearOrderedRing G
h : |(-1)| = 1
⊢ (-1) ^ 2 = 1

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr
G : Type u_1
inst✝ : LinearOrderedRing G
h : |(-1)| = 1
⊢ orderOf (-1) ≤ 2

Tactic:
exact orderOf_le_of_pow_eq_one zero_lt_two (by simp)

Result:
no goals

Proof state:
case inl
G : Type u_1
inst✝ : LinearOrderedRing G
x : G
h : |x| ≠ 1
⊢ orderOf x ≤ 2

Tactic:
simp [orderOf_abs_ne_one h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma inr_opProdIsoCoprod_inv : coprod.inr ≫ (opProdIsoCoprod A B).inv = prod.snd.op

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inr ≫ (opProdIsoCoprod A B).inv = prod.snd.op

Tactic:
rw [Iso.comp_inv_eq, snd_opProdIsoCoprod_hom]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem natSize_to_nat (n) : natSize n = Nat.size n

Proof state:
n : PosNum
⊢ n.natSize = (↑n).size

Tactic:
rw [← size_eq_natSize, size_to_nat]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem toDual_apply_right (i : ι) (m : M) : b.toDual (b i) m = b.repr m i

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i : ι
m : M
⊢ (b.toDual (b i)) m = (b.repr m) i

Tactic:
rw [← b.toDual_linearCombination_right, b.linearCombination_repr]

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
lemma isIso_app (V : Y.Opens) (hV : V ≤ f.opensRange) : IsIso (f.app V)

Proof state:
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
V : Y.Opens
hV : V ≤ f.opensRange
⊢ IsIso (f.app (f ''ᵁ f ⁻¹ᵁ V))

Tactic:
infer_instance

Result:
no goals

Proof state:
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
V : Y.Opens
hV : V ≤ f.opensRange
⊢ IsIso (f.app V)

Tactic:
rw [show V = f ''ᵁ f ⁻¹ᵁ V from Opens.ext (Set.image_preimage_eq_of_subset hV).symm]

Result:
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
V : Y.Opens
hV : V ≤ f.opensRange
⊢ IsIso (f.app (f ''ᵁ f ⁻¹ᵁ V))
-- Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
theorem cokernel_funext {C : Type*} [Category C] [HasZeroMorphisms C] {FC : C → C → Type*}
    {CC : C → Type*} [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC]
    {M N K : C} {f : M ⟶ N} [HasCokernel f] {g h : cokernel f ⟶ K}
    (w : ∀ n : ToType N, g (cokernel.π f n) = h (cokernel.π f n)) : g = h

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
M N K : C
f : M ⟶ N
inst✝ : HasCokernel f
g h : cokernel f ⟶ K
w :
  ∀ (n : ToType N),
    (ConcreteCategory.hom g) ((ConcreteCategory.hom (cokernel.π f)) n) =
      (ConcreteCategory.hom h) ((ConcreteCategory.hom (cokernel.π f)) n)
⊢ g = h

Tactic:
ext x

Result:
case h.w
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
M N K : C
f : M ⟶ N
inst✝ : HasCokernel f
g h : cokernel f ⟶ K
w :
  ∀ (n : ToType N),
    (ConcreteCategory.hom g) ((ConcreteCategory.hom (cokernel.π f)) n) =
      (ConcreteCategory.hom h) ((ConcreteCategory.hom (cokernel.π f)) n)
x : (forget C).obj N
⊢ (coequalizer.π f 0 ≫ g) x = (coequalizer.π f 0 ≫ h) x

Proof state:
case h.w
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
M N K : C
f : M ⟶ N
inst✝ : HasCokernel f
g h : cokernel f ⟶ K
w :
  ∀ (n : ToType N),
    (ConcreteCategory.hom g) ((ConcreteCategory.hom (cokernel.π f)) n) =
      (ConcreteCategory.hom h) ((ConcreteCategory.hom (cokernel.π f)) n)
x : (forget C).obj N
⊢ (coequalizer.π f 0 ≫ g) x = (coequalizer.π f 0 ≫ h) x

Tactic:
simpa using w x

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
lemma tendstoUniformly_congr {F F' : ι → α → β} {f : α → β} (hF : F =ᶠ[p] F') :
    TendstoUniformly F f p ↔ TendstoUniformly F' f p

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
p : Filter ι
F F' : ι → α → β
f : α → β
hF : F =ᶠ[p] F'
HF : ∃ s ∈ p, EqOn F F' s
h : TendstoUniformlyOn F' f p univ
⊢ ∀ᶠ (n : ι) in p, EqOn (F n) (F' n) univ

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
p : Filter ι
F F' : ι → α → β
f : α → β
hF : F =ᶠ[p] F'
⊢ TendstoUniformlyOn F f p univ ↔ TendstoUniformlyOn F' f p univ

Tactic:
have HF := EventuallyEq.exists_mem hF

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
p : Filter ι
F F' : ι → α → β
f : α → β
hF : F =ᶠ[p] F'
HF : ∃ s ∈ p, EqOn F F' s
⊢ TendstoUniformlyOn F f p univ ↔ TendstoUniformlyOn F' f p univ

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
p : Filter ι
F F' : ι → α → β
f : α → β
hF : F =ᶠ[p] F'
HF : ∃ s ∈ p, EqOn F F' s
h : TendstoUniformlyOn F f p univ
⊢ ∀ᶠ (n : ι) in p, EqOn (F n) (F' n) univ

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
p : Filter ι
F F' : ι → α → β
f : α → β
hF : F =ᶠ[p] F'
⊢ TendstoUniformly F f p ↔ TendstoUniformly F' f p

Tactic:
simp_rw [← tendstoUniformlyOn_univ] at *

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
p : Filter ι
F F' : ι → α → β
f : α → β
hF : F =ᶠ[p] F'
⊢ TendstoUniformlyOn F f p univ ↔ TendstoUniformlyOn F' f p univ

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
p : Filter ι
F F' : ι → α → β
f : α → β
hF : F =ᶠ[p] F'
HF : ∃ s ∈ p, EqOn F F' s
h : TendstoUniformlyOn F' f p univ
⊢ ∀ᶠ (n : ι) in p, EqOn (F' n) (F n) univ

Tactic:
simp_rw [eqOn_comm]

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
p : Filter ι
F F' : ι → α → β
f : α → β
hF : F =ᶠ[p] F'
HF : ∃ s ∈ p, EqOn F F' s
h : TendstoUniformlyOn F' f p univ
⊢ ∀ᶠ (n : ι) in p, EqOn (F n) (F' n) univ

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
p : Filter ι
F F' : ι → α → β
f : α → β
hF : F =ᶠ[p] F'
HF : ∃ s ∈ p, EqOn F F' s
⊢ TendstoUniformlyOn F f p univ ↔ TendstoUniformlyOn F' f p univ

Tactic:
exact ⟨fun h => h.congr (by aesop), fun h => h.congr (by simp_rw [eqOn_comm]; aesop)⟩

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/SlashActions.lean
theorem slash_action_eq'_iff (k : ℤ) (f : ℍ → ℂ) (γ : SL(2, ℤ)) (z : ℍ) :
    (f ∣[k] γ) z = f z ↔ f (γ • z) = ((γ 1 0 : ℂ) * z + (γ 1 1 : ℂ)) ^ k * f z

Proof state:
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ (f ∣[k] γ) z = f z ↔ f (γ • z) = (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * f z

Tactic:
simp only [SL_slash, slash_def, ModularForm.slash]

Result:
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ f (↑γ • z) * ↑(↑↑↑γ).det ^ (k - 1) * denom (↑γ) z ^ (-k) = f z ↔ f (γ • z) = (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * f z

Proof state:
case convert_4
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k ≠ 0

Tactic:
convert zpow_ne_zero k (denom_ne_zero γ z)

Result:
no goals

Proof state:
case h.e'_1.h.e'_2
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ f (↑γ • z) * ↑(↑↑↑γ).det ^ (k - 1) * denom (↑γ) z ^ (-k) = ((↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k)⁻¹ * f (γ • z)

Tactic:
rw [mul_comm]

Result:
case h.e'_1.h.e'_2
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ denom (↑γ) z ^ (-k) * (f (↑γ • z) * ↑(↑↑↑γ).det ^ (k - 1)) = ((↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k)⁻¹ * f (γ • z)

Proof state:
case h.e'_1.h.e'_2
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ denom (↑γ) z ^ (-k) * (f (↑γ • z) * ↑(↑↑↑γ).det ^ (k - 1)) = ((↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k)⁻¹ * f (γ • z)

Tactic:
simp only [denom, zpow_neg, det_coe, ofReal_one, one_zpow, mul_one,
  sl_moeb]

Result:
case h.e'_1.h.e'_2
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ ((↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k)⁻¹ * f (↑γ • z) = ((↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k)⁻¹ * f (↑γ • z)

Proof state:
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ f (↑γ • z) * ↑(↑↑↑γ).det ^ (k - 1) * denom (↑γ) z ^ (-k) = f z ↔ f (γ • z) = (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * f z

Tactic:
convert inv_mul_eq_iff_eq_mul₀ (G₀ := ℂ) _ using 2

Result:
case h.e'_1.h.e'_2
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ f (↑γ • z) * ↑(↑↑↑γ).det ^ (k - 1) * denom (↑γ) z ^ (-k) = ((↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k)⁻¹ * f (γ • z)

case convert_4
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k ≠ 0

Proof state:
case h.e'_1.h.e'_2
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ ((↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k)⁻¹ * f (↑γ • z) = ((↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k)⁻¹ * f (↑γ • z)

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
theorem dist_le_Ico_sum_dist (f : ℕ → α) {m n} (h : m ≤ n) :
    dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))

Proof state:
case base
α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n : ℕ
⊢ dist (f m) (f m) ≤ ∑ i ∈ Finset.Ico m m, dist (f i) (f (i + 1))

Tactic:
rw [Finset.Ico_self, Finset.sum_empty, dist_self]

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1)) + dist (f n) (f (n + 1)) =
    ∑ i ∈ Finset.Ico m (n + 1), dist (f i) (f (i + 1))

Tactic:
rw [Nat.Ico_succ_right_eq_insert_Ico hle, Finset.sum_insert, add_comm]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n : ℕ
h : m ≤ n
⊢ dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))

Tactic:
induction n, h using Nat.le_induction with
| base => rw [Finset.Ico_self, Finset.sum_empty, dist_self]
| succ n hle ihn =>
  calc
    dist (f m) (f (n + 1)) ≤ dist (f m) (f n) + dist (f n) (f (n + 1)) := dist_triangle _ _ _
    _ ≤ (∑ i ∈ Finset.Ico m n, _) + _ := add_le_add ihn le_rfl
    _ = ∑ i ∈ Finset.Ico m (n + 1), _ := by
    { rw [Nat.Ico_succ_right_eq_insert_Ico hle, Finset.sum_insert, add_comm]; simp }

Result:
no goals

Proof state:
case succ
α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ dist (f m) (f (n + 1)) ≤ ∑ i ∈ Finset.Ico m (n + 1), dist (f i) (f (i + 1))

Tactic:
calc
  dist (f m) (f (n + 1)) ≤ dist (f m) (f n) + dist (f n) (f (n + 1)) := dist_triangle _ _ _
  _ ≤ (∑ i ∈ Finset.Ico m n, _) + _ := add_le_add ihn le_rfl
  _ = ∑ i ∈ Finset.Ico m (n + 1), _ := by
  { rw [Nat.Ico_succ_right_eq_insert_Ico hle, Finset.sum_insert, add_comm]; simp }

Result:
no goals
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem coprime_classification' {x y z : ℤ} (h : PythagoreanTriple x y z)
    (h_coprime : Int.gcd x y = 1) (h_parity : x % 2 = 1) (h_pos : 0 < z) :
    ∃ m n,
      x = m ^ 2 - n ^ 2 ∧
        y = 2 * m * n ∧
          z = m ^ 2 + n ^ 2 ∧
            Int.gcd m n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m

Proof state:
case h.inl.right.inr
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_neg : z = -(m ^ 2 + n ^ 2)
⊢ 0 < z → False

Tactic:
rw [h_neg]

Result:
case h.inl.right.inr
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_neg : z = -(m ^ 2 + n ^ 2)
⊢ 0 < -(m ^ 2 + n ^ 2) → False

Proof state:
case h.inl.right.inr
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_neg : z = -(m ^ 2 + n ^ 2)
⊢ z = m ^ 2 + n ^ 2 ∧ (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

Tactic:
exfalso

Result:
case h.inl.right.inr
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_neg : z = -(m ^ 2 + n ^ 2)
⊢ False

Proof state:
case h.inl
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
⊢ x = m ^ 2 - n ^ 2 ∧
    y = 2 * -m * -n ∧
      z = m ^ 2 + n ^ 2 ∧ (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

Tactic:
apply And.intro h_odd.1

Result:
case h.inl
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
⊢ y = 2 * -m * -n ∧ z = m ^ 2 + n ^ 2 ∧ (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem!_eq_getElem?_getD [Inhabited α] (l : List α) (i : Nat) :
    l[i]! = (l[i]?).getD (default : α)

Proof state:
α : Type u_1
inst✝ : Inhabited α
l : List α
i : Nat
⊢ (match none with
    | some e => e
    | none => default) =
    none.getD default

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Inhabited α
l : List α
i : Nat
⊢ (match l[i]? with
    | some e => e
    | none => default) =
    l[i]?.getD default

Tactic:
match l[i]? with
| some _ => simp
| none => simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Inhabited α
l : List α
i : Nat
⊢ l[i]! = l[i]?.getD default

Tactic:
simp only [getElem!_def]

Result:
α : Type u_1
inst✝ : Inhabited α
l : List α
i : Nat
⊢ (match l[i]? with
    | some e => e
    | none => default) =
    l[i]?.getD default

Proof state:
α : Type u_1
inst✝ : Inhabited α
l : List α
i : Nat
val✝ : α
⊢ (match some val✝ with
    | some e => e
    | none => default) =
    (some val✝).getD default

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_const_mul_Ioi_zero {k : Type*} [LinearOrderedField k] {x : k} (hx : 0 < x) :
    (fun y => x * y) '' Ioi (0 : k) = Ioi 0

Proof state:
k : Type u_2
inst✝ : LinearOrderedField k
x : k
hx : 0 < x
this : ⇑(Units.mk0 x ⋯).mulLeft '' Ioi 0 = ⇑(Equiv.symm (Units.mk0 x ⋯).mulLeft) ⁻¹' Ioi 0
⊢ (fun y => x * y) '' Ioi 0 = Ioi 0

Tactic:
simp at this

Result:
k : Type u_2
inst✝ : LinearOrderedField k
x : k
hx : 0 < x
this : (fun a => x * a) '' Ioi 0 = (fun x_1 => x⁻¹ * x_1) ⁻¹' Ioi 0
⊢ (fun y => x * y) '' Ioi 0 = Ioi 0

Proof state:
k : Type u_2
inst✝ : LinearOrderedField k
x : k
hx : 0 < x
⊢ (fun y => x * y) '' Ioi 0 = Ioi 0

Tactic:
have := (Units.mk0 x hx.ne').mulLeft.image_eq_preimage (Ioi 0)

Result:
k : Type u_2
inst✝ : LinearOrderedField k
x : k
hx : 0 < x
this : ⇑(Units.mk0 x ⋯).mulLeft '' Ioi 0 = ⇑(Equiv.symm (Units.mk0 x ⋯).mulLeft) ⁻¹' Ioi 0
⊢ (fun y => x * y) '' Ioi 0 = Ioi 0

Proof state:
k : Type u_2
inst✝ : LinearOrderedField k
x : k
hx : 0 < x
this : (fun a => x * a) '' Ioi 0 = (fun x_1 => x⁻¹ * x_1) ⁻¹' Ioi 0
⊢ (fun y => x * y) '' Ioi 0 = Ioi 0

Tactic:
simp_all

Result:
no goals
-- Mathlib/Order/Filter/Finite.lean
theorem biInter_mem {β : Type v} {s : β → Set α} {is : Set β} (hf : is.Finite) :
    (⋂ i ∈ is, s i) ∈ f ↔ ∀ i ∈ is, s i ∈ f :=
  Finite.induction_on _ hf (by simp) fun _ _ hs => by simp [hs]

Proof state:
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Finite
⊢ ⋂ i ∈ ∅, s i ∈ f ↔ ∀ i ∈ ∅, s i ∈ f

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Finite
a✝ : β
s✝ : Set β
x✝¹ : a✝ ∉ s✝
x✝ : s✝.Finite
hs : ⋂ i ∈ s✝, s i ∈ f ↔ ∀ i ∈ s✝, s i ∈ f
⊢ ⋂ i ∈ insert a✝ s✝, s i ∈ f ↔ ∀ i ∈ insert a✝ s✝, s i ∈ f

Tactic:
simp [hs]

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
/-- Universe polymorphic version of the reverse implication of `mem_convexHull_iff_exists_fintype`.
-/
lemma mem_convexHull_of_exists_fintype {s : Set E} {x : E} [Fintype ι] (w : ι → R) (z : ι → E)
    (hw₀ : ∀ i, 0 ≤ w i) (hw₁ : ∑ i, w i = 1) (hz : ∀ i, z i ∈ s) (hx : ∑ i, w i • z i = x) :
    x ∈ convexHull R s

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
s : Set E
x : E
inst✝ : Fintype ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
hz : ∀ (i : ι), z i ∈ s
hx : ∑ i : ι, w i • z i = x
⊢ Finset.univ.centerMass w z ∈ (convexHull R) s

Tactic:
exact centerMass_mem_convexHull _ (by simpa using hw₀) (by simp [hw₁]) (by simpa using hz)

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
s : Set E
x : E
inst✝ : Fintype ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
hz : ∀ (i : ι), z i ∈ s
hx : ∑ i : ι, w i • z i = x
⊢ ∀ i ∈ Finset.univ, z i ∈ s

Tactic:
simpa using hz

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
s : Set E
x : E
inst✝ : Fintype ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
hz : ∀ (i : ι), z i ∈ s
hx : ∑ i : ι, w i • z i = x
⊢ 0 < ∑ i : ι, w i

Tactic:
simp [hw₁]

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
s : Set E
x : E
inst✝ : Fintype ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
hz : ∀ (i : ι), z i ∈ s
hx : ∑ i : ι, w i • z i = x
⊢ x ∈ (convexHull R) s

Tactic:
rw [← hx, ← centerMass_eq_of_sum_1 _ _ hw₁]

Result:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
s : Set E
x : E
inst✝ : Fintype ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
hz : ∀ (i : ι), z i ∈ s
hx : ∑ i : ι, w i • z i = x
⊢ Finset.univ.centerMass w z ∈ (convexHull R) s

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
s : Set E
x : E
inst✝ : Fintype ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
hz : ∀ (i : ι), z i ∈ s
hx : ∑ i : ι, w i • z i = x
⊢ ∀ i ∈ Finset.univ, 0 ≤ w i

Tactic:
simpa using hw₀

Result:
no goals