harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma coe_toENNReal {x : EReal} (hx : 0 ≤ x) : (x.toENNReal : EReal) = x

Proof state:
x : EReal
hx : 0 ≤ x
⊢ ↑x.toENNReal = x

Tactic:
rw [toENNReal]

Result:
x : EReal
hx : 0 ≤ x
⊢ ↑(if x = ⊤ then ⊤ else ENNReal.ofReal x.toReal) = x

Proof state:
case neg
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
⊢ ↑(ENNReal.ofReal x.toReal) = x

Tactic:
simp only [coe_ennreal_ofReal, ge_iff_le, hx, toReal_nonneg, max_eq_left]

Result:
case neg
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
⊢ ↑x.toReal = x

Proof state:
x : EReal
hx : 0 ≤ x
⊢ ↑(if x = ⊤ then ⊤ else ENNReal.ofReal x.toReal) = x

Tactic:
by_cases h_top : x = ⊤

Result:
case pos
x : EReal
hx : 0 ≤ x
h_top : x = ⊤
⊢ ↑(if x = ⊤ then ⊤ else ENNReal.ofReal x.toReal) = x

case neg
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
⊢ ↑(if x = ⊤ then ⊤ else ENNReal.ofReal x.toReal) = x

Proof state:
case neg
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
⊢ ↑x.toReal = x

Tactic:
exact coe_toReal h_top fun _ ↦ by simp_all only [le_bot_iff, zero_ne_bot]

Result:
no goals

Proof state:
case pos
x : EReal
hx : 0 ≤ x
h_top : x = ⊤
⊢ ↑(if x = ⊤ then ⊤ else ENNReal.ofReal x.toReal) = x

Tactic:
rw [if_pos h_top, h_top]

Result:
case pos
x : EReal
hx : 0 ≤ x
h_top : x = ⊤
⊢ ↑⊤ = ⊤

Proof state:
case pos
x : EReal
hx : 0 ≤ x
h_top : x = ⊤
⊢ ↑⊤ = ⊤

Tactic:
rfl

Result:
no goals

Proof state:
case neg
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
⊢ ↑(if x = ⊤ then ⊤ else ENNReal.ofReal x.toReal) = x

Tactic:
rw [if_neg h_top]

Result:
case neg
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
⊢ ↑(ENNReal.ofReal x.toReal) = x

Proof state:
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
x✝ : x = ⊥
⊢ False

Tactic:
simp_all only [le_bot_iff, zero_ne_bot]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Prod.lean
theorem Tendsto.prod_map_prod_atBot [Preorder γ] {F : Filter α} {G : Filter β} {f : α → γ}
    {g : β → γ} (hf : Tendsto f F atBot) (hg : Tendsto g G atBot) :
    Tendsto (Prod.map f g) (F ×ˢ G) atBot

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atBot
hg : Tendsto g G atBot
⊢ Tendsto (Prod.map f g) (F ×ˢ G) atBot

Tactic:
rw [← prod_atBot_atBot_eq]

Result:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atBot
hg : Tendsto g G atBot
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (atBot ×ˢ atBot)

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atBot
hg : Tendsto g G atBot
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (atBot ×ˢ atBot)

Tactic:
exact hf.prod_map hg

Result:
no goals
-- Mathlib/Data/Nat/Choose/Central.lean
theorem four_pow_lt_mul_centralBinom (n : ℕ) (n_big : 4 ≤ n) : 4 ^ n < n * centralBinom n

Proof state:
n : ℕ
n_big : 4 ≤ n
⊢ 4 ^ n < n * n.centralBinom

Tactic:
induction' n using Nat.strong_induction_on with n IH

Result:
case h
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
⊢ 4 ^ n < n * n.centralBinom

Proof state:
case h.inl
n : ℕ
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * n.centralBinom

Tactic:
exact False.elim ((not_lt.2 n_big) hn)

Result:
no goals

Proof state:
n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * n * n.centralBinom ≤ 2 * (2 * n + 1) * n.centralBinom

Tactic:
linarith

Result:
no goals

Proof state:
case h
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
⊢ 4 ^ n < n * n.centralBinom

Tactic:
rcases lt_trichotomy n 4 with (hn | rfl | hn)

Result:
case h.inl
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * n.centralBinom

case h.inr.inl
IH : ∀ m < 4, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ 4
⊢ 4 ^ 4 < 4 * centralBinom 4

case h.inr.inr
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
hn : 4 < n
⊢ 4 ^ n < n * n.centralBinom

Proof state:
case h.inr.inr
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
hn : 4 < n
⊢ 4 ^ n < n * n.centralBinom

Tactic:
obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := Nat.exists_eq_succ_of_ne_zero (Nat.not_eq_zero_of_lt hn)

Result:
case h.inr.inr.intro
n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 ^ (n + 1) < (n + 1) * (n + 1).centralBinom

Proof state:
case h.inl
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * n.centralBinom

Tactic:
clear IH

Result:
case h.inl
n : ℕ
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * n.centralBinom

Proof state:
case h.inr.inr.intro
n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 ^ (n + 1) < (n + 1) * (n + 1).centralBinom

Tactic:
calc
  4 ^ (n + 1) < 4 * (n * centralBinom n) := lt_of_eq_of_lt pow_succ' <|
    (mul_lt_mul_left <| zero_lt_four' ℕ).mpr (IH n n.lt_succ_self (Nat.le_of_lt_succ hn))
  _ ≤ 2 * (2 * n + 1) * centralBinom n := by rw [← mul_assoc]; linarith
  _ = (n + 1) * centralBinom (n + 1) := (succ_mul_centralBinom_succ n).symm

Result:
no goals

Proof state:
case h.inr.inl
IH : ∀ m < 4, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ 4
⊢ 4 ^ 4 < 4 * centralBinom 4

Tactic:
norm_num [centralBinom, choose]

Result:
no goals

Proof state:
n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * (n * n.centralBinom) ≤ 2 * (2 * n + 1) * n.centralBinom

Tactic:
rw [← mul_assoc]

Result:
n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * n * n.centralBinom ≤ 2 * (2 * n + 1) * n.centralBinom
-- Mathlib/Topology/Connected/LocallyConnected.lean
theorem locallyConnectedSpace_iff_connectedComponentIn_open :
    LocallyConnectedSpace α ↔
      ∀ F : Set α, IsOpen F → ∀ x ∈ F, IsOpen (connectedComponentIn F x)

Proof state:
α : Type u
inst✝ : TopologicalSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (F : Set α), IsOpen F → ∀ x ∈ F, IsOpen (connectedComponentIn F x)

Tactic:
constructor

Result:
case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ LocallyConnectedSpace α → ∀ (F : Set α), IsOpen F → ∀ x ∈ F, IsOpen (connectedComponentIn F x)

case mpr
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (F : Set α), IsOpen F → ∀ x ∈ F, IsOpen (connectedComponentIn F x)) → LocallyConnectedSpace α

Proof state:
case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ LocallyConnectedSpace α → ∀ (F : Set α), IsOpen F → ∀ x ∈ F, IsOpen (connectedComponentIn F x)

Tactic:
intro h

Result:
case mp
α : Type u
inst✝ : TopologicalSpace α
h : LocallyConnectedSpace α
⊢ ∀ (F : Set α), IsOpen F → ∀ x ∈ F, IsOpen (connectedComponentIn F x)

Proof state:
case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (F : Set α), IsOpen F → ∀ x ∈ F, IsOpen (connectedComponentIn F x)
⊢ LocallyConnectedSpace α

Tactic:
rw [locallyConnectedSpace_iff_subsets_isOpen_isConnected]

Result:
case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (F : Set α), IsOpen F → ∀ x ∈ F, IsOpen (connectedComponentIn F x)
⊢ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen V ∧ x ∈ V ∧ IsConnected V

Proof state:
case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (F : Set α), IsOpen F → ∀ x ∈ F, IsOpen (connectedComponentIn F x)
⊢ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen V ∧ x ∈ V ∧ IsConnected V

Tactic:
refine fun x U hU =>
    ⟨connectedComponentIn (interior U) x,
      (connectedComponentIn_subset _ _).trans interior_subset, h _ isOpen_interior x ?_,
      mem_connectedComponentIn ?_, isConnected_connectedComponentIn_iff.mpr ?_⟩ <;>
  exact mem_interior_iff_mem_nhds.mpr hU

Result:
no goals

Proof state:
case mpr
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (F : Set α), IsOpen F → ∀ x ∈ F, IsOpen (connectedComponentIn F x)) → LocallyConnectedSpace α

Tactic:
intro h

Result:
case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (F : Set α), IsOpen F → ∀ x ∈ F, IsOpen (connectedComponentIn F x)
⊢ LocallyConnectedSpace α

Proof state:
case mp
α : Type u
inst✝ : TopologicalSpace α
h : LocallyConnectedSpace α
⊢ ∀ (F : Set α), IsOpen F → ∀ x ∈ F, IsOpen (connectedComponentIn F x)

Tactic:
exact fun F hF x _ => hF.connectedComponentIn

Result:
no goals
-- Mathlib/Analysis/Convex/Join.lean
theorem convexJoin_assoc_aux (s t u : Set E) :
    convexJoin 𝕜 (convexJoin 𝕜 s t) u ⊆ convexJoin 𝕜 s (convexJoin 𝕜 t u)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr.refine_1
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂✝ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ a₂ * a₁ + (a₂ * b₁ + b₂) = 1

Tactic:
linear_combination a₂ * hab₁ + hab₂

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr.refine_2
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂✝ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ (a₂ * a₁) • x + (a₂ * b₁ + b₂) • ((a₂ * b₁ / (a₂ * b₁ + b₂)) • y + (b₂ / (a₂ * b₁ + b₂)) • z) =
    a₂ • (a₁ • x + b₁ • y) + b₂ • z

Tactic:
match_scalars <;> field_simp

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂✝ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ a₂ * b₁ / (a₂ * b₁ + b₂) + b₂ / (a₂ * b₁ + b₂) = 1

Tactic:
field_simp

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂✝ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ 0 ≤ a₂ * b₁ / (a₂ * b₁ + b₂)

Tactic:
positivity

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findSome?_cons_of_isNone (l) (h : (f a).isNone) : findSome? f (a :: l) = findSome? f l

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
h : (f a).isNone = true
⊢ findSome? f (a :: l) = findSome? f l

Tactic:
simp only [findSome?]

Result:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
h : (f a).isNone = true
⊢ (match f a with
    | some b => some b
    | none => findSome? f l) =
    findSome? f l

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
h : (f a).isNone = true
⊢ (match f a with
    | some b => some b
    | none => findSome? f l) =
    findSome? f l

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/RingTheory/WittVector/MulCoeff.lean
theorem nth_mul_coeff' (n : ℕ) :
    ∃ f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k,
    ∀ x y : 𝕎 k, f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) -
        x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)

Proof state:
case h.e_a.h.mk.mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑(Membership.mem (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y =>
    f₀ fun a =>
      Subtype.casesOn a fun a ha =>
        Function.uncurry ![x, y]
          (let S := fun a => a.2 = n ∨ a.2 < n;
          let_fun ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
x y : 𝕎 k
i : Fin 2
m : ℕ
ha : (i, m) ∈ Membership.mem (univ.val ×ˢ Multiset.range (n + 1))
⊢ ![truncateFun (n + 1) x, truncateFun (n + 1) y] (↑⟨(i, m), ha⟩).1 ⟨(↑⟨(i, m), ha⟩).2, ⋯⟩ =
    (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i] ∘ Subtype.val) ⟨(i, m), ha⟩

Tactic:
fin_cases i <;> rfl

Result:
no goals

Proof state:
case mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑(Membership.mem (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ Membership.mem (univ.val.product (n ::ₘ Multiset.range n))
⊢ Fin (Nat.succ 0).succ × Fin (n + 1)

Tactic:
let S : Set (Fin 2 × ℕ) := (fun a => a.2 = n ∨ a.2 < n)

Result:
case mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑(Membership.mem (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ Membership.mem (univ.val.product (n ::ₘ Multiset.range n))
S : Set (Fin 2 × ℕ) := fun a => a.2 = n ∨ a.2 < n
⊢ Fin (Nat.succ 0).succ × Fin (n + 1)
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem getD_leftInvSeq (ω : List B) (j : ℕ) :
    (lis ω).getD j 1 =
      π (ω.take j)
        * (Option.map (cs.simple) ω[j]?).getD 1
        * (π (ω.take j))⁻¹

Proof state:
case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j : ℕ
⊢ (cs.leftInvSeq (i :: ω)).getD j 1 =
    cs.wordProd (take j (i :: ω)) * (Option.map cs.simple (i :: ω)[j]?).getD 1 * (cs.wordProd (take j (i :: ω)))⁻¹

Tactic:
dsimp [leftInvSeq]

Result:
case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j : ℕ
⊢ (cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD j 1 =
    cs.wordProd (take j (i :: ω)) * (Option.map cs.simple (i :: ω)[j]?).getD 1 * (cs.wordProd (take j (i :: ω)))⁻¹

Proof state:
case cons.zero
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
⊢ (cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD 0 1 =
    cs.wordProd (take 0 (i :: ω)) * (Option.map cs.simple (i :: ω)[0]?).getD 1 * (cs.wordProd (take 0 (i :: ω)))⁻¹

Tactic:
simp [getD_cons_zero]

Result:
no goals

Proof state:
case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (MulAut.conj (cs.simple i)) ((cs.leftInvSeq ω).getD j' 1) =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (i :: ω)[j' + 1]?).getD ((MulAut.conj (cs.simple i)) 1) *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹

Tactic:
rw [ih j']

Result:
case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (MulAut.conj (cs.simple i))
      (cs.wordProd (take j' ω) * (Option.map cs.simple ω[j']?).getD 1 * (cs.wordProd (take j' ω))⁻¹) =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (i :: ω)[j' + 1]?).getD ((MulAut.conj (cs.simple i)) 1) *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_eq_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
    l.mapFinIdx f = l' ↔ ∃ h : l'.length = l.length, ∀ (i : Nat) (h : i < l.length), l'[i] = f i l[i] h

Proof state:
case mpr
α : Type u_1
β : Type u_2
l' : List β
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ (∃ h, ∀ (i : Nat) (h_1 : i < l.length), l'[i] = f i l[i] h_1) → l.mapFinIdx f = l'

Tactic:
rintro ⟨h, w⟩

Result:
case mpr.intro
α : Type u_1
β : Type u_2
l' : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h : l'.length = l.length
w : ∀ (i : Nat) (h_1 : i < l.length), l'[i] = f i l[i] h_1
⊢ l.mapFinIdx f = l'

Proof state:
case mpr.intro
α : Type u_1
β : Type u_2
l' : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h : l'.length = l.length
w : ∀ (i : Nat) (h_1 : i < l.length), l'[i] = f i l[i] h_1
⊢ l.mapFinIdx f = l'

Tactic:
apply ext_getElem <;> simp_all

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
l' : List β
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ l.mapFinIdx f = l' → ∃ h, ∀ (i : Nat) (h_1 : i < l.length), l'[i] = f i l[i] h_1

Tactic:
rintro rfl

Result:
case mp
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ ∃ h, ∀ (i : Nat) (h_1 : i < l.length), (l.mapFinIdx f)[i] = f i l[i] h_1

Proof state:
case mp
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ ∃ h, ∀ (i : Nat) (h_1 : i < l.length), (l.mapFinIdx f)[i] = f i l[i] h_1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l' : List β
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ l.mapFinIdx f = l' ↔ ∃ h, ∀ (i : Nat) (h_1 : i < l.length), l'[i] = f i l[i] h_1

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
l' : List β
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ l.mapFinIdx f = l' → ∃ h, ∀ (i : Nat) (h_1 : i < l.length), l'[i] = f i l[i] h_1

case mpr
α : Type u_1
β : Type u_2
l' : List β
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ (∃ h, ∀ (i : Nat) (h_1 : i < l.length), l'[i] = f i l[i] h_1) → l.mapFinIdx f = l'
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_eq_integral_of_ae_compl_eq_zero (h : ∀ᵐ x ∂μ, x ∉ s → f x = 0) :
    ∫ x in s, f x ∂μ = ∫ x, f x ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0
⊢ ∫ (x : X) in s, f x ∂μ = ∫ (x : X), f x ∂μ

Tactic:
symm

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0
⊢ ∫ (x : X), f x ∂μ = ∫ (x : X) in s, f x ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0
⊢ ∀ᵐ (x : X) ∂μ, x ∈ univ \ s → f x = 0

Tactic:
filter_upwards [h] with x hx h'x using hx h'x.2

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0
⊢ ∫ (x : X), f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
nth_rw 1 [← setIntegral_univ]

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0
⊢ ∫ (x : X) in univ, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0
⊢ ∫ (x : X) in univ, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
apply setIntegral_eq_of_subset_of_ae_diff_eq_zero nullMeasurableSet_univ (subset_univ _)

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0
⊢ ∀ᵐ (x : X) ∂μ, x ∈ univ \ s → f x = 0
-- Mathlib/Algebra/Lie/Abelian.lean
theorem ideal_oper_maxTrivSubmodule_eq_bot (I : LieIdeal R L) :
    ⁅I, maxTrivSubmodule R L M⁆ = ⊥

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
⊢ ∀ x ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}, x = 0

Tactic:
rintro m ⟨⟨x, hx⟩, ⟨⟨m, hm⟩, rfl⟩⟩

Result:
case intro.mk.intro.mk
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hx : x ∈ I
m : M
hm : m ∈ maxTrivSubmodule R L M
⊢ ⁅↑⟨x, hx⟩, ↑⟨m, hm⟩⁆ = 0

Proof state:
case intro.mk.intro.mk
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hx : x ∈ I
m : M
hm : m ∈ maxTrivSubmodule R L M
⊢ ⁅↑⟨x, hx⟩, ↑⟨m, hm⟩⁆ = 0

Tactic:
exact hm x

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
⊢ ⁅I, maxTrivSubmodule R L M⁆ = ⊥

Tactic:
rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.lieIdeal_oper_eq_linear_span,
  LieSubmodule.bot_toSubmodule, Submodule.span_eq_bot]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
⊢ ∀ x ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}, x = 0
-- Mathlib/Data/Real/EReal.lean
lemma _root_.ENNReal.toEReal_sub {x y : ℝ≥0∞} (hy_top : y ≠ ∞) (h_le : y ≤ x) :
    (x - y).toEReal = x.toEReal - y.toEReal

Proof state:
x y : ℝ≥0∞
hy_top : y ≠ ⊤
h_le : y ≤ x
⊢ ↑(x - y) = ↑x - ↑y

Tactic:
lift y to ℝ≥0 using hy_top

Result:
case intro
x : ℝ≥0∞
y : ℝ≥0
h_le : ↑y ≤ x
⊢ ↑(x - ↑y) = ↑x - ↑↑y

Proof state:
case intro.coe
y x : ℝ≥0
h_le : ↑y ≤ ↑x
⊢ ↑(↑x - ↑y) = ↑↑x - ↑↑y

Tactic:
simp only [coe_nnreal_eq_coe_real, ← ENNReal.coe_sub, NNReal.coe_sub (mod_cast h_le), coe_sub]

Result:
no goals

Proof state:
case intro
x : ℝ≥0∞
y : ℝ≥0
h_le : ↑y ≤ x
⊢ ↑(x - ↑y) = ↑x - ↑↑y

Tactic:
cases x with
| top => simp [coe_nnreal_eq_coe_real]
| coe x =>
  simp only [coe_nnreal_eq_coe_real, ← ENNReal.coe_sub, NNReal.coe_sub (mod_cast h_le), coe_sub]

Result:
no goals

Proof state:
case intro.top
y : ℝ≥0
h_le : ↑y ≤ ⊤
⊢ ↑(⊤ - ↑y) = ↑⊤ - ↑↑y

Tactic:
simp [coe_nnreal_eq_coe_real]

Result:
no goals
-- Mathlib/Topology/Order/UpperLowerSetTopology.lean
lemma isUpperSet_orderDual [Preorder α] [TopologicalSpace α] :
    Topology.IsUpperSet αᵒᵈ ↔ Topology.IsLowerSet α

Proof state:
case mp
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ Topology.IsUpperSet αᵒᵈ → Topology.IsLowerSet α

Tactic:
apply OrderDual.instIsLowerSet

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ Topology.IsLowerSet α → Topology.IsUpperSet αᵒᵈ

Tactic:
apply OrderDual.instIsUpperSet

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ Topology.IsUpperSet αᵒᵈ ↔ Topology.IsLowerSet α

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ Topology.IsUpperSet αᵒᵈ → Topology.IsLowerSet α

case mpr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ Topology.IsLowerSet α → Topology.IsUpperSet αᵒᵈ