harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_pi_div_thirty_two : cos (π / 32) = √(2 + √(2 + √(2 + √2))) / 2

Proof state:
⊢ cos (π / 32) = √(2 + √(2 + √(2 + √2))) / 2

Tactic:
trans cos (π / 2 ^ 5)

Result:
⊢ cos (π / 32) = cos (π / 2 ^ 5)


⊢ cos (π / 2 ^ 5) = √(2 + √(2 + √(2 + √2))) / 2

Proof state:
⊢ cos (π / 32) = cos (π / 2 ^ 5)

Tactic:
congr

Result:
case e_x.e_a

⊢ 32 = 2 ^ 5

Proof state:
⊢ cos (π / 2 ^ 5) = √(2 + √(2 + √(2 + √2))) / 2

Tactic:
simp

Result:
no goals

Proof state:
case e_x.e_a

⊢ 32 = 2 ^ 5

Tactic:
norm_num

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem add_def' (a b : Rat) : a + b = mkRat (a.num * b.den + b.num * a.den) (a.den * b.den)

Proof state:
a b : Rat
⊢ a + b = mkRat (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)

Tactic:
rw [add_def, normalize_eq_mkRat]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Expect.lean
lemma expect_le (hs : s.Nonempty) (h : ∀ x ∈ s, f x ≤ a) : 𝔼 i ∈ s, f i ≤ a :=
  (inv_smul_le_iff_of_pos <| mod_cast hs.card_pos).2 <| by
    rw [Nat.cast_smul_eq_nsmul]; exact sum_le_card_nsmul _ _ _ h

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : OrderedAddCommMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, f x ≤ a
⊢ ∑ i ∈ s, (fun i => f i) i ≤ #s • a

Tactic:
exact sum_le_card_nsmul _ _ _ h

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : OrderedAddCommMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, f x ≤ a
⊢ ∑ i ∈ s, (fun i => f i) i ≤ ↑(#s) • a

Tactic:
rw [Nat.cast_smul_eq_nsmul]

Result:
ι : Type u_1
α : Type u_2
inst✝² : OrderedAddCommMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, f x ≤ a
⊢ ∑ i ∈ s, (fun i => f i) i ≤ #s • a
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem trans_refl_restr' (s : Set β) :
    e.trans ((PartialEquiv.refl β).restr s) = e.restr (e.source ∩ e ⁻¹' s) :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) <| by
    simp only [trans_source, restr_source, refl_source, univ_inter]
    rw [← inter_assoc, inter_self]

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
⊢ e.source ∩ ↑e ⁻¹' s = e.source ∩ (e.source ∩ ↑e ⁻¹' s)

Tactic:
rw [← inter_assoc, inter_self]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
⊢ (e.trans ((PartialEquiv.refl β).restr s)).source = (e.restr (e.source ∩ ↑e ⁻¹' s)).source

Tactic:
simp only [trans_source, restr_source, refl_source, univ_inter]

Result:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
⊢ e.source ∩ ↑e ⁻¹' s = e.source ∩ (e.source ∩ ↑e ⁻¹' s)
-- Mathlib/Topology/Instances/Rat.lean
theorem uniformContinuous_add : UniformContinuous fun p : ℚ × ℚ => p.1 + p.2 :=
  Rat.isUniformEmbedding_coe_real.isUniformInducing.uniformContinuous_iff.2 <| by
    simp only [Function.comp_def, Rat.cast_add]
    exact Real.uniformContinuous_add.comp
      (Rat.uniformContinuous_coe_real.prodMap Rat.uniformContinuous_coe_real)

Proof state:
⊢ UniformContinuous fun x => ↑x.1 + ↑x.2

Tactic:
exact Real.uniformContinuous_add.comp
  (Rat.uniformContinuous_coe_real.prodMap Rat.uniformContinuous_coe_real)

Result:
no goals

Proof state:
⊢ UniformContinuous (Rat.cast ∘ fun p => p.1 + p.2)

Tactic:
simp only [Function.comp_def, Rat.cast_add]

Result:
⊢ UniformContinuous fun x => ↑x.1 + ↑x.2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem elim_const_const (c : γ) :
    Sum.elim (const _ c : α → γ) (const _ c : β → γ) = const _ c

Proof state:
case h
γ : Sort u_1
α : Type u_2
β : Type u_3
c : γ
⊢ ∀ (x : α ⊕ β), Sum.elim (const α c) (const β c) x = const (α ⊕ β) c x

Tactic:
rintro (_ | _) <;> rfl

Result:
no goals

Proof state:
γ : Sort u_1
α : Type u_2
β : Type u_3
c : γ
⊢ Sum.elim (const α c) (const β c) = const (α ⊕ β) c

Tactic:
apply funext

Result:
case h
γ : Sort u_1
α : Type u_2
β : Type u_3
c : γ
⊢ ∀ (x : α ⊕ β), Sum.elim (const α c) (const β c) x = const (α ⊕ β) c x
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem support_finset_sum [DecidableEq β] [AddCommMonoid M] {s : Finset α} {f : α → β →₀ M} :
    (Finset.sum s f).support ⊆ s.biUnion fun x => (f x).support

Proof state:
α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
s : Finset α
f : α → β →₀ M
⊢ (s.sum f).support ⊆ s.biUnion fun x => (f x).support

Tactic:
rw [← Finset.sup_eq_biUnion]

Result:
α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
s : Finset α
f : α → β →₀ M
⊢ (s.sum f).support ⊆ s.sup fun x => (f x).support

Proof state:
case h₂
α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
f : α → β →₀ M
a✝ : α
s✝ : Finset α
h✝ : a✝ ∉ s✝
ih : (s✝.sum f).support ⊆ s✝.sup fun x => (f x).support
⊢ ((Finset.cons a✝ s✝ h✝).sum f).support ⊆ (Finset.cons a✝ s✝ h✝).sup fun x => (f x).support

Tactic:
rw [Finset.sum_cons, Finset.sup_cons]

Result:
case h₂
α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
f : α → β →₀ M
a✝ : α
s✝ : Finset α
h✝ : a✝ ∉ s✝
ih : (s✝.sum f).support ⊆ s✝.sup fun x => (f x).support
⊢ (f a✝ + ∑ x ∈ s✝, f x).support ⊆ (f a✝).support ⊔ s✝.sup fun x => (f x).support

Proof state:
case h₁
α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
f : α → β →₀ M
⊢ (∅.sum f).support ⊆ ∅.sup fun x => (f x).support

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
s : Finset α
f : α → β →₀ M
⊢ (s.sum f).support ⊆ s.sup fun x => (f x).support

Tactic:
induction s using Finset.cons_induction_on with
| h₁ => rfl
| h₂ _ ih =>
  rw [Finset.sum_cons, Finset.sup_cons]
  exact support_add.trans (Finset.union_subset_union (Finset.Subset.refl _) ih)

Result:
no goals

Proof state:
case h₂
α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
f : α → β →₀ M
a✝ : α
s✝ : Finset α
h✝ : a✝ ∉ s✝
ih : (s✝.sum f).support ⊆ s✝.sup fun x => (f x).support
⊢ (f a✝ + ∑ x ∈ s✝, f x).support ⊆ (f a✝).support ⊔ s✝.sup fun x => (f x).support

Tactic:
exact support_add.trans (Finset.union_subset_union (Finset.Subset.refl _) ih)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Arsinh.lean
theorem arsinh_neg (x : ℝ) : arsinh (-x) = -arsinh x

Proof state:
case h
x : ℝ
⊢ (-x + √(1 + (-x) ^ 2)) * (x + √(1 + x ^ 2)) = 1

Tactic:
rw [neg_sq, neg_add_eq_sub, add_comm x, mul_comm, ← sq_sub_sq, sq_sqrt, add_sub_cancel_right]

Result:
case h
x : ℝ
⊢ 0 ≤ 1 + x ^ 2

Proof state:
x : ℝ
⊢ -x + √(1 + (-x) ^ 2) = (x + √(1 + x ^ 2))⁻¹

Tactic:
apply eq_inv_of_mul_eq_one_left

Result:
case h
x : ℝ
⊢ (-x + √(1 + (-x) ^ 2)) * (x + √(1 + x ^ 2)) = 1

Proof state:
x : ℝ
⊢ arsinh (-x) = -arsinh x

Tactic:
rw [← exp_eq_exp, exp_arsinh, exp_neg, exp_arsinh]

Result:
x : ℝ
⊢ -x + √(1 + (-x) ^ 2) = (x + √(1 + x ^ 2))⁻¹

Proof state:
case h
x : ℝ
⊢ 0 ≤ 1 + x ^ 2

Tactic:
exact add_nonneg zero_le_one (sq_nonneg _)

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIxxMod_iff (x₁ x₂ x₃ : α) : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ↔
    toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
⊢ toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p

Tactic:
rw [toIcoMod_eq_sub, toIocMod_eq_sub _ x₁, add_le_add_iff_right, ← neg_sub x₁ x₃, toIocMod_neg,
  neg_zero, le_sub_iff_add_le]

Result:
no goals
-- Mathlib/Algebra/Divisibility/Units.lean
theorem IsRelPrime.mul_dvd_of_right_isPrimal (H : IsRelPrime x y) (H1 : x ∣ z) (H2 : y ∣ z)
    (hy : IsPrimal y) : x * y ∣ z

Proof state:
case intro
α : Type u_1
inst✝ : CommMonoid α
x y : α
H : IsRelPrime x y
hy : IsPrimal y
w : α
H2 : y ∣ x * w
⊢ x * y ∣ x * w

Tactic:
exact mul_dvd_mul_left x (H.symm.dvd_of_dvd_mul_left_of_isPrimal H2 hy)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
H : IsRelPrime x y
H1 : x ∣ z
H2 : y ∣ z
hy : IsPrimal y
⊢ x * y ∣ z

Tactic:
obtain ⟨w, rfl⟩ := H1

Result:
case intro
α : Type u_1
inst✝ : CommMonoid α
x y : α
H : IsRelPrime x y
hy : IsPrimal y
w : α
H2 : y ∣ x * w
⊢ x * y ∣ x * w
-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem conjugateEquiv_counit_symm (α : R₁ ⟶ R₂) (d : D) :
    L₂.map (α.app _) ≫ adj₂.counit.app d =
      ((conjugateEquiv adj₁ adj₂).symm α).app _ ≫ adj₁.counit.app d

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
d : D
⊢ L₂.map (((conjugateEquiv adj₁ adj₂).toFun ((conjugateEquiv adj₁ adj₂).invFun α)).app d) ≫ adj₂.counit.app d =
    ((conjugateEquiv adj₁ adj₂).symm α).app (R₁.obj d) ≫ adj₁.counit.app d

Tactic:
exact (conjugateEquiv_counit adj₁ adj₂ ((conjugateEquiv adj₁ adj₂).symm α) d)

Result:
no goals

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
d : D
⊢ L₂.map (α.app d) ≫ adj₂.counit.app d = ((conjugateEquiv adj₁ adj₂).symm α).app (R₁.obj d) ≫ adj₁.counit.app d

Tactic:
conv_lhs => rw [← (conjugateEquiv adj₁ adj₂).right_inv α]

Result:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
d : D
⊢ L₂.map (((conjugateEquiv adj₁ adj₂).toFun ((conjugateEquiv adj₁ adj₂).invFun α)).app d) ≫ adj₂.counit.app d =
    ((conjugateEquiv adj₁ adj₂).symm α).app (R₁.obj d) ≫ adj₁.counit.app d
-- Mathlib/Data/Sign.lean
theorem exists_signed_sum_aux {α : Type u_1} [DecidableEq α] (s : Finset α) (f : α → ℤ) :
    ∃ (β : Type u_1) (t : Finset β) (sgn : β → SignType) (g : β → α),
      (∀ b, g b ∈ s) ∧
        (#t = ∑ a ∈ s, (f a).natAbs) ∧
          ∀ a ∈ s, (∑ b ∈ t, if g b = a then (sgn b : ℤ) else 0) = f a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ ∃ β t sgn g,
    (∀ (b : β), g b ∈ s) ∧ #t = ∑ a ∈ s, (f a).natAbs ∧ ∀ a ∈ s, (∑ b ∈ t, if g b = a then ↑(sgn b) else 0) = f a

Tactic:
refine
  ⟨(Σ _ : { x // x ∈ s }, ℕ), Finset.univ.sigma fun a => range (f a).natAbs,
    fun a => sign (f a.1), fun a => a.1, fun a => a.1.2, ?_, ?_⟩

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ #(univ.sigma fun a => range (f ↑a).natAbs) = ∑ a ∈ s, (f a).natAbs

case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ ∀ a ∈ s,
    (∑ b ∈ univ.sigma fun a => range (f ↑a).natAbs,
        if (fun a => ↑a.fst) b = a then ↑((fun a => sign (f ↑a.fst)) b) else 0) =
      f a

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ #(univ.sigma fun a => range (f ↑a).natAbs) = ∑ a ∈ s, (f a).natAbs

Tactic:
simp [sum_attach (f := fun a => (f a).natAbs)]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ ∀ a ∈ s,
    (∑ b ∈ univ.sigma fun a => range (f ↑a).natAbs,
        if (fun a => ↑a.fst) b = a then ↑((fun a => sign (f ↑a.fst)) b) else 0) =
      f a

Tactic:
intro x hx

Result:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
x : α
hx : x ∈ s
⊢ (∑ b ∈ univ.sigma fun a => range (f ↑a).natAbs,
      if (fun a => ↑a.fst) b = x then ↑((fun a => sign (f ↑a.fst)) b) else 0) =
    f x

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
x : α
hx : x ∈ s
⊢ (∑ b ∈ univ.sigma fun a => range (f ↑a).natAbs,
      if (fun a => ↑a.fst) b = x then ↑((fun a => sign (f ↑a.fst)) b) else 0) =
    f x

Tactic:
simp [sum_sigma, hx, ← Int.sign_eq_sign, Int.sign_mul_abs, mul_comm |f _|,
  sum_attach (s := s) (f := fun y => if y = x then f y else 0)]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem prod_Ico_succ_top {a b : ℕ} (hab : a ≤ b) (f : ℕ → M) :
    (∏ k ∈ Ico a (b + 1), f k) = (∏ k ∈ Ico a b, f k) * f b

Proof state:
M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
hab : a ≤ b
f : ℕ → M
⊢ ∏ k ∈ Ico a (b + 1), f k = (∏ k ∈ Ico a b, f k) * f b

Tactic:
rw [Nat.Ico_succ_right_eq_insert_Ico hab, prod_insert right_not_mem_Ico, mul_comm]

Result:
no goals
-- Mathlib/Topology/StoneCech.lean
theorem stoneCechExtend_extends : stoneCechExtend hg ∘ stoneCechUnit = g

Proof state:
case h
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
g : α → β
hg : Continuous g
inst✝ : CompactSpace β
x : α
⊢ preStoneCechExtend hg (preStoneCechUnit x) = g x

Tactic:
apply congrFun (preStoneCechExtend_extends hg)

Result:
no goals

Proof state:
case h
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
g : α → β
hg : Continuous g
inst✝ : CompactSpace β
x : α
⊢ (stoneCechExtend hg ∘ stoneCechUnit) x = g x

Tactic:
rw [stoneCechExtend, Function.comp_apply, stoneCechUnit, t2Quotient.lift_mk]

Result:
case h
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
g : α → β
hg : Continuous g
inst✝ : CompactSpace β
x : α
⊢ preStoneCechExtend hg (preStoneCechUnit x) = g x

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
g : α → β
hg : Continuous g
inst✝ : CompactSpace β
⊢ stoneCechExtend hg ∘ stoneCechUnit = g

Tactic:
ext x

Result:
case h
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
g : α → β
hg : Continuous g
inst✝ : CompactSpace β
x : α
⊢ (stoneCechExtend hg ∘ stoneCechUnit) x = g x
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Pairwise.lean
theorem pairwise_iff_get : Pairwise R l ↔ ∀ (i j) (_hij : i < j), R (get l i) (get l j)

Proof state:
case mpr
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)
⊢ ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]

Tactic:
intros i j hi hj h'

Result:
case mpr
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)
i j : Nat
hi : i < l.length
hj : j < l.length
h' : i < j
⊢ R l[i] l[j]

Proof state:
case mp
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
⊢ ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)

Tactic:
intros i j h'

Result:
case mp
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
i j : Fin l.length
h' : i < j
⊢ R (l.get i) (l.get j)

Proof state:
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
⊢ (∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]) ↔
    ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)

Tactic:
constructor <;> intro h

Result:
case mp
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
⊢ ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)

case mpr
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)
⊢ ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]

Proof state:
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
⊢ Pairwise R l ↔ ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)

Tactic:
rw [pairwise_iff_getElem]

Result:
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
⊢ (∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]) ↔
    ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)

Proof state:
case mp
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
i j : Fin l.length
h' : i < j
⊢ R (l.get i) (l.get j)

Tactic:
exact h _ _ _ _ h'

Result:
no goals

Proof state:
case mpr
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)
i j : Nat
hi : i < l.length
hj : j < l.length
h' : i < j
⊢ R l[i] l[j]

Tactic:
exact h ⟨i, hi⟩ ⟨j, hj⟩ h'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_cons_succ {l : List α} : (a::l)[i+1]? = l[i]?

Proof state:
α : Type u_1
a : α
i : Nat
l : List α
⊢ (a :: l)[i + 1]? = l[i]?

Tactic:
simp only [← get?_eq_getElem?]

Result:
α : Type u_1
a : α
i : Nat
l : List α
⊢ (a :: l).get? (i + 1) = l.get? i

Proof state:
α : Type u_1
a : α
i : Nat
l : List α
⊢ (a :: l).get? (i + 1) = l.get? i

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem descPochhammer_eval_zero {n : ℕ} :
    (descPochhammer R n).eval 0 = if n = 0 then 1 else 0

Proof state:
case zero
R : Type u
inst✝ : Ring R
⊢ eval 0 (descPochhammer R 0) = if 0 = 0 then 1 else 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ eval 0 (descPochhammer R n) = if n = 0 then 1 else 0

Tactic:
cases n

Result:
case zero
R : Type u
inst✝ : Ring R
⊢ eval 0 (descPochhammer R 0) = if 0 = 0 then 1 else 0

case succ
R : Type u
inst✝ : Ring R
n✝ : ℕ
⊢ eval 0 (descPochhammer R (n✝ + 1)) = if n✝ + 1 = 0 then 1 else 0

Proof state:
case succ
R : Type u
inst✝ : Ring R
n✝ : ℕ
⊢ eval 0 (descPochhammer R (n✝ + 1)) = if n✝ + 1 = 0 then 1 else 0

Tactic:
simp [X_mul, Nat.succ_ne_zero, descPochhammer_succ_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zipWith_mkArray {a : α} {b : β} {m n : Nat} :
    zipWith f (mkArray m a) (mkArray n b) = mkArray (min m n) (f a b)

Proof state:
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
a : α
b : β
m n : Nat
⊢ zipWith f (mkArray m a) (mkArray n b) = mkArray (min m n) (f a b)

Tactic:
simp [← List.toArray_replicate]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem algebraMap_apply (a : K) : algebraMap K K⸨X⸩ a = HahnSeries.C a

Proof state:
K : Type u_2
inst✝ : Field K
a : K
⊢ (algebraMap K K⸨X⸩) a = HahnSeries.C a

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Sized.rotateL_size {l x r} (hm : Sized r) :
    size (@Ordnode.rotateL α l x r) = size l + size r + 1

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hm : r.Sized
⊢ (l.rotateL x r).size = l.size + r.size + 1

Tactic:
cases r <;> simp [Ordnode.rotateL]

Result:
case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).size = l.size + size✝ + 1

Proof state:
case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).size = l.size + size✝ + 1

Tactic:
simp only [hm.1]

Result:
case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).size =
    l.size + (l✝.size + r✝.size + 1) + 1

Proof state:
case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).size =
    l.size + (l✝.size + r✝.size + 1) + 1

Tactic:
split_ifs <;> simp [node3L_size, node4L_size hm.2.1] <;> abel

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem ne_of_not_mem_push {a b : α} {l : Array α} (h : a ∉ l.push b) : a ≠ b

Proof state:
α : Type u_1
a b : α
l : Array α
h : ¬a ∈ l ∧ ¬a = b
⊢ a ≠ b

Tactic:
exact h.2

Result:
no goals

Proof state:
α : Type u_1
a b : α
l : Array α
h : ¬a ∈ l.push b
⊢ a ≠ b

Tactic:
simp only [mem_push, not_or] at h

Result:
α : Type u_1
a b : α
l : Array α
h : ¬a ∈ l ∧ ¬a = b
⊢ a ≠ b
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_ne_zero : exp x ≠ 0 := fun h =>
  exp_ne_zero x <| by rw [exp, ← ofReal_inj] at h; simp_all

Proof state:
x : ℝ
h : rexp x = 0
⊢ cexp ↑x = 0

Tactic:
rw [exp, ← ofReal_inj] at h

Result:
x : ℝ
h : ↑(cexp ↑x).re = ↑0
⊢ cexp ↑x = 0

Proof state:
x : ℝ
h : ↑(cexp ↑x).re = ↑0
⊢ cexp ↑x = 0

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem Coprime.coprime_dvd_left (H1 : m ∣ k) (H2 : Coprime k n) : Coprime m n

Proof state:
case H
m k n : Nat
H1 : m ∣ k
H2 : k.gcd n = 1
this : m.gcd n ∣ k.gcd n
⊢ m.gcd n ∣ 1

Tactic:
rwa [← H2]

Result:
no goals

Proof state:
case H
m k n : Nat
H1 : m ∣ k
H2 : k.gcd n = 1
⊢ m.gcd n ∣ 1

Tactic:
have := Nat.gcd_dvd_gcd_of_dvd_left n H1

Result:
case H
m k n : Nat
H1 : m ∣ k
H2 : k.gcd n = 1
this : m.gcd n ∣ k.gcd n
⊢ m.gcd n ∣ 1

Proof state:
case H
m k n : Nat
H1 : m ∣ k
H2 : k.Coprime n
⊢ m.gcd n ∣ 1

Tactic:
rw [Coprime] at H2

Result:
case H
m k n : Nat
H1 : m ∣ k
H2 : k.gcd n = 1
⊢ m.gcd n ∣ 1

Proof state:
m k n : Nat
H1 : m ∣ k
H2 : k.Coprime n
⊢ m.Coprime n

Tactic:
apply eq_one_of_dvd_one

Result:
case H
m k n : Nat
H1 : m ∣ k
H2 : k.Coprime n
⊢ m.gcd n ∣ 1
-- Mathlib/Data/Real/EReal.lean
protected lemma «exists» {p : EReal → Prop} : (∃ r, p r) ↔ p ⊥ ∨ p ⊤ ∨ ∃ r : ℝ, p r where
  mp

Proof state:
p : EReal → Prop
⊢ (∃ r, p r) → p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r

Tactic:
rintro ⟨r, hr⟩

Result:
case intro
p : EReal → Prop
r : EReal
hr : p r
⊢ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r

Proof state:
case intro
p : EReal → Prop
r : EReal
hr : p r
⊢ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r

Tactic:
cases r <;> aesop

Result:
no goals

Proof state:
p : EReal → Prop
⊢ (p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r) → ∃ r, p r

Tactic:
rintro (h | h | ⟨r, hr⟩) <;> exact ⟨_, ‹_›⟩

Result:
no goals
-- Mathlib/Order/Filter/Subsingleton.lean
theorem subsingleton_iff_bot_or_pure : l.Subsingleton ↔ l = ⊥ ∨ ∃ a, l = pure a

Proof state:
α : Type u_1
l : Filter α
⊢ l.Subsingleton ↔ l = ⊥ ∨ ∃ a, l = pure a

Tactic:
refine ⟨fun hl ↦ ?_, ?_⟩

Result:
case refine_1
α : Type u_1
l : Filter α
hl : l.Subsingleton
⊢ l = ⊥ ∨ ∃ a, l = pure a

case refine_2
α : Type u_1
l : Filter α
⊢ (l = ⊥ ∨ ∃ a, l = pure a) → l.Subsingleton

Proof state:
case refine_2
α : Type u_1
l : Filter α
⊢ (l = ⊥ ∨ ∃ a, l = pure a) → l.Subsingleton

Tactic:
rintro (rfl | ⟨a, rfl⟩) <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem hasSum_geometric_two : HasSum (fun n : ℕ ↦ ((1 : ℝ) / 2) ^ n) 2

Proof state:
⊢ HasSum (fun n => (1 / 2) ^ n) 2

Tactic:
convert hasSum_geometric_of_lt_one _ _ <;> norm_num

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem ite_eq_iff : ite P a b = c ↔ P ∧ a = c ∨ ¬P ∧ b = c :=
  dite_eq_iff.trans <| by rw [exists_prop, exists_prop]

Proof state:
α : Sort u_1
P : Prop
inst✝ : Decidable P
a b c : α
⊢ ((∃ h, a = c) ∨ ∃ h, b = c) ↔ P ∧ a = c ∨ ¬P ∧ b = c

Tactic:
rw [exists_prop, exists_prop]

Result:
no goals