harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem product_eq_productTR : @product = @productTR

Proof state:
case h.h.h.h
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ flatMap (fun a => map (Prod.mk a) l₂) l₁ = #[].toList ++ flatMap ?h.h.h.h.G l₁

case h.h.h.h.G
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ α → List (α × β)

case h.h.h.h.H
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ ∀ (acc : Array (α × β)) (a : α), (foldl (fun acc b => acc.push (a, b)) acc l₂).toList = acc.toList ++ ?h.h.h.h.G a

Tactic:
rfl

Result:
case h.h.h.h.H
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ ∀ (acc : Array (α × β)) (a : α),
    (foldl (fun acc b => acc.push (a, b)) acc l₂).toList = acc.toList ++ map (Prod.mk a) l₂

Proof state:
⊢ @product = @productTR

Tactic:
funext α β l₁ l₂

Result:
case h.h.h.h
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ l₁.product l₂ = l₁.productTR l₂

Proof state:
case h.h.h.h
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ l₁.product l₂ = l₁.productTR l₂

Tactic:
simp [product, productTR]

Result:
case h.h.h.h
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ flatMap (fun a => map (Prod.mk a) l₂) l₁ =
    (foldl (fun acc a => foldl (fun acc b => acc.push (a, b)) acc l₂) #[] l₁).toList

Proof state:
case h.h.h.h.H
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
acc✝ : Array (α × β)
a✝ : α
⊢ (foldl (fun acc b => acc.push (a✝, b)) acc✝ l₂).toList = acc✝.toList ++ map (Prod.mk a✝) l₂

Tactic:
apply Array.foldl_toList_eq_map

Result:
no goals

Proof state:
case h.h.h.h
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ flatMap (fun a => map (Prod.mk a) l₂) l₁ =
    (foldl (fun acc a => foldl (fun acc b => acc.push (a, b)) acc l₂) #[] l₁).toList

Tactic:
rw [Array.foldl_toList_eq_flatMap]

Result:
case h.h.h.h
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ flatMap (fun a => map (Prod.mk a) l₂) l₁ = #[].toList ++ flatMap ?h.h.h.h.G l₁

case h.h.h.h.G
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ α → List (α × β)

case h.h.h.h.H
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ ∀ (acc : Array (α × β)) (a : α), (foldl (fun acc b => acc.push (a, b)) acc l₂).toList = acc.toList ++ ?h.h.h.h.G a

Proof state:
case h.h.h.h.H
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ ∀ (acc : Array (α × β)) (a : α),
    (foldl (fun acc b => acc.push (a, b)) acc l₂).toList = acc.toList ++ map (Prod.mk a) l₂

Tactic:
intros

Result:
case h.h.h.h.H
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
acc✝ : Array (α × β)
a✝ : α
⊢ (foldl (fun acc b => acc.push (a✝, b)) acc✝ l₂).toList = acc✝.toList ++ map (Prod.mk a✝) l₂
-- Mathlib/Order/Filter/AtTopBot/Map.lean
theorem map_atTop (e : α ≃o β) : map (e : α → β) atTop = atTop

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
⊢ map (⇑e) atTop = atTop

Tactic:
rw [← e.comap_atTop, map_comap_of_surjective e.surjective]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/OfSequence.lean
lemma congr_f (i j : ℕ) (h : i = j) :
    f i = eqToHom (by rw [h]) ≫ f j ≫ eqToHom (by rw [h])

Proof state:
C : Type u_1
inst✝ : Category.{?u.122, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i j : ℕ
h : i = j
⊢ X (j + 1) = X (i + 1)

Tactic:
rw [h]

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i j : ℕ
h : i = j
⊢ f i = eqToHom ⋯ ≫ f j ≫ eqToHom ⋯

Tactic:
subst h

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i : ℕ
⊢ f i = eqToHom ⋯ ≫ f i ≫ eqToHom ⋯

Proof state:
C : Type u_1
inst✝ : Category.{?u.122, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i j : ℕ
h : i = j
⊢ X i = X j

Tactic:
rw [h]

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i : ℕ
⊢ f i = eqToHom ⋯ ≫ f i ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma mulOption_lt_mul_iff_P3 {i j} :
    ⟦mulOption x y i j⟧ < (⟦x * y⟧ : Game) ↔ P3 (x.moveLeft i) x (y.moveLeft j) y

Proof state:
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x.mulOption y i j⟧ < ⟦x * y⟧ ↔ P3 (x.moveLeft i) x (y.moveLeft j) y

Tactic:
dsimp only [mulOption, quot_sub, quot_add]

Result:
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x.moveLeft i * y⟧ + ⟦x * y.moveLeft j⟧ - ⟦x.moveLeft i * y.moveLeft j⟧ < ⟦x * y⟧ ↔
    P3 (x.moveLeft i) x (y.moveLeft j) y

Proof state:
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x.moveLeft i * y⟧ + ⟦x * y.moveLeft j⟧ - ⟦x.moveLeft i * y.moveLeft j⟧ < ⟦x * y⟧ ↔
    P3 (x.moveLeft i) x (y.moveLeft j) y

Tactic:
exact sub_lt_iff_lt_add'

Result:
no goals
-- Mathlib/Topology/Constructions.lean
lemma IsClosedEmbedding.sumElim {f : X → Z} {g : Y → Z}
    (hf : IsClosedEmbedding f) (hg : IsClosedEmbedding g) (h : Injective (Sum.elim f g)) :
    IsClosedEmbedding (Sum.elim f g)

Proof state:
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsClosedEmbedding f
hg : IsClosedEmbedding g
h : Injective (Sum.elim f g)
⊢ IsClosedEmbedding (Sum.elim f g)

Tactic:
rw [IsClosedEmbedding.isClosedEmbedding_iff_continuous_injective_isClosedMap] at hf hg ⊢

Result:
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : Continuous f ∧ Injective f ∧ IsClosedMap f
hg : Continuous g ∧ Injective g ∧ IsClosedMap g
h : Injective (Sum.elim f g)
⊢ Continuous (Sum.elim f g) ∧ Injective (Sum.elim f g) ∧ IsClosedMap (Sum.elim f g)

Proof state:
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : Continuous f ∧ Injective f ∧ IsClosedMap f
hg : Continuous g ∧ Injective g ∧ IsClosedMap g
h : Injective (Sum.elim f g)
⊢ Continuous (Sum.elim f g) ∧ Injective (Sum.elim f g) ∧ IsClosedMap (Sum.elim f g)

Tactic:
exact ⟨hf.1.sumElim hg.1, h, hf.2.2.sumElim hg.2.2⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem flatMapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
    {f : { x // p x } → m (List β)} {g : α → m (List β)} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    (l.flatMapM f) = l.unattach.flatMapM g

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
l : List { x // p x }
f : { x // p x } → m (List β)
g : α → m (List β)
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ flatMapM f l = flatMapM g l.unattach

Tactic:
unfold unattach

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
l : List { x // p x }
f : { x // p x } → m (List β)
g : α → m (List β)
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ flatMapM f l = flatMapM g (map (fun x => x.val) l)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
l : List { x // p x }
f : { x // p x } → m (List β)
g : α → m (List β)
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ flatMapM f l = flatMapM g (map (fun x => x.val) l)

Tactic:
induction l with
| nil => simp
| cons a l ih => simp [ih, hf]

Result:
no goals

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → m (List β)
g : α → m (List β)
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : flatMapM f l = flatMapM g (map (fun x => x.val) l)
⊢ flatMapM f (a :: l) = flatMapM g (map (fun x => x.val) (a :: l))

Tactic:
simp [ih, hf]

Result:
no goals

Proof state:
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → m (List β)
g : α → m (List β)
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ flatMapM f [] = flatMapM g (map (fun x => x.val) [])

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem condExpInd_nonneg {E} [NormedLatticeAddCommGroup E] [NormedSpace ℝ E] [OrderedSMul ℝ E]
    (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : E) (hx : 0 ≤ x) : 0 ≤ condExpInd E hm μ s x

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝³ : SigmaFinite (μ.trim hm)
E : Type u_7
inst✝² : NormedLatticeAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E
hx : 0 ≤ x
⊢ 0 ≤ (condExpInd E hm μ s) x

Tactic:
rw [← coeFn_le]

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝³ : SigmaFinite (μ.trim hm)
E : Type u_7
inst✝² : NormedLatticeAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E
hx : 0 ≤ x
⊢ ↑↑0 ≤ᶠ[ae μ] ↑↑((condExpInd E hm μ s) x)

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝³ : SigmaFinite (μ.trim hm)
E : Type u_7
inst✝² : NormedLatticeAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E
hx : 0 ≤ x
⊢ ↑↑0 ≤ᶠ[ae μ] ↑↑(condExpIndSMul hm hs hμs x)

Tactic:
exact (coeFn_zero E 1 μ).trans_le (condExpIndSMul_nonneg hs hμs x hx)

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝³ : SigmaFinite (μ.trim hm)
E : Type u_7
inst✝² : NormedLatticeAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E
hx : 0 ≤ x
⊢ ↑↑0 ≤ᶠ[ae μ] ↑↑((condExpInd E hm μ s) x)

Tactic:
refine EventuallyLE.trans_eq ?_ (condExpInd_ae_eq_condExpIndSMul hm hs hμs x).symm

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝³ : SigmaFinite (μ.trim hm)
E : Type u_7
inst✝² : NormedLatticeAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E
hx : 0 ≤ x
⊢ ↑↑0 ≤ᶠ[ae μ] ↑↑(condExpIndSMul hm hs hμs x)
-- Mathlib/Order/DirectedInverseSystem.lean
theorem isNatEquiv_piEquivLim [InverseSystem f] (H : ∀ x l, (equivLim x).1 l = f l.2.le x) :
    IsNatEquiv f (piEquivLim nat equivLim hi) := fun j k hj hk h t ↦ by
  obtain rfl | hj := hj.eq_or_lt
  · obtain rfl | hk := hk.eq_or_lt
    · simp [InverseSystem.map_self]
    · funext l
      simp_rw [piEquivLim, piSplitLE_lt hk, piSplitLE_eq, Equiv.trans_apply]
      rw [piLTProj, piLTLim_symm_apply hi ⟨k, hk⟩ (by exact l.2), invLimEquiv_apply_coe, H]
  · rw [piEquivLim, piSplitLE_lt (h.trans_lt hj), piSplitLE_lt hj]; apply nat

Proof state:
case inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝¹ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
equivLim : F i ≃ ↑(limit f i)
hi : IsSuccPrelimit i
inst✝ : InverseSystem f
H : ∀ (x : F i) (l : ↑(Iio i)), ↑(equivLim x) l = f ⋯ x
j k : ι
hj✝ : j ∈ Iic i
hk : k ∈ Iic i
h : k ≤ j
t : F j
hj : j < i
⊢ (piEquivLim nat equivLim hi ⟨k, hk⟩) (f h t) = piLTProj h ((piEquivLim nat equivLim hi ⟨j, hj✝⟩) t)

Tactic:
rw [piEquivLim, piSplitLE_lt (h.trans_lt hj), piSplitLE_lt hj]

Result:
case inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝¹ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
equivLim : F i ≃ ↑(limit f i)
hi : IsSuccPrelimit i
inst✝ : InverseSystem f
H : ∀ (x : F i) (l : ↑(Iio i)), ↑(equivLim x) l = f ⋯ x
j k : ι
hj✝ : j ∈ Iic i
hk : k ∈ Iic i
h : k ≤ j
t : F j
hj : j < i
⊢ ((equiv, equivLim.trans ((invLimEquiv nat).trans (piLTLim hi).symm)).1 ⟨k, ⋯⟩) (f h t) =
    piLTProj h (((equiv, equivLim.trans ((invLimEquiv nat).trans (piLTLim hi).symm)).1 ⟨j, hj⟩) t)

Proof state:
case inl.inr.h
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝¹ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝ : InverseSystem f
j k : ι
h : k ≤ j
t : F j
equiv : (j_1 : ↑(Iio j)) → F ↑j_1 ≃ piLT X ↑j_1
nat : IsNatEquiv f equiv
equivLim : F j ≃ ↑(limit f j)
hi : IsSuccPrelimit j
H : ∀ (x : F j) (l : ↑(Iio j)), ↑(equivLim x) l = f ⋯ x
hj : j ∈ Iic j
hk✝ : k ∈ Iic j
hk : k < j
l : ↑(Iio ↑⟨k, hk✝⟩)
⊢ (equiv ⟨k, hk⟩) (f h t) l = piLTProj h ((piLTLim hi).symm ((invLimEquiv nat) (equivLim t))) l

Tactic:
rw [piLTProj, piLTLim_symm_apply hi ⟨k, hk⟩ (by exact l.2), invLimEquiv_apply_coe, H]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true)

Proof state:
b : Bool
⊢ ((!b) = false) = (b = true)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_insertEntry_of_beq [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α}
    {v : β} (h : k == a) : getValue? a (insertEntry k v l) = some v

Proof state:
case false
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : (k == a) = true
h' : containsKey k l = false
⊢ getValue? a (insertEntry k v l) = some v

Tactic:
rw [insertEntry_of_containsKey_eq_false h', getValue?_cons_of_true h]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : (k == a) = true
⊢ getValue? a (insertEntry k v l) = some v

Tactic:
cases h' : containsKey k l

Result:
case false
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : (k == a) = true
h' : containsKey k l = false
⊢ getValue? a (insertEntry k v l) = some v

case true
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : (k == a) = true
h' : containsKey k l = true
⊢ getValue? a (insertEntry k v l) = some v

Proof state:
case true
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : (k == a) = true
h' : containsKey k l = true
⊢ getValue? a (insertEntry k v l) = some v

Tactic:
rw [insertEntry_of_containsKey h', getValue?_replaceEntry_of_true h' h]

Result:
no goals
-- Mathlib/GroupTheory/Coprod/Basic.lean
theorem con_inv_mul_cancel (x : FreeMonoid (G ⊕ H)) :
    coprodCon G H (ofList (x.toList.map (Sum.map Inv.inv Inv.inv)).reverse * x) 1

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
x : FreeMonoid (G ⊕ H)
⊢ mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList x)).reverse) * mk x = 1

Tactic:
induction x using FreeMonoid.inductionOn' with
| one => simp
| mul_of x xs ihx =>
  simp only [toList_of_mul, map_cons, reverse_cons, ofList_append, map_mul, ihx, ofList_singleton]
  rwa [mul_assoc, ← mul_assoc (mk (of _)), mk_of_inv_mul, one_mul]

Result:
no goals

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
x : FreeMonoid (G ⊕ H)
⊢ (coprodCon G H) (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList x)).reverse * x) 1

Tactic:
rw [← mk_eq_mk, map_mul, map_one]

Result:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
x : FreeMonoid (G ⊕ H)
⊢ mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList x)).reverse) * mk x = 1

Proof state:
case mul_of
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
x : G ⊕ H
xs : FreeMonoid (G ⊕ H)
ihx : mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList xs)).reverse) * mk xs = 1
⊢ mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList xs)).reverse) * mk (of (Sum.map Inv.inv Inv.inv x)) *
      (mk (of x) * mk xs) =
    1

Tactic:
rwa [mul_assoc, ← mul_assoc (mk (of _)), mk_of_inv_mul, one_mul]

Result:
no goals

Proof state:
case mul_of
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
x : G ⊕ H
xs : FreeMonoid (G ⊕ H)
ihx : mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList xs)).reverse) * mk xs = 1
⊢ mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList (of x * xs))).reverse) * mk (of x * xs) = 1

Tactic:
simp only [toList_of_mul, map_cons, reverse_cons, ofList_append, map_mul, ihx, ofList_singleton]

Result:
case mul_of
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
x : G ⊕ H
xs : FreeMonoid (G ⊕ H)
ihx : mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList xs)).reverse) * mk xs = 1
⊢ mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList xs)).reverse) * mk (of (Sum.map Inv.inv Inv.inv x)) *
      (mk (of x) * mk xs) =
    1

Proof state:
case one
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
⊢ mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList 1)).reverse) * mk 1 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem modEq_sub_iff_add_modEq' : a ≡ b - c [PMOD p] ↔ c + a ≡ b [PMOD p]

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a b c : α
⊢ a ≡ b - c [PMOD p] ↔ c + a ≡ b [PMOD p]

Tactic:
simp [ModEq, sub_sub]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary :
    a.toBasis.toMatrix b ∈ Matrix.unitaryGroup ι 𝕜

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
⊢ a.toBasis.toMatrix ⇑b ∈ Matrix.unitaryGroup ι 𝕜

Tactic:
rw [Matrix.mem_unitaryGroup_iff']

Result:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
⊢ star (a.toBasis.toMatrix ⇑b) * a.toBasis.toMatrix ⇑b = 1

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
⊢ star (a.toBasis.toMatrix ⇑b) * a.toBasis.toMatrix ⇑b = 1

Tactic:
exact a.toMatrix_orthonormalBasis_conjTranspose_mul_self b

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem append_right_eq_snoc {α : Sort*} {n : ℕ} (x : Fin n → α) (x₀ : Fin 1 → α) :
    Fin.append x x₀ = Fin.snoc x (x₀ 0)

Proof state:
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ append x x₀ = snoc x (x₀ 0)

Tactic:
ext i

Result:
case h
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin (n + 1)
⊢ append x x₀ i = snoc x (x₀ 0) i

Proof state:
case h.refine_2
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin 1
⊢ append x x₀ (natAdd n i) = snoc x (x₀ 0) (natAdd n i)

Tactic:
rw [Subsingleton.elim i 0, Fin.append_right]

Result:
case h.refine_2
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin 1
⊢ x₀ 0 = snoc x (x₀ 0) (natAdd n 0)

Proof state:
case h.refine_2
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin 1
⊢ x₀ 0 = snoc x (x₀ 0) (natAdd n 0)

Tactic:
exact (@snoc_last _ (fun _ => α) _ _).symm

Result:
no goals

Proof state:
case h.refine_1
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ append x x₀ (castAdd 1 i) = snoc x (x₀ 0) (castAdd 1 i)

Tactic:
rw [Fin.append_left]

Result:
case h.refine_1
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ x i = snoc x (x₀ 0) (castAdd 1 i)

Proof state:
case h.refine_1
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ ∀ (i : Fin n), append x x₀ (castAdd 1 i) = snoc x (x₀ 0) (castAdd 1 i)

Tactic:
intro i

Result:
case h.refine_1
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ append x x₀ (castAdd 1 i) = snoc x (x₀ 0) (castAdd 1 i)

Proof state:
case h
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin (n + 1)
⊢ append x x₀ i = snoc x (x₀ 0) i

Tactic:
refine Fin.addCases ?_ ?_ i <;> clear i

Result:
case h.refine_1
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ ∀ (i : Fin n), append x x₀ (castAdd 1 i) = snoc x (x₀ 0) (castAdd 1 i)

case h.refine_2
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ ∀ (i : Fin 1), append x x₀ (natAdd n i) = snoc x (x₀ 0) (natAdd n i)

Proof state:
case h.refine_1
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ x i = snoc x (x₀ 0) (castAdd 1 i)

Tactic:
exact (@snoc_castSucc _ (fun _ => α) _ _ i).symm

Result:
no goals

Proof state:
case h.refine_2
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ ∀ (i : Fin 1), append x x₀ (natAdd n i) = snoc x (x₀ 0) (natAdd n i)

Tactic:
intro i

Result:
case h.refine_2
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin 1
⊢ append x x₀ (natAdd n i) = snoc x (x₀ 0) (natAdd n i)
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma one_lt_zpow₀ (ha : 1 < a) (hn : 0 < n) : 1 < a ^ n

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
n : ℤ
ha : 1 < a
hn : 0 < n
⊢ 1 < a ^ n

Tactic:
simpa using zpow_right_strictMono₀ ha hn

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem Sorted.merge {l l' : List α} (h : Sorted r l) (h' : Sorted r l') :
    Sorted r (merge l l' (r · ·))

Proof state:
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
l l' : List α
h : Sorted r l
h' : Sorted r l'
⊢ Pairwise (fun a b => (fun x1 x2 => Decidable.decide (r x1 x2)) a b = true) l

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
l l' : List α
h : Sorted r l
h' : Sorted r l'
⊢ Pairwise (fun a b => (fun x1 x2 => Decidable.decide (r x1 x2)) a b = true) l'

Tactic:
simpa using h'

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
l l' : List α
h : Sorted r l
h' : Sorted r l'
a b c : α
h₁ : (fun x1 x2 => Decidable.decide (r x1 x2)) a b = true
h₂ : (fun x1 x2 => Decidable.decide (r x1 x2)) b c = true
⊢ (fun x1 x2 => Decidable.decide (r x1 x2)) a c = true

Tactic:
simpa using _root_.trans (by simpa using h₁) (by simpa using h₂)

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
l l' : List α
h : Sorted r l
h' : Sorted r l'
a b : α
⊢ ((fun x1 x2 => Decidable.decide (r x1 x2)) a b || (fun x1 x2 => Decidable.decide (r x1 x2)) b a) = true

Tactic:
simpa using IsTotal.total a b

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
l l' : List α
h : Sorted r l
h' : Sorted r l'
a b c : α
h₁ : (fun x1 x2 => Decidable.decide (r x1 x2)) a b = true
h₂ : (fun x1 x2 => Decidable.decide (r x1 x2)) b c = true
⊢ r b c

Tactic:
simpa using h₂

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
l l' : List α
h : Sorted r l
h' : Sorted r l'
a b c : α
h₁ : (fun x1 x2 => Decidable.decide (r x1 x2)) a b = true
h₂ : (fun x1 x2 => Decidable.decide (r x1 x2)) b c = true
⊢ r a ?m.63760

Tactic:
simpa using h₁

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem nndist_edist (x y : α) : nndist x y = (edist x y).toNNReal

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ nndist x y = (edist x y).toNNReal

Tactic:
simp [edist_nndist]

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem cauchy_sub : ∀ a b, (a - b : ℝ).cauchy = a.cauchy - b.cauchy
  | ⟨a⟩, ⟨b⟩ => by
    rw [sub_eq_add_neg, ← cauchy_neg, ← cauchy_add]
    rfl

Proof state:
a b : Cauchy abs
⊢ ({ cauchy := a } - { cauchy := b }).cauchy = ({ cauchy := a } + -{ cauchy := b }).cauchy

Tactic:
rfl

Result:
no goals

Proof state:
a b : Cauchy abs
⊢ ({ cauchy := a } - { cauchy := b }).cauchy = { cauchy := a }.cauchy - { cauchy := b }.cauchy

Tactic:
rw [sub_eq_add_neg, ← cauchy_neg, ← cauchy_add]

Result:
a b : Cauchy abs
⊢ ({ cauchy := a } - { cauchy := b }).cauchy = ({ cauchy := a } + -{ cauchy := b }).cauchy