harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem lintegral_sum {m : MeasurableSpace α} {ι} (f : α →ₛ ℝ≥0∞) (μ : ι → Measure α) :
    f.lintegral (Measure.sum μ) = ∑' i, f.lintegral (μ i)

Proof state:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
f : α →ₛ ℝ≥0∞
μ : ι → Measure α
⊢ f.lintegral (Measure.sum μ) = ∑' (i : ι), f.lintegral (μ i)

Tactic:
simp only [lintegral, Measure.sum_apply, f.measurableSet_preimage, ← Finset.tsum_subtype, ←
  ENNReal.tsum_mul_left]

Result:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
f : α →ₛ ℝ≥0∞
μ : ι → Measure α
⊢ ∑' (x : { x // x ∈ f.range }) (i : ι), ↑x * (μ i) (⇑f ⁻¹' {↑x}) =
    ∑' (i : ι) (x : { x // x ∈ f.range }), ↑x * (μ i) (⇑f ⁻¹' {↑x})

Proof state:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
f : α →ₛ ℝ≥0∞
μ : ι → Measure α
⊢ ∑' (x : { x // x ∈ f.range }) (i : ι), ↑x * (μ i) (⇑f ⁻¹' {↑x}) =
    ∑' (i : ι) (x : { x // x ∈ f.range }), ↑x * (μ i) (⇑f ⁻¹' {↑x})

Tactic:
apply ENNReal.tsum_comm

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem compChangeOfVariables_blocksFun (m M N : ℕ) {i : Σ n, Fin n → ℕ}
    (hi : i ∈ compPartialSumSource m M N) (j : Fin i.1) :
    (compChangeOfVariables m M N i hi).2.blocksFun
        ⟨j, (compChangeOfVariables_length m M N hi).symm ▸ j.2⟩ =
      i.2 j

Proof state:
case mk
m M N n : ℕ
f : Fin n → ℕ
hi : ⟨n, f⟩ ∈ compPartialSumSource m M N
j : Fin ⟨n, f⟩.fst
⊢ (compChangeOfVariables m M N ⟨n, f⟩ hi).snd.blocksFun ⟨↑j, ⋯⟩ = ⟨n, f⟩.snd j

Tactic:
dsimp [Composition.blocksFun, Composition.blocks, compChangeOfVariables]

Result:
case mk
m M N n : ℕ
f : Fin n → ℕ
hi : ⟨n, f⟩ ∈ compPartialSumSource m M N
j : Fin ⟨n, f⟩.fst
⊢ (ofFn fun a => f a)[↑j] = f j

Proof state:
case mk
m M N n : ℕ
f : Fin n → ℕ
hi : ⟨n, f⟩ ∈ compPartialSumSource m M N
j : Fin ⟨n, f⟩.fst
⊢ (ofFn fun a => f a)[↑j] = f j

Tactic:
simp only [map_ofFn, List.getElem_ofFn, Function.comp_apply]

Result:
no goals

Proof state:
m M N : ℕ
i : (n : ℕ) × (Fin n → ℕ)
hi : i ∈ compPartialSumSource m M N
j : Fin i.fst
⊢ (compChangeOfVariables m M N i hi).snd.blocksFun ⟨↑j, ⋯⟩ = i.snd j

Tactic:
rcases i with ⟨n, f⟩

Result:
case mk
m M N n : ℕ
f : Fin n → ℕ
hi : ⟨n, f⟩ ∈ compPartialSumSource m M N
j : Fin ⟨n, f⟩.fst
⊢ (compChangeOfVariables m M N ⟨n, f⟩ hi).snd.blocksFun ⟨↑j, ⋯⟩ = ⟨n, f⟩.snd j
-- Mathlib/Order/Interval/Set/Basic.lean
theorem compl_Ioc : (Ioc a b)ᶜ = Iic a ∪ Ioi b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (Ioc a b)ᶜ = Iic a ∪ Ioi b

Tactic:
ext i

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b i : α
⊢ i ∈ (Ioc a b)ᶜ ↔ i ∈ Iic a ∪ Ioi b

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b i : α
⊢ i ∈ (Ioc a b)ᶜ ↔ i ∈ Iic a ∪ Ioi b

Tactic:
rw [mem_compl_iff, mem_Ioc, mem_union, mem_Iic, mem_Ioi, not_and_or, not_lt, not_le]

Result:
no goals
-- Mathlib/Analysis/Complex/AbsMax.lean
theorem norm_eqOn_closedBall_of_isMaxOn {f : E → F} {z : E} {r : ℝ}
    (hd : DiffContOnCl ℂ f (ball z r)) (hz : IsMaxOn (norm ∘ f) (ball z r) z) :
    EqOn (norm ∘ f) (const E ‖f z‖) (closedBall z r)

Proof state:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hr : dist 1 0 = 1
⊢ MapsTo e (ball 0 1) (ball z r)

Tactic:
refine ((lipschitzWith_lineMap z w).mapsTo_ball (mt nndist_eq_zero.1 hne) 0 1).mono
  Subset.rfl ?_

Result:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hr : dist 1 0 = 1
⊢ ball ((lineMap z w) 0) (↑(nndist z w) * 1) ⊆ ball z r

Proof state:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hr : dist 1 0 = 1
⊢ ball ((lineMap z w) 0) (↑(nndist z w) * 1) ⊆ ball z r

Tactic:
simpa only [lineMap_apply_zero, mul_one, coe_nndist] using ball_subset_ball hw

Result:
no goals

Proof state:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
⊢ dist 1 0 = 1

Tactic:
simp

Result:
no goals

Proof state:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
⊢ EqOn (norm ∘ f) (Function.const E ‖f z‖) (closedBall z r)

Tactic:
intro w hw

Result:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : w ∈ closedBall z r
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w
-- Mathlib/Data/Int/Interval.lean
theorem card_fintype_Ico_of_le (h : a ≤ b) : (Fintype.card (Set.Ico a b) : ℤ) = b - a

Proof state:
a b : ℤ
h : a ≤ b
⊢ ↑(Fintype.card ↑(Set.Ico a b)) = b - a

Tactic:
rw [card_fintype_Ico, toNat_sub_of_le h]

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean
lemma IsDynCoverOf.preimage (h : Semiconj φ S T) {F : Set X} {V : Set (Y × Y)}
    (V_symm : SymmetricRel V) {n : ℕ} {t : Finset Y} (h' : IsDynCoverOf T (φ '' F) V n t) :
    ∃ s : Finset X, IsDynCoverOf S F ((map φ φ) ⁻¹' (V ○ V)) n s ∧ s.card ≤ t.card

Proof state:
case inr.intro.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_symm : SymmetricRel V
n : ℕ
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : Nonempty X
s : Finset Y
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
g : Y → Y
gs_cover : ∀ x ∈ s, g x ∈ ball x (dynEntourage T V n) ∩ φ '' F
f : Y → X
f_section : ∀ y ∈ φ '' F, f y ∈ F ∧ φ (f y) = y
s_cover : F ⊆ ⋃ i ∈ s, φ ⁻¹' ball i (dynEntourage T V n)
⊢ ⋃ i ∈ s, φ ⁻¹' ball i (dynEntourage T V n) ⊆ ⋃ y ∈ s, ball ((f ∘ g) y) (map φ φ ⁻¹' dynEntourage T (V ○ V) n)

Tactic:
refine iUnion₂_mono fun i i_s ↦ ?_

Result:
case inr.intro.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_symm : SymmetricRel V
n : ℕ
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : Nonempty X
s : Finset Y
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
g : Y → Y
gs_cover : ∀ x ∈ s, g x ∈ ball x (dynEntourage T V n) ∩ φ '' F
f : Y → X
f_section : ∀ y ∈ φ '' F, f y ∈ F ∧ φ (f y) = y
s_cover : F ⊆ ⋃ i ∈ s, φ ⁻¹' ball i (dynEntourage T V n)
i : Y
i_s : i ∈ s
⊢ φ ⁻¹' ball i (dynEntourage T V n) ⊆ ball ((f ∘ g) i) (map φ φ ⁻¹' dynEntourage T (V ○ V) n)

Proof state:
case inr.intro.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_symm : SymmetricRel V
n : ℕ
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : Nonempty X
s : Finset Y
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
g : Y → Y
gs_cover : ∀ x ∈ s, g x ∈ ball x (dynEntourage T V n) ∩ φ '' F
f : Y → X
f_section : ∀ y ∈ φ '' F, f y ∈ F ∧ φ (f y) = y
s_cover : F ⊆ ⋃ i ∈ s, φ ⁻¹' ball i (dynEntourage T V n)
⊢ ⋃ i ∈ s, φ ⁻¹' ball i (dynEntourage T V n) ⊆
    ⋃ x ∈ Finset.image (f ∘ g) s, ball x (dynEntourage S (map φ φ ⁻¹' (V ○ V)) n)

Tactic:
rw [← h.preimage_dynEntourage (V ○ V) n, Finset.set_biUnion_finset_image]

Result:
case inr.intro.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_symm : SymmetricRel V
n : ℕ
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : Nonempty X
s : Finset Y
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
g : Y → Y
gs_cover : ∀ x ∈ s, g x ∈ ball x (dynEntourage T V n) ∩ φ '' F
f : Y → X
f_section : ∀ y ∈ φ '' F, f y ∈ F ∧ φ (f y) = y
s_cover : F ⊆ ⋃ i ∈ s, φ ⁻¹' ball i (dynEntourage T V n)
⊢ ⋃ i ∈ s, φ ⁻¹' ball i (dynEntourage T V n) ⊆ ⋃ y ∈ s, ball ((f ∘ g) y) (map φ φ ⁻¹' dynEntourage T (V ○ V) n)
-- Mathlib/Data/List/Cycle.lean
theorem next_getElem (l : List α) (h : Nodup l) (i : Nat) (hi : i < l.length) :
    next l l[i] (get_mem _ _) =
      (l[(i + 1) % l.length]'(Nat.mod_lt _ (i.zero_le.trans_lt hi))) :=
  match l, h, i, hi with
  | [], _, i, hi => by simp at hi
  | [_], _, _, _ => by simp
  | x::y::l, _h, 0, h0 => by
    have h₁ : (x :: y :: l)[0] = x

Proof state:
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h✝ : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[i + 1] ≠ x
hi'✝ : i ≤ l.length
hi' : i < l.length
h : (x :: y :: l)[i + 1] = (x :: y :: l)[(x :: y :: l).length - 1]
⊢ False

Tactic:
have := nodup_iff_injective_get.1 hn h

Result:
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h✝ : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[i + 1] ≠ x
hi'✝ : i ≤ l.length
hi' : i < l.length
h : (x :: y :: l)[i + 1] = (x :: y :: l)[(x :: y :: l).length - 1]
this : ⟨i + 1, hi⟩ = ⟨(x :: y :: l).length - 1, ⋯⟩
⊢ False

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 < (x :: y :: l).length
H : (x :: y :: l)[i + 1] = x
this : i + 1 = 0
⊢ False

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : Function.Injective (x :: y :: l).get
i : ℕ
hi : i + 1 < (x :: y :: l).length
H : (x :: y :: l)[i + 1] = x
⊢ 0 < (x :: y :: l).length

Tactic:
simp

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[i + 1] ≠ x
hi'✝ : i ≤ l.length
hi' : i < l.length
⊢ (y :: l).next (x :: y :: l)[i + 1] ⋯ = (x :: y :: l)[(i + 1 + 1) % (x :: y :: l).length]

Tactic:
simp only [getElem_cons_succ]

Result:
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[i + 1] ≠ x
hi'✝ : i ≤ l.length
hi' : i < l.length
⊢ (y :: l).next (y :: l)[i] ⋯ = (x :: y :: l)[(i + 1 + 1) % (x :: y :: l).length]
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem comap_map {β} {f : α → β} (hf : Injective f) (m : OuterMeasure α) : comap f (map f m) = m :=
  ext fun s => by rw [comap_apply, map_apply, hf.preimage_image]

Proof state:
α : Type u_1
β : Type u_3
f : α → β
hf : Injective f
m : OuterMeasure α
s : Set α
⊢ ((comap f) ((map f) m)) s = m s

Tactic:
rw [comap_apply, map_apply, hf.preimage_image]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem mod_two_pos_mod_two_eq_one : x % 2 ^ j % 2 = 1 ↔ (0 < j) ∧ x % 2 = 1

Proof state:
x j : Nat
⊢ (decide (0 < j) && x.testBit 0) = true ↔ 0 < j ∧ x % 2 = 1

Tactic:
simp

Result:
no goals

Proof state:
x j : Nat
⊢ x % 2 ^ j % 2 = 1 ↔ 0 < j ∧ x % 2 = 1

Tactic:
rw [mod_two_eq_one_iff_testBit_zero, testBit_mod_two_pow]

Result:
x j : Nat
⊢ (decide (0 < j) && x.testBit 0) = true ↔ 0 < j ∧ x % 2 = 1
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKeyD_eq_fallback [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α}
    (h : containsKey a l = false) : getKeyD a l fallback = fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
a fallback : α
h : containsKey a l = false
⊢ getKeyD a l fallback = fallback

Tactic:
rw [containsKey_eq_isSome_getKey?, Bool.eq_false_iff, ne_eq,
  Option.not_isSome_iff_eq_none] at h

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
a fallback : α
h : getKey? a l = none
⊢ getKeyD a l fallback = fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
a fallback : α
h : getKey? a l = none
⊢ getKeyD a l fallback = fallback

Tactic:
rw [getKeyD_eq_getKey?, h, Option.getD_none]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_mul_X : eval₂ f x (p * X) = eval₂ f x p * x

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x (p * X) = eval₂ f x p * x

Tactic:
refine _root_.trans (eval₂_mul_noncomm _ _ fun k => ?_) (by rw [eval₂_X])

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
k : ℕ
⊢ Commute (f (X.coeff k)) x

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
k : ℕ
⊢ Commute (f (X.coeff k)) x

Tactic:
rcases em (k = 1) with (rfl | hk)

Result:
case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ Commute (f (X.coeff 1)) x

case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
k : ℕ
hk : ¬k = 1
⊢ Commute (f (X.coeff k)) x

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x p * eval₂ f x X = eval₂ f x p * x

Tactic:
rw [eval₂_X]

Result:
no goals

Proof state:
case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ Commute (f (X.coeff 1)) x

Tactic:
simp

Result:
no goals

Proof state:
case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
k : ℕ
hk : ¬k = 1
⊢ Commute (f (X.coeff k)) x

Tactic:
simp [coeff_X_of_ne_one hk]

Result:
no goals
-- Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean
theorem FreeAbelianGroup.toFinsupp_comp_toFreeAbelianGroup :
    toFinsupp.comp toFreeAbelianGroup = AddMonoidHom.id (X →₀ ℤ)

Proof state:
X : Type u_1
⊢ toFinsupp.comp toFreeAbelianGroup = AddMonoidHom.id (X →₀ ℤ)

Tactic:
ext x y

Result:
case H.h1.h
X : Type u_1
x y : X
⊢ (((toFinsupp.comp toFreeAbelianGroup).comp (singleAddHom x)) 1) y =
    (((AddMonoidHom.id (X →₀ ℤ)).comp (singleAddHom x)) 1) y

Proof state:
case H.h1.h
X : Type u_1
x y : X
⊢ ((toFinsupp.comp ((smulAddHom ℤ (FreeAbelianGroup X)).flip (of x))) 1) y = ((singleAddHom x) 1) y

Tactic:
simp only [toFinsupp, AddMonoidHom.coe_comp, Finsupp.singleAddHom_apply, Function.comp_apply,
  one_smul, lift.of, AddMonoidHom.flip_apply, smulAddHom_apply, AddMonoidHom.id_apply]

Result:
no goals

Proof state:
case H.h1.h
X : Type u_1
x y : X
⊢ (((toFinsupp.comp toFreeAbelianGroup).comp (singleAddHom x)) 1) y = ((singleAddHom x) 1) y

Tactic:
rw [AddMonoidHom.comp_assoc, Finsupp.toFreeAbelianGroup_comp_singleAddHom]

Result:
case H.h1.h
X : Type u_1
x y : X
⊢ ((toFinsupp.comp ((smulAddHom ℤ (FreeAbelianGroup X)).flip (of x))) 1) y = ((singleAddHom x) 1) y

Proof state:
case H.h1.h
X : Type u_1
x y : X
⊢ (((toFinsupp.comp toFreeAbelianGroup).comp (singleAddHom x)) 1) y =
    (((AddMonoidHom.id (X →₀ ℤ)).comp (singleAddHom x)) 1) y

Tactic:
simp only [AddMonoidHom.id_comp]

Result:
case H.h1.h
X : Type u_1
x y : X
⊢ (((toFinsupp.comp toFreeAbelianGroup).comp (singleAddHom x)) 1) y = ((singleAddHom x) 1) y
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem insert_val [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} {b : β a} :
    m.val.insert a b = m.insert a b

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
⊢ m.val.insert a b = (m.insert a b).val

Tactic:
simp [Raw.insert, m.2]

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem isRestriction_iff_exists : (N ≤r M) ↔ ∃ R, R ⊆ M.E ∧ N = M ↾ R

Proof state:
case mpr
α : Type u_1
M N : Matroid α
⊢ (∃ R ⊆ M.E, N = M ↾ R) → N ≤r M

Tactic:
rintro ⟨R, hR, rfl⟩

Result:
case mpr.intro.intro
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ M ↾ R ≤r M

Proof state:
case mpr.intro.intro
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ M ↾ R ≤r M

Tactic:
exact restrict_isRestriction M R hR

Result:
no goals

Proof state:
α : Type u_1
M N : Matroid α
⊢ N ≤r M ↔ ∃ R ⊆ M.E, N = M ↾ R

Tactic:
use IsRestriction.exists_eq_restrict

Result:
case mpr
α : Type u_1
M N : Matroid α
⊢ (∃ R ⊆ M.E, N = M ↾ R) → N ≤r M
-- Mathlib/MeasureTheory/Measure/MutuallySingular.lean
lemma mutuallySingular_tfae : List.TFAE
    [ μ ⟂ₘ ν,
      Disjoint μ ν,
      Disjoint (ae μ) (ae ν) ]

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : μ ⟂ₘ ν → Disjoint μ ν
tfae_2_to_1 : Disjoint μ ν → μ ⟂ₘ ν
tfae_1_to_3 : μ ⟂ₘ ν → Disjoint (ae μ) (ae ν)
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE

Tactic:
tfae_have 3 → 2
| h => disjoint_of_disjoint_ae h

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : μ ⟂ₘ ν → Disjoint μ ν
tfae_2_to_1 : Disjoint μ ν → μ ⟂ₘ ν
tfae_1_to_3 : μ ⟂ₘ ν → Disjoint (ae μ) (ae ν)
tfae_3_to_2 : Disjoint (ae μ) (ae ν) → Disjoint μ ν
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : μ ⟂ₘ ν → Disjoint μ ν
tfae_2_to_1 : Disjoint μ ν → μ ⟂ₘ ν
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE

Tactic:
tfae_have 1 → 3
| h => h.disjoint_ae

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : μ ⟂ₘ ν → Disjoint μ ν
tfae_2_to_1 : Disjoint μ ν → μ ⟂ₘ ν
tfae_1_to_3 : μ ⟂ₘ ν → Disjoint (ae μ) (ae ν)
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE

Tactic:
tfae_have 1 → 2
| h => h.disjoint

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : μ ⟂ₘ ν → Disjoint μ ν
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : μ ⟂ₘ ν → Disjoint μ ν
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE

Tactic:
tfae_have 2 → 1
| h => mutuallySingular_of_disjoint h

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : μ ⟂ₘ ν → Disjoint μ ν
tfae_2_to_1 : Disjoint μ ν → μ ⟂ₘ ν
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : μ ⟂ₘ ν → Disjoint μ ν
tfae_2_to_1 : Disjoint μ ν → μ ⟂ₘ ν
tfae_1_to_3 : μ ⟂ₘ ν → Disjoint (ae μ) (ae ν)
tfae_3_to_2 : Disjoint (ae μ) (ae ν) → Disjoint μ ν
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE

Tactic:
tfae_finish

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem pathComponent_congr (h : x ∈ pathComponent y) : pathComponent x = pathComponent y

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
⊢ pathComponent x = pathComponent y

Tactic:
ext z

Result:
case h
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent x ↔ z ∈ pathComponent y

Proof state:
case h.mpr
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent y
⊢ z ∈ pathComponent x

Tactic:
rw [pathComponent_symm] at h' ⊢

Result:
case h.mpr
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : y ∈ pathComponent z
⊢ x ∈ pathComponent z

Proof state:
case h.mp
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent x
⊢ y ∈ pathComponent z

Tactic:
exact (h.trans h').symm

Result:
no goals

Proof state:
case h.mpr
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent y → z ∈ pathComponent x

Tactic:
intro h'

Result:
case h.mpr
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent y
⊢ z ∈ pathComponent x

Proof state:
case h.mp
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent x
⊢ z ∈ pathComponent y

Tactic:
rw [pathComponent_symm]

Result:
case h.mp
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent x
⊢ y ∈ pathComponent z

Proof state:
case h.mp
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent x → z ∈ pathComponent y

Tactic:
intro h'

Result:
case h.mp
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent x
⊢ z ∈ pathComponent y

Proof state:
case h.mpr
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : y ∈ pathComponent z
⊢ x ∈ pathComponent z

Tactic:
exact h'.trans h

Result:
no goals

Proof state:
case h
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent x ↔ z ∈ pathComponent y

Tactic:
constructor

Result:
case h.mp
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent x → z ∈ pathComponent y

case h.mpr
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent y → z ∈ pathComponent x
-- Mathlib/CategoryTheory/Category/ReflQuiv.lean
theorem forgetToQuiv_faithful {V W : ReflQuiv} (F G : V ⥤rq W)
    (hyp : forgetToQuiv.map F = forgetToQuiv.map G) : F = G

Proof state:
case mk.mk.refl
V W : ReflQuiv
toPrefunctor✝ : ↑V ⥤q ↑W
map_id✝¹ map_id✝ : ∀ (X : ↑V), toPrefunctor✝.map (𝟙rq X) = 𝟙rq (toPrefunctor✝.obj X)
⊢ { toPrefunctor := toPrefunctor✝, map_id := map_id✝¹ } = { toPrefunctor := toPrefunctor✝, map_id := map_id✝ }

Tactic:
rfl

Result:
no goals

Proof state:
V W : ReflQuiv
F G : ↑V ⥤rq ↑W
hyp : forgetToQuiv.map F = forgetToQuiv.map G
⊢ F = G

Tactic:
cases F

Result:
case mk
V W : ReflQuiv
G : ↑V ⥤rq ↑W
toPrefunctor✝ : ↑V ⥤q ↑W
map_id✝ : ∀ (X : ↑V), toPrefunctor✝.map (𝟙rq X) = 𝟙rq (toPrefunctor✝.obj X)
hyp : forgetToQuiv.map { toPrefunctor := toPrefunctor✝, map_id := map_id✝ } = forgetToQuiv.map G
⊢ { toPrefunctor := toPrefunctor✝, map_id := map_id✝ } = G

Proof state:
case mk.mk
V W : ReflQuiv
toPrefunctor✝¹ : ↑V ⥤q ↑W
map_id✝¹ : ∀ (X : ↑V), toPrefunctor✝¹.map (𝟙rq X) = 𝟙rq (toPrefunctor✝¹.obj X)
toPrefunctor✝ : ↑V ⥤q ↑W
map_id✝ : ∀ (X : ↑V), toPrefunctor✝.map (𝟙rq X) = 𝟙rq (toPrefunctor✝.obj X)
hyp :
  forgetToQuiv.map { toPrefunctor := toPrefunctor✝¹, map_id := map_id✝¹ } =
    forgetToQuiv.map { toPrefunctor := toPrefunctor✝, map_id := map_id✝ }
⊢ { toPrefunctor := toPrefunctor✝¹, map_id := map_id✝¹ } = { toPrefunctor := toPrefunctor✝, map_id := map_id✝ }

Tactic:
cases hyp

Result:
case mk.mk.refl
V W : ReflQuiv
toPrefunctor✝ : ↑V ⥤q ↑W
map_id✝¹ map_id✝ : ∀ (X : ↑V), toPrefunctor✝.map (𝟙rq X) = 𝟙rq (toPrefunctor✝.obj X)
⊢ { toPrefunctor := toPrefunctor✝, map_id := map_id✝¹ } = { toPrefunctor := toPrefunctor✝, map_id := map_id✝ }

Proof state:
case mk
V W : ReflQuiv
G : ↑V ⥤rq ↑W
toPrefunctor✝ : ↑V ⥤q ↑W
map_id✝ : ∀ (X : ↑V), toPrefunctor✝.map (𝟙rq X) = 𝟙rq (toPrefunctor✝.obj X)
hyp : forgetToQuiv.map { toPrefunctor := toPrefunctor✝, map_id := map_id✝ } = forgetToQuiv.map G
⊢ { toPrefunctor := toPrefunctor✝, map_id := map_id✝ } = G

Tactic:
cases G

Result:
case mk.mk
V W : ReflQuiv
toPrefunctor✝¹ : ↑V ⥤q ↑W
map_id✝¹ : ∀ (X : ↑V), toPrefunctor✝¹.map (𝟙rq X) = 𝟙rq (toPrefunctor✝¹.obj X)
toPrefunctor✝ : ↑V ⥤q ↑W
map_id✝ : ∀ (X : ↑V), toPrefunctor✝.map (𝟙rq X) = 𝟙rq (toPrefunctor✝.obj X)
hyp :
  forgetToQuiv.map { toPrefunctor := toPrefunctor✝¹, map_id := map_id✝¹ } =
    forgetToQuiv.map { toPrefunctor := toPrefunctor✝, map_id := map_id✝ }
⊢ { toPrefunctor := toPrefunctor✝¹, map_id := map_id✝¹ } = { toPrefunctor := toPrefunctor✝, map_id := map_id✝ }