harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/MetricSpace/Dilation.lean
@[simp]
lemma _root_.Isometry.toDilation_ratio {f : α → β} {hf : Isometry f} : ratio hf.toDilation = 1

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
h : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (Isometry.toDilation f hf) = 1

Tactic:
push_neg at h

Result:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
h : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (Isometry.toDilation f hf) = 1

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (Isometry.toDilation f hf) = 1

Tactic:
exact ratio_of_trivial hf.toDilation h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
x y : α
h₁ : edist x y ≠ 0
h₂ : edist x y ≠ ⊤
⊢ edist ((Isometry.toDilation f hf) x) ((Isometry.toDilation f hf) y) = ↑1 * edist x y

Tactic:
simp [hf x y]

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
h : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (Isometry.toDilation f hf) = 1

Tactic:
obtain ⟨x, y, h₁, h₂⟩ := h

Result:
case neg.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
x y : α
h₁ : edist x y ≠ 0
h₂ : edist x y ≠ ⊤
⊢ ratio (Isometry.toDilation f hf) = 1

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ ratio (Isometry.toDilation f hf) = 1

Tactic:
by_cases h : ∀ x y : α, edist x y = 0 ∨ edist x y = ⊤

Result:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (Isometry.toDilation f hf) = 1

case neg
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
h : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (Isometry.toDilation f hf) = 1

Proof state:
case neg.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
x y : α
h₁ : edist x y ≠ 0
h₂ : edist x y ≠ ⊤
⊢ ratio (Isometry.toDilation f hf) = 1

Tactic:
exact ratio_unique h₁ h₂ (by simp [hf x y]) |>.symm

Result:
no goals
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem dNext_succ_chainComplex (f : ∀ i j, P.X i ⟶ Q.X j) (i : ℕ) :
    dNext (i + 1) f = P.d _ _ ≫ f i (i + 1)

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
⊢ (dNext (i + 1)) f = P.d (i + 1) i ≫ f i (i + 1)

Tactic:
dsimp [dNext]

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
⊢ P.d (i + 1) ((ComplexShape.down ℕ).next (i + 1)) ≫ f ((ComplexShape.down ℕ).next (i + 1)) (i + 1) =
    P.d (i + 1) i ≫ f i (i + 1)

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
⊢ P.d (i + 1) ((ComplexShape.down ℕ).next (i + 1)) ≫ f ((ComplexShape.down ℕ).next (i + 1)) (i + 1) =
    P.d (i + 1) i ≫ f i (i + 1)

Tactic:
have : (ComplexShape.down ℕ).next (i + 1) = i := ChainComplex.next_nat_succ _

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
this : (ComplexShape.down ℕ).next (i + 1) = i
⊢ P.d (i + 1) ((ComplexShape.down ℕ).next (i + 1)) ≫ f ((ComplexShape.down ℕ).next (i + 1)) (i + 1) =
    P.d (i + 1) i ≫ f i (i + 1)

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
this : (ComplexShape.down ℕ).next (i + 1) = i
⊢ P.d (i + 1) ((ComplexShape.down ℕ).next (i + 1)) ≫ f ((ComplexShape.down ℕ).next (i + 1)) (i + 1) =
    P.d (i + 1) i ≫ f i (i + 1)

Tactic:
congr 2

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Rank.lean
theorem rank_eq (h : Acc r a) :
    h.rank = ⨆ b : { b // r b a }, Order.succ (h.inv b.2).rank

Proof state:
α : Type u
a : α
r : α → α → Prop
h : Acc r a
⊢ ⋯.rank = ⨆ b, Order.succ ⋯.rank

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
a : α
r : α → α → Prop
h : Acc r a
⊢ h.rank = ⨆ b, Order.succ ⋯.rank

Tactic:
change (Acc.intro a fun _ => h.inv).rank = _

Result:
α : Type u
a : α
r : α → α → Prop
h : Acc r a
⊢ ⋯.rank = ⨆ b, Order.succ ⋯.rank
-- Mathlib/CategoryTheory/Yoneda.lean
theorem coreprW_hom_app (F : C ⥤ Type v₁) [F.IsCorepresentable] (X : C) (f : F.coreprX ⟶ X) :
    F.coreprW.hom.app X f = F.map f F.coreprx

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type v₁
inst✝ : F.IsCorepresentable
X : C
f : F.coreprX ⟶ X
⊢ F.coreprW.hom.app X f = F.map f F.coreprx

Tactic:
apply CorepresentableBy.homEquiv_eq

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem modular_T_smul (z : ℍ) : ModularGroup.T • z = (1 : ℝ) +ᵥ z

Proof state:
z : ℍ
⊢ ModularGroup.T • z = 1 +ᵥ z

Tactic:
simpa only [Int.cast_one] using modular_T_zpow_smul z 1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_eq_some_getElem_iff (xs : List α) (i : Nat) (h : i < xs.length) :
    (xs[i]? = some xs[i]) ↔ True

Proof state:
α : Type u_1
xs : List α
i : Nat
h : i < xs.length
⊢ xs[i]? = some xs[i] ↔ True

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem comp_left_top (r : Rel α β) : (⊤ : Rel γ α) • r = fun _ y ↦ y ∈ r.codom

Proof state:
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x : γ
z : β
⊢ (⊤ • r) x z ↔ z ∈ r.codom

Tactic:
simp [comp, Top.top, codom]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
⊢ ⊤ • r = fun x y => y ∈ r.codom

Tactic:
ext x z

Result:
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x : γ
z : β
⊢ (⊤ • r) x z ↔ z ∈ r.codom
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem tendsto_one_plus_div_rpow_exp (t : ℝ) :
    Tendsto (fun x : ℝ => (1 + t / x) ^ x) atTop (𝓝 (exp t))

Proof state:
t : ℝ
⊢ (rexp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x

Tactic:
have h₁ : (1 : ℝ) / 2 < 1 := by norm_num

Result:
t : ℝ
h₁ : 1 / 2 < 1
⊢ (rexp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x

Proof state:
t : ℝ
h₁ : 1 / 2 < 1
⊢ (rexp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x

Tactic:
have h₂ : Tendsto (fun x : ℝ => 1 + t / x) atTop (𝓝 1) := by
  simpa using (tendsto_inv_atTop_zero.const_mul t).const_add 1

Result:
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
⊢ (rexp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x

Proof state:
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
x : ℝ
hx : 1 / 2 ≤ 1 + t / x
hx' : 0 < 1 + t / x
⊢ (rexp ∘ fun x => x * log (1 + t / x)) x = (fun x => (1 + t / x) ^ x) x

Tactic:
simp [mul_comm x, exp_mul, exp_log hx']

Result:
no goals

Proof state:
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
x : ℝ
hx : 1 / 2 ≤ 1 + t / x
⊢ (rexp ∘ fun x => x * log (1 + t / x)) x = (fun x => (1 + t / x) ^ x) x

Tactic:
have hx' : 0 < 1 + t / x := by linarith

Result:
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
x : ℝ
hx : 1 / 2 ≤ 1 + t / x
hx' : 0 < 1 + t / x
⊢ (rexp ∘ fun x => x * log (1 + t / x)) x = (fun x => (1 + t / x) ^ x) x

Proof state:
t : ℝ
⊢ 1 / 2 < 1

Tactic:
norm_num

Result:
no goals

Proof state:
t : ℝ
h₁ : 1 / 2 < 1
⊢ Tendsto (fun x => 1 + t / x) atTop (𝓝 1)

Tactic:
simpa using (tendsto_inv_atTop_zero.const_mul t).const_add 1

Result:
no goals

Proof state:
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
x : ℝ
hx : 1 / 2 ≤ 1 + t / x
⊢ 0 < 1 + t / x

Tactic:
linarith

Result:
no goals

Proof state:
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
⊢ (rexp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x

Tactic:
refine (h₂.eventually_const_le h₁).mono fun x hx => ?_

Result:
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
x : ℝ
hx : 1 / 2 ≤ 1 + t / x
⊢ (rexp ∘ fun x => x * log (1 + t / x)) x = (fun x => (1 + t / x) ^ x) x

Proof state:
t : ℝ
⊢ Tendsto (fun x => (1 + t / x) ^ x) atTop (𝓝 (rexp t))

Tactic:
apply ((Real.continuous_exp.tendsto _).comp (tendsto_mul_log_one_plus_div_atTop t)).congr' _

Result:
t : ℝ
⊢ (rexp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x
-- Mathlib/Data/Vector/Snoc.lean
theorem mapAccumr_snoc {f : α → σ → σ × β} {s : σ} :
    mapAccumr f (xs.snoc x) s
    = let q := f x s
      let r := mapAccumr f xs q.1
      (r.1, r.2.snoc q.2)

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
f : α → σ → σ × β
s : σ
⊢ mapAccumr f (xs.snoc x) s =
    let q := f x s;
    let r := mapAccumr f xs q.1;
    (r.1, r.2.snoc q.2)

Tactic:
induction xs

Result:
case nil
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
f : α → σ → σ × β
s : σ
⊢ mapAccumr f (nil.snoc x) s =
    let q := f x s;
    let r := mapAccumr f nil q.1;
    (r.1, r.2.snoc q.2)

case cons
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
f : α → σ → σ × β
s : σ
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
a✝ :
  mapAccumr f (w✝.snoc x) s =
    let q := f x s;
    let r := mapAccumr f w✝ q.1;
    (r.1, r.2.snoc q.2)
⊢ mapAccumr f ((x✝ ::ᵥ w✝).snoc x) s =
    let q := f x s;
    let r := mapAccumr f (x✝ ::ᵥ w✝) q.1;
    (r.1, r.2.snoc q.2)

Proof state:
case nil
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
f : α → σ → σ × β
s : σ
⊢ mapAccumr f (nil.snoc x) s =
    let q := f x s;
    let r := mapAccumr f nil q.1;
    (r.1, r.2.snoc q.2)

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
f : α → σ → σ × β
s : σ
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
a✝ :
  mapAccumr f (w✝.snoc x) s =
    let q := f x s;
    let r := mapAccumr f w✝ q.1;
    (r.1, r.2.snoc q.2)
⊢ mapAccumr f ((x✝ ::ᵥ w✝).snoc x) s =
    let q := f x s;
    let r := mapAccumr f (x✝ ::ᵥ w✝) q.1;
    (r.1, r.2.snoc q.2)

Tactic:
simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem unop_inr {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) :
    c.unop.inr = c.snd.unop

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ c.unop.inr = c.snd.unop

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem dotProduct_comp_equiv_symm (e : n ≃ m) : u ⬝ᵥ x ∘ e.symm = u ∘ e ⬝ᵥ x

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
u : m → α
x : n → α
e : n ≃ m
⊢ u ⬝ᵥ x ∘ ⇑e.symm = u ∘ ⇑e ⬝ᵥ x

Tactic:
simpa only [Equiv.symm_symm] using (comp_equiv_symm_dotProduct u x e.symm).symm

Result:
no goals
-- Mathlib/Algebra/Group/Translate.lean
@[simp] lemma support_translate (a : G) (f : G → H) : support (τ a f) = a +ᵥ support f

Proof state:
G : Type u_5
H : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
a : G
f : G → H
⊢ support (τ a f) = a +ᵥ support f

Tactic:
ext

Result:
case h
G : Type u_5
H : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
a : G
f : G → H
x✝ : G
⊢ x✝ ∈ support (τ a f) ↔ x✝ ∈ a +ᵥ support f

Proof state:
case h
G : Type u_5
H : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
a : G
f : G → H
x✝ : G
⊢ x✝ ∈ support (τ a f) ↔ x✝ ∈ a +ᵥ support f

Tactic:
simp [mem_vadd_set_iff_neg_vadd_mem, sub_eq_neg_add]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_two_mul' : cos (2 * x) = cos x ^ 2 - sin x ^ 2 :=
  ofReal_injective <| by simp [cos_two_mul']

Proof state:
x : ℝ
⊢ ↑(cos (2 * x)) = ↑(cos x ^ 2 - sin x ^ 2)

Tactic:
simp [cos_two_mul']

Result:
no goals
-- Mathlib/CategoryTheory/Dialectica/Monoidal.lean
theorem hexagon_reverse (X Y Z : Dial C) :
    (associator X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (associator Z X Y).inv =
      tensorHom (𝟙 X) (braiding Y Z).hom ≫ (associator X Z Y).inv ≫
      tensorHom (braiding X Z).hom (𝟙 Y)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
⊢ (X.associator Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (Z.associator X Y).inv =
    tensorHom (𝟙 X) (Y.braiding Z).hom ≫ (X.associator Z Y).inv ≫ tensorHom (X.braiding Z).hom (𝟙 Y)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem takeWhile_go_succ (p : α → Bool) (a : α) (l : List α) (i : Nat) :
    takeWhile.go p (a :: l).toArray (i+1) r = takeWhile.go p l.toArray i r

Proof state:
case isTrue
α : Type u_1
r : Array α
p : α → Bool
a : α
l : List α
i : Nat
h✝ : i < l.length
⊢ (if p l[i] = true then takeWhile.go p (a :: l).toArray (i + 1 + 1) (r.push l[i]) else r) =
    if p l[i] = true then takeWhile.go p l.toArray (i + 1) (r.push l[i]) else r

case isFalse
α : Type u_1
r : Array α
p : α → Bool
a : α
l : List α
i : Nat
h✝ : ¬i < l.length
⊢ r = r

Tactic:
rw [takeWhile_go_succ]

Result:
case isFalse
α : Type u_1
r : Array α
p : α → Bool
a : α
l : List α
i : Nat
h✝ : ¬i < l.length
⊢ r = r

Proof state:
α : Type u_1
r : Array α
p : α → Bool
a : α
l : List α
i : Nat
⊢ (if h : i + 1 < (a :: l).toArray.size then
      let a_1 := (a :: l).toArray[i + 1];
      if p a_1 = true then takeWhile.go p (a :: l).toArray (i + 1 + 1) (r.push a_1) else r
    else r) =
    if h : i < l.toArray.size then
      let a := l.toArray[i];
      if p a = true then takeWhile.go p l.toArray (i + 1) (r.push a) else r
    else r

Tactic:
simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
  getElem_toArray, getElem_cons_succ]

Result:
α : Type u_1
r : Array α
p : α → Bool
a : α
l : List α
i : Nat
⊢ (if h : i < l.length then if p l[i] = true then takeWhile.go p (a :: l).toArray (i + 1 + 1) (r.push l[i]) else r
    else r) =
    if h : i < l.length then if p l[i] = true then takeWhile.go p l.toArray (i + 1) (r.push l[i]) else r else r

Proof state:
α : Type u_1
r : Array α
p : α → Bool
a : α
l : List α
i : Nat
⊢ takeWhile.go p (a :: l).toArray (i + 1) r = takeWhile.go p l.toArray i r

Tactic:
rw [takeWhile.go, takeWhile.go]

Result:
α : Type u_1
r : Array α
p : α → Bool
a : α
l : List α
i : Nat
⊢ (if h : i + 1 < (a :: l).toArray.size then
      let a_1 := (a :: l).toArray[i + 1];
      if p a_1 = true then takeWhile.go p (a :: l).toArray (i + 1 + 1) (r.push a_1) else r
    else r) =
    if h : i < l.toArray.size then
      let a := l.toArray[i];
      if p a = true then takeWhile.go p l.toArray (i + 1) (r.push a) else r
    else r

Proof state:
α : Type u_1
r : Array α
p : α → Bool
a : α
l : List α
i : Nat
⊢ (if h : i < l.length then if p l[i] = true then takeWhile.go p (a :: l).toArray (i + 1 + 1) (r.push l[i]) else r
    else r) =
    if h : i < l.length then if p l[i] = true then takeWhile.go p l.toArray (i + 1) (r.push l[i]) else r else r

Tactic:
split

Result:
case isTrue
α : Type u_1
r : Array α
p : α → Bool
a : α
l : List α
i : Nat
h✝ : i < l.length
⊢ (if p l[i] = true then takeWhile.go p (a :: l).toArray (i + 1 + 1) (r.push l[i]) else r) =
    if p l[i] = true then takeWhile.go p l.toArray (i + 1) (r.push l[i]) else r

case isFalse
α : Type u_1
r : Array α
p : α → Bool
a : α
l : List α
i : Nat
h✝ : ¬i < l.length
⊢ r = r

Proof state:
case isFalse
α : Type u_1
r : Array α
p : α → Bool
a : α
l : List α
i : Nat
h✝ : ¬i < l.length
⊢ r = r

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodySumFun_continuous :
    Continuous (convexBodySumFun : mixedSpace K → ℝ)

Proof state:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ w ∈ Finset.univ → Continuous fun a => ↑w.mult * ‖a.2 ⟨w, hw⟩‖

Tactic:
fun_prop

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ w ∈ Finset.univ → Continuous fun a => ↑w.mult * (normAtPlace w) a

Tactic:
obtain hw | hw := isReal_or_isComplex w

Result:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsReal
⊢ w ∈ Finset.univ → Continuous fun a => ↑w.mult * (normAtPlace w) a

case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ w ∈ Finset.univ → Continuous fun a => ↑w.mult * (normAtPlace w) a

Proof state:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ w ∈ Finset.univ → Continuous fun a => ↑w.mult * (normAtPlace w) a

Tactic:
simp only [normAtPlace_apply_of_isReal, normAtPlace_apply_of_isComplex, hw]

Result:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ w ∈ Finset.univ → Continuous fun a => ↑w.mult * ‖a.2 ⟨w, hw⟩‖

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Continuous convexBodySumFun

Tactic:
refine continuous_finset_sum Finset.univ fun w ↦ ?_

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ w ∈ Finset.univ → Continuous fun a => ↑w.mult * (normAtPlace w) a
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_singleton (a : α) [Fintype ({a} : Set α)] : ({a} : Set α).toFinset = {a}

Proof state:
case h
α : Type u_1
a : α
inst✝ : Fintype ↑{a}
a✝ : α
⊢ a✝ ∈ {a}.toFinset ↔ a✝ ∈ {a}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝ : Fintype ↑{a}
⊢ {a}.toFinset = {a}

Tactic:
ext

Result:
case h
α : Type u_1
a : α
inst✝ : Fintype ↑{a}
a✝ : α
⊢ a✝ ∈ {a}.toFinset ↔ a✝ ∈ {a}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem xor_eq_zero_iff {x y : BitVec w} : (x ^^^ y = 0#w) ↔ x = y

Proof state:
case mp
w : Nat
x y : BitVec w
h : x ^^^ y = 0#w
⊢ x = y

Tactic:
apply (xor_left_inj y).mp

Result:
case mp
w : Nat
x y : BitVec w
h : x ^^^ y = 0#w
⊢ x ^^^ y = y ^^^ y

Proof state:
case mpr
w : Nat
x y : BitVec w
h : x = y
⊢ x ^^^ y = 0#w

Tactic:
simp [h]

Result:
no goals

Proof state:
case mpr
w : Nat
x y : BitVec w
⊢ x = y → x ^^^ y = 0#w

Tactic:
intro h

Result:
case mpr
w : Nat
x y : BitVec w
h : x = y
⊢ x ^^^ y = 0#w

Proof state:
case mp
w : Nat
x y : BitVec w
⊢ x ^^^ y = 0#w → x = y

Tactic:
intro h

Result:
case mp
w : Nat
x y : BitVec w
h : x ^^^ y = 0#w
⊢ x = y

Proof state:
w : Nat
x y : BitVec w
⊢ x ^^^ y = 0#w ↔ x = y

Tactic:
constructor

Result:
case mp
w : Nat
x y : BitVec w
⊢ x ^^^ y = 0#w → x = y

case mpr
w : Nat
x y : BitVec w
⊢ x = y → x ^^^ y = 0#w

Proof state:
case mp
w : Nat
x y : BitVec w
h : x ^^^ y = 0#w
⊢ x ^^^ y = y ^^^ y

Tactic:
rwa [xor_self]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem Topology.IsInducing.specializes_iff (hf : IsInducing f) : f x ⤳ f y ↔ x ⤳ y

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
f : X → Y
hf : IsInducing f
⊢ f x ⤳ f y ↔ x ⤳ y

Tactic:
simp only [specializes_iff_mem_closure, hf.closure_eq_preimage_closure_image, image_singleton,
  mem_preimage]

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem lub_Iio_eq_self_or_Iio_eq_Iic [PartialOrder γ] {j : γ} (i : γ) (hj : IsLUB (Iio i) j) :
    j = i ∨ Iio i = Iic j

Proof state:
case inl
γ : Type v
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_eq_i : j = i
⊢ j = i ∨ Iio i = Iic j

Tactic:
exact Or.inl hj_eq_i

Result:
no goals

Proof state:
case inr.h
γ : Type v
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ Iio i = Iic j

Tactic:
exact Set.ext fun k => ⟨fun hk_lt => hj.1 hk_lt, fun hk_le_j => lt_of_le_of_lt hk_le_j hj_lt_i⟩

Result:
no goals

Proof state:
γ : Type v
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
⊢ j = i ∨ Iio i = Iic j

Tactic:
rcases eq_or_lt_of_le (lub_Iio_le i hj) with hj_eq_i | hj_lt_i

Result:
case inl
γ : Type v
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_eq_i : j = i
⊢ j = i ∨ Iio i = Iic j

case inr
γ : Type v
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ j = i ∨ Iio i = Iic j

Proof state:
case inr
γ : Type v
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ j = i ∨ Iio i = Iic j

Tactic:
right

Result:
case inr.h
γ : Type v
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ Iio i = Iic j
-- Mathlib/Order/UpperLower/Basic.lean
theorem mem_iSup₂_iff {f : ∀ i, κ i → UpperSet α} : (a ∈ ⨆ (i) (j), f i j) ↔ ∀ i j, a ∈ f i j

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
a : α
f : (i : ι) → κ i → UpperSet α
⊢ a ∈ ⨆ i, ⨆ j, f i j ↔ ∀ (i : ι) (j : κ i), a ∈ f i j

Tactic:
simp_rw [mem_iSup_iff]

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem single_zero_right (a : G) : single a (0 : k) = 0

Proof state:
case neg
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a a' : G
h : ¬a = a'
⊢ (single a 0).coeff a' = coeff 0 a'

Tactic:
rw [coeff_single_apply]

Result:
case neg
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a a' : G
h : ¬a = a'
⊢ (if a = a' then 0 else 0) = coeff 0 a'

Proof state:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a : G
⊢ single a 0 = 0

Tactic:
ext a'

Result:
case a
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a a' : G
⊢ (single a 0).coeff a' = coeff 0 a'

Proof state:
case a
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a a' : G
⊢ (single a 0).coeff a' = coeff 0 a'

Tactic:
by_cases h : a = a' <;> (rw [coeff_single_apply]; simp only [h, ↓reduceIte, coeff_zero])

Result:
no goals

Proof state:
case a
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a a' : G
⊢ (single a 0).coeff a' = coeff 0 a'

Tactic:
classical
by_cases h : a = a' <;> (rw [coeff_single_apply]; simp only [h, ↓reduceIte, coeff_zero])

Result:
no goals

Proof state:
case neg
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a a' : G
h : ¬a = a'
⊢ (if a = a' then 0 else 0) = coeff 0 a'

Tactic:
simp only [h, ↓reduceIte, coeff_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem mul_right_comm (a b c : Int) : a * b * c = a * c * b

Proof state:
a b c : Int
⊢ a * b * c = a * c * b

Tactic:
rw [Int.mul_assoc, Int.mul_assoc, Int.mul_comm b]

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma OrthogonalIdempotents.iff_mul_eq [DecidableEq I] :
    OrthogonalIdempotents e ↔ ∀ i j, e i * e j = if i = j then e i else 0 :=
  ⟨mul_eq, fun H ↦ ⟨fun i ↦ by simpa using H i i, fun i j e ↦ by simpa [e] using H i j⟩⟩

Proof state:
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : DecidableEq I
H : ∀ (i j : I), e i * e j = if i = j then e i else 0
i : I
⊢ IsIdempotentElem (e i)

Tactic:
simpa using H i i

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e✝ : I → R
inst✝ : DecidableEq I
H : ∀ (i j : I), e✝ i * e✝ j = if i = j then e✝ i else 0
i j : I
e : i ≠ j
⊢ (fun x1 x2 => e✝ x1 * e✝ x2 = 0) i j

Tactic:
simpa [e] using H i j

Result:
no goals