harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldl_filterMap (f : α → Option β) (g : γ → β → γ) (l : List α) (init : γ) :
    (l.filterMap f).foldl g init = l.foldl (fun x y => match f y with | some b => g x b | none => x) init

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : γ → β → γ
l : List α
init : γ
⊢ foldl g init (filterMap f l) =
    foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init l

Tactic:
induction l generalizing init with
| nil => rfl
| cons a l ih =>
  simp only [filterMap_cons, foldl_cons]
  cases f a <;> simp [ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : γ → β → γ
a : α
l : List α
ih :
  ∀ (init : γ),
    foldl g init (filterMap f l) =
      foldl
        (fun x y =>
          match f y with
          | some b => g x b
          | none => x)
        init l
init : γ
⊢ foldl g init
      (match f a with
      | none => filterMap f l
      | some b => b :: filterMap f l) =
    foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      (match f a with
      | some b => g init b
      | none => init)
      l

Tactic:
cases f a <;> simp [ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : γ → β → γ
a : α
l : List α
ih :
  ∀ (init : γ),
    foldl g init (filterMap f l) =
      foldl
        (fun x y =>
          match f y with
          | some b => g x b
          | none => x)
        init l
init : γ
⊢ foldl g init (filterMap f (a :: l)) =
    foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init (a :: l)

Tactic:
simp only [filterMap_cons, foldl_cons]

Result:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : γ → β → γ
a : α
l : List α
ih :
  ∀ (init : γ),
    foldl g init (filterMap f l) =
      foldl
        (fun x y =>
          match f y with
          | some b => g x b
          | none => x)
        init l
init : γ
⊢ foldl g init
      (match f a with
      | none => filterMap f l
      | some b => b :: filterMap f l) =
    foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      (match f a with
      | some b => g init b
      | none => init)
      l

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : γ → β → γ
init : γ
⊢ foldl g init (filterMap f []) =
    foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init []

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_smul [SMulZeroClass S R] (r : S) (p : R[X]) (n : ℕ) :
    coeff (r • p) n = r • coeff p n

Proof state:
case ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ (r • { toFinsupp := toFinsupp✝ }).coeff n = r • { toFinsupp := toFinsupp✝ }.coeff n

Tactic:
simp_rw [← ofFinsupp_smul, coeff]

Result:
case ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ (r • toFinsupp✝) n = r • toFinsupp✝ n

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
p : R[X]
n : ℕ
⊢ (r • p).coeff n = r • p.coeff n

Tactic:
rcases p with ⟨⟩

Result:
case ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ (r • { toFinsupp := toFinsupp✝ }).coeff n = r • { toFinsupp := toFinsupp✝ }.coeff n

Proof state:
case ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ (r • toFinsupp✝) n = r • toFinsupp✝ n

Tactic:
exact Finsupp.smul_apply _ _ _

Result:
no goals
-- Mathlib/Algebra/Star/Center.lean
theorem Set.union_star_self_comm (hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y)
    (hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y) :
    ∀ x ∈ s ∪ star s, ∀ y ∈ s ∪ star s, y * x = x * y

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y
hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y
⊢ ∀ x ∈ s ∪ star s, ∀ y ∈ s ∪ star s, y * x = x * y

Tactic:
change s ∪ star s ⊆ (s ∪ star s).centralizer

Result:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y
hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y
⊢ s ∪ star s ⊆ (s ∪ star s).centralizer

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y
hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y
⊢ (s ⊆ s.centralizer ∧ s ⊆ star s.centralizer) ∧ s ⊆ star s.centralizer ∧ s ⊆ s.centralizer

Tactic:
exact ⟨⟨hcomm, hcomm_star⟩, ⟨hcomm_star, hcomm⟩⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y
hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y
⊢ s ∪ star s ⊆ (s ∪ star s).centralizer

Tactic:
simp_rw [centralizer_union, ← star_centralizer, union_subset_iff, subset_inter_iff,
  star_subset_star, star_subset]

Result:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y
hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y
⊢ (s ⊆ s.centralizer ∧ s ⊆ star s.centralizer) ∧ s ⊆ star s.centralizer ∧ s ⊆ s.centralizer
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
theorem homEquiv_naturality_right_symm (f : X ⟶ G.obj Y) (g : Y ⟶ Y') :
    (adj.homEquiv X Y').symm (f ≫ G.map g) = (adj.homEquiv X Y).symm f ≫ g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ (adj.homEquiv X Y').symm (f ≫ G.map g) = (adj.homEquiv X Y).symm f ≫ g

Tactic:
rw [Equiv.symm_apply_eq]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = (adj.homEquiv X Y') ((adj.homEquiv X Y).symm f ≫ g)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = (adj.homEquiv X Y') ((adj.homEquiv X Y).symm f ≫ g)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_subset {a b : Set α} (f : α → β) (h : a ⊆ b) : f '' a ⊆ f '' b

Proof state:
α : Type u_1
β : Type u_2
a b : Set α
f : α → β
h : a ⊆ b
⊢ ∀ (x : β), (∃ x_1 ∈ a, f x_1 = x) → ∃ x_1 ∈ b, f x_1 = x

Tactic:
exact fun x => fun ⟨w, h1, h2⟩ => ⟨w, h h1, h2⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a b : Set α
f : α → β
h : a ⊆ b
⊢ f '' a ⊆ f '' b

Tactic:
simp only [subset_def, mem_image]

Result:
α : Type u_1
β : Type u_2
a b : Set α
f : α → β
h : a ⊆ b
⊢ ∀ (x : β), (∃ x_1 ∈ a, f x_1 = x) → ∃ x_1 ∈ b, f x_1 = x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem append_eq_filterMap_iff {f : α → Option β} :
    L₁ ++ L₂ = filterMap f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

Proof state:
α : Type u_1
β : Type u_2
L₁ L₂ : List β
l : List α
f : α → Option β
⊢ L₁ ++ L₂ = filterMap f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

Tactic:
rw [eq_comm, filterMap_eq_append_iff]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem div_opow_log_lt {b : Ordinal} (o : Ordinal) (hb : 1 < b) : o / (b ^ log b o) < b

Proof state:
b o : Ordinal.{u_1}
hb : 1 < b
⊢ o / b ^ log b o < b

Tactic:
rw [div_lt (opow_pos _ (zero_lt_one.trans hb)).ne', ← opow_succ]

Result:
b o : Ordinal.{u_1}
hb : 1 < b
⊢ o < b ^ succ (log b o)

Proof state:
b o : Ordinal.{u_1}
hb : 1 < b
⊢ o < b ^ succ (log b o)

Tactic:
exact lt_opow_succ_log_self hb o

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem mem_of_span_top_of_smul_mem (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ⊤) (x : M)
    (H : ∀ r : s, (r : R) • x ∈ M') : x ∈ M'

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ s ⊆ ↑(comap (LinearMap.toSpanSingleton R M x) M')

Tactic:
exact fun r hr ↦ H ⟨r, hr⟩

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ x ∈ M'

Tactic:
suffices LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M' by
  rw [← LinearMap.toSpanSingleton_one R M x]
  exact this (LinearMap.mem_range_self _ 1)

Result:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M'

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
this : LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M'
⊢ (LinearMap.toSpanSingleton R M x) 1 ∈ M'

Tactic:
exact this (LinearMap.mem_range_self _ 1)

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
this : LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M'
⊢ x ∈ M'

Tactic:
rw [← LinearMap.toSpanSingleton_one R M x]

Result:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
this : LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M'
⊢ (LinearMap.toSpanSingleton R M x) 1 ∈ M'

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M'

Tactic:
rw [LinearMap.range_eq_map, ← hs, map_le_iff_le_comap, Ideal.span, span_le]

Result:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ s ⊆ ↑(comap (LinearMap.toSpanSingleton R M x) M')
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.get_eq [BEq α] [Hashable α] {m : Raw α (fun _ => β)} {a : α} {h : a ∈ m} :
    Raw.Const.get m a h = Raw₀.Const.get
      ⟨m, by change dite .. = true at h; split at h <;> simp_all⟩ a
      (by change dite .. = true at h; split at h <;> simp_all) :=
  rfl

Proof state:
α : Type u
β✝ : α → Type v
γ : Type w
δ : α → Type w
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => β
a : α
h : (if h : 0 < m.buckets.size then Raw₀.contains ⟨m, h⟩ a else false) = true
⊢ 0 < m.buckets.size

Tactic:
split at h <;> simp_all

Result:
no goals

Proof state:
α : Type u
β✝ : α → Type v
γ : Type w
δ : α → Type w
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => β
a : α
h : a ∈ m
⊢ 0 < m.buckets.size

Tactic:
change dite .. = true at h

Result:
α : Type u
β✝ : α → Type v
γ : Type w
δ : α → Type w
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => β
a : α
h : (if h : 0 < m.buckets.size then Raw₀.contains ⟨m, h⟩ a else false) = true
⊢ 0 < m.buckets.size

Proof state:
α : Type u
β✝ : α → Type v
γ : Type w
δ : α → Type w
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => β
a : α
h : a ∈ m
⊢ Raw₀.contains ⟨m, ⋯⟩ a = true

Tactic:
change dite .. = true at h

Result:
α : Type u
β✝ : α → Type v
γ : Type w
δ : α → Type w
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => β
a : α
h : (if h : 0 < m.buckets.size then Raw₀.contains ⟨m, h⟩ a else false) = true
⊢ Raw₀.contains ⟨m, ⋯⟩ a = true

Proof state:
α : Type u
β✝ : α → Type v
γ : Type w
δ : α → Type w
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => β
a : α
h : (if h : 0 < m.buckets.size then Raw₀.contains ⟨m, h⟩ a else false) = true
⊢ Raw₀.contains ⟨m, ⋯⟩ a = true

Tactic:
split at h <;> simp_all

Result:
no goals
-- Mathlib/Topology/LocallyClosed.lean
lemma Topology.IsEmbedding.isLocallyClosed_iff {s : Set X}
    {f : X → Y} (hf : IsEmbedding f) :
    IsLocallyClosed s ↔ ∃ s' : Set Y, IsLocallyClosed s' ∧ s' ∩ range f = f '' s

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsEmbedding f
⊢ IsLocallyClosed s ↔ ∃ s', IsLocallyClosed s' ∧ s' ∩ range f = f '' s

Tactic:
simp_rw [hf.isInducing.isLocallyClosed_iff,
  ← (image_injective.mpr hf.injective).eq_iff, image_preimage_eq_inter_range]

Result:
no goals
-- Mathlib/Order/Interval/Set/SuccOrder.lean
lemma Ici.pred_eq_of_not_isMin
    [PredOrder J] {j : J} {i : Set.Ici j} (hi : ¬ IsMin i) :
    Order.pred i = ⟨Order.pred i.1, by
      rw [← coe_pred_of_not_isMin hi]
      apply Subtype.coe_prop⟩

Proof state:
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ Order.pred i = ⟨Order.pred ↑i, ⋯⟩

Tactic:
ext

Result:
case a
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ ↑(Order.pred i) = ↑⟨Order.pred ↑i, ⋯⟩

Proof state:
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ Order.pred ↑i ∈ Ici j

Tactic:
rw [← coe_pred_of_not_isMin hi]

Result:
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ ↑(Order.pred i) ∈ Ici j

Proof state:
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ ↑(Order.pred i) ∈ Ici j

Tactic:
apply Subtype.coe_prop

Result:
no goals

Proof state:
case a
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ ↑(Order.pred i) = ↑⟨Order.pred ↑i, ⋯⟩

Tactic:
simp only [coe_pred_of_not_isMin hi]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem inv_eq_of_mul_eq_one_right {a : α} (h : ↑u * a = 1) : ↑u⁻¹ = a :=
  calc
    ↑u⁻¹ = ↑u⁻¹ * 1

Proof state:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u * a = 1
⊢ ↑u⁻¹ = ↑u⁻¹ * 1

Tactic:
rw [mul_one]

Result:
no goals

Proof state:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u * a = 1
⊢ ↑u⁻¹ * 1 = a

Tactic:
rw [← h, inv_mul_cancel_left]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_subset_Ico (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Ico a₁ b₁ ⊆ Ico a₂ b₂

Proof state:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂

Tactic:
simpa [← coe_subset] using Set.Ico_subset_Ico ha hb

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem mod_two_eq_zero_iff_testBit_zero : (x % 2 = 0) ↔ x.testBit 0 = false

Proof state:
x : Nat
⊢ x % 2 = 0 ↔ x.testBit 0 = false

Tactic:
cases mod_two_eq_zero_or_one x <;> simp_all

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_zsmul_add [AddCommGroup G] [AddGroup H] [AddConstMapClass F G H a b]
    (f : F) (n : ℤ) (x : G) : f (n • a + x) = f x + n • b

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddCommGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
n : ℤ
x : G
⊢ f (n • a + x) = f x + n • b

Tactic:
rw [add_comm, map_add_zsmul]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem _root_.Wbtw.oangle_sign_eq_of_ne_left {p₁ p₂ p₃ : P} (p₄ : P) (h : Wbtw ℝ p₁ p₂ p₃)
    (hne : p₁ ≠ p₂) : (∡ p₁ p₄ p₂).sign = (∡ p₁ p₄ p₃).sign :=
  haveI hc : Collinear ℝ ({p₁, p₂, p₁, p₃} : Set P)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : Wbtw ℝ p₁ p₂ p₃
hne : p₁ ≠ p₂
⊢ Collinear ℝ {p₁, p₂, p₁, p₃}

Tactic:
simpa [Set.insert_comm p₂] using h.collinear

Result:
no goals
-- Mathlib/Topology/Instances/Rat.lean
theorem Int.dist_cast_rat (x y : ℤ) : dist (x : ℚ) y = dist x y

Proof state:
x y : ℤ
⊢ dist ↑x ↑y = dist x y

Tactic:
rw [← Int.dist_cast_real, ← Rat.dist_cast]

Result:
x y : ℤ
⊢ dist ↑↑x ↑↑y = dist ↑x ↑y

Proof state:
x y : ℤ
⊢ dist ↑↑x ↑↑y = dist ↑x ↑y

Tactic:
congr

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ext_iff_of_sUnion_eq_univ {S : Set (Set α)} (hc : S.Countable) (hs : ⋃₀ S = univ) :
    μ = ν ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s :=
  ext_iff_of_biUnion_eq_univ hc <| by rwa [← sUnion_eq_biUnion]

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S : Set (Set α)
hc : S.Countable
hs : ⋃₀ S = univ
⊢ ⋃ i ∈ S, i = univ

Tactic:
rwa [← sUnion_eq_biUnion]

Result:
no goals
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma ideal_le_comap_ideal {U V : X.affineOpens} (h : U ≤ V) :
    I.ideal V ≤ (I.ideal U).comap (X.presheaf.map (homOfLE h).op).hom

Proof state:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ I.ideal V ≤ Ideal.comap (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal U)

Tactic:
rw [← Ideal.map_le_iff_le_comap, ← I.map_ideal h]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem coe_m_add_one_pos : 0 < (m : ℝ) + 1

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
⊢ 0 < ↑m + 1

Tactic:
positivity

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Bisect.lean
theorem avg_lt_left (h : b < a) : avg a b < a

Proof state:
case h
b a : Nat
h : b < a
⊢ a + b < 2 * a

Tactic:
omega

Result:
no goals

Proof state:
b a : Nat
h : b < a
⊢ a.avg b < a

Tactic:
apply Nat.div_lt_of_lt_mul

Result:
case h
b a : Nat
h : b < a
⊢ a + b < 2 * a
-- Mathlib/Order/KrullDimension.lean
/--
Variant of `height_le_iff` ranging only over those series that end exactly on `a`.
-/
lemma height_le_iff' {a : α} {n : ℕ∞} :
    height a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, p.last = a → p.length ≤ n

Proof state:
case mp
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ (∀ ⦃p : LTSeries α⦄, RelSeries.last p ≤ a → ↑p.length ≤ n) → ∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n

Tactic:
exact fun h p hlast => h (le_of_eq hlast)

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ (∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n) → height a ≤ n

Tactic:
exact height_le

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ height a ≤ n → ∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n

Tactic:
rw [height_le_iff]

Result:
case mp
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ (∀ ⦃p : LTSeries α⦄, RelSeries.last p ≤ a → ↑p.length ≤ n) → ∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ height a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ height a ≤ n → ∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n

case mpr
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ (∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n) → height a ≤ n
-- Mathlib/Combinatorics/Colex.lean
/-- If `s ≤ t` in colex, and all elements in `t` are small, then all elements in `s` are small. -/
lemma forall_le_mono (hst : toColex s ≤ toColex t) (ht : ∀ b ∈ t, b ≤ a) : ∀ b ∈ s, b ≤ a

Proof state:
case pos
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h✝ : b ∈ t
⊢ b ≤ a

Tactic:
exact ht _ ‹_›

Result:
no goals

Proof state:
case neg.intro.intro.intro
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h✝ : b ∉ t
c : α
hct : c ∈ { ofColex := t }.ofColex
hbc : b ≤ c
⊢ b ≤ a

Tactic:
exact hbc.trans <| ht _ hct

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h✝ : b ∉ t
⊢ b ≤ a

Tactic:
obtain ⟨c, hct, -, hbc⟩ := hst hb ‹_›

Result:
case neg.intro.intro.intro
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h✝ : b ∉ t
c : α
hct : c ∈ { ofColex := t }.ofColex
hbc : b ≤ c
⊢ b ≤ a

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
⊢ b ≤ a

Tactic:
by_cases b ∈ t

Result:
case pos
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h✝ : b ∈ t
⊢ b ≤ a

case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h✝ : b ∉ t
⊢ b ≤ a

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
ht : ∀ b ∈ t, b ≤ a
⊢ ∀ b ∈ s, b ≤ a

Tactic:
rintro b hb

Result:
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
⊢ b ≤ a
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffEdist_closure : hausdorffEdist (closure s) (closure t) = hausdorffEdist s t

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEdist (closure s) (closure t) = hausdorffEdist s t

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem tan_oangle_sub_left_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    Real.Angle.tan (o.oangle (x - y) x) = ‖y‖ / ‖x‖

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 - y) x).tan = ‖y‖ / ‖x‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

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 y x = ↑(π / 2)
⊢ ((-o).oangle x (x - y)).tan = ‖y‖ / ‖x‖

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 y x = ↑(π / 2)
⊢ ((-o).oangle x (x - y)).tan = ‖y‖ / ‖x‖

Tactic:
exact (-o).tan_oangle_sub_right_of_oangle_eq_pi_div_two h

Result:
no goals
-- Mathlib/RingTheory/Extension.lean
lemma Cotangent.finite (hP : P.ker.FG) :
    Module.Finite S P.Cotangent

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
hP : P.ker.FG
⊢ (Submodule.map mk ⊤).FG

Tactic:
exact (P.ker.fg_top.mpr hP).map _

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
hP : P.ker.FG
⊢ (Submodule.restrictScalars P.Ring ⊤).FG

Tactic:
rw [Submodule.restrictScalars_top, ← LinearMap.range_eq_top.mpr Extension.Cotangent.mk_surjective,
  ← Submodule.map_top]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
hP : P.ker.FG
⊢ (Submodule.map mk ⊤).FG

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
hP : P.ker.FG
⊢ Module.Finite S P.Cotangent

Tactic:
refine ⟨.of_restrictScalars (R := P.Ring) _ ?_⟩

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
hP : P.ker.FG
⊢ (Submodule.restrictScalars P.Ring ⊤).FG