harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/RingedSpace/Basic.lean
theorem isUnit_of_isUnit_germ (U : Opens X) (f : X.presheaf.obj (op U))
    (h : ∀ (x) (hx : x ∈ U), IsUnit (X.presheaf.germ U x hx f)) : IsUnit f

Proof state:
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : ↑(X.presheaf.obj (op U))
gl_spec : ∀ (i : ↥U), (ConcreteCategory.hom ((sheaf X).val.map (iVU i).op)) gl = g i
⊢ ∀ (i : ↥U),
    (ConcreteCategory.hom ((sheaf X).val.map (iVU i).op)) (f * gl) =
      (ConcreteCategory.hom ((sheaf X).val.map (iVU i).op)) 1

Tactic:
intro i

Result:
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : ↑(X.presheaf.obj (op U))
gl_spec : ∀ (i : ↥U), (ConcreteCategory.hom ((sheaf X).val.map (iVU i).op)) gl = g i
i : ↥U
⊢ (ConcreteCategory.hom ((sheaf X).val.map (iVU i).op)) (f * gl) =
    (ConcreteCategory.hom ((sheaf X).val.map (iVU i).op)) 1
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem mul (h : PythagoreanTriple x y z) (k : ℤ) : PythagoreanTriple (k * x) (k * y) (k * z) :=
  calc
    k * x * (k * x) + k * y * (k * y) = k ^ 2 * (x * x + y * y)

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
k : ℤ
⊢ k * x * (k * x) + k * y * (k * y) = k ^ 2 * (x * x + y * y)

Tactic:
ring

Result:
no goals

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
k : ℤ
⊢ k ^ 2 * (z * z) = k * z * (k * z)

Tactic:
ring

Result:
no goals

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
k : ℤ
⊢ k ^ 2 * (x * x + y * y) = k ^ 2 * (z * z)

Tactic:
rw [h.eq]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem compl_lt_self [Nontrivial α] : xᶜ < x ↔ x = ⊤

Proof state:
α : Type u
x : α
inst✝¹ : BooleanAlgebra α
inst✝ : Nontrivial α
⊢ xᶜ < x ↔ x = ⊤

Tactic:
simpa using lt_compl_self (a := xᶜ)

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
private lemma A_c_eq_zero {A : Δ m} (ha : A.1 1 0 = 0) : A.1 0 0 * A.1 1 1 = m

Proof state:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
ha : ↑A 1 0 = 0
⊢ ↑A 0 0 * ↑A 1 1 = m

Tactic:
simpa only [det_fin_two, ha, mul_zero, sub_zero] using A.2

Result:
no goals
-- Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
theorem uniformCauchySeqOnFilter_of_fderiv (hf' : UniformCauchySeqOnFilter f' l (𝓝 x))
    (hf : ∀ᶠ n : ι × E in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2)
    (hfg : Cauchy (map (fun n => f n x) l)) : UniformCauchySeqOnFilter f l (𝓝 x)

Proof state:
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy (map (fun n => f n x) l)
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (fun n z => f' n.1 z - f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
ε : ℝ
hε : ε > 0
t : Set G
ht : t ∈ map (fun n => f n x) l
ht' : ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
n : ι × ι
hn : (fun n => f n.1 x ∈ t ∧ f n.2 x ∈ t) n
y : E
x✝ : (fun x => True) y
⊢ dist (0 (n, y).2) (f (n, y).1.1 x - f (n, y).1.2 x) < ε

Tactic:
simpa [norm_sub_rev, dist_eq_norm] using ht' _ hn.1 _ hn.2

Result:
no goals
-- Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
theorem uniformCauchySeqOnFilter_of_fderiv (hf' : UniformCauchySeqOnFilter f' l (𝓝 x))
    (hf : ∀ᶠ n : ι × E in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2)
    (hfg : Cauchy (map (fun n => f n x) l)) : UniformCauchySeqOnFilter f l (𝓝 x)

Proof state:
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf' : UniformCauchySeqOnFilter f' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy (map (fun n => f n x) l)
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ UniformCauchySeqOnFilter f l (𝓝 x)

Tactic:
letI : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 _

Result:
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf' : UniformCauchySeqOnFilter f' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy (map (fun n => f n x) l)
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ UniformCauchySeqOnFilter f l (𝓝 x)
-- Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
theorem uniformCauchySeqOnFilter_of_fderiv (hf' : UniformCauchySeqOnFilter f' l (𝓝 x))
    (hf : ∀ᶠ n : ι × E in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2)
    (hfg : Cauchy (map (fun n => f n x) l)) : UniformCauchySeqOnFilter f l (𝓝 x)

Proof state:
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy (map (fun n => f n x) l)
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (fun n z => f' n.1 z - f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this :
  TendstoUniformlyOnFilter (fun n z => f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0 (l ×ˢ l) (𝓝 x) ∧
    TendstoUniformlyOnFilter (fun n x_1 => f n.1 x - f n.2 x) 0 (l ×ˢ l) (𝓝 x)
⊢ TendstoUniformlyOnFilter (fun n z => f n.1 z - f n.2 z) 0 (l ×ˢ l) (𝓝 x)

Tactic:
have := this.1.add this.2

Result:
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy (map (fun n => f n x) l)
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (fun n z => f' n.1 z - f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
this✝¹ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this✝ :
  TendstoUniformlyOnFilter (fun n z => f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0 (l ×ˢ l) (𝓝 x) ∧
    TendstoUniformlyOnFilter (fun n x_1 => f n.1 x - f n.2 x) 0 (l ×ˢ l) (𝓝 x)
this :
  TendstoUniformlyOnFilter ((fun n z => f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) + fun n x_1 => f n.1 x - f n.2 x)
    (0 + 0) (l ×ˢ l) (𝓝 x)
⊢ TendstoUniformlyOnFilter (fun n z => f n.1 z - f n.2 z) 0 (l ×ˢ l) (𝓝 x)
-- Mathlib/Algebra/MonoidAlgebra/Grading.lean
theorem mem_grade_iff' (m : M) (a : R[M]) :
    a ∈ grade R m ↔ a ∈ (LinearMap.range (Finsupp.lsingle m : R →ₗ[R] M →₀ R) :
      Submodule R R[M])

Proof state:
M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
⊢ (∃ b, a = Finsupp.single m b) ↔ a ∈ LinearMap.range (Finsupp.lsingle m)

Tactic:
apply exists_congr

Result:
case h
M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
⊢ ∀ (a_1 : R), a = Finsupp.single m a_1 ↔ (Finsupp.lsingle m) a_1 = a

Proof state:
case h
M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
⊢ ∀ (a_1 : R), a = Finsupp.single m a_1 ↔ (Finsupp.lsingle m) a_1 = a

Tactic:
intro r

Result:
case h
M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
r : R
⊢ a = Finsupp.single m r ↔ (Finsupp.lsingle m) r = a

Proof state:
case h
M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
r : R
⊢ a = Finsupp.single m r ↔ (Finsupp.lsingle m) r = a

Tactic:
constructor <;> exact Eq.symm

Result:
no goals

Proof state:
M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
⊢ a ∈ grade R m ↔ a ∈ LinearMap.range (Finsupp.lsingle m)

Tactic:
rw [mem_grade_iff, Finsupp.support_subset_singleton']

Result:
M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
⊢ (∃ b, a = Finsupp.single m b) ↔ a ∈ LinearMap.range (Finsupp.lsingle m)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem forall_mem_mkArray {p : α → Prop} {a : α} {n} :
    (∀ b, b ∈ mkArray n a → p b) ↔ n = 0 ∨ p a

Proof state:
α : Type u_1
p : α → Prop
a : α
n : Nat
⊢ (∀ (b : α), b ∈ mkArray n a → p b) ↔ n = 0 ∨ p a

Tactic:
cases n <;> simp [mem_mkArray]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_eq_guard_findIdx_lt {xs : List α} {p : α → Bool} :
    xs.findIdx? p = Option.guard (fun i => i < xs.length) (xs.findIdx p)

Proof state:
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h : i < xs.length ∧ findIdx p xs = i
⊢ some i = Option.guard (fun i => i < xs.length) (findIdx p xs)

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
xs : List α
p : α → Bool
⊢ findIdx? p xs = Option.guard (fun i => i < xs.length) (findIdx p xs)

Tactic:
match h : xs.findIdx? p with
| none =>
  simp only [findIdx?_eq_none_iff] at h
  simp [findIdx_eq_length_of_false h, Option.guard]
| some i =>
  simp only [findIdx?_eq_some_iff_findIdx_eq] at h
  simp [h]

Result:
no goals

Proof state:
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h : findIdx? p xs = some i
⊢ some i = Option.guard (fun i => i < xs.length) (findIdx p xs)

Tactic:
simp only [findIdx?_eq_some_iff_findIdx_eq] at h

Result:
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h : i < xs.length ∧ findIdx p xs = i
⊢ some i = Option.guard (fun i => i < xs.length) (findIdx p xs)

Proof state:
α : Type u_1
xs : List α
p : α → Bool
h : findIdx? p xs = none
⊢ none = Option.guard (fun i => i < xs.length) (findIdx p xs)

Tactic:
simp only [findIdx?_eq_none_iff] at h

Result:
α : Type u_1
xs : List α
p : α → Bool
h : ∀ (x : α), x ∈ xs → p x = false
⊢ none = Option.guard (fun i => i < xs.length) (findIdx p xs)

Proof state:
α : Type u_1
xs : List α
p : α → Bool
h : ∀ (x : α), x ∈ xs → p x = false
⊢ none = Option.guard (fun i => i < xs.length) (findIdx p xs)

Tactic:
simp [findIdx_eq_length_of_false h, Option.guard]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem eq_mk : v = Vector.mk a h ↔ v.toArray = a

Proof state:
case mk
α✝ : Type u_1
n✝ : Nat
a : Array α✝
h : a.size = n✝
toArray✝ : Array α✝
size_toArray✝ : toArray✝.size = n✝
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ } = { toArray := a, size_toArray := h } ↔
    { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray = a

Tactic:
simp

Result:
no goals

Proof state:
α✝ : Type u_1
n✝ : Nat
v : Vector α✝ n✝
a : Array α✝
h : a.size = n✝
⊢ v = { toArray := a, size_toArray := h } ↔ v.toArray = a

Tactic:
cases v

Result:
case mk
α✝ : Type u_1
n✝ : Nat
a : Array α✝
h : a.size = n✝
toArray✝ : Array α✝
size_toArray✝ : toArray✝.size = n✝
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ } = { toArray := a, size_toArray := h } ↔
    { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray = a
-- Mathlib/Data/Nat/Log.lean
theorem log_of_one_lt_of_le {b n : ℕ} (h : 1 < b) (hn : b ≤ n) : log b n = log b (n / b) + 1

Proof state:
b n : ℕ
h : 1 < b
hn : b ≤ n
⊢ (if h : b ≤ n ∧ 1 < b then log b (n / b) + 1 else 0) = log b (n / b) + 1

Tactic:
exact if_pos ⟨hn, h⟩

Result:
no goals

Proof state:
b n : ℕ
h : 1 < b
hn : b ≤ n
⊢ log b n = log b (n / b) + 1

Tactic:
rw [log]

Result:
b n : ℕ
h : 1 < b
hn : b ≤ n
⊢ (if h : b ≤ n ∧ 1 < b then log b (n / b) + 1 else 0) = log b (n / b) + 1
-- Mathlib/Order/Lattice.lean
theorem sup_assoc (a b c : α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) :=
  eq_of_forall_ge_iff fun x => by simp only [sup_le_iff]; rw [and_assoc]

Proof state:
α : Type u
inst✝ : SemilatticeSup α
a b c x : α
⊢ a ⊔ b ⊔ c ≤ x ↔ a ⊔ (b ⊔ c) ≤ x

Tactic:
simp only [sup_le_iff]

Result:
α : Type u
inst✝ : SemilatticeSup α
a b c x : α
⊢ (a ≤ x ∧ b ≤ x) ∧ c ≤ x ↔ a ≤ x ∧ b ≤ x ∧ c ≤ x

Proof state:
α : Type u
inst✝ : SemilatticeSup α
a b c x : α
⊢ (a ≤ x ∧ b ≤ x) ∧ c ≤ x ↔ a ≤ x ∧ b ≤ x ∧ c ≤ x

Tactic:
rw [and_assoc]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem Infinite.encard_eq {s : Set α} (h : s.Infinite) : s.encard = ⊤

Proof state:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ s.encard = ⊤

Tactic:
rw [encard, ENat.card_eq_top_of_infinite]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
h : s.Infinite
⊢ s.encard = ⊤

Tactic:
have := h.to_subtype

Result:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ s.encard = ⊤
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem boundary_length : c.boundary ⟨c.length, c.length_lt_card_boundaries⟩ = Fin.last n

Proof state:
n : ℕ
c : CompositionAsSet n
⊢ c.boundary ⟨c.length, ⋯⟩ = Fin.last n

Tactic:
convert Finset.orderEmbOfFin_last rfl c.card_boundaries_pos

Result:
case h.e'_3
n : ℕ
c : CompositionAsSet n
⊢ Fin.last n = c.boundaries.max' ⋯

Proof state:
case h.e'_3
n : ℕ
c : CompositionAsSet n
⊢ Fin.last n = c.boundaries.max' ⋯

Tactic:
exact le_antisymm (Finset.le_max' _ _ c.getLast_mem) (Fin.le_last _)

Result:
no goals
-- Mathlib/Topology/PartitionOfUnity.lean
theorem coe_single (i : ι) (s : Set X) : ⇑(BumpCovering.single i s) = Pi.single i 1

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
i : ι
s : Set X
⊢ ⇑(BumpCovering.single i s) = Pi.single i 1

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_reverse {l : List α} {i} (h : i < l.reverse.length) :
    l.reverse[i] = l[l.length - 1 - i]'(Nat.sub_one_sub_lt_of_lt (by simpa using h))

Proof state:
α : Type u_1
l : List α
i : Nat
h : i < l.reverse.length
⊢ i < l.length

Tactic:
simpa using h

Result:
no goals

Proof state:
case x
α : Type u_1
l : List α
i : Nat
h : i < l.reverse.length
⊢ some l.reverse[i] = some l[l.length - 1 - i]

Tactic:
rw [← getElem?_eq_getElem, ← getElem?_eq_getElem]

Result:
case x
α : Type u_1
l : List α
i : Nat
h : i < l.reverse.length
⊢ l.reverse[i]? = l[l.length - 1 - i]?

Proof state:
case x
α : Type u_1
l : List α
i : Nat
h : i < l.reverse.length
⊢ l.reverse[i]? = l[l.length - 1 - i]?

Tactic:
rw [getElem?_reverse (by simpa using h)]

Result:
no goals

Proof state:
α : Type ?u.274003
l : List α
i : Nat
h : i < l.reverse.length
⊢ i < l.length

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
l : List α
i : Nat
h : i < l.reverse.length
⊢ l.reverse[i] = l[l.length - 1 - i]

Tactic:
apply Option.some.inj

Result:
case x
α : Type u_1
l : List α
i : Nat
h : i < l.reverse.length
⊢ some l.reverse[i] = some l[l.length - 1 - i]
-- Mathlib/Algebra/Order/Group/Unbundled/Int.lean
theorem abs_le_one_iff {a : ℤ} : |a| ≤ 1 ↔ a = 0 ∨ a = 1 ∨ a = -1

Proof state:
a : ℤ
n : ℕ
⊢ n = 0 ↔ -[n+1] = 1 ∨ -[n+1] = -1

Tactic:
rw [negSucc_eq']

Result:
a : ℤ
n : ℕ
⊢ n = 0 ↔ -↑n - 1 = 1 ∨ -↑n - 1 = -1

Proof state:
a : ℤ
n : ℕ
⊢ ↑n = 0 ∨ |↑n| = 1 ↔ ↑n = 0 ∨ ↑n = 1 ∨ ↑n = -1

Tactic:
simp [abs_eq_natAbs]

Result:
no goals

Proof state:
a : ℤ
⊢ a = 0 ∨ |a| = 1 ↔ a = 0 ∨ a = 1 ∨ a = -1

Tactic:
match a with
| (n : ℕ) => simp [abs_eq_natAbs]
| -[n+1] =>
    simp only [negSucc_ne_zero, abs_eq_natAbs, natAbs_negSucc, succ_eq_add_one,
      natCast_add, Nat.cast_ofNat_Int, add_left_eq_self, natCast_eq_zero, false_or, reduceNeg]
    rw [negSucc_eq']
    omega

Result:
no goals

Proof state:
a : ℤ
⊢ |a| ≤ 1 ↔ a = 0 ∨ a = 1 ∨ a = -1

Tactic:
rw [le_iff_lt_or_eq, abs_lt_one_iff]

Result:
a : ℤ
⊢ a = 0 ∨ |a| = 1 ↔ a = 0 ∨ a = 1 ∨ a = -1

Proof state:
a : ℤ
n : ℕ
⊢ -[n+1] = 0 ∨ |-[n+1]| = 1 ↔ -[n+1] = 0 ∨ -[n+1] = 1 ∨ -[n+1] = -1

Tactic:
simp only [negSucc_ne_zero, abs_eq_natAbs, natAbs_negSucc, succ_eq_add_one,
  natCast_add, Nat.cast_ofNat_Int, add_left_eq_self, natCast_eq_zero, false_or, reduceNeg]

Result:
a : ℤ
n : ℕ
⊢ n = 0 ↔ -[n+1] = 1 ∨ -[n+1] = -1

Proof state:
a : ℤ
n : ℕ
⊢ n = 0 ↔ -↑n - 1 = 1 ∨ -↑n - 1 = -1

Tactic:
omega

Result:
no goals
-- Mathlib/SetTheory/Surreal/Dyadic.lean
theorem birthday_half : birthday (powHalf 1) = 2

Proof state:
⊢ ((Ordinal.lsub fun i => ((powHalf 1).moveLeft i).birthday) ⊔
      Ordinal.lsub fun i => ((powHalf 1).moveRight i).birthday) =
    2

Tactic:
simp

Result:
no goals

Proof state:
⊢ (powHalf 1).birthday = 2

Tactic:
rw [birthday_def]

Result:
⊢ ((Ordinal.lsub fun i => ((powHalf 1).moveLeft i).birthday) ⊔
      Ordinal.lsub fun i => ((powHalf 1).moveRight i).birthday) =
    2
-- Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
theorem involute_eq_of_mem_even {x : CliffordAlgebra Q} (h : x ∈ evenOdd Q 0) : involute x = x

Proof state:
case ι_mul_ι_mul
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : CliffordAlgebra Q
m₁ m₂ : M
x : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 0
ihx : involute x = x
⊢ involute ((ι Q) m₁ * (ι Q) m₂ * x) = (ι Q) m₁ * (ι Q) m₂ * x

Tactic:
rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg]

Result:
no goals

Proof state:
case algebraMap
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
r : R
⊢ involute ((algebraMap R (CliffordAlgebra Q)) r) = (algebraMap R (CliffordAlgebra Q)) r

Tactic:
exact AlgHom.commutes _ _

Result:
no goals

Proof state:
case add
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ x y : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 0
_hy : y ∈ evenOdd Q 0
ihx : involute x = x
ihy : involute y = y
⊢ involute (x + y) = x + y

Tactic:
rw [map_add, ihx, ihy]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
h : x ∈ evenOdd Q 0
⊢ involute x = x

Tactic:
induction x, h using even_induction with
| algebraMap r => exact AlgHom.commutes _ _
| add x y _hx _hy ihx ihy =>
  rw [map_add, ihx, ihy]
| ι_mul_ι_mul m₁ m₂ x _hx ihx =>
  rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem prod_normalizedFactors_eq {a : α} (ane0 : a ≠ 0) :
    (normalizedFactors a).prod = normalize a

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ normalize (normalizedFactors a).prod = normalize a

Tactic:
exact normalize_eq_normalize_iff.mpr (dvd_dvd_iff_associated.mpr (prod_normalizedFactors ane0))

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (normalizedFactors a).prod = normalize (normalizedFactors a).prod

Tactic:
rw [normalizedFactors, ← map_multiset_prod, normalize_idem]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (normalizedFactors a).prod = normalize a

Tactic:
trans normalize (normalizedFactors a).prod

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (normalizedFactors a).prod = normalize (normalizedFactors a).prod

α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ normalize (normalizedFactors a).prod = normalize a
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma coverEntropyEntourage_le_log_coverMincard_div {T : X → X} {F : Set X} (F_inv : MapsTo T F F)
    {U : Set (X × X)} (U_symm : SymmetricRel U) {n : ℕ} (n_pos : 0 < n) :
    coverEntropyEntourage T F (U ○ U) ≤ log (coverMincard T F U n) / n

Proof state:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
rcases eq_or_ne (log (coverMincard T F U n)) ⊥ with logm_bot | logm_nneg

Result:
case inl
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_bot : (↑(coverMincard T F U n)).log = ⊥
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

case inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n
-- Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean
theorem lift_lift_assoc {A : C} {B : Mon_ C} (f g h : A ⟶ B.X) :
    lift (lift f g ≫ B.mul) h ≫ B.mul = lift f (lift g h ≫ B.mul) ≫ B.mul

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Mon_ C
f g h : A ⟶ B.X
this : lift (lift f g) h ≫ B.mul ▷ B.X ≫ B.mul = lift (lift f g) h ≫ (α_ B.X B.X B.X).hom ≫ B.X ◁ B.mul ≫ B.mul
⊢ lift (lift f g ≫ B.mul) h ≫ B.mul = lift f (lift g h ≫ B.mul) ≫ B.mul

Tactic:
rwa [lift_whiskerRight_assoc, lift_lift_associator_hom_assoc, lift_whiskerLeft_assoc] at this

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Mon_ C
f g h : A ⟶ B.X
⊢ lift (lift f g ≫ B.mul) h ≫ B.mul = lift f (lift g h ≫ B.mul) ≫ B.mul

Tactic:
have := lift (lift f g) h ≫= B.mul_assoc

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Mon_ C
f g h : A ⟶ B.X
this : lift (lift f g) h ≫ B.mul ▷ B.X ≫ B.mul = lift (lift f g) h ≫ (α_ B.X B.X B.X).hom ≫ B.X ◁ B.mul ≫ B.mul
⊢ lift (lift f g ≫ B.mul) h ≫ B.mul = lift f (lift g h ≫ B.mul) ≫ B.mul