harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/GradedObject/Single.lean
lemma single_map_singleObjApplyIsoOfEq_hom (j : J) {X Y : C} (f : X ⟶ Y) (i : J) (h : i = j) :
    (single j).map f i ≫ (singleObjApplyIsoOfEq j Y i h).hom =
      (singleObjApplyIsoOfEq j X i h).hom ≫ f

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : HasInitial C
inst✝ : DecidableEq J
j : J
X Y : C
f : X ⟶ Y
i : J
h : i = j
⊢ (single j).map f i ≫ (singleObjApplyIsoOfEq j Y i h).hom = (singleObjApplyIsoOfEq j X i h).hom ≫ f

Tactic:
subst h

Result:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : HasInitial C
inst✝ : DecidableEq J
X Y : C
f : X ⟶ Y
i : J
⊢ (single i).map f i ≫ (singleObjApplyIsoOfEq i Y i ⋯).hom = (singleObjApplyIsoOfEq i X i ⋯).hom ≫ f

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : HasInitial C
inst✝ : DecidableEq J
X Y : C
f : X ⟶ Y
i : J
⊢ (single i).map f i ≫ (singleObjApplyIsoOfEq i Y i ⋯).hom = (singleObjApplyIsoOfEq i X i ⋯).hom ≫ f

Tactic:
simp [singleObjApplyIsoOfEq, single]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/WithTop.lean
@[simp] lemma bot_mul (hb : b ≠ 0) : ⊥ * b = ⊥

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
hb : b ≠ 0
⊢ ⊥ * b = ⊥

Tactic:
rw [bot_mul', if_neg hb]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
theorem isCaratheodory_sum {s : ℕ → Set α} (h : ∀ i, IsCaratheodory m (s i))
    (hd : Pairwise (Disjoint on s)) {t : Set α} :
    ∀ {n}, (∑ i ∈ Finset.range n, m (t ∩ s i)) = m (t ∩ ⋃ i < n, s i)
  | 0 => by simp [Nat.not_lt_zero, m.empty]
  | Nat.succ n => by
    rw [biUnion_lt_succ, Finset.sum_range_succ, Set.union_comm, isCaratheodory_sum h hd,
      m.measure_inter_union _ (h n), add_comm]
    intro a
    simpa using fun (h₁ : a ∈ s n) i (hi : i < n) h₂ => (hd (ne_of_gt hi)).le_bot ⟨h₁, h₂⟩

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
n : ℕ
a : α
⊢ a ∈ s n ∩ ⋃ k, ⋃ (_ : k < n), s k → a ∈ ∅

Tactic:
simpa using fun (h₁ : a ∈ s n) i (hi : i < n) h₂ => (hd (ne_of_gt hi)).le_bot ⟨h₁, h₂⟩

Result:
no goals

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ ∑ i ∈ Finset.range 0, m (t ∩ s i) = m (t ∩ ⋃ i, ⋃ (_ : i < 0), s i)

Tactic:
simp [Nat.not_lt_zero, m.empty]

Result:
no goals

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
n : ℕ
⊢ ∑ i ∈ Finset.range n.succ, m (t ∩ s i) = m (t ∩ ⋃ i, ⋃ (_ : i < n.succ), s i)

Tactic:
rw [biUnion_lt_succ, Finset.sum_range_succ, Set.union_comm, isCaratheodory_sum h hd,
  m.measure_inter_union _ (h n), add_comm]

Result:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
n : ℕ
⊢ s n ∩ ⋃ k, ⋃ (_ : k < n), s k ⊆ ∅

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
n : ℕ
⊢ s n ∩ ⋃ k, ⋃ (_ : k < n), s k ⊆ ∅

Tactic:
intro a

Result:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
n : ℕ
a : α
⊢ a ∈ s n ∩ ⋃ k, ⋃ (_ : k < n), s k → a ∈ ∅
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem sum_mult_eq [NumberField K] :
    ∑ w : InfinitePlace K, mult w = Module.finrank ℚ K

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ : InfinitePlace K
x✝ : x✝¹ ∈ Finset.univ
⊢ x✝¹.mult = ∑ i ∈ Finset.filter (fun i => mk i = x✝¹) Finset.univ, 1

Tactic:
rw [Finset.sum_const, smul_eq_mul, mul_one, card_filter_mk_eq]

Result:
no goals

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∑ w : InfinitePlace K, w.mult = Module.finrank ℚ K

Tactic:
rw [← Embeddings.card K ℂ, Fintype.card, Finset.card_eq_sum_ones, ← Finset.univ.sum_fiberwise
  (fun φ => InfinitePlace.mk φ)]

Result:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∑ w : InfinitePlace K, w.mult = ∑ j : InfinitePlace K, ∑ i ∈ Finset.filter (fun i => mk i = j) Finset.univ, 1

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∑ w : InfinitePlace K, w.mult = ∑ j : InfinitePlace K, ∑ i ∈ Finset.filter (fun i => mk i = j) Finset.univ, 1

Tactic:
exact Finset.sum_congr rfl
  (fun _ _ => by rw [Finset.sum_const, smul_eq_mul, mul_one, card_filter_mk_eq])

Result:
no goals

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∑ w : InfinitePlace K, w.mult = Module.finrank ℚ K

Tactic:
classical
rw [← Embeddings.card K ℂ, Fintype.card, Finset.card_eq_sum_ones, ← Finset.univ.sum_fiberwise
  (fun φ => InfinitePlace.mk φ)]
exact Finset.sum_congr rfl
  (fun _ _ => by rw [Finset.sum_const, smul_eq_mul, mul_one, card_filter_mk_eq])

Result:
no goals
-- Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean
lemma exp_llr_of_ac (μ ν : Measure α) [SigmaFinite μ] [Measure.HaveLebesgueDecomposition μ ν]
    (hμν : μ ≪ ν) :
    (fun x ↦ exp (llr μ ν x)) =ᵐ[μ] fun x ↦ (μ.rnDeriv ν x).toReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ (fun x => rexp (llr μ ν x)) =ᶠ[ae μ] fun x => (μ.rnDeriv ν x).toReal

Tactic:
filter_upwards [hμν.ae_le (exp_llr μ ν), Measure.rnDeriv_pos hμν] with x hx_eq hx_pos

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
x : α
hx_eq : rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
⊢ rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
x : α
hx_eq : rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
⊢ rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal

Tactic:
rw [hx_eq, if_neg hx_pos.ne']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem or_assoc (x y z : BitVec w) :
    x ||| y ||| z = x ||| (y ||| z)

Proof state:
case pred
w : Nat
x y z : BitVec w
i : Nat
a✝ : i < w
⊢ (x ||| y ||| z).getLsbD i = (x ||| (y ||| z)).getLsbD i

Tactic:
simp [Bool.or_assoc]

Result:
no goals

Proof state:
w : Nat
x y z : BitVec w
⊢ x ||| y ||| z = x ||| (y ||| z)

Tactic:
ext i

Result:
case pred
w : Nat
x y z : BitVec w
i : Nat
a✝ : i < w
⊢ (x ||| y ||| z).getLsbD i = (x ||| (y ||| z)).getLsbD i
-- Mathlib/LinearAlgebra/RootSystem/Reduced.lean
lemma coxeterWeightIn_eq_four_iff_not_linearIndependent :
    P.coxeterWeightIn S i j = 4 ↔ ¬ LinearIndependent R ![P.root i, P.root j]

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst✝⁶ : Finite ι
inst✝⁵ : CharZero R
inst✝⁴ : NoZeroSMulDivisors R M
inst✝³ : LinearOrderedCommRing S
inst✝² : Algebra S R
inst✝¹ : FaithfulSMul S R
inst✝ : P.IsValuedIn S
⊢ P.coxeterWeightIn S i j = 4 ↔ ¬LinearIndependent R ![P.root i, P.root j]

Tactic:
rw [P.linearIndependent_iff_coxeterWeightIn_ne_four S, not_not]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sup_himp_distrib (a b c : α) : a ⊔ b ⇨ c = (a ⇨ c) ⊓ (b ⇨ c) :=
  eq_of_forall_le_iff fun d => by
    rw [le_inf_iff, le_himp_comm, sup_le_iff]
    simp_rw [le_himp_comm]

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ≤ d ⇨ c ∧ b ≤ d ⇨ c ↔ d ≤ a ⇨ c ∧ d ≤ b ⇨ c

Tactic:
simp_rw [le_himp_comm]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ≤ a ⊔ b ⇨ c ↔ d ≤ (a ⇨ c) ⊓ (b ⇨ c)

Tactic:
rw [le_inf_iff, le_himp_comm, sup_le_iff]

Result:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ≤ d ⇨ c ∧ b ≤ d ⇨ c ↔ d ≤ a ⇨ c ∧ d ≤ b ⇨ c
-- Mathlib/Combinatorics/SimpleGraph/Girth.lean
lemma three_le_egirth : 3 ≤ G.egirth

Proof state:
case pos
α : Type u_1
G : SimpleGraph α
h : G.egirth = ⊤
⊢ 3 ≤ ⊤

Tactic:
apply le_top

Result:
no goals

Proof state:
case neg
α : Type u_1
G : SimpleGraph α
h : ∃ a w, w.IsCycle ∧ G.egirth = ↑w.length
⊢ 3 ≤ G.egirth

Tactic:
have ⟨_, _, _⟩ := h

Result:
case neg
α : Type u_1
G : SimpleGraph α
h : ∃ a w, w.IsCycle ∧ G.egirth = ↑w.length
w✝¹ : α
w✝ : G.Walk w✝¹ w✝¹
h✝ : w✝.IsCycle ∧ G.egirth = ↑w✝.length
⊢ 3 ≤ G.egirth

Proof state:
case neg
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
⊢ 3 ≤ G.egirth

Tactic:
rw [← exists_egirth_eq_length] at h

Result:
case neg
α : Type u_1
G : SimpleGraph α
h : ∃ a w, w.IsCycle ∧ G.egirth = ↑w.length
⊢ 3 ≤ G.egirth

Proof state:
α : Type u_1
G : SimpleGraph α
⊢ 3 ≤ G.egirth

Tactic:
by_cases h : G.IsAcyclic

Result:
case pos
α : Type u_1
G : SimpleGraph α
h : G.IsAcyclic
⊢ 3 ≤ G.egirth

case neg
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
⊢ 3 ≤ G.egirth

Proof state:
case neg
α : Type u_1
G : SimpleGraph α
h : ∃ a w, w.IsCycle ∧ G.egirth = ↑w.length
w✝¹ : α
w✝ : G.Walk w✝¹ w✝¹
h✝ : w✝.IsCycle ∧ G.egirth = ↑w✝.length
⊢ 3 ≤ G.egirth

Tactic:
simp_all only [Nat.cast_inj, Nat.ofNat_le_cast, Walk.IsCycle.three_le_length]

Result:
no goals

Proof state:
case pos
α : Type u_1
G : SimpleGraph α
h : G.IsAcyclic
⊢ 3 ≤ G.egirth

Tactic:
rw [← egirth_eq_top] at h

Result:
case pos
α : Type u_1
G : SimpleGraph α
h : G.egirth = ⊤
⊢ 3 ≤ G.egirth

Proof state:
case pos
α : Type u_1
G : SimpleGraph α
h : G.egirth = ⊤
⊢ 3 ≤ G.egirth

Tactic:
rw [h]

Result:
case pos
α : Type u_1
G : SimpleGraph α
h : G.egirth = ⊤
⊢ 3 ≤ ⊤
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma mulIndicator_biUnion_apply (s : Finset ι) (t : ι → Set κ) {f : κ → β}
    (h : (s : Set ι).PairwiseDisjoint t) (x : κ) :
    mulIndicator (⋃ i ∈ s, t i) f x = ∏ i ∈ s, mulIndicator (t i) f x

Proof state:
ι : Type u_1
β : Type u_4
inst✝ : CommMonoid β
κ : Type u_7
s : Finset ι
t : ι → Set κ
f : κ → β
h : (↑s).PairwiseDisjoint t
x : κ
⊢ (⋃ i ∈ s, t i).mulIndicator f x = ∏ i ∈ s, (t i).mulIndicator f x

Tactic:
rw [mulIndicator_biUnion s t h]

Result:
no goals
-- Mathlib/Topology/Order/NhdsSet.lean
theorem Ioi_mem_nhdsSet_Ioc (h : a ≤ b) : Ioi a ∈ 𝓝ˢ (Ioc b c) :=
  nhdsSet_mono Ioc_subset_Ioi_self <| by simpa

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c : α
h : a ≤ b
⊢ Ioi a ∈ 𝓝ˢ (Ioi b)

Tactic:
simpa

Result:
no goals
-- Mathlib/Order/Atoms/Finite.lean
theorem univ : (Finset.univ : Finset α) = {⊤, ⊥}

Proof state:
α : Type u_1
inst✝³ : LE α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ {IsSimpleOrder.equivBool.symm true, IsSimpleOrder.equivBool.symm false} = {⊤, ⊥}

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : LE α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ Finset.univ = {⊤, ⊥}

Tactic:
change Finset.map _ (Finset.univ : Finset Bool) = _

Result:
α : Type u_1
inst✝³ : LE α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ Finset.map { toFun := ⇑IsSimpleOrder.equivBool.symm, inj' := ⋯ } Finset.univ = {⊤, ⊥}

Proof state:
α : Type u_1
inst✝³ : LE α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ Finset.map { toFun := ⇑IsSimpleOrder.equivBool.symm, inj' := ⋯ } Finset.univ = {⊤, ⊥}

Tactic:
rw [Fintype.univ_bool]

Result:
α : Type u_1
inst✝³ : LE α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ Finset.map { toFun := ⇑IsSimpleOrder.equivBool.symm, inj' := ⋯ } {true, false} = {⊤, ⊥}

Proof state:
α : Type u_1
inst✝³ : LE α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ Finset.map { toFun := ⇑IsSimpleOrder.equivBool.symm, inj' := ⋯ } {true, false} = {⊤, ⊥}

Tactic:
simp only [Finset.map_insert, Function.Embedding.coeFn_mk, Finset.map_singleton]

Result:
α : Type u_1
inst✝³ : LE α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
⊢ {IsSimpleOrder.equivBool.symm true, IsSimpleOrder.equivBool.symm false} = {⊤, ⊥}
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_diff' (h : s ⊆ t) (f : α → G) :
    mulIndicator (t \ s) f = mulIndicator t f / mulIndicator s f

Proof state:
α : Type u_1
G : Type u_5
inst✝ : Group G
s t : Set α
h : s ⊆ t
f : α → G
⊢ (t \ s).mulIndicator f = t.mulIndicator f / s.mulIndicator f

Tactic:
rw [mulIndicator_diff h, div_eq_mul_inv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_not {x : BitVec v} : (~~~x).getLsbD i = (decide (i < v) && ! x.getLsbD i)

Proof state:
v i : Nat
x : BitVec v
⊢ (~~~x).getLsbD i = (decide (i < v) && !x.getLsbD i)

Tactic:
by_cases h' : i < v <;> simp_all [not_def]

Result:
no goals
-- Mathlib/Topology/NhdsSet.lean
theorem IsClosed.nhdsSet_le_sup' (h : IsClosed t) :
    𝓝ˢ s ≤ 𝓝ˢ (t ∩ s) ⊔ 𝓟 (tᶜ)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed t
⊢ 𝓝ˢ s ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ

Tactic:
exact h.nhdsSet_le_sup s

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed t
⊢ 𝓝ˢ s ≤ 𝓝ˢ (t ∩ s) ⊔ 𝓟 tᶜ

Tactic:
rw [Set.inter_comm]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed t
⊢ 𝓝ˢ s ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ
-- Mathlib/Order/SupIndep.lean
theorem sSupIndep_iff {α : Type*} [CompleteLattice α] (s : Set α) :
    sSupIndep s ↔ iSupIndep ((↑) : s → α)

Proof state:
α : Type u_5
inst✝ : CompleteLattice α
s : Set α
⊢ sSupIndep s ↔ iSupIndep Subtype.val

Tactic:
simp_rw [iSupIndep, sSupIndep, SetCoe.forall, sSup_eq_iSup]

Result:
α : Type u_5
inst✝ : CompleteLattice α
s : Set α
⊢ (∀ ⦃a : α⦄, a ∈ s → Disjoint a (⨆ a_2 ∈ s \ {a}, a_2)) ↔
    ∀ (x : α) (h : x ∈ s), Disjoint x (⨆ j, ⨆ (_ : j ≠ ⟨x, h⟩), ↑j)

Proof state:
α : Type u_5
inst✝ : CompleteLattice α
s : Set α
⊢ (∀ ⦃a : α⦄, a ∈ s → Disjoint a (⨆ a_2 ∈ s \ {a}, a_2)) ↔
    ∀ (x : α) (h : x ∈ s), Disjoint x (⨆ j, ⨆ (_ : j ≠ ⟨x, h⟩), ↑j)

Tactic:
refine forall₂_congr fun a ha => ?_

Result:
α : Type u_5
inst✝ : CompleteLattice α
s : Set α
a : α
ha : a ∈ s
⊢ Disjoint a (⨆ a_1 ∈ s \ {a}, a_1) ↔ Disjoint a (⨆ j, ⨆ (_ : j ≠ ⟨a, ha⟩), ↑j)

Proof state:
α : Type u_5
inst✝ : CompleteLattice α
s : Set α
a : α
ha : a ∈ s
⊢ Disjoint a (⨆ a_1 ∈ s \ {a}, a_1) ↔ Disjoint a (⨆ j, ⨆ (_ : j ≠ ⟨a, ha⟩), ↑j)

Tactic:
simp [iSup_subtype, iSup_and]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldl_flatten (f : β → α → β) (b : β) (L : Vector (Vector α m) n) :
    (flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b

Proof state:
case of
β : Type u_1
α : Type u_2
m n : Nat
f : β → α → β
b : β
xss✝ : Array (Array α)
h₁✝ : xss✝.size = n
h₂✝ : ∀ (xs : Array α), xs ∈ xss✝ → xs.size = m
⊢ foldl f b
      {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
              xss✝.attach,
          size_toArray := ⋯ }.flatten =
    foldl (fun b l => foldl f b l) b
      {
        toArray :=
          Array.map
            (fun x =>
              match x with
              | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
            xss✝.attach,
        size_toArray := ⋯ }

Tactic:
simp [Array.foldl_flatten', Array.foldl_map']

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
m n : Nat
f : β → α → β
b : β
L : Vector (Vector α m) n
⊢ foldl f b L.flatten = foldl (fun b l => foldl f b l) b L

Tactic:
cases L using vector₂_induction

Result:
case of
β : Type u_1
α : Type u_2
m n : Nat
f : β → α → β
b : β
xss✝ : Array (Array α)
h₁✝ : xss✝.size = n
h₂✝ : ∀ (xs : Array α), xs ∈ xss✝ → xs.size = m
⊢ foldl f b
      {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
              xss✝.attach,
          size_toArray := ⋯ }.flatten =
    foldl (fun b l => foldl f b l) b
      {
        toArray :=
          Array.map
            (fun x =>
              match x with
              | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
            xss✝.attach,
        size_toArray := ⋯ }
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem basisDivisor_add_symm {x y : F} (hxy : x ≠ y) :
    basisDivisor x y + basisDivisor y x = 1

Proof state:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ basisDivisor x y + basisDivisor y x = 1

Tactic:
rw [← sum_basis Function.injective_id.injOn ⟨x, mem_insert_self _ {y}⟩,
  sum_insert (not_mem_singleton.mpr hxy), sum_singleton, basis_pair_left hxy,
  basis_pair_right hxy, id, id]

Result:
no goals

Proof state:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ basisDivisor x y + basisDivisor y x = 1

Tactic:
classical
rw [← sum_basis Function.injective_id.injOn ⟨x, mem_insert_self _ {y}⟩,
  sum_insert (not_mem_singleton.mpr hxy), sum_singleton, basis_pair_left hxy,
  basis_pair_right hxy, id, id]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem toSignedMeasure_eq_toSignedMeasure_iff {μ ν : Measure α} [IsFiniteMeasure μ]
    [IsFiniteMeasure ν] : μ.toSignedMeasure = ν.toSignedMeasure ↔ μ = ν

Proof state:
case refine_1.h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
⊢ μ i = ν i

Tactic:
have : μ.toSignedMeasure i = ν.toSignedMeasure i := by rw [h]

Result:
case refine_1.h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
this : ↑μ.toSignedMeasure i = ↑ν.toSignedMeasure i
⊢ μ i = ν i

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
⊢ μ = ν

Tactic:
ext1 i hi

Result:
case refine_1.h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
⊢ μ i = ν i

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
⊢ ↑μ.toSignedMeasure i = ↑ν.toSignedMeasure i

Tactic:
rw [h]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ = ν
⊢ μ.toSignedMeasure = ν.toSignedMeasure

Tactic:
congr

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ μ.toSignedMeasure = ν.toSignedMeasure ↔ μ = ν

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
⊢ μ = ν

case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ = ν
⊢ μ.toSignedMeasure = ν.toSignedMeasure

Proof state:
case refine_1.h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
this : ↑μ.toSignedMeasure i = ↑ν.toSignedMeasure i
⊢ μ i = ν i

Tactic:
rwa [toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi,
    ENNReal.toReal_eq_toReal] at this
  <;> exact measure_ne_top _ _

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem xy_coprime (n) : (xn a1 n).Coprime (yn a1 n) :=
  Nat.coprime_of_dvd' fun k _ kx ky => by
    let p := pell_eq a1 n
    rw [← p]
    exact Nat.dvd_sub (le_of_lt <| Nat.lt_of_sub_eq_succ p) (kx.mul_left _) (ky.mul_left _)

Proof state:
a : ℕ
a1 : 1 < a
n k : ℕ
x✝ : Nat.Prime k
kx : k ∣ xn a1 n
ky : k ∣ yn a1 n
p : xn a1 n * xn a1 n - Pell.d a1 * yn a1 n * yn a1 n = 1 := pell_eq a1 n
⊢ k ∣ xn a1 n * xn a1 n - Pell.d a1 * yn a1 n * yn a1 n

Tactic:
exact Nat.dvd_sub (le_of_lt <| Nat.lt_of_sub_eq_succ p) (kx.mul_left _) (ky.mul_left _)

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n k : ℕ
x✝ : Nat.Prime k
kx : k ∣ xn a1 n
ky : k ∣ yn a1 n
⊢ k ∣ 1

Tactic:
let p := pell_eq a1 n

Result:
a : ℕ
a1 : 1 < a
n k : ℕ
x✝ : Nat.Prime k
kx : k ∣ xn a1 n
ky : k ∣ yn a1 n
p : xn a1 n * xn a1 n - Pell.d a1 * yn a1 n * yn a1 n = 1 := pell_eq a1 n
⊢ k ∣ 1

Proof state:
a : ℕ
a1 : 1 < a
n k : ℕ
x✝ : Nat.Prime k
kx : k ∣ xn a1 n
ky : k ∣ yn a1 n
p : xn a1 n * xn a1 n - Pell.d a1 * yn a1 n * yn a1 n = 1 := pell_eq a1 n
⊢ k ∣ 1

Tactic:
rw [← p]

Result:
a : ℕ
a1 : 1 < a
n k : ℕ
x✝ : Nat.Prime k
kx : k ∣ xn a1 n
ky : k ∣ yn a1 n
p : xn a1 n * xn a1 n - Pell.d a1 * yn a1 n * yn a1 n = 1 := pell_eq a1 n
⊢ k ∣ xn a1 n * xn a1 n - Pell.d a1 * yn a1 n * yn a1 n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_eq_right {m n : Nat} (H : n ∣ m) : gcd m n = n

Proof state:
m n : Nat
H : n ∣ m
⊢ m.gcd n = n

Tactic:
rw [gcd_comm, gcd_eq_left H]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem injective_iff_injective_of_iUnion_eq_univ :
    Injective f ↔ ∀ i, Injective ((U i).restrictPreimage f)

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
⊢ f x ∈ iUnion U

Tactic:
rw [hU]

Result:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
⊢ f x ∈ univ

Proof state:
case intro
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
i : ι
hi : f x ∈ U i
⊢ x = y

Tactic:
injection @H i ⟨x, hi⟩ ⟨y, show f y ∈ U i from e ▸ hi⟩ (Subtype.ext e)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
⊢ x = y

Tactic:
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp
    (show f x ∈ Set.iUnion U by rw [hU]; trivial)

Result:
case intro
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
i : ι
hi : f x ∈ U i
⊢ x = y

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Injective f ↔ ∀ (i : ι), Injective ((U i).restrictPreimage f)

Tactic:
refine ⟨fun H i => (U i).restrictPreimage_injective H, fun H x y e => ?_⟩

Result:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
⊢ x = y

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
⊢ f x ∈ univ

Tactic:
trivial

Result:
no goals