harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffEdist_le_of_mem_edist {r : ℝ≥0∞} (H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r)
    (H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r) : hausdorffEdist s t ≤ r

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
⊢ hausdorffEdist s t ≤ r

Tactic:
refine hausdorffEdist_le_of_infEdist (fun x xs ↦ ?_) (fun x xt ↦ ?_)

Result:
case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
x : α
xs : x ∈ s
⊢ infEdist x t ≤ r

case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
x : α
xt : x ∈ t
⊢ infEdist x s ≤ r

Proof state:
case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
x : α
xs : x ∈ s
⊢ infEdist x t ≤ r

Tactic:
rcases H1 x xs with ⟨y, yt, hy⟩

Result:
case refine_1.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
x : α
xs : x ∈ s
y : α
yt : y ∈ t
hy : edist x y ≤ r
⊢ infEdist x t ≤ r

Proof state:
case refine_1.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
x : α
xs : x ∈ s
y : α
yt : y ∈ t
hy : edist x y ≤ r
⊢ infEdist x t ≤ r

Tactic:
exact le_trans (infEdist_le_edist_of_mem yt) hy

Result:
no goals

Proof state:
case refine_2.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
x : α
xt : x ∈ t
y : α
ys : y ∈ s
hy : edist x y ≤ r
⊢ infEdist x s ≤ r

Tactic:
exact le_trans (infEdist_le_edist_of_mem ys) hy

Result:
no goals

Proof state:
case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
x : α
xt : x ∈ t
⊢ infEdist x s ≤ r

Tactic:
rcases H2 x xt with ⟨y, ys, hy⟩

Result:
case refine_2.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
x : α
xt : x ∈ t
y : α
ys : y ∈ s
hy : edist x y ≤ r
⊢ infEdist x s ≤ r
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem mem_of_mem_erase {a b : α} {l : Array α} (h : a ∈ l.erase b) : a ∈ l

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
l : List α
h : a ∈ { toList := l }.erase b
⊢ a ∈ l.erase ?m.36325

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a b : α
l : List α
h : a ∈ { toList := l }.erase b
⊢ a ∈ { toList := l }

Tactic:
simpa using List.mem_of_mem_erase (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
l : Array α
h : a ∈ l.erase b
⊢ a ∈ l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
a b : α
l : List α
h : a ∈ { toList := l }.erase b
⊢ a ∈ { toList := l }
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem linearIndepOn_iff_linearCombinationOnₛ :
    LinearIndepOn R v s ↔ Injective (Finsupp.linearCombinationOn ι M R v s)

Proof state:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ LinearIndepOn R v s ↔ Injective ⇑(Finsupp.linearCombinationOn ι M R v s)

Tactic:
rw [← linearIndependent_restrict_iff]

Result:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ LinearIndependent (ι := ↑s) R (s.restrict v) ↔ Injective ⇑(Finsupp.linearCombinationOn ι M R v s)

Proof state:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ LinearIndependent (ι := ↑s) R (s.restrict v) ↔ Injective ⇑(Finsupp.linearCombinationOn ι M R v s)

Tactic:
simp [LinearIndependent, Finsupp.linearCombination_restrict]

Result:
no goals
-- Mathlib/NumberTheory/Bernoulli.lean
theorem bernoulli_spec' (n : ℕ) :
    (∑ k ∈ antidiagonal n, ((k.1 + k.2).choose k.2 : ℚ) / (k.2 + 1) * bernoulli k.1) =
      if n = 0 then 1 else 0

Proof state:
case h.e'_2
n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
h₂ : ↑n + 1 ≠ 0
h₃ : (1 + n).choose n = n + 1
H :
  ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1 +
      ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1 =
    1
p : ℕ × ℕ
h : p ∈ antidiagonal n.succ \ {(1, n)}
⊢ ↑((p.1 + p.2).choose p.2) / (↑p.2 + 1) * bernoulli p.1 = ↑((p.1 + p.2).choose p.2) / (↑p.2 + 1) * bernoulli' p.1

Tactic:
obtain ⟨h', h''⟩ : p ∈ _ ∧ p ≠ _ := by rwa [mem_sdiff, mem_singleton] at h

Result:
case h.e'_2.intro
n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
h₂ : ↑n + 1 ≠ 0
h₃ : (1 + n).choose n = n + 1
H :
  ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1 +
      ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1 =
    1
p : ℕ × ℕ
h : p ∈ antidiagonal n.succ \ {(1, n)}
h' : p ∈ antidiagonal n.succ
h'' : p ≠ (1, n)
⊢ ↑((p.1 + p.2).choose p.2) / (↑p.2 + 1) * bernoulli p.1 = ↑((p.1 + p.2).choose p.2) / (↑p.2 + 1) * bernoulli' p.1

Proof state:
case zero

⊢ ∑ k ∈ antidiagonal 0, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = if 0 = 0 then 1 else 0

Tactic:
simp

Result:
no goals

Proof state:
case succ
n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
h₂ : ↑n + 1 ≠ 0
h₃ : (1 + n).choose n = n + 1
⊢ ∑ k ∈ antidiagonal (n + 1), ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = 0

Tactic:
have H := bernoulli'_spec' n.succ

Result:
case succ
n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
h₂ : ↑n + 1 ≠ 0
h₃ : (1 + n).choose n = n + 1
H : ∑ k ∈ antidiagonal n.succ, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli' k.1 = 1
⊢ ∑ k ∈ antidiagonal (n + 1), ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = 0

Proof state:
n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
⊢ ↑n + 1 ≠ 0

Tactic:
norm_cast

Result:
no goals

Proof state:
case succ
n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
h₂ : ↑n + 1 ≠ 0
h₃ : (1 + n).choose n = n + 1
H : ∑ k ∈ antidiagonal n.succ, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli' k.1 = 1
⊢ ∑ k ∈ antidiagonal (n + 1), ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = 0

Tactic:
rw [sum_eq_add_sum_diff_singleton h₁] at H ⊢

Result:
case succ
n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
h₂ : ↑n + 1 ≠ 0
h₃ : (1 + n).choose n = n + 1
H :
  ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1 +
      ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1 =
    1
⊢ ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli (1, n).1 +
      ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli x.1 =
    0
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem range_eq_empty_of_isEmpty {β} [hα : IsEmpty α] (f : α →ₛ β) : f.range = ∅

Proof state:
case intro
α : Type u_1
inst✝ : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
y : β
hy_mem : y ∈ f.range
⊢ False

Tactic:
rw [SimpleFunc.mem_range, Set.mem_range] at hy_mem

Result:
case intro
α : Type u_1
inst✝ : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
y : β
hy_mem : ∃ y_1, f y_1 = y
⊢ False

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
⊢ ¬f.range.Nonempty

Tactic:
by_contra h

Result:
α : Type u_1
inst✝ : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
h : f.range.Nonempty
⊢ False

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
⊢ f.range = ∅

Tactic:
rw [← Finset.not_nonempty_iff_eq_empty]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
⊢ ¬f.range.Nonempty

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
h : f.range.Nonempty
⊢ False

Tactic:
obtain ⟨y, hy_mem⟩ := h

Result:
case intro
α : Type u_1
inst✝ : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
y : β
hy_mem : y ∈ f.range
⊢ False

Proof state:
case intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
y : β
x : α
hxy : f x = y
⊢ False

Tactic:
rw [isEmpty_iff] at hα

Result:
case intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
β : Type u_5
hα : α → False
f : α →ₛ β
y : β
x : α
hxy : f x = y
⊢ False

Proof state:
case intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
β : Type u_5
hα : α → False
f : α →ₛ β
y : β
x : α
hxy : f x = y
⊢ False

Tactic:
exact hα x

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝ : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
y : β
hy_mem : ∃ y_1, f y_1 = y
⊢ False

Tactic:
obtain ⟨x, hxy⟩ := hy_mem

Result:
case intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
y : β
x : α
hxy : f x = y
⊢ False
-- Mathlib/RingTheory/Valuation/Integers.lean
lemma valuation_pos_iff_ne_zero (hv : Integers v O) {x : O} :
    0 < v (algebraMap O F x) ↔ x ≠ 0

Proof state:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
⊢ v ((algebraMap O F) x) ≤ 0 ↔ x = 0

Tactic:
simp [map_eq_zero_iff _ hv.hom_inj]

Result:
no goals

Proof state:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
⊢ 0 < v ((algebraMap O F) x) ↔ x ≠ 0

Tactic:
rw [← not_le]

Result:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
⊢ ¬v ((algebraMap O F) x) ≤ 0 ↔ x ≠ 0

Proof state:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
⊢ ¬v ((algebraMap O F) x) ≤ 0 ↔ x ≠ 0

Tactic:
refine not_congr ?_

Result:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
⊢ v ((algebraMap O F) x) ≤ 0 ↔ x = 0
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_smul_of_nonneg {r : ℝ} (hr : 0 ≤ r) (s : Set E) :
    μ (r • s) = ENNReal.ofReal (r ^ finrank ℝ E) * μ s

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hr : 0 ≤ r
s : Set E
⊢ μ (r • s) = ENNReal.ofReal (r ^ finrank ℝ E) * μ s

Tactic:
rw [addHaar_smul, abs_pow, abs_of_nonneg hr]

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
theorem rel_add_left {as₀ as₁} :
    ∀ {bs}, Rel r (as₀ + as₁) bs ↔ ∃ bs₀ bs₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁ :=
  @(Multiset.induction_on as₀ (by simp) fun a s ih bs ↦ by
      simp only [ih, cons_add, rel_cons_left]
      constructor
      · intro h
        rcases h with ⟨b, bs', hab, h, rfl⟩
        rcases h with ⟨bs₀, bs₁, h₀, h₁, rfl⟩
        exact ⟨b ::ₘ bs₀, bs₁, ⟨b, bs₀, hab, h₀, rfl⟩, h₁, by simp⟩
      · intro h
        rcases h with ⟨bs₀, bs₁, h, h₁, rfl⟩
        rcases h with ⟨b, bs, hab, h₀, rfl⟩
        exact ⟨b, bs + bs₁, hab, ⟨bs, bs₁, h₀, h₁, rfl⟩, by simp⟩)

Proof state:
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
b : β
hab : r a b
bs₀ bs₁ : Multiset β
h₀ : Rel r s bs₀
h₁ : Rel r as₁ bs₁
⊢ b ::ₘ (bs₀ + bs₁) = b ::ₘ bs₀ + bs₁

Tactic:
simp

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
b : β
hab : r a b
bs₀ bs₁ : Multiset β
h₀ : Rel r s bs₀
h₁ : Rel r as₁ bs₁
⊢ ∃ bs₀_1 bs₁_1,
    (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀_1 = b ::ₘ bs') ∧ Rel r as₁ bs₁_1 ∧ b ::ₘ (bs₀ + bs₁) = bs₀_1 + bs₁_1

Tactic:
exact ⟨b ::ₘ bs₀, bs₁, ⟨b, bs₀, hab, h₀, rfl⟩, h₁, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs₁ : Multiset β
h₁ : Rel r as₁ bs₁
b : β
bs : Multiset β
hab : r a b
h₀ : Rel r s bs
⊢ b ::ₘ bs + bs₁ = b ::ₘ (bs + bs₁)

Tactic:
simp

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
⊢ (∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs') →
    ∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁

Tactic:
intro h

Result:
case mp
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
h : ∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs'
⊢ ∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem smul_map_inv_div_map_inv_of_isMulTwoCocycle
    {f : G × G → M} (hf : IsMulTwoCocycle f) (g : G) :
    g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)

Proof state:
G : Type u_1
M : Type u_2
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G × G → M
hf : IsMulTwoCocycle f
g : G
this : f (1, 1) * f (g, g⁻¹) = g • f (g⁻¹, g) * f (g, 1)
⊢ g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)

Tactic:
exact div_eq_div_iff_mul_eq_mul.2 this.symm

Result:
no goals

Proof state:
G : Type u_1
M : Type u_2
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G × G → M
hf : IsMulTwoCocycle f
g : G
this : f (g * g⁻¹, g) * f (g, g⁻¹) = g • f (g⁻¹, g) * f (g, g⁻¹ * g)
⊢ g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)

Tactic:
simp only [mul_inv_cancel, inv_mul_cancel, map_one_fst_of_isMulTwoCocycle hf g] at this

Result:
G : Type u_1
M : Type u_2
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G × G → M
hf : IsMulTwoCocycle f
g : G
this : f (1, 1) * f (g, g⁻¹) = g • f (g⁻¹, g) * f (g, 1)
⊢ g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)

Proof state:
G : Type u_1
M : Type u_2
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G × G → M
hf : IsMulTwoCocycle f
g : G
⊢ g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)

Tactic:
have := hf g g⁻¹ g

Result:
G : Type u_1
M : Type u_2
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G × G → M
hf : IsMulTwoCocycle f
g : G
this : f (g * g⁻¹, g) * f (g, g⁻¹) = g • f (g⁻¹, g) * f (g, g⁻¹ * g)
⊢ g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem dist_nonneg (x y : ∀ n, E n) : 0 ≤ dist x y

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ 0 ≤ dist x y

Tactic:
rcases eq_or_ne x y with (rfl | h)

Result:
case inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
⊢ 0 ≤ dist x x

case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ 0 ≤ dist x y

Proof state:
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ 0 ≤ dist x y

Tactic:
simp [dist, h, zero_le_two]

Result:
no goals

Proof state:
case inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
⊢ 0 ≤ dist x x

Tactic:
simp [dist]

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem heq_comp {C} [Category C] {X Y Z X' Y' Z' : C}
    {f : X ⟶ Y} {g : Y ⟶ Z} {f' : X' ⟶ Y'} {g' : Y' ⟶ Z'}
    (eq1 : X = X') (eq2 : Y = Y') (eq3 : Z = Z')
    (H1 : HEq f f') (H2 : HEq g g') :
    HEq (f ≫ g) (f' ≫ g')

Proof state:
case refl
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y Z Y' Z' : C
f : X ⟶ Y
g : Y ⟶ Z
g' : Y' ⟶ Z'
eq2 : Y = Y'
eq3 : Z = Z'
H2 : HEq g g'
f' : X ⟶ Y'
H1 : HEq f f'
⊢ HEq (f ≫ g) (f' ≫ g')

Tactic:
cases eq2

Result:
case refl.refl
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y Z Z' : C
f : X ⟶ Y
g : Y ⟶ Z
eq3 : Z = Z'
g' : Y ⟶ Z'
H2 : HEq g g'
f' : X ⟶ Y
H1 : HEq f f'
⊢ HEq (f ≫ g) (f' ≫ g')

Proof state:
case refl.refl.refl.refl
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y Z : C
f : X ⟶ Y
g g' : Y ⟶ Z
H2 : HEq g g'
⊢ HEq (f ≫ g) (f ≫ g')

Tactic:
cases H2

Result:
case refl.refl.refl.refl.refl
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ HEq (f ≫ g) (f ≫ g)

Proof state:
case refl.refl
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y Z Z' : C
f : X ⟶ Y
g : Y ⟶ Z
eq3 : Z = Z'
g' : Y ⟶ Z'
H2 : HEq g g'
f' : X ⟶ Y
H1 : HEq f f'
⊢ HEq (f ≫ g) (f' ≫ g')

Tactic:
cases eq3

Result:
case refl.refl.refl
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
H1 : HEq f f'
g' : Y ⟶ Z
H2 : HEq g g'
⊢ HEq (f ≫ g) (f' ≫ g')

Proof state:
case refl.refl.refl.refl.refl
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ HEq (f ≫ g) (f ≫ g)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y Z X' Y' Z' : C
f : X ⟶ Y
g : Y ⟶ Z
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
eq1 : X = X'
eq2 : Y = Y'
eq3 : Z = Z'
H1 : HEq f f'
H2 : HEq g g'
⊢ HEq (f ≫ g) (f' ≫ g')

Tactic:
cases eq1

Result:
case refl
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y Z Y' Z' : C
f : X ⟶ Y
g : Y ⟶ Z
g' : Y' ⟶ Z'
eq2 : Y = Y'
eq3 : Z = Z'
H2 : HEq g g'
f' : X ⟶ Y'
H1 : HEq f f'
⊢ HEq (f ≫ g) (f' ≫ g')

Proof state:
case refl.refl.refl
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
H1 : HEq f f'
g' : Y ⟶ Z
H2 : HEq g g'
⊢ HEq (f ≫ g) (f' ≫ g')

Tactic:
cases H1

Result:
case refl.refl.refl.refl
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y Z : C
f : X ⟶ Y
g g' : Y ⟶ Z
H2 : HEq g g'
⊢ HEq (f ≫ g) (f ≫ g')
-- Mathlib/Analysis/Complex/Hadamard.lean
/-- The supremum of the norm of `scale f l u` on the line `z.re = 1` is the same as
  the supremum of `f` on the line `z.re = u`. -/
lemma sSupNormIm_scale_right (f : ℂ → E) {l u : ℝ} (hul : l < u) :
    sSupNormIm (scale f l u) 1 = sSupNormIm f u

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ sSupNormIm (scale f l u) 1 = sSupNormIm f u

Tactic:
simp_rw [sSupNormIm, image_comp]

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ sSup (norm '' (scale f l u '' (re ⁻¹' {1}))) = sSup (norm '' (f '' (re ⁻¹' {u})))

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ ↑u - ↑l ≠ 0

Tactic:
norm_cast

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ ¬u - l = 0

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ scale f l u '' (re ⁻¹' {1}) = f '' (re ⁻¹' {u})

Tactic:
ext e

Result:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
⊢ e ∈ scale f l u '' (re ⁻¹' {1}) ↔ e ∈ f '' (re ⁻¹' {u})
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem mul_single_apply_aux [Mul G] (f : MonoidAlgebra k G) {r : k} {x y z : G}
    (H : ∀ a ∈ f.support, a * x = z ↔ a = y) : (f * single x r) z = f y * r

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
x y z : G
H : ∀ a ∈ f.support, a * x = z ↔ a = y
⊢ (if y ∈ f.support then f y * r else 0) = f y * r

Tactic:
split_ifs with h <;> simp at h <;> simp [h]

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
x y z : G
H : ∀ a ∈ f.support, a * x = z ↔ a = y
⊢ (f * single x r) z = f y * r

Tactic:
exact
calc
(f * single x r) z
_ = sum f fun a b => ite (a * x = z) (b * r) 0 :=
(mul_apply _ _ _).trans <| Finsupp.sum_congr fun _ _ => sum_single_index (by simp)
_ = f.sum fun a b => ite (a = y) (b * r) 0 := Finsupp.sum_congr fun x hx => by
simp only [H _ hx]
_ = if y ∈ f.support then f y * r else 0 := f.support.sum_ite_eq' _ _
_ = _ := by split_ifs with h <;> simp at h <;> simp [h]

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
x y z : G
H : ∀ a ∈ f.support, a * x = z ↔ a = y
x✝¹ : G
x✝ : x✝¹ ∈ f.support
⊢ (if x✝¹ * x = z then f x✝¹ * 0 else 0) = 0

Tactic:
simp

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
x✝ y z : G
H : ∀ a ∈ f.support, a * x✝ = z ↔ a = y
x : G
hx : x ∈ f.support
⊢ (if x * x✝ = z then f x * r else 0) = if x = y then f x * r else 0

Tactic:
simp only [H _ hx]

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
x y z : G
H : ∀ a ∈ f.support, a * x = z ↔ a = y
⊢ (f * single x r) z = f y * r

Tactic:
classical exact
  calc
    (f * single x r) z
    _ = sum f fun a b => ite (a * x = z) (b * r) 0 :=
      (mul_apply _ _ _).trans <| Finsupp.sum_congr fun _ _ => sum_single_index (by simp)
    _ = f.sum fun a b => ite (a = y) (b * r) 0 := Finsupp.sum_congr fun x hx => by
      simp only [H _ hx]
    _ = if y ∈ f.support then f y * r else 0 := f.support.sum_ite_eq' _ _
    _ = _ := by split_ifs with h <;> simp at h <;> simp [h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_pi_div_two : cos (π / 2) = 0 :=
  calc
    cos (π / 2) = Real.cos (π / 2)

Proof state:
⊢ cos (↑π / 2) = cos ↑(π / 2)

Tactic:
simp

Result:
no goals

Proof state:
⊢ ↑(Real.cos (π / 2)) = 0

Tactic:
simp

Result:
no goals

Proof state:
⊢ cos (↑π / 2) = ↑(Real.cos (π / 2))

Tactic:
rw [ofReal_cos]

Result:
⊢ cos (↑π / 2) = cos ↑(π / 2)
-- Mathlib/NumberTheory/DiophantineApproximation/ContinuedFractions.lean
theorem exists_convs_eq_rat {q : ℚ}
    (h : |ξ - q| < 1 / (2 * (q.den : ℝ) ^ 2)) : ∃ n, (GenContFract.of ξ).convs n = q

Proof state:
case intro
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
n : ℕ
hn : q = ξ.convergent n
⊢ ∃ n, (GenContFract.of ξ).convs n = ↑q

Tactic:
exact ⟨n, hn.symm ▸ convs_eq_convergent ξ n⟩

Result:
no goals

Proof state:
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
⊢ ∃ n, (GenContFract.of ξ).convs n = ↑q

Tactic:
obtain ⟨n, hn⟩ := exists_rat_eq_convergent h

Result:
case intro
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
n : ℕ
hn : q = ξ.convergent n
⊢ ∃ n, (GenContFract.of ξ).convs n = ↑q