harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffEdist_le_ediam (hs : s.Nonempty) (ht : t.Nonempty) :
    hausdorffEdist s t ≤ diam (s ∪ t)

Proof state:
case intro.intro.refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ diam (s ∪ t)

Tactic:
intro z hz

Result:
case intro.intro.refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
z : α
hz : z ∈ s
⊢ ∃ y ∈ t, edist z y ≤ diam (s ∪ t)

Proof state:
case intro.intro.refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
z : α
hz : z ∈ t
⊢ ∃ y ∈ s, edist z y ≤ diam (s ∪ t)

Tactic:
exact ⟨x, xs, edist_le_diam_of_mem (subset_union_right hz) (subset_union_left xs)⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ hausdorffEdist s t ≤ diam (s ∪ t)

Tactic:
refine hausdorffEdist_le_of_mem_edist ?_ ?_

Result:
case intro.intro.refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ diam (s ∪ t)

case intro.intro.refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ diam (s ∪ t)

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ hausdorffEdist s t ≤ diam (s ∪ t)

Tactic:
rcases hs with ⟨x, xs⟩

Result:
case intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
ht : t.Nonempty
x : α
xs : x ∈ s
⊢ hausdorffEdist s t ≤ diam (s ∪ t)

Proof state:
case intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
ht : t.Nonempty
x : α
xs : x ∈ s
⊢ hausdorffEdist s t ≤ diam (s ∪ t)

Tactic:
rcases ht with ⟨y, yt⟩

Result:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ hausdorffEdist s t ≤ diam (s ∪ t)

Proof state:
case intro.intro.refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ diam (s ∪ t)

Tactic:
intro z hz

Result:
case intro.intro.refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
z : α
hz : z ∈ t
⊢ ∃ y ∈ s, edist z y ≤ diam (s ∪ t)

Proof state:
case intro.intro.refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
z : α
hz : z ∈ s
⊢ ∃ y ∈ t, edist z y ≤ diam (s ∪ t)

Tactic:
exact ⟨y, yt, edist_le_diam_of_mem (subset_union_left hz) (subset_union_right yt)⟩

Result:
no goals
-- Mathlib/Data/Prod/Basic.lean
theorem map_injective [Nonempty α] [Nonempty β] {f : α → γ} {g : β → δ} :
    Injective (map f g) ↔ Injective f ∧ Injective g :=
  ⟨fun h =>
    ⟨fun a₁ a₂ ha => by
      inhabit β
      injection
        @h (a₁, default) (a₂, default) (congr_arg (fun c : γ => Prod.mk c (g default)) ha :),
      fun b₁ b₂ hb => by
      inhabit α
      injection @h (default, b₁) (default, b₂) (congr_arg (Prod.mk (f default)) hb :)⟩,
    fun h => h.1.prodMap h.2⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
a₁ a₂ : α
ha : f a₁ = f a₂
⊢ a₁ = a₂

Tactic:
inhabit β

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
a₁ a₂ : α
ha : f a₁ = f a₂
inhabited_h : Inhabited β
⊢ a₁ = a₂

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
a₁ a₂ : α
ha : f a₁ = f a₂
inhabited_h : Inhabited β
⊢ a₁ = a₂

Tactic:
injection
  @h (a₁, default) (a₂, default) (congr_arg (fun c : γ => Prod.mk c (g default)) ha :)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
b₁ b₂ : β
hb : g b₁ = g b₂
⊢ b₁ = b₂

Tactic:
inhabit α

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
b₁ b₂ : β
hb : g b₁ = g b₂
inhabited_h : Inhabited α
⊢ b₁ = b₂

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
b₁ b₂ : β
hb : g b₁ = g b₂
inhabited_h : Inhabited α
⊢ b₁ = b₂

Tactic:
injection @h (default, b₁) (default, b₂) (congr_arg (Prod.mk (f default)) hb :)

Result:
no goals
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upperCrossingTime_eq_of_upcrossingsBefore_lt (hab : a < b)
    (hn : upcrossingsBefore a b f N ω < n) : upperCrossingTime a b f N n ω = N

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upcrossingsBefore a b f N ω < n
⊢ upperCrossingTime a b f N n ω = N

Tactic:
refine le_antisymm upperCrossingTime_le (not_lt.1 ?_)

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upcrossingsBefore a b f N ω < n
⊢ ¬upperCrossingTime a b f N n ω < N

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upcrossingsBefore a b f N ω < n
⊢ ¬upperCrossingTime a b f N n ω < N

Tactic:
convert not_mem_of_csSup_lt hn (upperCrossingTime_lt_bddAbove hab) using 1

Result:
no goals
-- Mathlib/Analysis/Complex/AbelLimit.lean
/-- Auxiliary lemma for Abel's limit theorem. The difference between the sum `l` at 1 and the
power series's value at a point `z` away from 1 can be rewritten as `1 - z` times a power series
whose coefficients are tail sums of `l`. -/
lemma abel_aux (h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)) {z : ℂ} (hz : ‖z‖ < 1) :
    Tendsto (fun n ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i)
      atTop (𝓝 (l - ∑' n, f n * z ^ n))

Proof state:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i
k :
  Tendsto (fun n => (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
this :
  Tendsto (fun n => (1 - z) * ∑ i ∈ range n, (l - ∑ k ∈ range (i + 1), f k) * z ^ i) atTop
    (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
⊢ Tendsto (fun n => (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop
    (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))

Tactic:
rwa [mul_zero, zero_add] at this

Result:
no goals

Proof state:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i
k :
  Tendsto (fun n => (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
this :
  Tendsto
    (fun x =>
      (1 - z) * ∑ i ∈ range x, (l - s x) * z ^ i +
        (1 - z) * ∑ j ∈ range x, (∑ k ∈ range x, f k - ∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
⊢ Tendsto (fun n => (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop
    (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))

Tactic:
conv at this =>
  enter [1, n]
  rw [← mul_add, ← sum_add_distrib]
  enter [2, 2, i]
  rw [← add_mul, sub_add_sub_cancel]

Result:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i
k :
  Tendsto (fun n => (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
this :
  Tendsto (fun n => (1 - z) * ∑ i ∈ range n, (l - ∑ k ∈ range (i + 1), f k) * z ^ i) atTop
    (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
⊢ Tendsto (fun n => (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop
    (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))
-- Mathlib/Algebra/Category/ModuleCat/Subobject.lean
theorem toKernelSubobject_arrow {M N : ModuleCat R} {f : M ⟶ N} (x : LinearMap.ker f.hom) :
    (kernelSubobject f).arrow (toKernelSubobject x) = x.1

Proof state:
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
x : ↥(LinearMap.ker (Hom.hom f))
⊢ (ConcreteCategory.hom (kernelSubobject f).arrow) (toKernelSubobject x) = ↑x

Tactic:
simp [toKernelSubobject, -hom_comp, ← ConcreteCategory.comp_apply]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem Submodule.orthogonal_eq_bot_iff [HasOrthogonalProjection K] : Kᗮ = ⊥ ↔ K = ⊤

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
⊢ Kᗮ = ⊥ → K = ⊤

Tactic:
intro h

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
h : Kᗮ = ⊥
⊢ K = ⊤

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
h : K = ⊤
⊢ Kᗮ = ⊥

Tactic:
rw [h, Submodule.top_orthogonal_eq_bot]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
h : Kᗮ = ⊥
⊢ K = ⊤

Tactic:
have : K ⊔ Kᗮ = ⊤ := Submodule.sup_orthogonal_of_completeSpace

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
h : Kᗮ = ⊥
this : K ⊔ Kᗮ = ⊤
⊢ K = ⊤

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
h : Kᗮ = ⊥
this : K ⊔ Kᗮ = ⊤
⊢ K = ⊤

Tactic:
rwa [h, sup_comm, bot_sup_eq] at this

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
⊢ Kᗮ = ⊥ ↔ K = ⊤

Tactic:
refine ⟨?_, fun h => by rw [h, Submodule.top_orthogonal_eq_bot]⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
⊢ Kᗮ = ⊥ → K = ⊤
-- Mathlib/Order/Filter/Ker.lean
theorem ker_sup (f g : Filter α) : ker (f ⊔ g) = ker f ∪ ker g

Proof state:
α : Type u_2
f g : Filter α
⊢ (f ⊔ g).ker = f.ker ∪ g.ker

Tactic:
rw [← sSup_pair, ker_sSup, biUnion_pair]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
lemma map_polynomial : (W'.map f).toJacobian.polynomial = MvPolynomial.map f W'.polynomial

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
⊢ (map W' f).toJacobian.polynomial = (MvPolynomial.map f) W'.polynomial

Tactic:
simp only [polynomial]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
⊢ X y ^ 2 + C (map W' f).toJacobian.a₁ * X x * X y * X z + C (map W' f).toJacobian.a₃ * X y * X z ^ 3 -
      (X x ^ 3 + C (map W' f).toJacobian.a₂ * X x ^ 2 * X z ^ 2 + C (map W' f).toJacobian.a₄ * X x * X z ^ 4 +
        C (map W' f).toJacobian.a₆ * X z ^ 6) =
    (MvPolynomial.map f)
      (X y ^ 2 + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 3 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z ^ 2 + C W'.a₄ * X x * X z ^ 4 + C W'.a₆ * X z ^ 6))

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
⊢ X y ^ 2 + C (map W' f).toJacobian.a₁ * X x * X y * X z + C (map W' f).toJacobian.a₃ * X y * X z ^ 3 -
      (X x ^ 3 + C (map W' f).toJacobian.a₂ * X x ^ 2 * X z ^ 2 + C (map W' f).toJacobian.a₄ * X x * X z ^ 4 +
        C (map W' f).toJacobian.a₆ * X z ^ 6) =
    (MvPolynomial.map f)
      (X y ^ 2 + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 3 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z ^ 2 + C W'.a₄ * X x * X z ^ 4 + C W'.a₆ * X z ^ 6))

Tactic:
map_simp

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
/-- Variant of `Nat.lt_div_iff_mul_lt` that assumes `d ∣ n`. -/
protected lemma lt_div_iff_mul_lt' (hdn : d ∣ n) (a : ℕ) : a < n / d ↔ d * a < n

Proof state:
case inr
d n : ℕ
hdn : d ∣ n
a : ℕ
hd : d > 0
⊢ a < n / d ↔ d * a < n

Tactic:
rw [← Nat.mul_lt_mul_left hd, ← Nat.eq_mul_of_div_eq_right hdn rfl]

Result:
no goals

Proof state:
case inl
n a : ℕ
hdn : 0 ∣ n
⊢ a < n / 0 ↔ 0 * a < n

Tactic:
simp [Nat.zero_dvd.1 hdn]

Result:
no goals

Proof state:
d n : ℕ
hdn : d ∣ n
a : ℕ
⊢ a < n / d ↔ d * a < n

Tactic:
obtain rfl | hd := d.eq_zero_or_pos

Result:
case inl
n a : ℕ
hdn : 0 ∣ n
⊢ a < n / 0 ↔ 0 * a < n

case inr
d n : ℕ
hdn : d ∣ n
a : ℕ
hd : d > 0
⊢ a < n / d ↔ d * a < n
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem le_opNorm_of_le {c : ℝ} {x} (h : ‖x‖ ≤ c) : ‖f x‖ ≤ ‖f‖ * c :=
  le_trans (f.le_opNorm x) (by gcongr; exact f.opNorm_nonneg)

Proof state:
case a0
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
c : ℝ
x : V₁
h : ‖x‖ ≤ c
⊢ 0 ≤ ‖f‖

Tactic:
exact f.opNorm_nonneg

Result:
no goals

Proof state:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
c : ℝ
x : V₁
h : ‖x‖ ≤ c
⊢ ‖f‖ * ‖x‖ ≤ ‖f‖ * c

Tactic:
gcongr

Result:
case a0
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
c : ℝ
x : V₁
h : ‖x‖ ≤ c
⊢ 0 ≤ ‖f‖
-- Mathlib/Algebra/Ring/Hom/Defs.lean
theorem codomain_trivial_iff_map_one_eq_zero : (0 : β) = 1 ↔ f 1 = 0

Proof state:
α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
⊢ 0 = 1 ↔ f 1 = 0

Tactic:
rw [map_one, eq_comm]

Result:
no goals
-- Mathlib/Data/Nat/Fib/Basic.lean
theorem fib_gcd (m n : ℕ) : fib (gcd m n) = gcd (fib m) (fib n)

Proof state:
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
⊢ fib (m.gcd n) = (fib m).gcd (fib (n % m + n / m * m))

Tactic:
rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _]

Result:
no goals

Proof state:
case H1
m n : ℕ
a✝ : 0 < m
h' : fib ((n % m).gcd m) = (fib (n % m)).gcd (fib m)
⊢ fib (m.gcd n) = (fib m).gcd (fib n)

Tactic:
rw [← gcd_rec m n] at h'

Result:
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
⊢ fib (m.gcd n) = (fib m).gcd (fib n)

Proof state:
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
⊢ fib (m.gcd n) = (fib m).gcd (fib n)

Tactic:
conv_rhs => rw [← mod_add_div' n m]

Result:
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
⊢ fib (m.gcd n) = (fib m).gcd (fib (n % m + n / m * m))

Proof state:
case H0
n✝ : ℕ
⊢ fib (gcd 0 n✝) = (fib 0).gcd (fib n✝)

Tactic:
simp

Result:
no goals

Proof state:
m n : ℕ
⊢ fib (m.gcd n) = (fib m).gcd (fib n)

Tactic:
induction m, n using Nat.gcd.induction with
| H0 => simp
| H1 m n _ h' =>
  rw [← gcd_rec m n] at h'
  conv_rhs => rw [← mod_add_div' n m]
  rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _]

Result:
no goals
-- Mathlib/RingTheory/Norm/Basic.lean
theorem norm_zero [Nontrivial S] [Module.Free R S] [Module.Finite R S] : norm R (0 : S) = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : Algebra R S
inst✝² : Nontrivial S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
⊢ (norm R) 0 = 0

Tactic:
nontriviality

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : Algebra R S
inst✝² : Nontrivial S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a✝ : Nontrivial R
⊢ (norm R) 0 = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : Algebra R S
inst✝² : Nontrivial S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a✝ : Nontrivial R
⊢ (norm R) 0 = 0

Tactic:
rw [norm_apply, coe_lmul_eq_mul, map_zero, LinearMap.det_zero' (Module.Free.chooseBasis R S)]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem zero {m : MeasurableSpace α} (μ : Measure α) (hC : 0 ≤ C) :
    DominatedFinMeasAdditive μ (0 : Set α → β) C

Proof state:
α : Type u_1
β : Type u_7
inst✝ : SeminormedAddCommGroup β
C : ℝ
m : MeasurableSpace α
μ : Measure α
hC : 0 ≤ C
s : Set α
x✝¹ : MeasurableSet s
x✝ : μ s < ⊤
⊢ 0 ≤ C * (μ s).toReal

Tactic:
exact mul_nonneg hC toReal_nonneg

Result:
no goals

Proof state:
α : Type u_1
β : Type u_7
inst✝ : SeminormedAddCommGroup β
C : ℝ
m : MeasurableSpace α
μ : Measure α
hC : 0 ≤ C
⊢ DominatedFinMeasAdditive μ 0 C

Tactic:
refine ⟨FinMeasAdditive.zero, fun s _ _ => ?_⟩

Result:
α : Type u_1
β : Type u_7
inst✝ : SeminormedAddCommGroup β
C : ℝ
m : MeasurableSpace α
μ : Measure α
hC : 0 ≤ C
s : Set α
x✝¹ : MeasurableSet s
x✝ : μ s < ⊤
⊢ ‖0 s‖ ≤ C * (μ s).toReal

Proof state:
α : Type u_1
β : Type u_7
inst✝ : SeminormedAddCommGroup β
C : ℝ
m : MeasurableSpace α
μ : Measure α
hC : 0 ≤ C
s : Set α
x✝¹ : MeasurableSet s
x✝ : μ s < ⊤
⊢ ‖0 s‖ ≤ C * (μ s).toReal

Tactic:
rw [Pi.zero_apply, norm_zero]

Result:
α : Type u_1
β : Type u_7
inst✝ : SeminormedAddCommGroup β
C : ℝ
m : MeasurableSpace α
μ : Measure α
hC : 0 ≤ C
s : Set α
x✝¹ : MeasurableSet s
x✝ : μ s < ⊤
⊢ 0 ≤ C * (μ s).toReal
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem pair_preimage_singleton (f : α →ₛ β) (g : α →ₛ γ) (b : β) (c : γ) :
    pair f g ⁻¹' {(b, c)} = f ⁻¹' {b} ∩ g ⁻¹' {c}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
f : α →ₛ β
g : α →ₛ γ
b : β
c : γ
⊢ ⇑(f.pair g) ⁻¹' {(b, c)} = ⇑f ⁻¹' {b} ∩ ⇑g ⁻¹' {c}

Tactic:
rw [← singleton_prod_singleton]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
f : α →ₛ β
g : α →ₛ γ
b : β
c : γ
⊢ ⇑(f.pair g) ⁻¹' {b} ×ˢ {c} = ⇑f ⁻¹' {b} ∩ ⇑g ⁻¹' {c}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
f : α →ₛ β
g : α →ₛ γ
b : β
c : γ
⊢ ⇑(f.pair g) ⁻¹' {b} ×ˢ {c} = ⇑f ⁻¹' {b} ∩ ⇑g ⁻¹' {c}

Tactic:
exact pair_preimage _ _ _ _

Result:
no goals
-- Mathlib/CategoryTheory/Enriched/Ordinary/Basic.lean
@[simp, reassoc]
lemma eHomWhiskerLeft_comp (X : C) {Y Y' Y'' : C} (g : Y ⟶ Y') (g' : Y' ⟶ Y'') :
    eHomWhiskerLeft V X (g ≫ g') = eHomWhiskerLeft V X g ≫ eHomWhiskerLeft V X g'

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ eHomWhiskerLeft V X (g ≫ g') = eHomWhiskerLeft V X g ≫ eHomWhiskerLeft V X g'

Tactic:
dsimp [eHomWhiskerLeft]

Result:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (EnrichedCategory.Hom X Y)).inv ≫ EnrichedCategory.Hom X Y ◁ (eHomEquiv V) (g ≫ g') ≫ eComp V X Y Y'' =
    ((ρ_ (EnrichedCategory.Hom X Y)).inv ≫ EnrichedCategory.Hom X Y ◁ (eHomEquiv V) g ≫ eComp V X Y Y') ≫
      (ρ_ (EnrichedCategory.Hom X Y')).inv ≫ EnrichedCategory.Hom X Y' ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (EnrichedCategory.Hom X Y)).inv ≫ EnrichedCategory.Hom X Y ◁ (eHomEquiv V) (g ≫ g') ≫ eComp V X Y Y'' =
    ((ρ_ (EnrichedCategory.Hom X Y)).inv ≫ EnrichedCategory.Hom X Y ◁ (eHomEquiv V) g ≫ eComp V X Y Y') ≫
      (ρ_ (EnrichedCategory.Hom X Y')).inv ≫ EnrichedCategory.Hom X Y' ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''

Tactic:
rw [assoc, assoc, eHomEquiv_comp, MonoidalCategory.whiskerLeft_comp_assoc,
  MonoidalCategory.whiskerLeft_comp_assoc, ← e_assoc, tensorHom_def,
  MonoidalCategory.whiskerRight_id_assoc, MonoidalCategory.whiskerLeft_comp_assoc,
  MonoidalCategory.whiskerLeft_comp_assoc, MonoidalCategory.whiskerLeft_comp_assoc,
  whiskerLeft_rightUnitor_assoc, whiskerLeft_rightUnitor_inv_assoc,
  triangle_assoc_comp_left_inv_assoc, MonoidalCategory.whiskerRight_id_assoc,
  Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc,
  associator_inv_naturality_right_assoc, Iso.hom_inv_id_assoc,
  whisker_exchange_assoc, MonoidalCategory.whiskerRight_id_assoc, Iso.inv_hom_id_assoc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem union_zeroLocus (s s' : Set A) :
    zeroLocus 𝒜 s ∪ zeroLocus 𝒜 s' = zeroLocus 𝒜 (Ideal.span s ⊓ Ideal.span s' : Ideal A)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s s' : Set A
⊢ zeroLocus 𝒜 s ∪ zeroLocus 𝒜 s' = zeroLocus 𝒜 ↑(Ideal.span s ⊓ Ideal.span s')

Tactic:
rw [zeroLocus_inf]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s s' : Set A
⊢ zeroLocus 𝒜 s ∪ zeroLocus 𝒜 s' = zeroLocus 𝒜 ↑(Ideal.span s) ∪ zeroLocus 𝒜 ↑(Ideal.span s')

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s s' : Set A
⊢ zeroLocus 𝒜 s ∪ zeroLocus 𝒜 s' = zeroLocus 𝒜 ↑(Ideal.span s) ∪ zeroLocus 𝒜 ↑(Ideal.span s')

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem Sorted.decide [DecidableRel r] (l : List α) (h : Sorted r l) :
    Sorted (fun a b => decide (r a b) = true) l

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
h✝ : Sorted r l
a b : α
h : r a b
⊢ Decidable.decide (r a b) = true

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
h : Sorted r l
⊢ Sorted (fun a b => Decidable.decide (r a b) = true) l

Tactic:
refine h.imp fun {a b} h => by simpa using h

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
@[simp] lemma pow_eq_zero_iff (hn : n ≠ 0) : a ^ n = 0 ↔ a = 0 :=
  ⟨pow_eq_zero, by rintro rfl; exact zero_pow hn⟩

Proof state:
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
a : M₀
n : ℕ
inst✝ : NoZeroDivisors M₀
hn : n ≠ 0
⊢ a = 0 → a ^ n = 0

Tactic:
rintro rfl

Result:
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
n : ℕ
inst✝ : NoZeroDivisors M₀
hn : n ≠ 0
⊢ 0 ^ n = 0

Proof state:
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
n : ℕ
inst✝ : NoZeroDivisors M₀
hn : n ≠ 0
⊢ 0 ^ n = 0

Tactic:
exact zero_pow hn

Result:
no goals