harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Control/LawfulFix.lean
theorem ωScottContinuous_curry :
    ωScottContinuous (monotoneCurry α β γ) :=
  ωScottContinuous.of_map_ωSup_of_orderHom fun c ↦ by
    ext x y
    dsimp [curry, ωSup]
    rw [map_comp, map_comp]
    rfl

Proof state:
case h.h
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
x : α
y : β x
⊢ ωSup (c.map (evalOrderHom ⟨x, y⟩)) =
    ωSup (c.map (((evalOrderHom y).comp (evalOrderHom x)).comp (monotoneCurry α β γ)))

Tactic:
rfl

Result:
no goals

Proof state:
case h.h
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
x : α
y : β x
⊢ ωSup (c.map (evalOrderHom ⟨x, y⟩)) = ωSup (((c.map (monotoneCurry α β γ)).map (evalOrderHom x)).map (evalOrderHom y))

Tactic:
rw [map_comp, map_comp]

Result:
case h.h
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
x : α
y : β x
⊢ ωSup (c.map (evalOrderHom ⟨x, y⟩)) =
    ωSup (c.map (((evalOrderHom y).comp (evalOrderHom x)).comp (monotoneCurry α β γ)))

Proof state:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
⊢ (monotoneCurry α β γ) (ωSup c) = ωSup (c.map (monotoneCurry α β γ))

Tactic:
ext x y

Result:
case h.h
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
x : α
y : β x
⊢ (monotoneCurry α β γ) (ωSup c) x y = ωSup (c.map (monotoneCurry α β γ)) x y

Proof state:
case h.h
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
x : α
y : β x
⊢ (monotoneCurry α β γ) (ωSup c) x y = ωSup (c.map (monotoneCurry α β γ)) x y

Tactic:
dsimp [curry, ωSup]

Result:
case h.h
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
x : α
y : β x
⊢ ωSup (c.map (evalOrderHom ⟨x, y⟩)) = ωSup (((c.map (monotoneCurry α β γ)).map (evalOrderHom x)).map (evalOrderHom y))
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem isMultiplicative_moebius : IsMultiplicative μ

Proof state:
⊢ μ 1 = 1

Tactic:
simp

Result:
no goals

Proof state:
⊢ μ 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → μ (m * n) = μ m * μ n

Tactic:
refine ⟨by simp, fun {n m} hn hm hnm => ?_⟩

Result:
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : n.Coprime m
⊢ μ (n * m) = μ n * μ m

Proof state:
⊢ μ.IsMultiplicative

Tactic:
rw [IsMultiplicative.iff_ne_zero]

Result:
⊢ μ 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → μ (m * n) = μ m * μ n

Proof state:
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : n.Coprime m
⊢ μ (n * m) = μ n * μ m

Tactic:
simp only [moebius, ZeroHom.coe_mk, coe_mk, ZeroHom.toFun_eq_coe, Eq.ndrec, ZeroHom.coe_mk,
  IsUnit.mul_iff, Nat.isUnit_iff, squarefree_mul hnm, ite_zero_mul_ite_zero,
  cardFactors_mul hn hm, pow_add]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
lemma lt_coe_succ_iff_le {x : PartENat} {n : ℕ} (hx : x ≠ ⊤) : x < n.succ ↔ x ≤ n

Proof state:
x : PartENat
n : ℕ
hx : x ≠ ⊤
⊢ x < ↑n.succ ↔ x ≤ ↑n

Tactic:
rw [Nat.succ_eq_add_one n, Nat.cast_add, Nat.cast_one, lt_add_one_iff_lt hx]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem map_neighborFinset_induce_of_neighborSet_subset {v : s} (h : G.neighborSet v ⊆ s) :
    ((G.induce s).neighborFinset v).map (.subtype s) = G.neighborFinset v

Proof state:
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : ↑s
h : G.neighborSet ↑v ⊆ s
⊢ map (Embedding.subtype s) ((induce s G).neighborFinset v) = G.neighborFinset ↑v

Tactic:
rwa [← Set.toFinset_subset_toFinset, ← neighborFinset_def, ← inter_eq_left,
  ← map_neighborFinset_induce v] at h

Result:
no goals
-- Mathlib/Data/Bool/Count.lean
theorem count_add_count_not (l : List Bool) (b : Bool) : count b l + count (!b) l = length l

Proof state:
l : List Bool
b : Bool
⊢ count b l + count (!b) l = l.length

Tactic:
rw [add_comm, count_not_add_count]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem skeletal : Skeletal SimplexCategory := fun X Y ⟨I⟩ => by
  suffices Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1)) by
    ext
    simpa
  apply Fintype.card_congr
  exact ((skeletalFunctor ⋙ forget NonemptyFinLinOrd).mapIso I).toEquiv

Proof state:
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ X = Y

Tactic:
suffices Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1)) by
  ext
  simpa

Result:
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))

Proof state:
case a
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
this : Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))
⊢ X.len = Y.len

Tactic:
simpa

Result:
no goals

Proof state:
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))

Tactic:
apply Fintype.card_congr

Result:
case f
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ Fin (X.len + 1) ≃ Fin (Y.len + 1)

Proof state:
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
this : Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))
⊢ X = Y

Tactic:
ext

Result:
case a
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
this : Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))
⊢ X.len = Y.len

Proof state:
case f
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ Fin (X.len + 1) ≃ Fin (Y.len + 1)

Tactic:
exact ((skeletalFunctor ⋙ forget NonemptyFinLinOrd).mapIso I).toEquiv

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem natCast_modEq_natCast {a b n : ℕ} : a ≡ b [PMOD (n : α)] ↔ a ≡ b [MOD n]

Proof state:
α : Type u_1
inst✝¹ : AddCommGroupWithOne α
inst✝ : CharZero α
a b n : ℕ
⊢ ↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [MOD n]

Tactic:
simp_rw [← Int.natCast_modEq_iff, ← modEq_iff_int_modEq, ← @intCast_modEq_intCast α,
  Int.cast_natCast]

Result:
no goals
-- Mathlib/Order/ModularLattice.lean
theorem disjoint_sup_left_of_disjoint_sup_right [Lattice α] [OrderBot α]
    [IsModularLattice α] (h : Disjoint b c) (hsup : Disjoint a (b ⊔ c)) :
    Disjoint (a ⊔ b) c

Proof state:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint (c ⊔ b) a

Tactic:
rwa [sup_comm, disjoint_comm] at hsup

Result:
no goals

Proof state:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint (a ⊔ b) c

Tactic:
rw [disjoint_comm, sup_comm]

Result:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint c (b ⊔ a)

Proof state:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint c (b ⊔ a)

Tactic:
apply Disjoint.disjoint_sup_right_of_disjoint_sup_left h.symm

Result:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint (c ⊔ b) a
-- Mathlib/RingTheory/Derivation/Basic.lean
theorem map_intCast (n : ℤ) : D (n : A) = 0

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
n : ℤ
⊢ D ↑n = 0

Tactic:
rw [← zsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma isGreatest_spectrum [Nontrivial A] (a : A) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : Nontrivial A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ IsGreatest (σ ℝ≥0 a) ‖a‖₊

Tactic:
simpa [cfc_id ℝ≥0 a] using IsGreatest.nnnorm_cfc_nnreal id a

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem power_le_power_left : ∀ {a b c : Cardinal}, a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c

Proof state:
case mk.mk.mk.intro
a✝ : Cardinal.{u_1}
α : Type u_1
b✝ : Cardinal.{u_1}
β : Type u_1
c✝ : Cardinal.{u_1}
γ : Type u_1
hα : Quot.mk (⇑isEquivalent) α ≠ 0
e : β ↪ γ
a : α
⊢ Quot.mk (⇑isEquivalent) α ^ Quot.mk (⇑isEquivalent) β ≤ Quot.mk (⇑isEquivalent) α ^ Quot.mk (⇑isEquivalent) γ

Tactic:
exact ⟨@Function.Embedding.arrowCongrLeft _ _ _ ⟨a⟩ e⟩

Result:
no goals

Proof state:
⊢ ∀ {a b c : Cardinal.{u_1}}, a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c

Tactic:
rintro ⟨α⟩ ⟨β⟩ ⟨γ⟩ hα ⟨e⟩

Result:
case mk.mk.mk.intro
a✝ : Cardinal.{u_1}
α : Type u_1
b✝ : Cardinal.{u_1}
β : Type u_1
c✝ : Cardinal.{u_1}
γ : Type u_1
hα : Quot.mk (⇑isEquivalent) α ≠ 0
e : β ↪ γ
⊢ Quot.mk (⇑isEquivalent) α ^ Quot.mk (⇑isEquivalent) β ≤ Quot.mk (⇑isEquivalent) α ^ Quot.mk (⇑isEquivalent) γ

Proof state:
case mk.mk.mk.intro
a✝ : Cardinal.{u_1}
α : Type u_1
b✝ : Cardinal.{u_1}
β : Type u_1
c✝ : Cardinal.{u_1}
γ : Type u_1
hα : Quot.mk (⇑isEquivalent) α ≠ 0
e : β ↪ γ
⊢ Quot.mk (⇑isEquivalent) α ^ Quot.mk (⇑isEquivalent) β ≤ Quot.mk (⇑isEquivalent) α ^ Quot.mk (⇑isEquivalent) γ

Tactic:
let ⟨a⟩ := mk_ne_zero_iff.1 hα

Result:
case mk.mk.mk.intro
a✝ : Cardinal.{u_1}
α : Type u_1
b✝ : Cardinal.{u_1}
β : Type u_1
c✝ : Cardinal.{u_1}
γ : Type u_1
hα : Quot.mk (⇑isEquivalent) α ≠ 0
e : β ↪ γ
a : α
⊢ Quot.mk (⇑isEquivalent) α ^ Quot.mk (⇑isEquivalent) β ≤ Quot.mk (⇑isEquivalent) α ^ Quot.mk (⇑isEquivalent) γ
-- Mathlib/Topology/UnitInterval.lean
theorem symm_le_symm {i j : I} : σ i ≤ σ j ↔ j ≤ i

Proof state:
i j : ↑I
⊢ σ i ≤ σ j ↔ j ≤ i

Tactic:
simp only [symm, Subtype.mk_le_mk, sub_le_sub_iff, add_le_add_iff_left, Subtype.coe_le_coe]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Defs.lean
@[simp]
lemma toFinset_Iic (a : α) [Fintype (Iic a)] : (Iic a).toFinset = Finset.Iic a

Proof state:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
a : α
inst✝ : Fintype ↑(Iic a)
⊢ (Iic a).toFinset = Finset.Iic a

Tactic:
ext

Result:
case h
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
a : α
inst✝ : Fintype ↑(Iic a)
a✝ : α
⊢ a✝ ∈ (Iic a).toFinset ↔ a✝ ∈ Finset.Iic a

Proof state:
case h
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
a : α
inst✝ : Fintype ↑(Iic a)
a✝ : α
⊢ a✝ ∈ (Iic a).toFinset ↔ a✝ ∈ Finset.Iic a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem sbtw_lineMap_iff [NoZeroSMulDivisors R V] {x y : P} {r : R} :
    Sbtw R x (lineMap x y r) y ↔ x ≠ y ∧ r ∈ Set.Ioo (0 : R) 1

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
⊢ Sbtw R x ((lineMap x y) r) y ↔ x ≠ y ∧ r ∈ Set.Ioo 0 1

Tactic:
rw [sbtw_iff_mem_image_Ioo_and_ne, and_comm, and_congr_right]

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
⊢ x ≠ y → ((lineMap x y) r ∈ ⇑(lineMap x y) '' Set.Ioo 0 1 ↔ r ∈ Set.Ioo 0 1)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
⊢ x ≠ y → ((lineMap x y) r ∈ ⇑(lineMap x y) '' Set.Ioo 0 1 ↔ r ∈ Set.Ioo 0 1)

Tactic:
intro hxy

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
hxy : x ≠ y
⊢ (lineMap x y) r ∈ ⇑(lineMap x y) '' Set.Ioo 0 1 ↔ r ∈ Set.Ioo 0 1

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
hxy : x ≠ y
⊢ (lineMap x y) r ∈ ⇑(lineMap x y) '' Set.Ioo 0 1 ↔ r ∈ Set.Ioo 0 1

Tactic:
rw [(lineMap_injective R hxy).mem_set_image]

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem erase_eq_sub_single [AddGroup G] (f : α →₀ G) (a : α) : f.erase a = f - single a (f a)

Proof state:
α : Type u_1
G : Type u_9
inst✝ : AddGroup G
f : α →₀ G
a : α
⊢ erase a f = f - single a (f a)

Tactic:
ext a'

Result:
case h
α : Type u_1
G : Type u_9
inst✝ : AddGroup G
f : α →₀ G
a a' : α
⊢ (erase a f) a' = (f - single a (f a)) a'

Proof state:
case h.inl
α : Type u_1
G : Type u_9
inst✝ : AddGroup G
f : α →₀ G
a : α
⊢ (erase a f) a = (f - single a (f a)) a

Tactic:
simp

Result:
no goals

Proof state:
case h.inr
α : Type u_1
G : Type u_9
inst✝ : AddGroup G
f : α →₀ G
a a' : α
h : a ≠ a'
⊢ (erase a f) a' = (f - single a (f a)) a'

Tactic:
simp [erase_ne h.symm, single_eq_of_ne h]

Result:
no goals

Proof state:
case h
α : Type u_1
G : Type u_9
inst✝ : AddGroup G
f : α →₀ G
a a' : α
⊢ (erase a f) a' = (f - single a (f a)) a'

Tactic:
rcases eq_or_ne a a' with (rfl | h)

Result:
case h.inl
α : Type u_1
G : Type u_9
inst✝ : AddGroup G
f : α →₀ G
a : α
⊢ (erase a f) a = (f - single a (f a)) a

case h.inr
α : Type u_1
G : Type u_9
inst✝ : AddGroup G
f : α →₀ G
a a' : α
h : a ≠ a'
⊢ (erase a f) a' = (f - single a (f a)) a'
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem singleton_div_ball_one : {x} / ball 1 δ = ball x δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ {x} / ball 1 δ = ball x δ

Tactic:
rw [singleton_div_ball, div_one]

Result:
no goals
-- Mathlib/GroupTheory/PushoutI.lean
theorem cons_eq_smul {i : ι} (g : G i)
    (w : NormalWord d) (hmw : w.fstIdx ≠ some i)
    (hgr : g ∉ (φ i).range) : cons g w hmw hgr = of (φ := φ) i g  • w

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
hmw : w.fstIdx ≠ some i
hgr : g ∉ (φ i).range
⊢ CoprodI.of ((φ i) (cons g w hmw hgr).head) • (cons g w hmw hgr).toWord =
    CoprodI.of ((φ i) ((of i) g • w).head) • ((of i) g • w).toWord

Tactic:
simp only [cons, ne_eq, Word.cons_eq_smul, MonoidHom.apply_ofInjective_symm,
  equiv_fst_eq_mul_inv, mul_assoc, map_mul, map_inv, mul_smul, inv_smul_smul, summand_smul_def,
  equivPair, rcons, Word.equivPair_symm, Word.rcons_eq_smul, Equiv.coe_fn_mk,
  Word.equivPair_tail_eq_inv_smul, Equiv.coe_fn_symm_mk, smul_inv_smul]

Result:
no goals

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
hmw : w.fstIdx ≠ some i
hgr : g ∉ (φ i).range
⊢ cons g w hmw hgr = (of i) g • w

Tactic:
apply ext_smul i

Result:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
hmw : w.fstIdx ≠ some i
hgr : g ∉ (φ i).range
⊢ CoprodI.of ((φ i) (cons g w hmw hgr).head) • (cons g w hmw hgr).toWord =
    CoprodI.of ((φ i) ((of i) g • w).head) • ((of i) g • w).toWord
-- Mathlib/Data/List/Chain.lean
lemma Chain'.iterate_eq_of_apply_eq {α : Type*} {f : α → α} {l : List α}
    (hl : l.Chain' (fun x y ↦ f x = y)) (i : ℕ) (hi : i < l.length) :
    f^[i] l[0] = l[i]

Proof state:
case succ
α : Type u_1
f : α → α
l : List α
hl : ∀ (i : ℕ) (h : i < l.length - 1), f (l.get ⟨i, ⋯⟩) = l.get ⟨i + 1, ⋯⟩
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ f l[i] = l[i + 1]

Tactic:
apply hl

Result:
case succ.h
α : Type u_1
f : α → α
l : List α
hl : ∀ (i : ℕ) (h : i < l.length - 1), f (l.get ⟨i, ⋯⟩) = l.get ⟨i + 1, ⋯⟩
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ i < l.length - 1

Proof state:
α : Type u_1
f : α → α
l : List α
hl : Chain' (fun x y => f x = y) l
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ i < l.length

Tactic:
omega

Result:
no goals

Proof state:
case succ
α : Type u_1
f : α → α
l : List α
hl : Chain' (fun x y => f x = y) l
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ f l[i] = l[i + 1]

Tactic:
rw [List.chain'_iff_get] at hl

Result:
case succ
α : Type u_1
f : α → α
l : List α
hl : ∀ (i : ℕ) (h : i < l.length - 1), f (l.get ⟨i, ⋯⟩) = l.get ⟨i + 1, ⋯⟩
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ f l[i] = l[i + 1]

Proof state:
case succ.h
α : Type u_1
f : α → α
l : List α
hl : ∀ (i : ℕ) (h : i < l.length - 1), f (l.get ⟨i, ⋯⟩) = l.get ⟨i + 1, ⋯⟩
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ i < l.length - 1

Tactic:
omega

Result:
no goals

Proof state:
case zero
α : Type u_1
f : α → α
l : List α
hl : Chain' (fun x y => f x = y) l
hi : 0 < l.length
⊢ f^[0] l[0] = l[0]

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
f : α → α
l : List α
hl : Chain' (fun x y => f x = y) l
i : ℕ
hi : i < l.length
⊢ f^[i] l[0] = l[i]

Tactic:
induction' i with i h

Result:
case zero
α : Type u_1
f : α → α
l : List α
hl : Chain' (fun x y => f x = y) l
hi : 0 < l.length
⊢ f^[0] l[0] = l[0]

case succ
α : Type u_1
f : α → α
l : List α
hl : Chain' (fun x y => f x = y) l
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ f^[i + 1] l[0] = l[i + 1]

Proof state:
case succ
α : Type u_1
f : α → α
l : List α
hl : Chain' (fun x y => f x = y) l
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ f^[i + 1] l[0] = l[i + 1]

Tactic:
rw [Function.iterate_succ', Function.comp_apply, h (by omega)]

Result:
case succ
α : Type u_1
f : α → α
l : List α
hl : Chain' (fun x y => f x = y) l
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ f l[i] = l[i + 1]
-- Mathlib/Algebra/Homology/Embedding/Basic.lean
lemma r_eq_none (i' : ι') (hi : ∀ i, e.f i ≠ i') :
    e.r i' = none :=
  dif_neg (by
    rintro ⟨i, hi'⟩
    exact hi i hi')

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
hi : ∀ (i : ι), e.f i ≠ i'
⊢ ¬∃ i, e.f i = i'

Tactic:
rintro ⟨i, hi'⟩

Result:
case intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
hi : ∀ (i : ι), e.f i ≠ i'
i : ι
hi' : e.f i = i'
⊢ False

Proof state:
case intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
hi : ∀ (i : ι), e.f i ≠ i'
i : ι
hi' : e.f i = i'
⊢ False

Tactic:
exact hi i hi'

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem id_whiskerLeft_symm {X X' : C} (f : X ⟶ X') :
    f = (λ_ X).inv ≫ 𝟙_ C ◁ f ≫ (λ_ X').hom

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' : C
f : X ⟶ X'
⊢ f = (λ_ X).inv ≫ 𝟙_ C ◁ f ≫ (λ_ X').hom

Tactic:
simp only [id_whiskerLeft, assoc, inv_hom_id, comp_id, inv_hom_id_assoc]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma integral_condKernel (a : α) (hf : Integrable f (κ a)) :
    ∫ b, ∫ ω, f (b, ω) ∂(Kernel.condKernel κ (a, b)) ∂(Kernel.fst κ a) = ∫ x, f x ∂(κ a)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
hf : Integrable f (κ a)
⊢ ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω), f x ∂κ a

Tactic:
conv_rhs => rw [← κ.disintegrate κ.condKernel]

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
hf : Integrable f (κ a)
⊢ ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω), f x ∂(κ.fst ⊗ₖ κ.condKernel) a

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
hf : Integrable f (κ a)
⊢ ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω), f x ∂(κ.fst ⊗ₖ κ.condKernel) a

Tactic:
rw [← κ.disintegrate κ.condKernel] at hf

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
hf : Integrable f ((κ.fst ⊗ₖ κ.condKernel) a)
⊢ ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω), f x ∂(κ.fst ⊗ₖ κ.condKernel) a

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
hf : Integrable f ((κ.fst ⊗ₖ κ.condKernel) a)
⊢ ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω), f x ∂(κ.fst ⊗ₖ κ.condKernel) a

Tactic:
rw [integral_compProd hf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem flatMap_toArray {β} (f : α → Array β) (as : List α) :
    as.toArray.flatMap f = (as.flatMap (fun a => (f a).toList)).toArray

Proof state:
case cons.h
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
ih : Array.flatMap f as.toArray = (flatMap (fun a => (f a).toList) as).toArray
⊢ (Array.flatMap f (a :: as).toArray).toList = (flatMap (fun a => (f a).toList) (a :: as)).toArray.toList

Tactic:
simp [ih, flatMap_toArray_cons]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → Array β
⊢ Array.flatMap f #[] = (flatMap (fun a => (f a).toList) []).toArray

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Array β
as : List α
⊢ Array.flatMap f as.toArray = (flatMap (fun a => (f a).toList) as).toArray

Tactic:
induction as with
| nil => simp
| cons a as ih =>
  apply ext'
  simp [ih, flatMap_toArray_cons]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
ih : Array.flatMap f as.toArray = (flatMap (fun a => (f a).toList) as).toArray
⊢ Array.flatMap f (a :: as).toArray = (flatMap (fun a => (f a).toList) (a :: as)).toArray

Tactic:
apply ext'

Result:
case cons.h
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
ih : Array.flatMap f as.toArray = (flatMap (fun a => (f a).toList) as).toArray
⊢ (Array.flatMap f (a :: as).toArray).toList = (flatMap (fun a => (f a).toList) (a :: as)).toArray.toList
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ne_of_lt {x y : BitVec n} : x < y → x ≠ y

Proof state:
n : Nat
x y : BitVec n
⊢ x.toNat < y.toNat → ¬x.toNat = y.toNat

Tactic:
apply Nat.ne_of_lt

Result:
no goals

Proof state:
n : Nat
x y : BitVec n
⊢ x < y → x ≠ y

Tactic:
simp only [lt_def, ne_eq, toNat_eq]

Result:
n : Nat
x y : BitVec n
⊢ x.toNat < y.toNat → ¬x.toNat = y.toNat