harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/OfFn.lean
theorem mem_ofFn {n} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ ∃ i, f i = a

Proof state:
case mp
α : Type u_1
n : Nat
f : Fin n → α
a : α
⊢ a ∈ ofFn f → ∃ i, f i = a

Tactic:
intro w

Result:
case mp
α : Type u_1
n : Nat
f : Fin n → α
a : α
w : a ∈ ofFn f
⊢ ∃ i, f i = a

Proof state:
case mp
α : Type u_1
n : Nat
f : Fin n → α
a : α
w : a ∈ ofFn f
⊢ ∃ i, f i = a

Tactic:
obtain ⟨i, h, rfl⟩ := getElem_of_mem w

Result:
case mp.intro.intro
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
h : i < n
w : (ofFn f)[i] ∈ ofFn f
⊢ ∃ i_1, f i_1 = (ofFn f)[i]

Proof state:
case mpr.intro
α : Type u_1
n : Nat
f : Fin n → α
i : Fin n
⊢ f i ∈ ofFn f

Tactic:
apply mem_of_getElem (i := i) <;> simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
h : i < n
w : (ofFn f)[i] ∈ ofFn f
⊢ i < n

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
h : i < n
w : (ofFn f)[i] ∈ ofFn f
⊢ f ⟨i, h⟩ = (ofFn f)[i]

Tactic:
simp

Result:
no goals

Proof state:
case mp.intro.intro
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
h : i < n
w : (ofFn f)[i] ∈ ofFn f
⊢ ∃ i_1, f i_1 = (ofFn f)[i]

Tactic:
exact ⟨⟨i, by simpa using h⟩, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
a : α
⊢ a ∈ ofFn f ↔ ∃ i, f i = a

Tactic:
constructor

Result:
case mp
α : Type u_1
n : Nat
f : Fin n → α
a : α
⊢ a ∈ ofFn f → ∃ i, f i = a

case mpr
α : Type u_1
n : Nat
f : Fin n → α
a : α
⊢ (∃ i, f i = a) → a ∈ ofFn f

Proof state:
case mpr
α : Type u_1
n : Nat
f : Fin n → α
a : α
⊢ (∃ i, f i = a) → a ∈ ofFn f

Tactic:
rintro ⟨i, rfl⟩

Result:
case mpr.intro
α : Type u_1
n : Nat
f : Fin n → α
i : Fin n
⊢ f i ∈ ofFn f
-- Mathlib/Order/WithBot.lean
lemma untop_le_iff (hx : x ≠ ⊤) : untop x hx ≤ b ↔ x ≤ b

Proof state:
α : Type u_1
b : α
inst✝ : LE α
x : WithTop α
hx : x ≠ ⊤
⊢ x.untop hx ≤ b ↔ x ≤ ↑b

Tactic:
lift x to α using id hx

Result:
case intro
α : Type u_1
b : α
inst✝ : LE α
x : α
hx : ↑x ≠ ⊤
⊢ (↑x).untop hx ≤ b ↔ ↑x ≤ ↑b

Proof state:
case intro
α : Type u_1
b : α
inst✝ : LE α
x : α
hx : ↑x ≠ ⊤
⊢ (↑x).untop hx ≤ b ↔ ↑x ≤ ↑b

Tactic:
simp

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma not_coe_le_bot (a : α) : ¬(a : WithBot α) ≤ ⊥

Proof state:
α : Type u_1
inst✝ : LE α
a : α
⊢ ¬↑a ≤ ⊥

Tactic:
simp [le_def]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycleOn.zpow_apply_eq_zpow_apply {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s)
    {m n : ℤ} : (f ^ m) a = (f ^ n) a ↔ m ≡ n [ZMOD #s]

Proof state:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
m n : ℤ
⊢ (f ^ m) a = (f ^ n) a ↔ (f ^ (n - m)) a = a

Tactic:
simp [sub_eq_neg_add, zpow_add, eq_inv_iff_eq, eq_comm]

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
m n : ℤ
⊢ (f ^ m) a = (f ^ n) a ↔ m ≡ n [ZMOD ↑(#s)]

Tactic:
rw [Int.modEq_iff_dvd, ← hf.zpow_apply_eq ha]

Result:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
m n : ℤ
⊢ (f ^ m) a = (f ^ n) a ↔ (f ^ (n - m)) a = a
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_sqrt_one_sub_sq : ∫ x in (-1 : ℝ)..1, √(1 - x ^ 2 : ℝ) = π / 2 :=
  calc
    _ = ∫ x in sin (-(π / 2)).. sin (π / 2), √(1 - x ^ 2 : ℝ)

Proof state:
⊢ Continuous fun x => √(1 - x ^ 2)

Tactic:
fun_prop

Result:
no goals

Proof state:
x✝ : ℝ
h : -(π / 2) < x✝ ∧ x✝ ≤ π / 2
⊢ √(1 - sin x✝ ^ 2) * cos x✝ = cos x✝ ^ 2

Tactic:
rw [← Real.cos_eq_sqrt_one_sub_sin_sq (le_of_lt h.1) h.2, pow_two]

Result:
no goals

Proof state:
x✝ : ℝ
h : x✝ ∈ Ι (-(π / 2)) (π / 2)
⊢ √(1 - sin x✝ ^ 2) * cos x✝ = cos x✝ ^ 2

Tactic:
rw [uIoc_of_le (neg_le_self (le_of_lt (half_pos Real.pi_pos))), Set.mem_Ioc] at h

Result:
x✝ : ℝ
h : -(π / 2) < x✝ ∧ x✝ ≤ π / 2
⊢ √(1 - sin x✝ ^ 2) * cos x✝ = cos x✝ ^ 2

Proof state:
⊢ ∫ (x : ℝ) in -1 ..1, √(1 - x ^ 2) = ∫ (x : ℝ) in sin (-(π / 2))..sin (π / 2), √(1 - x ^ 2)

Tactic:
rw [sin_neg, sin_pi_div_two]

Result:
no goals

Proof state:
⊢ ∫ (x : ℝ) in -(π / 2)..π / 2, √(1 - sin x ^ 2) * cos x = ∫ (x : ℝ) in -(π / 2)..π / 2, cos x ^ 2

Tactic:
refine integral_congr_ae (MeasureTheory.ae_of_all _ fun _ h => ?_)

Result:
x✝ : ℝ
h : x✝ ∈ Ι (-(π / 2)) (π / 2)
⊢ √(1 - sin x✝ ^ 2) * cos x✝ = cos x✝ ^ 2

Proof state:
⊢ ∫ (x : ℝ) in -(π / 2)..π / 2, cos x ^ 2 = π / 2

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Quiver/ReflQuiver.lean
theorem ext {V : Type u} [ReflQuiver.{v₁} V] {W : Type u₂} [ReflQuiver.{v₂} W]
    {F G : ReflPrefunctor V W}
    (h_obj : ∀ X, F.obj X = G.obj X)
    (h_map : ∀ (X Y : V) (f : X ⟶ Y),
      F.map f = Eq.recOn (h_obj Y).symm (Eq.recOn (h_obj X).symm (G.map f))) : F = G

Proof state:
case mk.mk.mk.mk.e_toPrefunctor.e_map.h.h.h
V : Type u
inst✝¹ : ReflQuiver V
W : Type u₂
inst✝ : ReflQuiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : V), { obj := F_obj, map := map✝¹ }.map (𝟙rq X) = 𝟙rq ({ obj := F_obj, map := map✝¹ }.obj X)
map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : V), { obj := F_obj, map := map✝ }.map (𝟙rq X) = 𝟙rq ({ obj := F_obj, map := map✝ }.obj X)
h_obj :
  ∀ (X : V),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹ }.obj X = { obj := F_obj, map := map✝, map_id := map_id✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹ }.map f =
      Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := F_obj, map := map✝, map_id := map_id✝ }.map f))
X Y : V
f : X ⟶ Y
⊢ map✝¹ f = map✝ f

Tactic:
simpa using h_map X Y f

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem proj_prop_eq_self (hh : ∀ i x, x ∈ C → x i ≠ false → J i) : π C J = C

Proof state:
case h
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
⊢ x ∈ π C J ↔ x ∈ C

Tactic:
refine ⟨fun ⟨y, hy, h⟩ ↦ ?_, fun h ↦ ⟨x, h, ?_⟩⟩

Result:
case h.refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
x✝ : x ∈ π C J
y : I → Bool
hy : y ∈ C
h : Proj J y = x
⊢ x ∈ C

case h.refine_2
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
h : x ∈ C
⊢ Proj J x = x

Proof state:
case h.refine_2
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
h : x ∈ C
⊢ Proj J x = x

Tactic:
rw [proj_eq_self]

Result:
case h.refine_2.h
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
h : x ∈ C
⊢ ∀ (i : I), x i ≠ false → J i

Proof state:
case h.refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
x✝ : x ∈ π C J
y : I → Bool
hy : y ∈ C
h : Proj J y = x
⊢ x ∈ C

Tactic:
rwa [← h, proj_eq_self]

Result:
case h.refine_1.h
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
x✝ : x ∈ π C J
y : I → Bool
hy : y ∈ C
h : Proj J y = x
⊢ ∀ (i : I), y i ≠ false → J i

Proof state:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
⊢ π C J = C

Tactic:
ext x

Result:
case h
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
⊢ x ∈ π C J ↔ x ∈ C
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem edgeSet_sInf (s : Set G.Subgraph) :
    (sInf s).edgeSet = (⋂ G' ∈ s, edgeSet G') ∩ G.edgeSet

Proof state:
case h.h
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
x✝ y✝ : V
⊢ s(x✝, y✝) ∈ (sInf s).edgeSet ↔ s(x✝, y✝) ∈ (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet

Tactic:
simp

Result:
no goals

Proof state:
case h
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
e : Sym2 V
⊢ e ∈ (sInf s).edgeSet ↔ e ∈ (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet

Tactic:
induction e

Result:
case h.h
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
x✝ y✝ : V
⊢ s(x✝, y✝) ∈ (sInf s).edgeSet ↔ s(x✝, y✝) ∈ (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet

Proof state:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
⊢ (sInf s).edgeSet = (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet

Tactic:
ext e

Result:
case h
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
e : Sym2 V
⊢ e ∈ (sInf s).edgeSet ↔ e ∈ (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourier_zero' {x : AddCircle T} : @toCircle T 0 = (1 : ℂ)

Proof state:
T : ℝ
x : AddCircle T
⊢ ↑(toCircle 0) = 1

Tactic:
have : fourier 0 x = @toCircle T 0 := by rw [fourier_apply, zero_smul]

Result:
T : ℝ
x : AddCircle T
this : (fourier 0) x = ↑(toCircle 0)
⊢ ↑(toCircle 0) = 1

Proof state:
T : ℝ
x : AddCircle T
⊢ (fourier 0) x = ↑(toCircle 0)

Tactic:
rw [fourier_apply, zero_smul]

Result:
no goals

Proof state:
T : ℝ
x : AddCircle T
this : (fourier 0) x = ↑(toCircle 0)
⊢ ↑(toCircle 0) = 1

Tactic:
rw [← this]

Result:
T : ℝ
x : AddCircle T
this : (fourier 0) x = ↑(toCircle 0)
⊢ (fourier 0) x = 1

Proof state:
T : ℝ
x : AddCircle T
this : (fourier 0) x = ↑(toCircle 0)
⊢ (fourier 0) x = 1

Tactic:
exact fourier_zero

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
@[reassoc]
lemma curry'_whiskerRight_comp {X Y Z : C} [Closed X] [Closed Y] (f : X ⟶ Y) :
    curry' f ▷ _ ≫ comp X Y Z = (λ_ _).hom ≫ (pre f).app Z

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ curry' f ▷ (ihom Y).obj Z ≫ comp X Y Z = (λ_ ((ihom Y).obj Z)).hom ≫ (pre f).app Z

Tactic:
rw [← cancel_epi (λ_ _).inv, Iso.inv_hom_id_assoc]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ (λ_ ((ihom Y).obj Z)).inv ≫ curry' f ▷ (ihom Y).obj Z ≫ comp X Y Z = (pre f).app Z

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ (λ_ ((ihom Y).obj Z)).inv ≫ curry' f ▷ (ihom Y).obj Z ≫ comp X Y Z = (pre f).app Z

Tactic:
apply uncurry_injective

Result:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ uncurry ((λ_ ((ihom Y).obj Z)).inv ≫ curry' f ▷ (ihom Y).obj Z ≫ comp X Y Z) = uncurry ((pre f).app Z)

Proof state:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ uncurry ((λ_ ((ihom Y).obj Z)).inv ≫ curry' f ▷ (ihom Y).obj Z ≫ comp X Y Z) = uncurry ((pre f).app Z)

Tactic:
rw [uncurry_pre, comp_eq, ← curry_natural_left, ← curry_natural_left, uncurry_curry,
  compTranspose_eq, associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc,
  whiskerLeft_curry'_ihom_ev_app, comp_whiskerRight_assoc, triangle_assoc_comp_right_assoc,
  whiskerLeft_inv_hom_assoc]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem pow_left (a : ℤ) (e b : ℕ) : J(a ^ e | b) = J(a | b) ^ e :=
  Nat.recOn e (by rw [_root_.pow_zero, _root_.pow_zero, one_left]) fun _ ih => by
    rw [_root_.pow_succ, _root_.pow_succ, mul_left, ih]

Proof state:
a : ℤ
e b x✝ : ℕ
ih : J(a ^ x✝ | b) = J(a | b) ^ x✝
⊢ J(a ^ x✝.succ | b) = J(a | b) ^ x✝.succ

Tactic:
rw [_root_.pow_succ, _root_.pow_succ, mul_left, ih]

Result:
no goals

Proof state:
a : ℤ
e b : ℕ
⊢ J(a ^ zero | b) = J(a | b) ^ zero

Tactic:
rw [_root_.pow_zero, _root_.pow_zero, one_left]

Result:
no goals
-- Mathlib/Data/List/Lattice.lean
theorem mem_inter_of_mem_of_mem (h₁ : a ∈ l₁) (h₂ : a ∈ l₂) : a ∈ l₁ ∩ l₂ :=
  mem_filter_of_mem h₁ <| by simpa using h₂

Proof state:
α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h₁ : a ∈ l₁
h₂ : a ∈ l₂
⊢ elem a l₂ = true

Tactic:
simpa using h₂

Result:
no goals
-- Mathlib/Algebra/Field/Subfield/Basic.lean
theorem fieldRange_eq_map : f.fieldRange = Subfield.map f ⊤

Proof state:
case h
K : Type u
L : Type v
inst✝¹ : DivisionRing K
inst✝ : DivisionRing L
f : K →+* L
x✝ : L
⊢ x✝ ∈ f.fieldRange ↔ x✝ ∈ Subfield.map f ⊤

Tactic:
simp

Result:
no goals

Proof state:
K : Type u
L : Type v
inst✝¹ : DivisionRing K
inst✝ : DivisionRing L
f : K →+* L
⊢ f.fieldRange = Subfield.map f ⊤

Tactic:
ext

Result:
case h
K : Type u
L : Type v
inst✝¹ : DivisionRing K
inst✝ : DivisionRing L
f : K →+* L
x✝ : L
⊢ x✝ ∈ f.fieldRange ↔ x✝ ∈ Subfield.map f ⊤
-- Mathlib/SetTheory/Cardinal/HasCardinalLT.lean
lemma hasCardinalLT_option_iff (X : Type u) (κ : Cardinal.{w})
    (hκ : Cardinal.aleph0 ≤ κ) :
    HasCardinalLT (Option X) κ ↔ HasCardinalLT X κ

Proof state:
X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
x✝ : HasCardinalLT X κ
⊢ HasCardinalLT PUnit.{1} Cardinal.aleph0

Tactic:
rw [hasCardinalLT_aleph0_iff]

Result:
X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
x✝ : HasCardinalLT X κ
⊢ Finite PUnit.{1}

Proof state:
X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
x✝ : HasCardinalLT X κ
⊢ Finite PUnit.{1}

Tactic:
infer_instance

Result:
no goals

Proof state:
X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT (Option X) κ ↔ HasCardinalLT X κ

Tactic:
rw [hasCardinalLT_iff_of_equiv (Equiv.optionEquivSumPUnit.{0} X),
  hasCardinalLT_sum_iff _ _ _ hκ, and_iff_left_iff_imp]

Result:
X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT X κ → HasCardinalLT PUnit.{1} κ

Proof state:
X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT X κ → HasCardinalLT PUnit.{1} κ

Tactic:
refine fun _ ↦ HasCardinalLT.of_le ?_ hκ

Result:
X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
x✝ : HasCardinalLT X κ
⊢ HasCardinalLT PUnit.{1} Cardinal.aleph0
-- Mathlib/Topology/Order/LeftRightLim.lean
theorem leftLim : Monotone (leftLim f)

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x : α
h : x ≤ x
⊢ leftLim f x ≤ leftLim f x

Tactic:
exact le_rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
⊢ Monotone (leftLim f)

Tactic:
intro x y h

Result:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
⊢ leftLim f x ≤ leftLim f y

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
hxy : x < y
⊢ leftLim f x ≤ leftLim f y

Tactic:
exact (hf.leftLim_le le_rfl).trans (hf.le_leftLim hxy)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
⊢ leftLim f x ≤ leftLim f y

Tactic:
rcases eq_or_lt_of_le h with (rfl | hxy)

Result:
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x : α
h : x ≤ x
⊢ leftLim f x ≤ leftLim f x

case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
hxy : x < y
⊢ leftLim f x ≤ leftLim f y
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem prod_range_reflect (f : ℕ → M) (n : ℕ) :
    (∏ j ∈ range n, f (n - 1 - j)) = ∏ j ∈ range n, f j

Proof state:
case succ
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
n✝ : ℕ
⊢ ∏ j ∈ range (n✝ + 1), f (n✝ + 1 - 1 - j) = ∏ j ∈ range (n✝ + 1), f j

Tactic:
simp only [← Nat.Ico_zero_eq_range, Nat.succ_sub_succ_eq_sub, tsub_zero]

Result:
case succ
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
n✝ : ℕ
⊢ ∏ x ∈ Ico 0 (n✝ + 1), f (n✝ - x) = ∏ x ∈ Ico 0 (n✝ + 1), f x

Proof state:
case succ
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
n✝ : ℕ
⊢ ∏ x ∈ Ico 0 (n✝ + 1), f (n✝ - x) = ∏ x ∈ Ico 0 (n✝ + 1), f x

Tactic:
rw [prod_Ico_reflect _ _ le_rfl]

Result:
case succ
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
n✝ : ℕ
⊢ ∏ j ∈ Ico (n✝ + 1 - (n✝ + 1)) (n✝ + 1 - 0), f j = ∏ x ∈ Ico 0 (n✝ + 1), f x

Proof state:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ j ∈ range n, f (n - 1 - j) = ∏ j ∈ range n, f j

Tactic:
cases n

Result:
case zero
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
⊢ ∏ j ∈ range 0, f (0 - 1 - j) = ∏ j ∈ range 0, f j

case succ
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
n✝ : ℕ
⊢ ∏ j ∈ range (n✝ + 1), f (n✝ + 1 - 1 - j) = ∏ j ∈ range (n✝ + 1), f j

Proof state:
case zero
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
⊢ ∏ j ∈ range 0, f (0 - 1 - j) = ∏ j ∈ range 0, f j

Tactic:
simp

Result:
no goals

Proof state:
case succ
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
n✝ : ℕ
⊢ ∏ j ∈ Ico (n✝ + 1 - (n✝ + 1)) (n✝ + 1 - 0), f j = ∏ x ∈ Ico 0 (n✝ + 1), f x

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
theorem orthogonal_span_singleton_eq_toLin_ker {B : BilinForm K V} (x : V) :
    B.orthogonal (K ∙ x) = LinearMap.ker (LinearMap.BilinForm.toLinHomAux₁ B x)

Proof state:
case h
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x y : V
⊢ (∀ (n : V), (∃ a, a • x = n) → B.IsOrtho n y) ↔ (B.toLinHomAux₁ x) y = 0

Tactic:
constructor

Result:
case h.mp
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x y : V
⊢ (∀ (n : V), (∃ a, a • x = n) → B.IsOrtho n y) → (B.toLinHomAux₁ x) y = 0

case h.mpr
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x y : V
⊢ (B.toLinHomAux₁ x) y = 0 → ∀ (n : V), (∃ a, a • x = n) → B.IsOrtho n y

Proof state:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
⊢ B.orthogonal (Submodule.span K {x}) = ker (B.toLinHomAux₁ x)

Tactic:
ext y

Result:
case h
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x y : V
⊢ y ∈ B.orthogonal (Submodule.span K {x}) ↔ y ∈ ker (B.toLinHomAux₁ x)

Proof state:
case h
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x y : V
⊢ y ∈ B.orthogonal (Submodule.span K {x}) ↔ y ∈ ker (B.toLinHomAux₁ x)

Tactic:
simp_rw [mem_orthogonal_iff, LinearMap.mem_ker, Submodule.mem_span_singleton]

Result:
case h
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x y : V
⊢ (∀ (n : V), (∃ a, a • x = n) → B.IsOrtho n y) ↔ (B.toLinHomAux₁ x) y = 0

Proof state:
case h.mpr
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x y : V
⊢ (B.toLinHomAux₁ x) y = 0 → ∀ (n : V), (∃ a, a • x = n) → B.IsOrtho n y

Tactic:
rintro h _ ⟨z, rfl⟩

Result:
case h.mpr.intro
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x y : V
h : (B.toLinHomAux₁ x) y = 0
z : K
⊢ B.IsOrtho (z • x) y

Proof state:
case h.mp
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x y : V
⊢ (∀ (n : V), (∃ a, a • x = n) → B.IsOrtho n y) → (B.toLinHomAux₁ x) y = 0

Tactic:
exact fun h => h x ⟨1, one_smul _ _⟩

Result:
no goals

Proof state:
case h.mpr.intro
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x y : V
h : (B.toLinHomAux₁ x) y = 0
z : K
⊢ z = 0 ∨ (B x) y = 0

Tactic:
exact Or.intro_right _ h

Result:
no goals

Proof state:
case h.mpr.intro
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x y : V
h : (B.toLinHomAux₁ x) y = 0
z : K
⊢ B.IsOrtho (z • x) y

Tactic:
rw [IsOrtho, smul_left, mul_eq_zero]

Result:
case h.mpr.intro
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x y : V
h : (B.toLinHomAux₁ x) y = 0
z : K
⊢ z = 0 ∨ (B x) y = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_abs_eq_ite_of_ne_intMin {x : BitVec w} (hx : x ≠ intMin w) :
  x.abs.toInt = if x.msb then -x.toInt else x.toInt

Proof state:
w : Nat
x : BitVec w
hx : x ≠ intMin w
⊢ x.abs.toInt = if x.msb = true then -x.toInt else x.toInt

Tactic:
simp [toInt_abs_eq_ite, hx]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean
lemma add_right (h1 : μ ≪ ν) (ν' : Measure α) : μ ≪ ν + ν'

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
ν' : Measure α
s : Set α
hs : ν s = 0 ∧ ν' s = 0
⊢ μ s = 0

Tactic:
exact h1 hs.1

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
ν' : Measure α
⊢ μ ≪ ν + ν'

Tactic:
intro s hs

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
ν' : Measure α
s : Set α
hs : (ν + ν') s = 0
⊢ μ s = 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
ν' : Measure α
s : Set α
hs : (ν + ν') s = 0
⊢ μ s = 0

Tactic:
simp only [coe_add, Pi.add_apply, add_eq_zero] at hs ⊢

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
ν' : Measure α
s : Set α
hs : ν s = 0 ∧ ν' s = 0
⊢ μ s = 0
-- Mathlib/.lake/packages/lean4/src/lean/lake/Lake/Util/Name.lean
theorem beq_false (m n : Name) : (m == n) = false ↔ ¬ (m = n)

Proof state:
m n : Name
⊢ (m == n) = false ↔ ¬(m == n) = true

Tactic:
cases m == n <;> simp +decide

Result:
no goals

Proof state:
m n : Name
⊢ (m == n) = false ↔ ¬m = n

Tactic:
rw [← beq_iff_eq (a := m) (b := n)]

Result:
m n : Name
⊢ (m == n) = false ↔ ¬(m == n) = true