harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Indexes.lean
theorem get_mapIdx (l : List α) (f : ℕ → α → β) (i : ℕ) (h : i < l.length)
    (h' : i < (l.mapIdx f).length := h.trans_le length_mapIdx.ge) :
    (l.mapIdx f).get ⟨i, h'⟩ = f i (l.get ⟨i, h⟩)

Proof state:
α : Type u
β : Type v
l : List α
f : ℕ → α → β
i : ℕ
h : i < l.length
h' : optParam (i < (mapIdx f l).length) ⋯
⊢ (mapIdx f l).get ⟨i, h'⟩ = f i (l.get ⟨i, h⟩)

Tactic:
simp [mapIdx_eq_zipIdx_map, enum_eq_zip_range]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_X_pow_mul (p : R[X]) (n d : ℕ) :
    coeff (Polynomial.X ^ n * p) (d + n) = coeff p d

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (X ^ n * p).coeff (d + n) = p.coeff d

Tactic:
rw [(commute_X_pow p n).eq, coeff_mul_X_pow]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma IsCycle.isPath_of_append_left {p : G.Walk u v} {q : G.Walk v u} (h : ¬ q.Nil)
    (hcyc : (p.append q).IsCycle) : p.IsPath :=
  p.isPath_reverse_iff.mp ((reverse_append _ _ ▸ hcyc.reverse).isPath_of_append_right (by simpa))

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬q.Nil
hcyc : (p.append q).IsCycle
⊢ ¬q.reverse.Nil

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_mul_eq_div_mul_one_div : a / (b * c) = a / b * (1 / c)

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b c : α
⊢ a / (b * c) = a / b * (1 / c)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem anyM_eq_anyM_loop [Monad m] (p : α → m Bool) (as : Array α) (start stop) :
    anyM p as start stop = anyM.loop p as (min stop as.size) (Nat.min_le_right ..) start

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as : Array α
start stop : Nat
⊢ (if h : stop ≤ as.size then anyM.loop p as stop ⋯ start else anyM.loop p as as.size ⋯ start) =
    anyM.loop p as (if stop ≤ as.size then stop else as.size) ⋯ start

Tactic:
split <;> rfl

Result:
no goals

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as : Array α
start stop : Nat
⊢ anyM p as start stop = anyM.loop p as (min stop as.size) ⋯ start

Tactic:
simp only [anyM, Nat.min_def]

Result:
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as : Array α
start stop : Nat
⊢ (if h : stop ≤ as.size then anyM.loop p as stop ⋯ start else anyM.loop p as as.size ⋯ start) =
    anyM.loop p as (if stop ≤ as.size then stop else as.size) ⋯ start
-- Mathlib/LinearAlgebra/Quotient/Defs.lean
theorem quotientRel_def {x y : M} : p.quotientRel x y ↔ x - y ∈ p :=
  Iff.trans
    (by
      rw [leftRel_apply, sub_eq_add_neg, neg_add, neg_neg]
      rfl)
    neg_mem_iff

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x y : M
⊢ -x + y ∈ p.toAddSubgroup ↔ -x + y ∈ p

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x y : M
⊢ p.quotientRel x y ↔ -(x - y) ∈ p

Tactic:
rw [leftRel_apply, sub_eq_add_neg, neg_add, neg_neg]

Result:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x y : M
⊢ -x + y ∈ p.toAddSubgroup ↔ -x + y ∈ p
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem mod_left (a : ℤ) (b : ℕ) : J(a | b) = J(a % b | b) :=
  congr_arg List.prod <|
    List.pmap_congr_left _
      (by
        -- Porting note: Lean does not synthesize the instance [Fact (Nat.Prime p)] automatically
        -- (it is needed for `legendreSym.mod` on line 227). Thus, we name the hypothesis
        -- `Nat.Prime p` explicitly on line 224 and prove `Fact (Nat.Prime p)` on line 225.
        rintro p hp _ h₂
        letI : Fact p.Prime := ⟨h₂⟩
        conv_rhs =>
          rw [legendreSym.mod, Int.emod_emod_of_dvd _ (Int.natCast_dvd_natCast.2 <|
            dvd_of_mem_primeFactorsList hp), ← legendreSym.mod])

Proof state:
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
h₁✝ h₂ : Nat.Prime p
⊢ legendreSym p a = legendreSym p (a % ↑b)

Tactic:
letI : Fact p.Prime := ⟨h₂⟩

Result:
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
h₁✝ h₂ : Nat.Prime p
this : Fact (Nat.Prime p) := { out := h₂ }
⊢ legendreSym p a = legendreSym p (a % ↑b)

Proof state:
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
h₁✝ h₂ : Nat.Prime p
this : Fact (Nat.Prime p) := { out := h₂ }
⊢ legendreSym p a = legendreSym p (a % ↑b)

Tactic:
conv_rhs =>
  rw [legendreSym.mod, Int.emod_emod_of_dvd _ (Int.natCast_dvd_natCast.2 <|
    dvd_of_mem_primeFactorsList hp), ← legendreSym.mod]

Result:
no goals

Proof state:
a : ℤ
b : ℕ
⊢ ∀ a_1 ∈ b.primeFactorsList, ∀ (h₁ h₂ : Nat.Prime a_1), legendreSym a_1 a = legendreSym a_1 (a % ↑b)

Tactic:
rintro p hp _ h₂

Result:
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
h₁✝ h₂ : Nat.Prime p
⊢ legendreSym p a = legendreSym p (a % ↑b)
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Iso.lean
theorem pullbackConeOfRightIso_π_app_none : (pullbackConeOfRightIso f g).π.app none = f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ (pullbackConeOfRightIso f g).π.app none = f

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn' (hf : HasFPowerSeriesOnBall f p x r) :
    TendstoLocallyUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop
      (EMetric.ball (x : E) r)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ TendstoLocallyUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop (EMetric.ball x r)

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
⊢ TendstoLocallyUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop (EMetric.ball x r)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
⊢ TendstoLocallyUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop (EMetric.ball x r)

Tactic:
simpa using hf.tendstoLocallyUniformlyOn'

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
lemma nextCoeff_ne_zero : p.nextCoeff ≠ 0 ↔ p.natDegree ≠ 0 ∧ p.coeff (p.natDegree - 1) ≠ 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.nextCoeff ≠ 0 ↔ p.natDegree ≠ 0 ∧ p.coeff (p.natDegree - 1) ≠ 0

Tactic:
simp [nextCoeff]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
theorem braiding_inv_snd {X Y : C} : (β_ X Y).inv ≫ snd _ _ = fst _ _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y : C
⊢ (β_ X Y).inv ≫ snd X Y = fst Y X

Tactic:
simp [braiding_eq_braiding, fst, snd]

Result:
no goals
-- Mathlib/Order/RelIso/Basic.lean
theorem Function.Surjective.wellFounded_iff {f : α → β} (hf : Surjective f)
    (o : ∀ {a b}, r a b ↔ s (f a) (f b)) :
    WellFounded r ↔ WellFounded s :=
  Iff.intro
    (RelHomClass.wellFounded (⟨surjInv hf,
      fun h => by simpa only [o, surjInv_eq hf] using h⟩ : s →r r))
    (RelHomClass.wellFounded (⟨f, o.1⟩ : r →r s))

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a✝ b✝ : β
h : s a✝ b✝
⊢ r (surjInv hf a✝) (surjInv hf b✝)

Tactic:
simpa only [o, surjInv_eq hf] using h

Result:
no goals
-- Mathlib/Logic/Basic.lean
lemma heq_of_eq_cast (e : β = α) : a = cast e b → HEq a b

Proof state:
α β : Sort u
b : β
e : β = α
⊢ HEq (cast e b) b

Tactic:
simp

Result:
no goals

Proof state:
α β : Sort u
a : α
b : β
e : β = α
⊢ a = cast e b → HEq a b

Tactic:
rintro rfl

Result:
α β : Sort u
b : β
e : β = α
⊢ HEq (cast e b) b
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem T_eq (n : ℤ) : T R n = 2 * X * T R (n - 1) - T R (n - 2)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ T R n = 2 * X * T R (n - 1) - T R (n - 2)

Tactic:
linear_combination (norm := ring_nf) T_add_two R (n - 2)

Result:
no goals
-- Mathlib/Dynamics/Ergodic/Ergodic.lean
theorem measure_self_or_compl_eq_zero (hf : PreErgodic f μ) (hs : MeasurableSet s)
    (hs' : f ⁻¹' s = s) : μ s = 0 ∨ μ sᶜ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : PreErgodic f μ
hs : MeasurableSet s
hs' : f ⁻¹' s = s
⊢ μ s = 0 ∨ μ sᶜ = 0

Tactic:
simpa using hf.ae_empty_or_univ hs hs'

Result:
no goals
-- Mathlib/Order/Sublattice.lean
lemma le_pi {s : Set κ} {L : ∀ i, Sublattice (π i)} {M : Sublattice (∀ i, π i)} :
    M ≤ pi s L ↔ ∀ i ∈ s, M ≤ comap (Pi.evalLatticeHom i) (L i)

Proof state:
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
L : (i : κ) → Sublattice (π i)
M : Sublattice ((i : κ) → π i)
⊢ M ≤ pi s L ↔ ∀ i ∈ s, M ≤ comap (Pi.evalLatticeHom i) (L i)

Tactic:
simp [SetLike.le_def]

Result:
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
L : (i : κ) → Sublattice (π i)
M : Sublattice ((i : κ) → π i)
⊢ (∀ ⦃x : (i : κ) → π i⦄, x ∈ M → ∀ i ∈ s, x i ∈ L i) ↔ ∀ i ∈ s, ∀ ⦃x : (i : κ) → π i⦄, x ∈ M → x i ∈ L i

Proof state:
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
L : (i : κ) → Sublattice (π i)
M : Sublattice ((i : κ) → π i)
⊢ (∀ ⦃x : (i : κ) → π i⦄, x ∈ M → ∀ i ∈ s, x i ∈ L i) ↔ ∀ i ∈ s, ∀ ⦃x : (i : κ) → π i⦄, x ∈ M → x i ∈ L i

Tactic:
aesop

Result:
no goals
-- Mathlib/Topology/Gluing.lean
theorem preimage_range (i j : D.J) : 𝖣.ι j ⁻¹' Set.range (𝖣.ι i) = Set.range (D.f j i)

Proof state:
D : GlueData
i j : D.J
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (D.ι i)) =
    Set.range ⇑(ConcreteCategory.hom (D.f j i))

Tactic:
rw [← Set.preimage_image_eq (Set.range (D.f j i)) (D.ι_injective j), ← Set.image_univ, ←
  Set.image_univ, ← Set.image_comp, ← coe_comp, Set.image_univ, Set.image_univ, ← image_inter,
  Set.preimage_range_inter]

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem not_lt_iff_not_le_or_ge : ¬a < b ↔ ¬a ≤ b ∨ b ≤ a

Proof state:
α : Type u_2
inst✝ : Preorder α
a b : α
⊢ ¬a < b ↔ ¬a ≤ b ∨ b ≤ a

Tactic:
rw [lt_iff_le_not_le, Classical.not_and_iff_or_not_not, Classical.not_not]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Inductions.lean
theorem divX_eq_zero_iff : divX p = 0 ↔ p = C (p.coeff 0) :=
  ⟨fun h => by simpa [eq_comm, h] using divX_mul_X_add p, fun h => by rw [h, divX_C]⟩

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.divX = 0
⊢ p = C (p.coeff 0)

Tactic:
simpa [eq_comm, h] using divX_mul_X_add p

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p = C (p.coeff 0)
⊢ p.divX = 0

Tactic:
rw [h, divX_C]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem le_antisymm : ∀ {x y : Bool}, x ≤ y → y ≤ x → x = y

Proof state:
⊢ ∀ {x y : Bool}, x ≤ y → y ≤ x → x = y

Tactic:
decide

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Exhaustion.lean
lemma measure_sigmaFiniteSetGE_le (μ ν : Measure α) [IsFiniteMeasure ν] (n : ℕ) :
    ν (μ.sigmaFiniteSetGE ν n)
      ≤ ⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
n : ℕ
⊢ ν (μ.sigmaFiniteSetGE ν n) ≤ ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s

Tactic:
refine (le_iSup (f := fun s ↦ _)
  (sigmaFinite_restrict_sigmaFiniteSetGE μ ν n)).trans ?_

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
n : ℕ
⊢ ⨆ (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))), ν (μ.sigmaFiniteSetGE ν n) ≤
    ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
n : ℕ
⊢ ⨆ (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))), ν (μ.sigmaFiniteSetGE ν n) ≤
    ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s

Tactic:
exact le_iSup₂ (f := fun s _ ↦ ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) (μ.sigmaFiniteSetGE ν n)
  (measurableSet_sigmaFiniteSetGE n)

Result:
no goals
-- Mathlib/Data/Finset/Dedup.lean
theorem toFinset_dedup (m : Multiset α) : m.dedup.toFinset = m.toFinset

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ m.dedup.toFinset = m.toFinset

Tactic:
simp_rw [toFinset, dedup_idem]

Result:
no goals
-- Mathlib/GroupTheory/FixedPointFree.lean
theorem commute_all_of_involutive (hφ : FixedPointFree φ) (h2 : Function.Involutive φ) (g h : G) :
    Commute g h

Proof state:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
g h : G
⊢ Commute g h

Tactic:
have key := map_mul φ g h

Result:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
g h : G
key : φ (g * h) = φ g * φ h
⊢ Commute g h

Proof state:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
g h : G
key : φ (g * h) = φ g * φ h
⊢ Commute g h

Tactic:
rwa [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_eq_inv, mul_inv_rev, inv_inv, inv_inv] at key

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem fract_add_ZSpan (m : E) {v : E} (h : v ∈ span ℤ (Set.range b)) :
    fract b (m + v) = fract b m

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ⇑b)
⊢ fract b (m + v) = fract b m

Tactic:
rw [add_comm, fract_zSpan_add b m h]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem tendsto_comp_val_Ioi_atTop [Preorder α] [IsDirected α (· ≤ ·)] [NoMaxOrder α]
    {a : α} {f : α → β} {l : Filter β} :
    Tendsto (fun x : Ioi a => f x) atTop l ↔ Tendsto f atTop l

Proof state:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : NoMaxOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x => f ↑x) atTop l ↔ Tendsto f atTop l

Tactic:
rw [← map_val_Ioi_atTop a, tendsto_map'_iff, Function.comp_def]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem coe_iInf₂ (f : ∀ i, κ i → UpperSet α) :
    (↑(⨅ (i) (j), f i j) : Set α) = ⋃ (i) (j), f i j

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
f : (i : ι) → κ i → UpperSet α
⊢ ↑(⨅ i, ⨅ j, f i j) = ⋃ i, ⋃ j, ↑(f i j)

Tactic:
simp_rw [coe_iInf]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem ne_ones_iff {c : Composition n} : c ≠ ones n ↔ ∃ i ∈ c.blocks, 1 < i

Proof state:
n : ℕ
c : Composition n
⊢ (¬∀ i ∈ c.blocks, i = 1) ↔ ∃ i ∈ c.blocks, 1 < i

Tactic:
have : ∀ j ∈ c.blocks, j = 1 ↔ j ≤ 1 := fun j hj => by simp [le_antisymm_iff, c.one_le_blocks hj]

Result:
n : ℕ
c : Composition n
this : ∀ j ∈ c.blocks, j = 1 ↔ j ≤ 1
⊢ (¬∀ i ∈ c.blocks, i = 1) ↔ ∃ i ∈ c.blocks, 1 < i

Proof state:
n : ℕ
c : Composition n
this : ∀ j ∈ c.blocks, j = 1 ↔ j ≤ 1
⊢ (¬∀ i ∈ c.blocks, i = 1) ↔ ∃ i ∈ c.blocks, 1 < i

Tactic:
simp +contextual [this]

Result:
no goals

Proof state:
n : ℕ
c : Composition n
⊢ c ≠ ones n ↔ ∃ i ∈ c.blocks, 1 < i

Tactic:
refine (not_congr eq_ones_iff).trans ?_

Result:
n : ℕ
c : Composition n
⊢ (¬∀ i ∈ c.blocks, i = 1) ↔ ∃ i ∈ c.blocks, 1 < i

Proof state:
n : ℕ
c : Composition n
j : ℕ
hj : j ∈ c.blocks
⊢ j = 1 ↔ j ≤ 1

Tactic:
simp [le_antisymm_iff, c.one_le_blocks hj]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem AECover.integrable_of_lintegral_enorm_bounded [l.NeBot] [l.IsCountablyGenerated]
    {φ : ι → Set α} (hφ : AECover μ l φ) {f : α → E} (I : ℝ) (hfm : AEStronglyMeasurable f μ)
    (hbounded : ∀ᶠ i in l, ∫⁻ x in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I) : Integrable f μ

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : l.NeBot
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I
⊢ Tendsto (fun c => ∫⁻ (x : α) in φ c, ‖f x‖ₑ ∂μ) l (𝓝 (∫⁻ (a : α), ‖f a‖ₑ ∂μ))

Tactic:
exact hφ.lintegral_tendsto_of_countably_generated hfm.enorm

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : l.NeBot
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I
⊢ Integrable f μ

Tactic:
refine ⟨hfm, (le_of_tendsto ?_ hbounded).trans_lt ENNReal.ofReal_lt_top⟩

Result:
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : l.NeBot
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I
⊢ Tendsto (fun c => ∫⁻ (x : α) in φ c, ‖f x‖ₑ ∂μ) l (𝓝 (∫⁻ (a : α), ‖f a‖ₑ ∂μ))
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.mem_closure_iff_of_not_mem (hI : M.Indep I) (heI : e ∉ I) :
    e ∈ M.closure I ↔ M.Dep (insert e I)

Proof state:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
⊢ e ∈ M.closure I ↔ M.Dep (insert e I)

Tactic:
rw [hI.insert_dep_iff, mem_diff, and_iff_left heI]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
/-- The lower part of the second column of the snake diagram is exact. -/
lemma exact_C₂_down : (ShortComplex.mk S.v₁₂.τ₂ S.v₂₃.τ₂
    (by rw [← comp_τ₂, S.w₁₃, zero_τ₂])).Exact :=
  exact_of_g_is_cokernel _ S.h₃τ₂

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.46635, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₁₂.τ₂ ≫ S.v₂₃.τ₂ = 0

Tactic:
rw [← comp_τ₂, S.w₁₃, zero_τ₂]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
lemma continuousOn_one_add_mul_inv {z : ℂ} (hz : 1 + z ∈ slitPlane) :
    ContinuousOn (fun t : ℝ ↦ (1 + t • z)⁻¹) (Set.Icc 0 1) :=
  ContinuousOn.inv₀ (by fun_prop)
    (fun _ ht ↦ slitPlane_ne_zero <| StarConvex.add_smul_mem starConvex_one_slitPlane hz ht.1 ht.2)

Proof state:
z : ℂ
hz : 1 + z ∈ slitPlane
⊢ ContinuousOn (fun t => 1 + t • z) (Set.Icc 0 1)

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
/-- Geometric progressions of length three are unchanged under `2`-Freiman isomorphisms. -/
@[to_additive
"Arithmetic progressions of length three are unchanged under `2`-Freiman isomorphisms."]
lemma IsMulFreimanIso.threeGPFree_congr (hf : IsMulFreimanIso 2 s t f) :
    ThreeGPFree s ↔ ThreeGPFree t

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
⊢ ThreeGPFree s ↔ ThreeGPFree t

Tactic:
rw [← threeGPFree_image hf subset_rfl, hf.bijOn.image_eq]

Result:
no goals
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Icc_succ_left_eq_Ioc_of_not_isMax (ha : ¬ IsMax a) (b : α) : Icc (succ a) b = Ioc a b :=
  coe_injective <| by simpa using Set.Icc_succ_left_eq_Ioc_of_not_isMax ha _

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
b : α
⊢ ↑(Icc (succ a) b) = ↑(Ioc a b)

Tactic:
simpa using Set.Icc_succ_left_eq_Ioc_of_not_isMax ha _

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem Filter.HasBasis.equicontinuousWithinAt_iff {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop}
    {s₁ : κ₁ → Set X} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → X → α} {S : Set X} {x₀ : X}
    (hX : (𝓝[S] x₀).HasBasis p₁ s₁) (hα : (𝓤 α).HasBasis p₂ s₂) :
    EquicontinuousWithinAt F S x₀ ↔
      ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ i, (F i x₀, F i x) ∈ s₂ k₂

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia, p₁ ia ∧ ∀ x ∈ s₁ ia, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α (s₂ ib)}) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂

Tactic:
rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt,
  hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)]

Result:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia, p₁ ia ∧ ∀ x ∈ s₁ ia, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α (s₂ ib)}) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem decide_forall_mem {xs : Array α} {p : α → Prop} [DecidablePred p] :
    decide (∀ x, x ∈ xs → p x) = xs.all p

Proof state:
α : Type u_1
xs : Array α
p : α → Prop
inst✝ : DecidablePred p
⊢ decide (∀ (x : α), x ∈ xs → p x) = xs.all fun b => decide (p b)

Tactic:
simp [all_eq']

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioo_filter_lt (a b c : α) : {x ∈ Ioo a b | x < c} = Ioo a (min b c)

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c a✝ : α
⊢ a✝ ∈ filter (fun x => x < c) (Ioo a b) ↔ a✝ ∈ Ioo a (b ⊓ c)

Tactic:
simp [and_assoc]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ filter (fun x => x < c) (Ioo a b) = Ioo a (b ⊓ c)

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c a✝ : α
⊢ a✝ ∈ filter (fun x => x < c) (Ioo a b) ↔ a✝ ∈ Ioo a (b ⊓ c)
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_permute' (σ : Perm n) (M : Matrix n n R) :
    (M.submatrix id σ).det = Perm.sign σ * M.det

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
σ : Perm n
M : Matrix n n R
⊢ (M.submatrix id ⇑σ).det = ↑↑(sign σ) * M.det

Tactic:
rw [← det_transpose, transpose_submatrix, det_permute, det_transpose]

Result:
no goals
-- Mathlib/Topology/PartitionOfUnity.lean
theorem mem_finsupport (x₀ : X) {i} :
    i ∈ ρ.finsupport x₀ ↔ i ∈ support fun i ↦ ρ i x₀

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
i : ι
⊢ i ∈ ρ.finsupport x₀ ↔ i ∈ support fun i => (ρ i) x₀

Tactic:
simp only [finsupport, mem_support, Finite.mem_toFinset, mem_setOf_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_shiftLeft {x : BitVec w} {n : Nat} :
    (x <<< n).msb = x.getMsbD n

Proof state:
w : Nat
x : BitVec w
n : Nat
⊢ (x <<< n).msb = x.getMsbD n

Tactic:
simp [BitVec.msb]

Result:
no goals