harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem _root_.Filter.Eventually.volume_pos_of_nhds_real {p : ℝ → Prop} {a : ℝ}
    (h : ∀ᶠ x in 𝓝 a, p x) : (0 : ℝ≥0∞) < volume { x | p x }

Proof state:
case intro.intro.intro
p : ℝ → Prop
a : ℝ
h : ∀ᶠ (x : ℝ) in 𝓝 a, p x
l u : ℝ
hx : a ∈ Ioo l u
hs : Ioo l u ⊆ {x | p x}
⊢ 0 < volume (Ioo l u)

Tactic:
simpa [-mem_Ioo] using hx.1.trans hx.2

Result:
no goals

Proof state:
case intro.intro.intro
p : ℝ → Prop
a : ℝ
h : ∀ᶠ (x : ℝ) in 𝓝 a, p x
l u : ℝ
hx : a ∈ Ioo l u
hs : Ioo l u ⊆ {x | p x}
⊢ 0 < volume {x | p x}

Tactic:
refine lt_of_lt_of_le ?_ (measure_mono hs)

Result:
case intro.intro.intro
p : ℝ → Prop
a : ℝ
h : ∀ᶠ (x : ℝ) in 𝓝 a, p x
l u : ℝ
hx : a ∈ Ioo l u
hs : Ioo l u ⊆ {x | p x}
⊢ 0 < volume (Ioo l u)

Proof state:
p : ℝ → Prop
a : ℝ
h : ∀ᶠ (x : ℝ) in 𝓝 a, p x
⊢ 0 < volume {x | p x}

Tactic:
rcases h.exists_Ioo_subset with ⟨l, u, hx, hs⟩

Result:
case intro.intro.intro
p : ℝ → Prop
a : ℝ
h : ∀ᶠ (x : ℝ) in 𝓝 a, p x
l u : ℝ
hx : a ∈ Ioo l u
hs : Ioo l u ⊆ {x | p x}
⊢ 0 < volume {x | p x}
-- Mathlib/Data/NNReal/Defs.lean
@[simp, norm_cast] lemma coe_lt_one : (r : ℝ) < 1 ↔ r < 1

Proof state:
r : ℝ≥0
⊢ ↑r < 1 ↔ r < 1

Tactic:
rw [← coe_lt_coe, coe_one]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Basic.lean
theorem measure_iUnion_le [Countable ι] (s : ι → Set α) : μ (⋃ i, s i) ≤ ∑' i, μ (s i)

Proof state:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable ι
s : ι → Set α
t : ℕ → Set α
⊢ μ (⋃ i, t i) = μ (⋃ i, disjointed t i)

Tactic:
rw [iUnion_disjointed]

Result:
no goals

Proof state:
case h.h
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable ι
s : ι → Set α
t : ℕ → Set α
a✝ : ℕ
⊢ disjointed t a✝ ⊆ t a✝

Tactic:
exact disjointed_subset ..

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable ι
s : ι → Set α
t : ℕ → Set α
⊢ ∑' (i : ℕ), μ (disjointed t i) ≤ ∑' (i : ℕ), μ (t i)

Tactic:
gcongr

Result:
case h.h
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable ι
s : ι → Set α
t : ℕ → Set α
a✝ : ℕ
⊢ disjointed t a✝ ⊆ t a✝

Proof state:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable ι
s : ι → Set α
t : ℕ → Set α
⊢ (fun x1 x2 => x1 ≤ x2) (μ (⨆ i, t i)) (∑' (i : ℕ), μ (t i))

Tactic:
calc
  μ (⋃ i, t i) = μ (⋃ i, disjointed t i) := by rw [iUnion_disjointed]
  _ ≤ ∑' i, μ (disjointed t i) :=
    OuterMeasureClass.measure_iUnion_nat_le _ _ (disjoint_disjointed _)
  _ ≤ ∑' i, μ (t i) := by gcongr; exact disjointed_subset ..

Result:
no goals
-- Mathlib/Tactic/Abel.lean
theorem unfold_sub {α} [SubtractionMonoid α] (a b c : α) (h : a + -b = c) : a - b = c

Proof state:
α : Type u_1
inst✝ : SubtractionMonoid α
a b c : α
h : a + -b = c
⊢ a - b = c

Tactic:
rw [sub_eq_add_neg, h]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem pred : @Primrec' 1 fun v => v.head.pred :=
  (prec' head (const 0) head).of_eq fun v => by simp; cases v.head <;> rfl

Proof state:
v : List.Vector ℕ (Nat.succ 0)
⊢ Nat.rec 0 (fun y IH => y) v.head = v.head - 1

Tactic:
cases v.head <;> rfl

Result:
no goals

Proof state:
v : List.Vector ℕ (Nat.succ 0)
⊢ Nat.rec 0 (fun y IH => (y ::ᵥ IH ::ᵥ v).head) v.head = v.head.pred

Tactic:
simp

Result:
v : List.Vector ℕ (Nat.succ 0)
⊢ Nat.rec 0 (fun y IH => y) v.head = v.head - 1
-- Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean
/-- If each component of the unit is a monomorphism, then the left adjoint is faithful. -/
lemma faithful_L_of_mono_unit_app [∀ X, Mono (h.unit.app X)] : L.Faithful where
  map_injective {X Y f g} hfg

Proof state:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), Mono (h.unit.app X)
X Y : C
f g : X ⟶ Y
hfg : L.map f = L.map g
⊢ f ≫ h.unit.app Y = g ≫ h.unit.app Y

Tactic:
apply (h.homEquiv X (L.obj Y)).symm.injective

Result:
case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), Mono (h.unit.app X)
X Y : C
f g : X ⟶ Y
hfg : L.map f = L.map g
⊢ (h.homEquiv X (L.obj Y)).symm (f ≫ h.unit.app Y) = (h.homEquiv X (L.obj Y)).symm (g ≫ h.unit.app Y)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), Mono (h.unit.app X)
X Y : C
f g : X ⟶ Y
hfg : L.map f = L.map g
⊢ f = g

Tactic:
apply Mono.right_cancellation (f := h.unit.app Y)

Result:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), Mono (h.unit.app X)
X Y : C
f g : X ⟶ Y
hfg : L.map f = L.map g
⊢ f ≫ h.unit.app Y = g ≫ h.unit.app Y

Proof state:
case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), Mono (h.unit.app X)
X Y : C
f g : X ⟶ Y
hfg : L.map f = L.map g
⊢ (h.homEquiv X (L.obj Y)).symm (f ≫ h.unit.app Y) = (h.homEquiv X (L.obj Y)).symm (g ≫ h.unit.app Y)

Tactic:
simpa using hfg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem insert_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} :
    m.insert a b = (Raw₀.insert ⟨m, h.size_buckets_pos⟩ a b).1

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

Tactic:
simp [Raw.insert, h.size_buckets_pos]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem castAdd_lt {m : Nat} (n : Nat) (i : Fin m) : (castAdd n i : Nat) < m

Proof state:
m n : Nat
i : Fin m
⊢ ↑(castAdd n i) < m

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem restrict_split (h : I ≤ J) (i : ι) (x : ℝ) : (split J i x).restrict I = split I i x

Proof state:
ι : Type u_1
I J : Box ι
h : I ≤ J
i : ι
x : ℝ
⊢ (split J i x).restrict I = split I i x

Tactic:
refine ((isPartitionSplit J i x).restrict h).eq_of_boxes_subset ?_

Result:
ι : Type u_1
I J : Box ι
h : I ≤ J
i : ι
x : ℝ
⊢ ((split J i x).restrict I).boxes ⊆ (split I i x).boxes

Proof state:
ι : Type u_1
I J : Box ι
h : I ≤ J
i : ι
x : ℝ
⊢ ∀ ⦃x_1 : Box ι⦄,
    (∃ J', (↑J' = ↑J ∩ {y | y i ≤ x} ∨ ↑J' = ↑J ∩ {y | x < y i}) ∧ ↑x_1 = ↑I ∩ ↑J') →
      ↑x_1 = ↑I ∩ {y | y i ≤ x} ∨ ↑x_1 = ↑I ∩ {y | x < y i}

Tactic:
have : ∀ s, (I ∩ s : Set (ι → ℝ)) ⊆ J := fun s => inter_subset_left.trans h

Result:
ι : Type u_1
I J : Box ι
h : I ≤ J
i : ι
x : ℝ
this : ∀ (s : Set (ι → ℝ)), ↑I ∩ s ⊆ ↑J
⊢ ∀ ⦃x_1 : Box ι⦄,
    (∃ J', (↑J' = ↑J ∩ {y | y i ≤ x} ∨ ↑J' = ↑J ∩ {y | x < y i}) ∧ ↑x_1 = ↑I ∩ ↑J') →
      ↑x_1 = ↑I ∩ {y | y i ≤ x} ∨ ↑x_1 = ↑I ∩ {y | x < y i}

Proof state:
ι : Type u_1
I J : Box ι
h : I ≤ J
i : ι
x : ℝ
this : ∀ (s : Set (ι → ℝ)), ↑I ∩ s ⊆ ↑J
⊢ ∀ ⦃x_1 : Box ι⦄,
    (∃ J', (↑J' = ↑J ∩ {y | y i ≤ x} ∨ ↑J' = ↑J ∩ {y | x < y i}) ∧ ↑x_1 = ↑I ∩ ↑J') →
      ↑x_1 = ↑I ∩ {y | y i ≤ x} ∨ ↑x_1 = ↑I ∩ {y | x < y i}

Tactic:
rintro J₁ ⟨J₂, H₂ | H₂, H₁⟩ <;> [left; right] <;>
  simp [H₁, H₂, inter_left_comm (I : Set (ι → ℝ)), this]

Result:
no goals

Proof state:
ι : Type u_1
I J : Box ι
h : I ≤ J
i : ι
x : ℝ
⊢ ((split J i x).restrict I).boxes ⊆ (split I i x).boxes

Tactic:
simp only [Finset.subset_iff, mem_boxes, mem_restrict', exists_prop, mem_split_iff']

Result:
ι : Type u_1
I J : Box ι
h : I ≤ J
i : ι
x : ℝ
⊢ ∀ ⦃x_1 : Box ι⦄,
    (∃ J', (↑J' = ↑J ∩ {y | y i ≤ x} ∨ ↑J' = ↑J ∩ {y | x < y i}) ∧ ↑x_1 = ↑I ∩ ↑J') →
      ↑x_1 = ↑I ∩ {y | y i ≤ x} ∨ ↑x_1 = ↑I ∩ {y | x < y i}
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem biprod.add_eq_lift_desc_id [HasBinaryBiproduct Y Y] :
    f + g = biprod.lift f g ≫ biprod.desc (𝟙 Y) (𝟙 Y)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f g : X ⟶ Y
inst✝ : HasBinaryBiproduct Y Y
⊢ f + g = lift f g ≫ desc (𝟙 Y) (𝟙 Y)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt_add_of_neg_add_lt_left {a b c : Int} (h : -b + a < c) : a < b + c

Proof state:
a b c : Int
h : a + -b < c
⊢ a < b + c

Tactic:
exact Int.lt_add_of_sub_left_lt h

Result:
no goals

Proof state:
a b c : Int
h : -b + a < c
⊢ a < b + c

Tactic:
rw [Int.add_comm] at h

Result:
a b c : Int
h : a + -b < c
⊢ a < b + c
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_eq_length {l : List α} : count a l = l.length ↔ ∀ b ∈ l, a = b

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ count a l = l.length ↔ ∀ (b : α), b ∈ l → a = b

Tactic:
rw [count, countP_eq_length]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ (∀ (a_1 : α), a_1 ∈ l → (a_1 == a) = true) ↔ ∀ (b : α), b ∈ l → a = b

Proof state:
case refine_1
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ∀ (a_1 : α), a_1 ∈ l → (a_1 == a) = true
b : α
hb : b ∈ l
⊢ b = a

Tactic:
simpa using h b hb

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ (∀ (a_1 : α), a_1 ∈ l → (a_1 == a) = true) ↔ ∀ (b : α), b ∈ l → a = b

Tactic:
refine ⟨fun h b hb => Eq.symm ?_, fun h b hb => ?_⟩

Result:
case refine_1
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ∀ (a_1 : α), a_1 ∈ l → (a_1 == a) = true
b : α
hb : b ∈ l
⊢ b = a

case refine_2
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ∀ (b : α), b ∈ l → a = b
b : α
hb : b ∈ l
⊢ (b == a) = true

Proof state:
case refine_2
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ∀ (b : α), b ∈ l → a = b
b : α
hb : b ∈ l
⊢ (b == a) = true

Tactic:
rw [h b hb, beq_self_eq_true]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
theorem not_isUniform_iff :
    ¬G.IsUniform ε s t ↔ ∃ s', s' ⊆ s ∧ ∃ t', t' ⊆ t ∧ #s * ε ≤ #s' ∧
      #t * ε ≤ #t' ∧ ε ≤ |G.edgeDensity s' t' - G.edgeDensity s t|

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
⊢ ¬G.IsUniform ε s t ↔
    ∃ s' ⊆ s, ∃ t' ⊆ t, ↑(#s) * ε ≤ ↑(#s') ∧ ↑(#t) * ε ≤ ↑(#t') ∧ ε ≤ ↑|G.edgeDensity s' t' - G.edgeDensity s t|

Tactic:
unfold IsUniform

Result:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
⊢ (¬∀ ⦃s' : Finset α⦄,
        s' ⊆ s →
          ∀ ⦃t' : Finset α⦄,
            t' ⊆ t → ↑(#s) * ε ≤ ↑(#s') → ↑(#t) * ε ≤ ↑(#t') → |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < ε) ↔
    ∃ s' ⊆ s, ∃ t' ⊆ t, ↑(#s) * ε ≤ ↑(#s') ∧ ↑(#t) * ε ≤ ↑(#t') ∧ ε ≤ ↑|G.edgeDensity s' t' - G.edgeDensity s t|

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
⊢ (¬∀ ⦃s' : Finset α⦄,
        s' ⊆ s →
          ∀ ⦃t' : Finset α⦄,
            t' ⊆ t → ↑(#s) * ε ≤ ↑(#s') → ↑(#t) * ε ≤ ↑(#t') → |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < ε) ↔
    ∃ s' ⊆ s, ∃ t' ⊆ t, ↑(#s) * ε ≤ ↑(#s') ∧ ↑(#t) * ε ≤ ↑(#t') ∧ ε ≤ ↑|G.edgeDensity s' t' - G.edgeDensity s t|

Tactic:
simp only [not_forall, not_lt, exists_prop, exists_and_left, Rat.cast_abs, Rat.cast_sub]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem zpow_period_add_smul (i : ℤ) (g : G) (a : α) :
    g ^ (period g a + i) • a = g ^ i • a

Proof state:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
i : ℤ
g : G
a : α
⊢ g ^ (↑(period g a) + i) • a = g ^ i • a

Tactic:
rw [← zpow_mod_period_smul, Int.add_emod_self_left, zpow_mod_period_smul]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
theorem eisenstein_lemma_aux (p : ℕ) [Fact p.Prime] [Fact (p % 2 = 1)] {a : ℕ} (ha2 : a % 2 = 1)
    (hap : (a : ZMod p) ≠ 0) :
    #{x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val} ≡
      ∑ x ∈ Ico 1 (p / 2).succ, x * a / p [MOD 2] :=
  have ha2 : (a : ZMod 2) = (1 : ℕ) := (eq_iff_modEq_nat _).2 ha2
  (eq_iff_modEq_nat 2).1 <| sub_eq_zero.1 <| by
    simpa [add_left_comm, sub_eq_add_neg, ← mul_sum, mul_comm, ha2, Nat.cast_sum,
      add_neg_eq_iff_eq_add.symm, neg_eq_self_mod_two, add_assoc] using
      Eq.symm (eisenstein_lemma_aux₁ p hap)

Proof state:
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (p % 2 = 1)
a : ℕ
ha2✝ : a % 2 = 1
hap : ↑a ≠ 0
ha2 : ↑a = ↑1
⊢ ↑(#(filter (fun x => p / 2 < (↑a * ↑x).val) (Ico 1 (p / 2).succ))) - ↑(∑ x ∈ Ico 1 (p / 2).succ, x * a / p) = 0

Tactic:
simpa [add_left_comm, sub_eq_add_neg, ← mul_sum, mul_comm, ha2, Nat.cast_sum,
  add_neg_eq_iff_eq_add.symm, neg_eq_self_mod_two, add_assoc] using
  Eq.symm (eisenstein_lemma_aux₁ p hap)

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem restrictScalars_adjoin_of_algEquiv
    {L L' : Type*} [Field L] [Field L']
    [Algebra F L] [Algebra L E] [Algebra F L'] [Algebra L' E]
    [IsScalarTower F L E] [IsScalarTower F L' E] (i : L ≃ₐ[F] L')
    (hi : algebraMap L E = (algebraMap L' E) ∘ i) (S : Set E) :
    (adjoin L S).restrictScalars F = (adjoin L' S).restrictScalars F

Proof state:
case e_s.e_a.h
F : Type u_1
inst✝¹⁰ : Field F
E : Type u_2
inst✝⁹ : Field E
inst✝⁸ : Algebra F E
L : Type u_3
L' : Type u_4
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L
inst✝⁴ : Algebra L E
inst✝³ : Algebra F L'
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L E
inst✝ : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i
S : Set E
x : E
⊢ x ∈ Set.range ⇑(algebraMap L E) ↔ x ∈ Set.range ⇑(algebraMap L' E)

Tactic:
exact ⟨fun ⟨y, h⟩ ↦ ⟨i y, by rw [← h, hi]; rfl⟩,
  fun ⟨y, h⟩ ↦ ⟨i.symm y, by rw [← h, hi, Function.comp_apply, AlgEquiv.apply_symm_apply]⟩⟩

Result:
no goals

Proof state:
F : Type u_1
inst✝¹⁰ : Field F
E : Type u_2
inst✝⁹ : Field E
inst✝⁸ : Algebra F E
L : Type u_3
L' : Type u_4
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L
inst✝⁴ : Algebra L E
inst✝³ : Algebra F L'
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L E
inst✝ : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i
S : Set E
⊢ (restrictScalars F (adjoin L S)).toSubfield = (restrictScalars F (adjoin L' S)).toSubfield

Tactic:
change Subfield.closure _ = Subfield.closure _

Result:
F : Type u_1
inst✝¹⁰ : Field F
E : Type u_2
inst✝⁹ : Field E
inst✝⁸ : Algebra F E
L : Type u_3
L' : Type u_4
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L
inst✝⁴ : Algebra L E
inst✝³ : Algebra F L'
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L E
inst✝ : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i
S : Set E
⊢ Subfield.closure (Set.range ⇑(algebraMap L E) ∪ S) = Subfield.closure (Set.range ⇑(algebraMap L' E) ∪ S)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem slt_eq_ult (x y : BitVec w) :
    x.slt y = (x.msb != y.msb).xor (x.ult y)

Proof state:
case neg
w : Nat
x y : BitVec w
h : ¬x.msb = y.msb
⊢ x.slt y = (x.msb != y.msb ^^ x.ult y)

Tactic:
have h' : x.msb != y.msb := by simp_all

Result:
case neg
w : Nat
x y : BitVec w
h : ¬x.msb = y.msb
h' : (x.msb != y.msb) = true
⊢ x.slt y = (x.msb != y.msb ^^ x.ult y)

Proof state:
w : Nat
x y : BitVec w
⊢ x.slt y = (x.msb != y.msb ^^ x.ult y)

Tactic:
by_cases h : x.msb = y.msb

Result:
case pos
w : Nat
x y : BitVec w
h : x.msb = y.msb
⊢ x.slt y = (x.msb != y.msb ^^ x.ult y)

case neg
w : Nat
x y : BitVec w
h : ¬x.msb = y.msb
⊢ x.slt y = (x.msb != y.msb ^^ x.ult y)

Proof state:
case pos
w : Nat
x y : BitVec w
h : x.msb = y.msb
⊢ x.slt y = (x.msb != y.msb ^^ x.ult y)

Tactic:
simp [h, slt_eq_ult_of_msb_eq]

Result:
no goals

Proof state:
case neg
w : Nat
x y : BitVec w
h : ¬x.msb = y.msb
h' : (x.msb != y.msb) = true
⊢ x.slt y = (x.msb != y.msb ^^ x.ult y)

Tactic:
simp [slt_eq_not_ult_of_msb_neq h, h']

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
h : ¬x.msb = y.msb
⊢ (x.msb != y.msb) = true

Tactic:
simp_all

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_eq_natDegree_iff (hf : f ≠ 0) :
    f.natSepDegree = f.natDegree ↔ f.Separable

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ f.Separable

Tactic:
simp_rw [← card_rootSet_eq_natDegree_iff_of_splits hf (SplittingField.splits f),
  rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]

Result:
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ (f.aroots f.SplittingField).toFinset.card = f.natDegree

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ f.Separable

Tactic:
classical
simp_rw [← card_rootSet_eq_natDegree_iff_of_splits hf (SplittingField.splits f),
  rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
rfl

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ (f.aroots f.SplittingField).toFinset.card = f.natDegree

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem irrational_int_div_iff : Irrational (m / x) ↔ m ≠ 0 ∧ Irrational x

Proof state:
m : ℤ
x : ℝ
⊢ Irrational (↑m / x) ↔ m ≠ 0 ∧ Irrational x

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem prod_multiset_root_eq_finset_root [DecidableEq R] :
    (p.roots.map fun a => X - C a).prod =
      p.roots.toFinset.prod fun a => (X - C a) ^ rootMultiplicity a p

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
inst✝ : DecidableEq R
⊢ (Multiset.map (fun a => X - C a) p.roots).prod = ∏ a ∈ p.roots.toFinset, (X - C a) ^ rootMultiplicity a p

Tactic:
simp only [count_roots, Finset.prod_multiset_map_count]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue_modifyKey_self [EquivBEq α] {k : α} {f : β → β} (l : List ((_ : α) × β))
    (hl : DistinctKeys l) {h : containsKey k (modifyKey k f l)} :
    haveI h' : containsKey k l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : containsKey k (modifyKey k f l) = true
⊢ getValue k (modifyKey k f l) h = f (getValue k l ⋯)

Tactic:
simp [getValue_modifyKey, hl]

Result:
no goals

Proof state:
α : Type u
β✝ : α → Type v
γ : α → Type w
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : containsKey k (modifyKey k f l) = true
⊢ containsKey k l = true

Tactic:
rwa [containsKey_modifyKey] at h

Result:
no goals
-- Mathlib/Logic/Equiv/Functor.lean
theorem mapEquiv_refl_refl : mapEquiv F (Equiv.refl α) (Equiv.refl α') = Equiv.refl (F α α')

Proof state:
α : Type u
α' : Type v
F : Type u → Type v → Type w
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
⊢ mapEquiv F (Equiv.refl α) (Equiv.refl α') = Equiv.refl (F α α')

Tactic:
ext x

Result:
case H
α : Type u
α' : Type v
F : Type u → Type v → Type w
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
x : F α α'
⊢ (mapEquiv F (Equiv.refl α) (Equiv.refl α')) x = (Equiv.refl (F α α')) x

Proof state:
case H
α : Type u
α' : Type v
F : Type u → Type v → Type w
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
x : F α α'
⊢ (mapEquiv F (Equiv.refl α) (Equiv.refl α')) x = (Equiv.refl (F α α')) x

Tactic:
simp [id_bimap]

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem wcovBy_iff_covBy_or_eq : a ⩿ b ↔ a ⋖ b ∨ a = b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ a ⩿ b ↔ a ⋖ b ∨ a = b

Tactic:
rw [le_antisymm_iff, wcovBy_iff_covBy_or_le_and_le]

Result:
no goals
-- Mathlib/Data/Nat/Size.lean
theorem size_bit {b n} (h : bit b n ≠ 0) : size (bit b n) = succ (size n)

Proof state:
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ binaryRec 0 (fun x x => succ) (bit b n) = (binaryRec 0 (fun x x => succ) n).succ

Tactic:
conv =>
  lhs
  rw [binaryRec]
  simp [h]

Result:
no goals

Proof state:
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ (bit b n).size = n.size.succ

Tactic:
unfold size

Result:
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ binaryRec 0 (fun x x => succ) (bit b n) = (binaryRec 0 (fun x x => succ) n).succ
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem sin_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : Real.Angle.sin (o.oangle x (x + y)) * ‖x + y‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle x (x + y)).sin * ‖x + y‖ = ‖y‖

Tactic:
have hs : (o.oangle x (x + y)).sign = 1 := by
  rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ (o.oangle x (x + y)).sin * ‖x + y‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ (o.oangle x (x + y)).sin * ‖x + y‖ = ‖y‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
  InnerProductGeometry.sin_angle_add_mul_norm_of_inner_eq_zero
    (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle x (x + y)).sign = 1

Tactic:
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals