harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Metrizable/Uniformity.lean
theorem UniformSpace.metrizableSpace [UniformSpace X] [IsCountablyGenerated (𝓤 X)] [T0Space X] :
    TopologicalSpace.MetrizableSpace X

Proof state:
X : Type u_1
inst✝² : UniformSpace X
inst✝¹ : (𝓤 X).IsCountablyGenerated
inst✝ : T0Space X
this : MetricSpace X := UniformSpace.metricSpace X
⊢ TopologicalSpace.MetrizableSpace X

Tactic:
infer_instance

Result:
no goals

Proof state:
X : Type u_1
inst✝² : UniformSpace X
inst✝¹ : (𝓤 X).IsCountablyGenerated
inst✝ : T0Space X
⊢ TopologicalSpace.MetrizableSpace X

Tactic:
letI := UniformSpace.metricSpace X

Result:
X : Type u_1
inst✝² : UniformSpace X
inst✝¹ : (𝓤 X).IsCountablyGenerated
inst✝ : T0Space X
this : MetricSpace X := UniformSpace.metricSpace X
⊢ TopologicalSpace.MetrizableSpace X
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Basic.lean
theorem seq_eq_bind {α β : Type u} [Monad m] [LawfulMonad m] (mf : m (α → β)) (x : m α) : mf <*> x = mf >>= fun f => f <$> x

Proof state:
m : Type u → Type u_1
α β : Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
mf : m (α → β)
x : m α
⊢ mf <*> x = do
    let f ← mf
    f <$> x

Tactic:
rw [bind_map]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Yoneda/Injective.lean
theorem injective_iff_preservesEpimorphisms_preadditive_yoneda_obj' (J : C) :
    Injective J ↔ (preadditiveYonedaObj J).PreservesEpimorphisms

Proof state:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
h : (preadditiveYonedaObj J ⋙ forget (ModuleCat (End J))).PreservesEpimorphisms
⊢ (preadditiveYonedaObj J).PreservesEpimorphisms

Tactic:
exact
  Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveYonedaObj J) (forget _)

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Injective J ↔ (preadditiveYonedaObj J).PreservesEpimorphisms

Tactic:
rw [injective_iff_preservesEpimorphisms_yoneda_obj]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ (yoneda.obj J).PreservesEpimorphisms ↔ (preadditiveYonedaObj J).PreservesEpimorphisms

Proof state:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ (preadditiveYonedaObj J).PreservesEpimorphisms → (yoneda.obj J).PreservesEpimorphisms

Tactic:
intro

Result:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
a✝ : (preadditiveYonedaObj J).PreservesEpimorphisms
⊢ (yoneda.obj J).PreservesEpimorphisms

Proof state:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
a✝ : (preadditiveYonedaObj J).PreservesEpimorphisms
⊢ (yoneda.obj J).PreservesEpimorphisms

Tactic:
exact (inferInstance : (preadditiveYonedaObj J ⋙ forget _).PreservesEpimorphisms)

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ (yoneda.obj J).PreservesEpimorphisms ↔ (preadditiveYonedaObj J).PreservesEpimorphisms

Tactic:
refine ⟨fun h : (preadditiveYonedaObj J ⋙ (forget <| ModuleCat (End J))).PreservesEpimorphisms =>
  ?_, ?_⟩

Result:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
h : (preadditiveYonedaObj J ⋙ forget (ModuleCat (End J))).PreservesEpimorphisms
⊢ (preadditiveYonedaObj J).PreservesEpimorphisms

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ (preadditiveYonedaObj J).PreservesEpimorphisms → (yoneda.obj J).PreservesEpimorphisms
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_sphere_of_ne_zero (x : E) {r : ℝ} (hr : r ≠ 0) : μ (sphere x r) = 0

Proof state:
case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : r ≠ 0
h : r < 0
⊢ μ (sphere x r) = 0

Tactic:
simp only [empty_diff, measure_empty, ← closedBall_diff_ball, closedBall_eq_empty.2 h]

Result:
no goals

Proof state:
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : r ≠ 0
h : 0 < r
⊢ μ (sphere x r) = 0

Tactic:
rw [← closedBall_diff_ball,
  measure_diff ball_subset_closedBall measurableSet_ball.nullMeasurableSet
    measure_ball_lt_top.ne,
  addHaar_ball_of_pos μ _ h, addHaar_closedBall μ _ h.le, tsub_self]

Result:
no goals

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
x : E
r : ℝ
hr : r ≠ 0
⊢ μ (sphere x r) = 0

Tactic:
rcases hr.lt_or_lt with (h | h)

Result:
case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : r ≠ 0
h : r < 0
⊢ μ (sphere x r) = 0

case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : r ≠ 0
h : 0 < r
⊢ μ (sphere x r) = 0
-- Mathlib/Data/Finsupp/Order.lean
theorem add_eq_zero_iff (f g : ι →₀ α) : f + g = 0 ↔ f = 0 ∧ g = 0

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
⊢ f + g = 0 ↔ f = 0 ∧ g = 0

Tactic:
simp [DFunLike.ext_iff, forall_and]

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem isPredLimit_toDual_iff : IsPredLimit (toDual a) ↔ IsSuccLimit a

Proof state:
α : Type u_1
a : α
inst✝ : Preorder α
⊢ IsPredLimit (toDual a) ↔ IsSuccLimit a

Tactic:
simp [IsSuccLimit, IsPredLimit]

Result:
no goals
-- Mathlib/Algebra/Order/Pi.lean
@[to_additive] lemma extend_le_one (hg : g ≤ 1) (he : e ≤ 1) : extend f g e ≤ 1 :=
  fun _b ↦ by classical exact dite_le_one (fun _ ↦ hg _) (fun _ ↦ he _)

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : One γ
inst✝ : LE γ
f : α → β
g : α → γ
e : β → γ
hg : g ≤ 1
he : e ≤ 1
_b : β
⊢ extend f g e _b ≤ 1 _b

Tactic:
exact dite_le_one (fun _ ↦ hg _) (fun _ ↦ he _)

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : One γ
inst✝ : LE γ
f : α → β
g : α → γ
e : β → γ
hg : g ≤ 1
he : e ≤ 1
_b : β
⊢ extend f g e _b ≤ 1 _b

Tactic:
classical exact dite_le_one (fun _ ↦ hg _) (fun _ ↦ he _)

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem le_to_int {m n : ZNum} : (m : ℤ) ≤ n ↔ m ≤ n

Proof state:
m n : ZNum
⊢ ¬↑n < ↑m ↔ m ≤ n

Tactic:
exact not_congr lt_to_int

Result:
no goals

Proof state:
m n : ZNum
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
rw [← not_lt]

Result:
m n : ZNum
⊢ ¬↑n < ↑m ↔ m ≤ n
-- Mathlib/Order/JordanHolder.lean
theorem second_iso_of_eq {x y a b : X} (hm : IsMaximal x a) (ha : x ⊔ y = a) (hb : x ⊓ y = b) :
    Iso (x, a) (b, y)

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y a b : X
hm : IsMaximal x a
ha : x ⊔ y = a
hb : x ⊓ y = b
⊢ Iso (x, a) (b, y)

Tactic:
substs a b

Result:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hm : IsMaximal x (x ⊔ y)
⊢ Iso (x, x ⊔ y) (x ⊓ y, y)

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hm : IsMaximal x (x ⊔ y)
⊢ Iso (x, x ⊔ y) (x ⊓ y, y)

Tactic:
exact second_iso hm

Result:
no goals
-- Mathlib/Analysis/Calculus/FirstDerivativeTest.lean
theorem isLocalMax_of_deriv {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b)
    (hd : ∀ᶠ x in 𝓝[≠] b, DifferentiableAt ℝ f x)
    (h₀ : ∀ᶠ x in 𝓝[<] b, 0 ≤ deriv f x) (h₁ : ∀ᶠ x in 𝓝[>] b, deriv f x ≤ 0) :
    IsLocalMax f b :=
  isLocalMax_of_deriv' h (nhdsLT_le_nhdsNE _ (by tauto)) (nhdsGT_le_nhdsNE _ (by tauto)) h₀ h₁

Proof state:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd : ∀ᶠ (x : ℝ) in 𝓝[≠] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, 0 ≤ deriv f x
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≤ 0
⊢ {x | (fun x => DifferentiableAt ℝ f x) x} ∈ 𝓝[≠] b

Tactic:
tauto

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
lemma exists_finset_linearIndependent_of_le_rank {n : ℕ} (hn : n ≤ Module.rank R M) :
    ∃ s : Finset M, s.card = n ∧ LinearIndepOn R id (s : Set M)

Proof state:
case inr.intro.intro.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this✝ :
  ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n < Module.rank R M
s : Set M
hs : #↑s = ↑n
hs' : LinearIndepOn R id s
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
exact ⟨s.toFinset, by simpa using hs, by simpa⟩

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this✝ :
  ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #↑↑⟨s, hs⟩ = ↑n
this : Finite ↑s
val✝ : Fintype ↑s
⊢ LinearIndepOn R id ↑s.toFinset

Tactic:
simpa

Result:
no goals

Proof state:
case inr.intro.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this :
  ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n < Module.rank R M
s : Set M
hs : #↑s = ↑n
hs' : LinearIndepOn R id s
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
have : Finite s := lt_aleph0_iff_finite.mp (hs ▸ nat_lt_aleph0 n)

Result:
case inr.intro.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this✝ :
  ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n < Module.rank R M
s : Set M
hs : #↑s = ↑n
hs' : LinearIndepOn R id s
this : Finite ↑s
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
have := nonempty_linearIndependent_set

Result:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this :
  ∀ (R : Type ?u.127759) (M : Type ?u.127758) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s
-- Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean
theorem tensorDistribEquiv_toLinearMap :
    (tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂)).toLinearMap = tensorDistrib R R

Proof state:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module.Free R M₁
inst✝² : Module.Finite R M₁
inst✝¹ : Module.Free R M₂
inst✝ : Module.Finite R M₂
⊢ ↑(tensorDistribEquiv R) = tensorDistrib R R

Tactic:
ext B₁ B₂ : 3

Result:
case a.h.h
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module.Free R M₁
inst✝² : Module.Finite R M₁
inst✝¹ : Module.Free R M₂
inst✝ : Module.Finite R M₂
B₁ : BilinForm R M₁
B₂ : BilinForm R M₂
⊢ ((AlgebraTensorModule.curry ↑(tensorDistribEquiv R)) B₁) B₂ = ((AlgebraTensorModule.curry (tensorDistrib R R)) B₁) B₂

Proof state:
case a.h.h
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module.Free R M₁
inst✝² : Module.Finite R M₁
inst✝¹ : Module.Free R M₂
inst✝ : Module.Finite R M₂
B₁ : BilinForm R M₁
B₂ : BilinForm R M₂
⊢ ((AlgebraTensorModule.curry ↑(tensorDistribEquiv R)) B₁) B₂ = ((AlgebraTensorModule.curry (tensorDistrib R R)) B₁) B₂

Tactic:
ext

Result:
case a.h.h.a.h.h.a.h.h
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module.Free R M₁
inst✝² : Module.Finite R M₁
inst✝¹ : Module.Free R M₂
inst✝ : Module.Finite R M₂
B₁ : BilinForm R M₁
B₂ : BilinForm R M₂
x✝³ : M₁
x✝² : M₂
x✝¹ : M₁
x✝ : M₂
⊢ ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry (((AlgebraTensorModule.curry ↑(tensorDistribEquiv R)) B₁) B₂)) x✝³) x✝²))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry (((AlgebraTensorModule.curry (tensorDistrib R R)) B₁) B₂)) x✝³) x✝²))
        x✝¹)
      x✝

Proof state:
case a.h.h.a.h.h.a.h.h
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module.Free R M₁
inst✝² : Module.Finite R M₁
inst✝¹ : Module.Free R M₂
inst✝ : Module.Finite R M₂
B₁ : BilinForm R M₁
B₂ : BilinForm R M₂
x✝³ : M₁
x✝² : M₂
x✝¹ : M₁
x✝ : M₂
⊢ ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry (((AlgebraTensorModule.curry ↑(tensorDistribEquiv R)) B₁) B₂)) x✝³) x✝²))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry (((AlgebraTensorModule.curry (tensorDistrib R R)) B₁) B₂)) x✝³) x✝²))
        x✝¹)
      x✝

Tactic:
exact mul_comm _ _

Result:
no goals
-- Mathlib/Order/Bounds/Image.lean
theorem BddBelow.bddBelow_image2_of_bddAbove :
    BddBelow s → BddAbove t → BddBelow (Set.image2 f s t)

Proof state:
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddBelow (image2 f s t)

Tactic:
exact ⟨f a b, mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds h₀ h₁ ha hb⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ BddBelow s → BddAbove t → BddBelow (image2 f s t)

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Result:
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddBelow (image2 f s t)
-- Mathlib/Computability/PostTuringMachine.lean
theorem tr_reaches {σ₁ σ₂ f₁ f₂} {tr : σ₁ → σ₂ → Prop} (H : Respects f₁ f₂ tr) {a₁ a₂}
    (aa : tr a₁ a₂) {b₁} (ab : Reaches f₁ a₁ b₁) : ∃ b₂, tr b₁ b₂ ∧ Reaches f₂ a₂ b₂

Proof state:
case inr
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ : σ₁
ab✝ : Reaches f₁ a₁ b₁
ab : TransGen (fun a b => b ∈ f₁ a) a₁ b₁
⊢ ∃ b₂, tr b₁ b₂ ∧ Reaches f₂ a₂ b₂

Tactic:
have ⟨b₂, bb, h⟩ := tr_reaches₁ H aa ab

Result:
case inr
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ : σ₁
ab✝ : Reaches f₁ a₁ b₁
ab : TransGen (fun a b => b ∈ f₁ a) a₁ b₁
b₂ : σ₂
bb : tr b₁ b₂
h : Reaches₁ f₂ a₂ b₂
⊢ ∃ b₂, tr b₁ b₂ ∧ Reaches f₂ a₂ b₂

Proof state:
case inr
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ : σ₁
ab✝ : Reaches f₁ a₁ b₁
ab : TransGen (fun a b => b ∈ f₁ a) a₁ b₁
b₂ : σ₂
bb : tr b₁ b₂
h : Reaches₁ f₂ a₂ b₂
⊢ ∃ b₂, tr b₁ b₂ ∧ Reaches f₂ a₂ b₂

Tactic:
exact ⟨b₂, bb, h.to_reflTransGen⟩

Result:
no goals

Proof state:
case inl
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₂ : σ₂
b₁ : σ₁
aa : tr b₁ a₂
ab : Reaches f₁ b₁ b₁
⊢ ∃ b₂, tr b₁ b₂ ∧ Reaches f₂ a₂ b₂

Tactic:
exact ⟨_, aa, ReflTransGen.refl⟩

Result:
no goals

Proof state:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ : σ₁
ab : Reaches f₁ a₁ b₁
⊢ ∃ b₂, tr b₁ b₂ ∧ Reaches f₂ a₂ b₂

Tactic:
rcases reflTransGen_iff_eq_or_transGen.1 ab with (rfl | ab)

Result:
case inl
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₂ : σ₂
b₁ : σ₁
aa : tr b₁ a₂
ab : Reaches f₁ b₁ b₁
⊢ ∃ b₂, tr b₁ b₂ ∧ Reaches f₂ a₂ b₂

case inr
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ : σ₁
ab✝ : Reaches f₁ a₁ b₁
ab : TransGen (fun a b => b ∈ f₁ a) a₁ b₁
⊢ ∃ b₂, tr b₁ b₂ ∧ Reaches f₂ a₂ b₂
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem sublist_flatten_of_mem {L : List (List α)} {l} (h : l ∈ L) : l <+ L.flatten

Proof state:
case nil
α : Type u_1
l : List α
h : l ∈ []
⊢ l <+ [].flatten

Tactic:
cases h

Result:
no goals

Proof state:
case cons.inl
α : Type u_1
l : List α
L : List (List α)
ih : l ∈ L → l <+ L.flatten
h : l ∈ l :: L
⊢ l <+ (l :: L).flatten

Tactic:
simp [h]

Result:
no goals

Proof state:
case cons.inr
α : Type u_1
l l' : List α
L : List (List α)
ih : l ∈ L → l <+ L.flatten
h✝ : l ∈ l' :: L
h : l ∈ L
⊢ l <+ (l' :: L).flatten

Tactic:
simp [ih h, flatten_cons, sublist_append_of_sublist_right]

Result:
no goals

Proof state:
case cons
α : Type u_1
l l' : List α
L : List (List α)
ih : l ∈ L → l <+ L.flatten
h : l ∈ l' :: L
⊢ l <+ (l' :: L).flatten

Tactic:
rcases mem_cons.1 h with (rfl | h)

Result:
case cons.inl
α : Type u_1
l : List α
L : List (List α)
ih : l ∈ L → l <+ L.flatten
h : l ∈ l :: L
⊢ l <+ (l :: L).flatten

case cons.inr
α : Type u_1
l l' : List α
L : List (List α)
ih : l ∈ L → l <+ L.flatten
h✝ : l ∈ l' :: L
h : l ∈ L
⊢ l <+ (l' :: L).flatten
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem order_neg [Zero Γ] {f : HahnSeries Γ R} : (-f).order = f.order

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : Zero Γ
f : HahnSeries Γ R
⊢ (-f).order = f.order

Tactic:
by_cases hf : f = 0

Result:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : Zero Γ
f : HahnSeries Γ R
hf : f = 0
⊢ (-f).order = f.order

case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : Zero Γ
f : HahnSeries Γ R
hf : ¬f = 0
⊢ (-f).order = f.order

Proof state:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : Zero Γ
f : HahnSeries Γ R
hf : f = 0
⊢ (-f).order = f.order

Tactic:
simp only [hf, neg_zero]

Result:
no goals

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : Zero Γ
f : HahnSeries Γ R
hf : ¬f = 0
⊢ (-f).order = f.order

Tactic:
simp only [order, support_neg, neg_eq_zero]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem prod_image_seq_comm (s : Set α) (t : Set β) :
    (Prod.mk '' s).seq t = seq ((fun b a => (a, b)) '' t) s

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ ((fun x => Prod.swap ∘ x) ∘ Prod.mk '' t).seq s = ((fun b a => (a, b)) '' t).seq s

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (Prod.mk '' s).seq t = ((fun b a => (a, b)) '' t).seq s

Tactic:
rw [← prod_eq_seq, ← image_swap_prod, prod_eq_seq, image_seq, ← image_comp]

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ ((fun x => Prod.swap ∘ x) ∘ Prod.mk '' t).seq s = ((fun b a => (a, b)) '' t).seq s
-- Mathlib/Logic/Equiv/Defs.lean
theorem trans_eq_refl_iff_symm_eq {f : α ≃ β} {g : β ≃ α} :
    f.trans g = Equiv.refl α ↔ f.symm = g

Proof state:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f = g.symm ↔ f.symm = g

Tactic:
exact ⟨fun h ↦ h ▸ rfl, fun h ↦ h ▸ rfl⟩

Result:
no goals

Proof state:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f.trans g = Equiv.refl α ↔ f.symm = g

Tactic:
rw [trans_eq_refl_iff_eq_symm]

Result:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f = g.symm ↔ f.symm = g
-- Mathlib/Data/ZMod/Basic.lean
theorem cast_zero : (cast (0 : ZMod n) : R) = 0

Proof state:
n : ℕ
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ (match (motive := (x : ℕ) → ZMod x → R) n with
      | 0 => Int.cast
      | n.succ => fun i => ↑i.val)
      0 =
    0

Tactic:
cases n

Result:
case zero
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ (match (motive := (x : ℕ) → ZMod x → R) 0 with
      | 0 => Int.cast
      | n.succ => fun i => ↑i.val)
      0 =
    0

case succ
R : Type u_1
inst✝ : AddGroupWithOne R
n✝ : ℕ
⊢ (match (motive := (x : ℕ) → ZMod x → R) n✝ + 1 with
      | 0 => Int.cast
      | n.succ => fun i => ↑i.val)
      0 =
    0

Proof state:
case succ
R : Type u_1
inst✝ : AddGroupWithOne R
n✝ : ℕ
⊢ (match (motive := (x : ℕ) → ZMod x → R) n✝ + 1 with
      | 0 => Int.cast
      | n.succ => fun i => ↑i.val)
      0 =
    0

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ cast 0 = 0

Tactic:
delta ZMod.cast

Result:
n : ℕ
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ (match (motive := (x : ℕ) → ZMod x → R) n with
      | 0 => Int.cast
      | n.succ => fun i => ↑i.val)
      0 =
    0

Proof state:
case zero
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ (match (motive := (x : ℕ) → ZMod x → R) 0 with
      | 0 => Int.cast
      | n.succ => fun i => ↑i.val)
      0 =
    0

Tactic:
exact Int.cast_zero

Result:
no goals
-- Mathlib/Data/Int/Log.lean
theorem zpow_log_le_self {b : ℕ} {r : R} (hb : 1 < b) (hr : 0 < r) : (b : R) ^ log b r ≤ r

Proof state:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ b ^ Nat.log b ⌊r⌋₊ ≤ ⌊r⌋₊

Tactic:
exact Nat.pow_log_le_self b (Nat.floor_pos.mpr hr1).ne'

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ ↑b ^ log b r ≤ r

Tactic:
rw [log_of_one_le_right _ hr1]

Result:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ ↑b ^ ↑(Nat.log b ⌊r⌋₊) ≤ r

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ ↑b ^ log b r ≤ r

Tactic:
rcases le_total 1 r with hr1 | hr1

Result:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ ↑b ^ log b r ≤ r

case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : r ≤ 1
⊢ ↑b ^ log b r ≤ r

Proof state:
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : r ≤ 1
⊢ (↑(b ^ Nat.clog b ⌈r⁻¹⌉₊))⁻¹ ≤ r

Tactic:
exact inv_le_of_inv_le₀ hr (Nat.ceil_le.1 <| Nat.le_pow_clog hb _)

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ ↑b ^ ↑(Nat.log b ⌊r⌋₊) ≤ r

Tactic:
rw [zpow_natCast, ← Nat.cast_pow, ← Nat.le_floor_iff hr.le]

Result:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ b ^ Nat.log b ⌊r⌋₊ ≤ ⌊r⌋₊

Proof state:
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : r ≤ 1
⊢ ↑b ^ log b r ≤ r

Tactic:
rw [log_of_right_le_one _ hr1, zpow_neg, zpow_natCast, ← Nat.cast_pow]

Result:
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : r ≤ 1
⊢ (↑(b ^ Nat.clog b ⌈r⁻¹⌉₊))⁻¹ ≤ r