harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Lattice.lean
theorem image2_iUnion₂_left (s : ∀ i, κ i → Set α) (t : Set β) :
    image2 f (⋃ (i) (j), s i j) t = ⋃ (i) (j), image2 f (s i j) t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
⊢ image2 f (⋃ i, ⋃ j, s i j) t = ⋃ i, ⋃ j, image2 f (s i j) t

Tactic:
simp_rw [image2_iUnion_left]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Sort.lean
theorem comp_perm_comp_sort_eq_comp_sort : (f ∘ σ) ∘ sort (f ∘ σ) = f ∘ sort f

Proof state:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ (f ∘ ⇑σ) ∘ ⇑(sort (f ∘ ⇑σ)) = f ∘ ⇑(sort f)

Tactic:
rw [Function.comp_assoc, ← Equiv.Perm.coe_mul]

Result:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ f ∘ ⇑(σ * sort (f ∘ ⇑σ)) = f ∘ ⇑(sort f)

Proof state:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ f ∘ ⇑(σ * sort (f ∘ ⇑σ)) = f ∘ ⇑(sort f)

Tactic:
exact unique_monotone (monotone_sort (f ∘ σ)) (monotone_sort f)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma b₆_of_char_three : W.b₆ = W.a₃ ^ 2 + W.a₆

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.b₆ = W.a₃ ^ 2 + W.a₆

Tactic:
rw [b₆]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.a₃ ^ 2 + 4 * W.a₆ = W.a₃ ^ 2 + W.a₆

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.a₃ ^ 2 + 4 * W.a₆ = W.a₃ ^ 2 + W.a₆

Tactic:
linear_combination W.a₆ * CharP.cast_eq_zero R 3

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem degree_divByMonic_lt (p : R[X]) {q : R[X]} (hq : Monic q) (hp0 : p ≠ 0)
    (h0q : 0 < degree q) : degree (p /ₘ q) < degree p :=
  if hpq : degree p < degree q then by
    haveI := Nontrivial.of_polynomial_ne hp0
    rw [(divByMonic_eq_zero_iff hq).2 hpq, degree_eq_natDegree hp0]
    exact WithBot.bot_lt_coe _
  else by
    haveI := Nontrivial.of_polynomial_ne hp0
    rw [← degree_add_divByMonic hq (not_lt.1 hpq), degree_eq_natDegree hq.ne_zero,
      degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 hpq)]
    exact
      Nat.cast_lt.2
        (Nat.lt_add_of_pos_left (Nat.cast_lt.1 <|
          by simpa [degree_eq_natDegree hq.ne_zero] using h0q))

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
hp0 : p ≠ 0
h0q : 0 < q.degree
hpq : p.degree < q.degree
this : Nontrivial R
⊢ (p /ₘ q).degree < p.degree

Tactic:
rw [(divByMonic_eq_zero_iff hq).2 hpq, degree_eq_natDegree hp0]

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
hp0 : p ≠ 0
h0q : 0 < q.degree
hpq : p.degree < q.degree
this : Nontrivial R
⊢ degree 0 < ↑p.natDegree

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
hp0 : p ≠ 0
h0q : 0 < q.degree
hpq : p.degree < q.degree
this : Nontrivial R
⊢ degree 0 < ↑p.natDegree

Tactic:
exact WithBot.bot_lt_coe _

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
hp0 : p ≠ 0
h0q : 0 < q.degree
hpq : ¬p.degree < q.degree
⊢ (p /ₘ q).degree < p.degree

Tactic:
haveI := Nontrivial.of_polynomial_ne hp0

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
hp0 : p ≠ 0
h0q : 0 < q.degree
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ (p /ₘ q).degree < p.degree

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
hp0 : p ≠ 0
h0q : 0 < q.degree
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ (p /ₘ q).degree < p.degree

Tactic:
rw [← degree_add_divByMonic hq (not_lt.1 hpq), degree_eq_natDegree hq.ne_zero,
  degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 hpq)]

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
hp0 : p ≠ 0
h0q : 0 < q.degree
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ ↑(p /ₘ q).natDegree < ↑q.natDegree + ↑(p /ₘ q).natDegree

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
hp0 : p ≠ 0
h0q : 0 < q.degree
hpq : p.degree < q.degree
⊢ (p /ₘ q).degree < p.degree

Tactic:
haveI := Nontrivial.of_polynomial_ne hp0

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
hp0 : p ≠ 0
h0q : 0 < q.degree
hpq : p.degree < q.degree
this : Nontrivial R
⊢ (p /ₘ q).degree < p.degree

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
hp0 : p ≠ 0
h0q : 0 < q.degree
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ ↑0 < ↑↑q.natDegree

Tactic:
simpa [degree_eq_natDegree hq.ne_zero] using h0q

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
hp0 : p ≠ 0
h0q : 0 < q.degree
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ ↑(p /ₘ q).natDegree < ↑q.natDegree + ↑(p /ₘ q).natDegree

Tactic:
exact
  Nat.cast_lt.2
    (Nat.lt_add_of_pos_left (Nat.cast_lt.1 <|
      by simpa [degree_eq_natDegree hq.ne_zero] using h0q))

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
lemma coprime_add_iff_right (h : a ∣ b) : Coprime a (b + c) ↔ Coprime a c

Proof state:
a b c : ℕ
h : a ∣ b
⊢ a.Coprime (b + c) ↔ a.Coprime c

Tactic:
obtain ⟨n, rfl⟩ := h

Result:
case intro
a c n : ℕ
⊢ a.Coprime (a * n + c) ↔ a.Coprime c

Proof state:
case intro
a c n : ℕ
⊢ a.Coprime (a * n + c) ↔ a.Coprime c

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem mem_iSup_of_mem {ι : Sort*} {S : ι → Submonoid M} (i : ι) :
    ∀ {x : M}, x ∈ S i → x ∈ iSup S

Proof state:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
i : ι
⊢ S i ≤ iSup S

Tactic:
exact le_iSup _ _

Result:
no goals

Proof state:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
i : ι
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S

Tactic:
rw [← SetLike.le_def]

Result:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
i : ι
⊢ S i ≤ iSup S
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem nnnorm_mul_le (a b : α) : ‖a * b‖₊ ≤ ‖a‖₊ * ‖b‖₊

Proof state:
α : Type u_2
inst✝ : NonUnitalSeminormedRing α
a b : α
⊢ ‖a * b‖₊ ≤ ‖a‖₊ * ‖b‖₊

Tactic:
simpa only [← norm_toNNReal, ← Real.toNNReal_mul (norm_nonneg _)] using
  Real.toNNReal_mono (norm_mul_le _ _)

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_target : (f.extend I).target = I.symm ⁻¹' f.target ∩ range I

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ (f.extend I).target = ↑I.symm ⁻¹' f.target ∩ range ↑I

Tactic:
simp_rw [extend, PartialEquiv.trans_target, I.target_eq, I.toPartialEquiv_coe_symm, inter_comm]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
@[reassoc (attr := simp), elementwise (attr := simp)]
lemma cocyclesMap_comp_isoOneCocycles_hom :
    cocyclesMap f φ 1 ≫ (isoOneCocycles B).hom = (isoOneCocycles A).hom ≫ mapOneCocycles f φ

Proof state:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
⊢ cocyclesMap f φ 1 ≫ (isoOneCocycles B).hom = (isoOneCocycles A).hom ≫ mapOneCocycles f φ

Tactic:
simp_rw [← cancel_mono (moduleCatLeftHomologyData (shortComplexH1 B)).i, mapOneCocycles,
    Category.assoc, cyclesMap'_i, isoOneCocycles, ← Category.assoc]

Result:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
⊢ (cocyclesMap f φ 1 ≫
        (HomologicalComplex.cyclesIsoSc' (inhomogeneousCochains B) 0 1 2 isoOneCocycles.proof_3
              isoOneCocycles.proof_4 ≪≫
            cyclesMapIso (shortComplexH1Iso B) ≪≫ (shortComplexH1 B).moduleCatCyclesIso).hom) ≫
      (shortComplexH1 B).moduleCatLeftHomologyData.i =
    ((HomologicalComplex.cyclesIsoSc' (inhomogeneousCochains A) 0 1 2 isoOneCocycles.proof_3 isoOneCocycles.proof_4 ≪≫
            cyclesMapIso (shortComplexH1Iso A) ≪≫ (shortComplexH1 A).moduleCatCyclesIso).hom ≫
        (shortComplexH1 A).moduleCatLeftHomologyData.i) ≫
      (mapShortComplexH1 f φ).τ₂

Proof state:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
⊢ (cocyclesMap f φ 1 ≫
        (HomologicalComplex.cyclesIsoSc' (inhomogeneousCochains B) 0 1 2 isoOneCocycles.proof_3
              isoOneCocycles.proof_4 ≪≫
            cyclesMapIso (shortComplexH1Iso B) ≪≫ (shortComplexH1 B).moduleCatCyclesIso).hom) ≫
      (shortComplexH1 B).moduleCatLeftHomologyData.i =
    ((HomologicalComplex.cyclesIsoSc' (inhomogeneousCochains A) 0 1 2 isoOneCocycles.proof_3 isoOneCocycles.proof_4 ≪≫
            cyclesMapIso (shortComplexH1Iso A) ≪≫ (shortComplexH1 A).moduleCatCyclesIso).hom ≫
        (shortComplexH1 A).moduleCatLeftHomologyData.i) ≫
      (mapShortComplexH1 f φ).τ₂

Tactic:
simp [cochainsMap_f_1_comp_oneCochainsLequiv f, mapShortComplexH1, ← LinearEquiv.toModuleIso_hom]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem Coprime.lcm_eq_mul {m n : ℕ} (h : Coprime m n) : lcm m n = m * n

Proof state:
m n : ℕ
h : m.Coprime n
⊢ m.lcm n = m * n

Tactic:
rw [← one_mul (lcm m n), ← h.gcd_eq_one, gcd_mul_lcm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_containsThenInsertIfNew [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
    {m : Raw₀ α β} (h : Raw.WFImp m.1) {a : α} {b : β a} :
    Perm (toListModel (m.containsThenInsertIfNew a b).2.1.2)
      (insertEntryIfNew a b (toListModel m.1.2))

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ toListModel (m.containsThenInsertIfNew a b).snd.val.buckets ~ insertEntryIfNew a b (toListModel m.val.buckets)

Tactic:
rw [containsThenInsertIfNew_eq_insertIfNewₘ]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ toListModel (m.insertIfNewₘ a b).val.buckets ~ insertEntryIfNew a b (toListModel m.val.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ toListModel (m.insertIfNewₘ a b).val.buckets ~ insertEntryIfNew a b (toListModel m.val.buckets)

Tactic:
exact toListModel_insertIfNewₘ h

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem toMeasure_apply₀ (m : OuterMeasure α) (h : ms ≤ m.caratheodory) {s : Set α}
    (hs : NullMeasurableSet s (m.toMeasure h)) : m.toMeasure h s = m s

Proof state:
α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
hs : NullMeasurableSet s (m.toMeasure h)
⊢ (m.toMeasure h) s = m s

Tactic:
refine le_antisymm ?_ (le_toMeasure_apply _ _ _)

Result:
α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
hs : NullMeasurableSet s (m.toMeasure h)
⊢ (m.toMeasure h) s ≤ m s

Proof state:
α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
hs : NullMeasurableSet s (m.toMeasure h)
⊢ (m.toMeasure h) s ≤ m s

Tactic:
rcases hs.exists_measurable_subset_ae_eq with ⟨t, hts, htm, heq⟩

Result:
case intro.intro.intro
α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
hs : NullMeasurableSet s (m.toMeasure h)
t : Set α
hts : t ⊆ s
htm : MeasurableSet t
heq : t =ᶠ[ae (m.toMeasure h)] s
⊢ (m.toMeasure h) s ≤ m s

Proof state:
case intro.intro.intro
α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
hs : NullMeasurableSet s (m.toMeasure h)
t : Set α
hts : t ⊆ s
htm : MeasurableSet t
heq : t =ᶠ[ae (m.toMeasure h)] s
⊢ (m.toMeasure h) s ≤ m s

Tactic:
calc
  m.toMeasure h s = m.toMeasure h t := measure_congr heq.symm
  _ = m t := toMeasure_apply m h htm
  _ ≤ m s := m.mono hts

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sdiff_sup_self (a b : α) : b \ a ⊔ a = b ⊔ a

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b \ a ⊔ a = b ⊔ a

Tactic:
rw [sup_comm, sup_sdiff_self, sup_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem isPrefixOf_nil_left [BEq α] : isPrefixOf ([] : List α) l = true

Proof state:
α : Type u
l : List α
inst✝ : BEq α
⊢ nil.isPrefixOf l = true

Tactic:
simp [isPrefixOf]

Result:
no goals
-- Mathlib/Data/List/OfFn.lean
theorem ofFn_getElem_eq_map {β : Type*} (l : List α) (f : α → β) :
    ofFn (fun i : Fin l.length => f <| l[(i : Nat)]) = l.map f

Proof state:
α : Type u
β : Type u_1
l : List α
f : α → β
⊢ (ofFn fun i => f l[↑i]) = map f l

Tactic:
rw [← Function.comp_def, ← map_ofFn, ofFn_getElem]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem bit0_of_bit0 : ∀ n, n + n = bit0 n
  | 1 => rfl
  | bit0 p => congr_arg bit0 (bit0_of_bit0 p)
  | bit1 p => show bit0 (succ (p + p)) = _ by rw [bit0_of_bit0 p, succ]

Proof state:
p : PosNum
⊢ (p + p).succ.bit0 = p.bit1.bit0

Tactic:
rw [bit0_of_bit0 p, succ]

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_intCast [DecidableEq n] [Ring α] [StarRing α] (d : ℤ) :
    (d : Matrix n n α)ᴴ = d

Proof state:
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Ring α
inst✝ : StarRing α
d : ℤ
⊢ (↑d)ᴴ = ↑d

Tactic:
simp [conjTranspose, Matrix.map_intCast, diagonal_intCast]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma fromAffine_ne_zero [Nontrivial R] {X Y : R} (h : W'.toAffine.Nonsingular X Y) :
    fromAffine (.some h) ≠ 0 := fun h0 ↦ by
  obtain ⟨u, eq⟩ := Quotient.eq.mp <| (Point.ext_iff ..).mp h0
  simpa [Units.smul_def, smul_fin3] using congr_fun eq z

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : Nontrivial R
X Y : R
h : (toAffine W').Nonsingular X Y
h0 : fromAffine (Affine.Point.some h) = 0
⊢ False

Tactic:
obtain ⟨u, eq⟩ := Quotient.eq.mp <| (Point.ext_iff ..).mp h0

Result:
case intro
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : Nontrivial R
X Y : R
h : (toAffine W').Nonsingular X Y
h0 : fromAffine (Affine.Point.some h) = 0
u : Rˣ
eq : (fun m => m • ![1, 1, 0]) u = ![X, Y, 1]
⊢ False

Proof state:
case intro
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : Nontrivial R
X Y : R
h : (toAffine W').Nonsingular X Y
h0 : fromAffine (Affine.Point.some h) = 0
u : Rˣ
eq : (fun m => m • ![1, 1, 0]) u = ![X, Y, 1]
⊢ False

Tactic:
simpa [Units.smul_def, smul_fin3] using congr_fun eq z

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_signExtend_of_le {x : BitVec w} (hv : v ≤ w) :
    (x.signExtend v).toInt = Int.bmod x.toNat (2^v)

Proof state:
w v : Nat
x : BitVec w
hv : v ≤ w
⊢ (signExtend v x).toInt = (↑x.toNat).bmod (2 ^ v)

Tactic:
simp [signExtend_eq_setWidth_of_lt _ hv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem length_zip (l₁ : List α) (l₂ : List β) :
    length (zip l₁ l₂) = min (length l₁) (length l₂)

Proof state:
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
⊢ (l₁.zip l₂).length = min l₁.length l₂.length

Tactic:
simp [zip]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem preimage_invFun_of_not_mem [n : Nonempty α] {f : α → β} (hf : Injective f) {s : Set α}
    (h : Classical.choice n ∉ s) : invFun f ⁻¹' s = f '' s

Proof state:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∉ s
⊢ invFun f ⁻¹' s = f '' s

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∉ s
x : β
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s

Proof state:
case h.inr
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∉ s
x : β
hx : x ∉ range f
this : x ∉ f '' s
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s

Tactic:
simp only [mem_preimage, invFun_neg hx, h, this]

Result:
no goals

Proof state:
case h.inr
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∉ s
x : β
hx : x ∉ range f
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s

Tactic:
have : x ∉ f '' s := fun h' => hx (image_subset_range _ _ h')

Result:
case h.inr
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∉ s
x : β
hx : x ∉ range f
this : x ∉ f '' s
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s

Proof state:
case h
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∉ s
x : β
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s

Tactic:
rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)

Result:
case h.inl.intro
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∉ s
a : α
⊢ f a ∈ invFun f ⁻¹' s ↔ f a ∈ f '' s

case h.inr
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∉ s
x : β
hx : x ∉ range f
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s

Proof state:
case h.inl.intro
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∉ s
a : α
⊢ f a ∈ invFun f ⁻¹' s ↔ f a ∈ f '' s

Tactic:
rw [mem_preimage, leftInverse_invFun hf, hf.mem_set_image]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_comp_mul_deriv' {f f' g : ℝ → ℝ} (h : ∀ x ∈ uIcc a b, HasDerivAt f (f' x) x)
    (h' : ContinuousOn f' (uIcc a b)) (hg : ContinuousOn g (f '' [[a, b]])) :
    (∫ x in a..b, (g ∘ f) x * f' x) = ∫ x in f a..f b, g x

Proof state:
a b : ℝ
f f' g : ℝ → ℝ
h : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x
h' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g (f '' [[a, b]])
⊢ ∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (x : ℝ) in f a..f b, g x

Tactic:
simpa [mul_comm] using integral_comp_smul_deriv' h h' hg

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
lemma qaryEntropy_pos (hp₀ : 0 < p) (hp₁ : p < 1) : 0 < qaryEntropy q p

Proof state:
q : ℕ
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 < p * log ↑(↑q - 1) + binEntropy p

Tactic:
have := binEntropy_pos hp₀ hp₁

Result:
q : ℕ
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
this : 0 < binEntropy p
⊢ 0 < p * log ↑(↑q - 1) + binEntropy p

Proof state:
q : ℕ
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 < qaryEntropy q p

Tactic:
unfold qaryEntropy

Result:
q : ℕ
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 < p * log ↑(↑q - 1) + binEntropy p

Proof state:
q : ℕ
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
this : 0 < binEntropy p
⊢ 0 < p * log ↑(↑q - 1) + binEntropy p

Tactic:
positivity

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem toList_ne_singleton (y : α) : toList p x ≠ [y]

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ p.toList x ≠ [y]

Tactic:
intro H

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
H : p.toList x = [y]
⊢ False

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
H : p.toList x = [y]
⊢ False

Tactic:
simpa [card_support_ne_one] using congr_arg length H

Result:
no goals
-- Mathlib/RingTheory/Kaehler/CotangentComplex.lean
@[simp]
lemma map_id :
    CotangentSpace.map (.id P) = LinearMap.id

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ CotangentSpace.map (Hom.id P) = LinearMap.id

Tactic:
ext

Result:
case a.h.hf.H
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
a✝ : P.Ring
⊢ (((AlgebraTensorModule.curry (CotangentSpace.map (Hom.id P))) 1).compDer (D R P.Ring)) a✝ =
    (((AlgebraTensorModule.curry LinearMap.id) 1).compDer (D R P.Ring)) a✝

Proof state:
case a.h.hf.H
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
a✝ : P.Ring
⊢ (((AlgebraTensorModule.curry (CotangentSpace.map (Hom.id P))) 1).compDer (D R P.Ring)) a✝ =
    (((AlgebraTensorModule.curry LinearMap.id) 1).compDer (D R P.Ring)) a✝

Tactic:
simp

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem compl_iSup₂ (f : ∀ i, κ i → LowerSet α) :
    (⨆ (i) (j), f i j).compl = ⨆ (i) (j), (f i j).compl

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
f : (i : ι) → κ i → LowerSet α
⊢ (⨆ i, ⨆ j, f i j).compl = ⨆ i, ⨆ j, (f i j).compl

Tactic:
simp_rw [LowerSet.compl_iSup]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem Iio_ae_eq_Iic' (ha : μ {a} = 0) : Iio a =ᵐ[μ] Iic a

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : PartialOrder α
a : α
ha : μ {a} = 0
⊢ Iio a =ᶠ[ae μ] Iic a

Tactic:
rw [← Iic_diff_right, diff_ae_eq_self, measure_mono_null Set.inter_subset_right ha]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
theorem pullbackIsoProdSubtype_hom_fst (f : X ⟶ Z) (g : Y ⟶ Z) :
    (pullbackIsoProdSubtype f g).hom ≫ pullbackFst f g = pullback.fst _ _

Proof state:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoProdSubtype f g).hom ≫ pullbackFst f g = pullback.fst f g

Tactic:
rw [← Iso.eq_inv_comp, pullbackIsoProdSubtype_inv_fst]

Result:
no goals
-- Mathlib/Probability/IdentDistrib.lean
theorem essSup_eq [ConditionallyCompleteLinearOrder γ] [TopologicalSpace γ] [OpensMeasurableSpace γ]
    [OrderClosedTopology γ] (h : IdentDistrib f g μ ν) : essSup f μ = essSup g ν

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝³ : ConditionallyCompleteLinearOrder γ
inst✝² : TopologicalSpace γ
inst✝¹ : OpensMeasurableSpace γ
inst✝ : OrderClosedTopology γ
h : IdentDistrib f g μ ν
⊢ essSup f μ = essSup g ν

Tactic:
have I : ∀ a, μ {x : α | a < f x} = ν {x : β | a < g x} := fun a =>
  h.measure_mem_eq measurableSet_Ioi

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝³ : ConditionallyCompleteLinearOrder γ
inst✝² : TopologicalSpace γ
inst✝¹ : OpensMeasurableSpace γ
inst✝ : OrderClosedTopology γ
h : IdentDistrib f g μ ν
I : ∀ (a : γ), μ {x | a < f x} = ν {x | a < g x}
⊢ essSup f μ = essSup g ν

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝³ : ConditionallyCompleteLinearOrder γ
inst✝² : TopologicalSpace γ
inst✝¹ : OpensMeasurableSpace γ
inst✝ : OrderClosedTopology γ
h : IdentDistrib f g μ ν
I : ∀ (a : γ), μ {x | a < f x} = ν {x | a < g x}
⊢ essSup f μ = essSup g ν

Tactic:
simp_rw [essSup_eq_sInf, I]

Result:
no goals
-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem IsPurelyInseparable.sepDegree_eq_one [IsPurelyInseparable F E] :
    sepDegree F E = 1

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsPurelyInseparable F E
⊢ sepDegree F E = 1

Tactic:
rw [sepDegree, separableClosure.eq_bot_of_isPurelyInseparable, IntermediateField.rank_bot]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem getLsbD_sub {i : Nat} {i_lt : i < w} {x y : BitVec w} :
    (x - y).getLsbD i
      = (x.getLsbD i ^^ ((~~~y + 1#w).getLsbD i ^^ carry i x (~~~y + 1#w) false))

Proof state:
case i_lt
w i : Nat
i_lt : i < w
x y : BitVec w
⊢ i < w

Tactic:
omega

Result:
no goals

Proof state:
w i : Nat
i_lt : i < w
x y : BitVec w
⊢ (x - y).getLsbD i = (x.getLsbD i ^^ ((~~~y + 1#w).getLsbD i ^^ carry i x (~~~y + 1#w) false))

Tactic:
rw [sub_toAdd, BitVec.neg_eq_not_add, getLsbD_add]

Result:
case i_lt
w i : Nat
i_lt : i < w
x y : BitVec w
⊢ i < w