harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/LiftingProperties/Adjunction.lean
theorem hasLiftingProperty_iff (adj : G ⊣ F) {A B : C} {X Y : D} (i : A ⟶ B) (p : X ⟶ Y) :
    HasLiftingProperty (G.map i) p ↔ HasLiftingProperty i (F.map p)

Proof state:
case mp.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ ⋯.HasLift

Tactic:
infer_instance

Result:
no goals

Proof state:
case mpr.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ ⋯.HasLift

Tactic:
infer_instance

Result:
no goals

Proof state:
case mpr.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ sq.HasLift

Tactic:
rw [← sq.right_adjoint_hasLift_iff adj]

Result:
case mpr.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ ⋯.HasLift

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty (G.map i) p ↔ HasLiftingProperty i (F.map p)

Tactic:
constructor <;> intro <;> constructor <;> intro f g sq

Result:
case mp.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ sq.HasLift

case mpr.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ sq.HasLift

Proof state:
case mp.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ sq.HasLift

Tactic:
rw [← sq.left_adjoint_hasLift_iff adj]

Result:
case mp.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ ⋯.HasLift
-- Mathlib/Data/List/Rotate.lean
theorem zipWith_rotate_one {β : Type*} (f : α → α → β) (x y : α) (l : List α) :
    zipWith f (x :: y :: l) ((x :: y :: l).rotate 1) = f x y :: zipWith f (y :: l) (l ++ [x])

Proof state:
α : Type u
β : Type u_1
f : α → α → β
x y : α
l : List α
⊢ zipWith f (x :: y :: l) ((x :: y :: l).rotate 1) = f x y :: zipWith f (y :: l) (l ++ [x])

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk'_mul_cancel_left (x) (y : S) : f.mk' ((y : M) * x) y = f.toMap x

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ f.mk' (↑y * x) y = f.toMap x

Tactic:
rw [mul_comm, mk'_mul_cancel_right]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem and_le_right : ∀ x y : Bool, (x && y) ≤ y

Proof state:
⊢ ∀ (x y : Bool), (x && y) ≤ y

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
@[to_additive (attr := simp)] lemma monovary_inv_right : Monovary f g⁻¹ ↔ Antivary f g

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : OrderedCommGroup α
inst✝ : OrderedCommGroup β
f : ι → α
g : ι → β
⊢ Monovary f g⁻¹ ↔ Antivary f g

Tactic:
simpa [Monovary, Antivary] using forall_swap

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_eq_of_isRotated {l l' : List α} (hd : Nodup l) (h : l ~r l') :
    formPerm l = formPerm l'

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hd : l.Nodup
h : l ~r l'
⊢ l.formPerm = l'.formPerm

Tactic:
obtain ⟨n, rfl⟩ := h

Result:
case intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
hd : l.Nodup
n : ℕ
⊢ l.formPerm = (l.rotate n).formPerm

Proof state:
case intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
hd : l.Nodup
n : ℕ
⊢ l.formPerm = (l.rotate n).formPerm

Tactic:
exact (formPerm_rotate l hd n).symm

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem _root_.Function.Injective.list_map {f : α → β} (h : Injective f) :
    Injective (map f)
  | [], [], _ => rfl
  | x :: xs, y :: ys, hxy => by
    injection hxy with hxy hxys
    rw [h hxy, h.list_map hxys]

Proof state:
α : Type u
β : Type v
f : α → β
h : Injective f
x : α
xs : List α
y : α
ys : List α
hxy : f x = f y
hxys : map f xs = map f ys
⊢ x :: xs = y :: ys

Tactic:
rw [h hxy, h.list_map hxys]

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
h : Injective f
x : α
xs : List α
y : α
ys : List α
hxy : map f (x :: xs) = map f (y :: ys)
⊢ x :: xs = y :: ys

Tactic:
injection hxy with hxy hxys

Result:
α : Type u
β : Type v
f : α → β
h : Injective f
x : α
xs : List α
y : α
ys : List α
hxy : f x = f y
hxys : map f xs = map f ys
⊢ x :: xs = y :: ys
-- Mathlib/Data/Finsupp/Single.lean
theorem single_eq_of_ne (h : a ≠ a') : (single a b : α →₀ M) a' = 0

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
⊢ (single a b) a' = 0

Tactic:
exact Pi.single_eq_of_ne' h _

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
⊢ (single a b) a' = 0

Tactic:
classical exact Pi.single_eq_of_ne' h _

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_add [AddGroupWithOne α] : ∀ m n, ((m + n : ZNum) : α) = m + n
  | 0, a => by cases a <;> exact (_root_.zero_add _).symm
  | b, 0 => by cases b <;> exact (_root_.add_zero _).symm
  | pos _, pos _ => PosNum.cast_add _ _
  | pos a, neg b => by simpa only [sub_eq_add_neg] using PosNum.cast_sub' (α := α) _ _
  | neg a, pos b =>
    have : (↑b + -↑a : α) = -↑a + ↑b

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
b : ZNum
⊢ ↑(b + 0) = ↑b + ↑0

Tactic:
cases b <;> exact (_root_.add_zero _).symm

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(pos a + neg b) = ↑(pos a) + ↑(neg b)

Tactic:
simpa only [sub_eq_add_neg] using PosNum.cast_sub' (α := α) _ _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑b + -↑a = -↑a + ↑b

Tactic:
rw [← PosNum.cast_to_int a, ← PosNum.cast_to_int b, ← Int.cast_neg, ← Int.cast_add (-a)]

Result:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑↑b + ↑(-↑a) = ↑(-↑a + ↑b)

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ -↑(a + b) = -↑a + -↑b

Tactic:
rw [PosNum.cast_add, neg_eq_iff_eq_neg, neg_add_rev, neg_neg, neg_neg,
    ← PosNum.cast_to_int a, ← PosNum.cast_to_int b, ← Int.cast_add, ← Int.cast_add, add_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a : ZNum
⊢ ↑(0 + a) = ↑0 + ↑a

Tactic:
cases a <;> exact (_root_.zero_add _).symm

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑↑b + ↑(-↑a) = ↑(-↑a + ↑b)

Tactic:
simp [add_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem fold_eq_finRange_foldl {α : Type u} (n : Nat) (f : (i : Nat) → i < n → α → α) (init : α) :
    fold n f init = (List.finRange n).foldl (fun acc ⟨i, h⟩ => f i h acc) init

Proof state:
case succ
α : Type u
init : α
n : Nat
ih :
  ∀ (f : (i : Nat) → i < n → α → α),
    n.fold f init =
      List.foldl
        (fun acc x =>
          match x with
          | ⟨i, h⟩ => f i h acc)
        init (List.finRange n)
f : (i : Nat) → i < n + 1 → α → α
⊢ (n + 1).fold f init =
    List.foldl
      (fun acc x =>
        match x with
        | ⟨i, h⟩ => f i h acc)
      init (List.finRange (n + 1))

Tactic:
simp [ih, List.finRange_succ_last, List.foldl_map]

Result:
no goals

Proof state:
α : Type u
n : Nat
f : (i : Nat) → i < n → α → α
init : α
⊢ n.fold f init =
    List.foldl
      (fun acc x =>
        match x with
        | ⟨i, h⟩ => f i h acc)
      init (List.finRange n)

Tactic:
induction n with
| zero => simp
| succ n ih =>
  simp [ih, List.finRange_succ_last, List.foldl_map]

Result:
no goals

Proof state:
case zero
α : Type u
init : α
f : (i : Nat) → i < 0 → α → α
⊢ fold 0 f init =
    List.foldl
      (fun acc x =>
        match x with
        | ⟨i, h⟩ => f i h acc)
      init (List.finRange 0)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem disjoint_list_sum_left {a : Multiset α} {l : List (Multiset α)} :
    Disjoint l.sum a ↔ ∀ b ∈ l, Disjoint b a

Proof state:
α : Type u_3
a : Multiset α
l : List (Multiset α)
⊢ Disjoint l.sum a ↔ ∀ b ∈ l, Disjoint b a

Tactic:
induction l with
| nil =>
  simp only [zero_disjoint, List.not_mem_nil, IsEmpty.forall_iff, forall_const, List.sum_nil]
| cons b bs ih =>
  simp_rw [List.sum_cons, disjoint_add_left, List.mem_cons, forall_eq_or_imp]
  simp [and_congr_left_iff, ih]

Result:
no goals

Proof state:
case cons
α : Type u_3
a b : Multiset α
bs : List (Multiset α)
ih : Disjoint bs.sum a ↔ ∀ b ∈ bs, Disjoint b a
⊢ Disjoint b a ∧ Disjoint bs.sum a ↔ Disjoint b a ∧ ∀ a_1 ∈ bs, Disjoint a_1 a

Tactic:
simp [and_congr_left_iff, ih]

Result:
no goals

Proof state:
case cons
α : Type u_3
a b : Multiset α
bs : List (Multiset α)
ih : Disjoint bs.sum a ↔ ∀ b ∈ bs, Disjoint b a
⊢ Disjoint (b :: bs).sum a ↔ ∀ b_1 ∈ b :: bs, Disjoint b_1 a

Tactic:
simp_rw [List.sum_cons, disjoint_add_left, List.mem_cons, forall_eq_or_imp]

Result:
case cons
α : Type u_3
a b : Multiset α
bs : List (Multiset α)
ih : Disjoint bs.sum a ↔ ∀ b ∈ bs, Disjoint b a
⊢ Disjoint b a ∧ Disjoint bs.sum a ↔ Disjoint b a ∧ ∀ a_1 ∈ bs, Disjoint a_1 a

Proof state:
case nil
α : Type u_3
a : Multiset α
⊢ Disjoint [].sum a ↔ ∀ b ∈ [], Disjoint b a

Tactic:
simp only [zero_disjoint, List.not_mem_nil, IsEmpty.forall_iff, forall_const, List.sum_nil]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem foldl_attachWith
    (l : Array α) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : β → { x // q x} → β} {b} (w : stop = l.size) :
    (l.attachWith q H).foldl f b 0 stop = l.attach.foldl (fun b ⟨a, h⟩ => f b ⟨a, H _ h⟩) b

Proof state:
case mk
α : Type u_1
β : Type u_2
q : α → Prop
f : β → { x // q x } → β
b : β
l : List α
H : ∀ (a : α), a ∈ { toList := l } → q a
⊢ foldl f b ({ toList := l }.attachWith q H) 0 { toList := l }.size =
    foldl
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
      b { toList := l }.attach

Tactic:
simp [List.foldl_attachWith, List.foldl_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
q : α → Prop
H : ∀ (a : α), a ∈ l → q a
f : β → { x // q x } → β
b : β
⊢ foldl f b (l.attachWith q H) 0 l.size =
    foldl
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
      b l.attach

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
q : α → Prop
f : β → { x // q x } → β
b : β
l : List α
H : ∀ (a : α), a ∈ { toList := l } → q a
⊢ foldl f b ({ toList := l }.attachWith q H) 0 { toList := l }.size =
    foldl
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
      b { toList := l }.attach

Proof state:
α : Type u_1
β : Type u_2
stop : Nat
l : Array α
q : α → Prop
H : ∀ (a : α), a ∈ l → q a
f : β → { x // q x } → β
b : β
w : stop = l.size
⊢ foldl f b (l.attachWith q H) 0 stop =
    foldl
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
      b l.attach

Tactic:
subst w

Result:
α : Type u_1
β : Type u_2
l : Array α
q : α → Prop
H : ∀ (a : α), a ∈ l → q a
f : β → { x // q x } → β
b : β
⊢ foldl f b (l.attachWith q H) 0 l.size =
    foldl
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
      b l.attach
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_reverse {i : Nat} {x : BitVec w} :
    (x.reverse).getMsbD i = x.getLsbD i

Proof state:
w i : Nat
x : BitVec w
⊢ (decide (i < w) && (decide (w - 1 - i < w) && x.getLsbD (w - 1 - (w - 1 - i)))) = x.getLsbD i

Tactic:
by_cases hi : i < w

Result:
case pos
w i : Nat
x : BitVec w
hi : i < w
⊢ (decide (i < w) && (decide (w - 1 - i < w) && x.getLsbD (w - 1 - (w - 1 - i)))) = x.getLsbD i

case neg
w i : Nat
x : BitVec w
hi : ¬i < w
⊢ (decide (i < w) && (decide (w - 1 - i < w) && x.getLsbD (w - 1 - (w - 1 - i)))) = x.getLsbD i

Proof state:
w i : Nat
x : BitVec w
⊢ x.reverse.getMsbD i = x.getLsbD i

Tactic:
simp only [getMsbD_eq_getLsbD, getLsbD_reverse]

Result:
w i : Nat
x : BitVec w
⊢ (decide (i < w) && (decide (w - 1 - i < w) && x.getLsbD (w - 1 - (w - 1 - i)))) = x.getLsbD i

Proof state:
case pos.e_i
w i : Nat
x : BitVec w
hi : i < w
⊢ w - 1 - (w - 1 - i) = i

Tactic:
omega

Result:
no goals

Proof state:
case pos
w i : Nat
x : BitVec w
hi : i < w
⊢ x.getLsbD (w - 1 - (w - 1 - i)) = x.getLsbD i

Tactic:
congr

Result:
case pos.e_i
w i : Nat
x : BitVec w
hi : i < w
⊢ w - 1 - (w - 1 - i) = i

Proof state:
case neg
w i : Nat
x : BitVec w
hi : ¬i < w
⊢ (decide (i < w) && (decide (w - 1 - i < w) && x.getLsbD (w - 1 - (w - 1 - i)))) = x.getLsbD i

Tactic:
simp [hi, show i ≥ w by omega]

Result:
no goals

Proof state:
w i : Nat
x : BitVec w
hi : i < w
⊢ w - 1 - i < w

Tactic:
omega

Result:
no goals

Proof state:
w i : Nat
x : BitVec w
hi : ¬i < w
⊢ i ≥ w

Tactic:
omega

Result:
no goals

Proof state:
case pos
w i : Nat
x : BitVec w
hi : i < w
⊢ (decide (i < w) && (decide (w - 1 - i < w) && x.getLsbD (w - 1 - (w - 1 - i)))) = x.getLsbD i

Tactic:
simp only [hi, decide_true, show w - 1 - i < w by omega, Bool.true_and]

Result:
case pos
w i : Nat
x : BitVec w
hi : i < w
⊢ x.getLsbD (w - 1 - (w - 1 - i)) = x.getLsbD i
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem det_invOf [Invertible A] [Invertible A.det] : (⅟ A).det = ⅟ A.det

Proof state:
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible A.det
⊢ (⅟A).det = ⅟A.det

Tactic:
letI := detInvertibleOfInvertible A

Result:
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible A.det
this : Invertible A.det := A.detInvertibleOfInvertible
⊢ (⅟A).det = ⅟A.det

Proof state:
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible A.det
this : Invertible A.det := A.detInvertibleOfInvertible
⊢ (⅟A).det = ⅟A.det

Tactic:
convert (rfl : _ = ⅟ A.det)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false [BEq α] [EquivBEq α]
    {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α}
    (h': containsKey k l = false) (h : toInsert.contains k = false) :
    getKey? k (insertListIfNewUnit l toInsert) = none

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
h' : containsKey k l = false
h : toInsert.contains k = false
⊢ containsKey k l = false

Tactic:
exact h'

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
h' : containsKey k l = false
h : toInsert.contains k = false
⊢ getKey? k (insertListIfNewUnit l toInsert) = none

Tactic:
rw [getKey?_eq_getEntry?,
  getEntry?_insertListIfNewUnit_of_contains_eq_false h, Option.map_eq_none', getEntry?_eq_none]

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
h' : containsKey k l = false
h : toInsert.contains k = false
⊢ containsKey k l = false
-- Mathlib/Data/Set/Lattice.lean
theorem image2_sInter_subset_right (s : Set α) (T : Set (Set β)) :
    image2 f s (⋂₀ T) ⊆ ⋂ t ∈ T, image2 f s t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
T : Set (Set β)
⊢ image2 f s (⋂ i ∈ T, i) ⊆ ⋂ t ∈ T, image2 f s t

Tactic:
exact image2_iInter₂_subset_right ..

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
T : Set (Set β)
⊢ image2 f s (⋂₀ T) ⊆ ⋂ t ∈ T, image2 f s t

Tactic:
rw [sInter_eq_biInter]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
T : Set (Set β)
⊢ image2 f s (⋂ i ∈ T, i) ⊆ ⋂ t ∈ T, image2 f s t
-- Mathlib/Data/Set/Card.lean
theorem Finite.injOn_of_encard_image_eq (hs : s.Finite) (h : (f '' s).encard = s.encard) :
    InjOn f s

Proof state:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
h : (f '' s).encard = s.encard
hne : Nonempty α
⊢ InjOn f s

Tactic:
rw [← (f.invFunOn_injOn_image s).encard_image] at h

Result:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
hne : Nonempty α
h : (Function.invFunOn f s '' (f '' s)).encard = s.encard
⊢ InjOn f s

Proof state:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
hne : Nonempty α
h : (Function.invFunOn f s '' (f '' s)).encard = s.encard
⊢ Function.invFunOn f s '' (f '' s) = s

Tactic:
exact hs.eq_of_subset_of_encard_le (f.invFunOn_image_image_subset s) h.symm.le

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
hne : Nonempty α
h : (Function.invFunOn f s '' (f '' s)).encard = s.encard
⊢ InjOn f s

Tactic:
rw [injOn_iff_invFunOn_image_image_eq_self]

Result:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
hne : Nonempty α
h : (Function.invFunOn f s '' (f '' s)).encard = s.encard
⊢ Function.invFunOn f s '' (f '' s) = s

Proof state:
case inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
h : (f '' s).encard = s.encard
h' : IsEmpty α
⊢ InjOn f ∅

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
h : (f '' s).encard = s.encard
⊢ InjOn f s

Tactic:
obtain (h' | hne) := isEmpty_or_nonempty α

Result:
case inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
h : (f '' s).encard = s.encard
h' : IsEmpty α
⊢ InjOn f s

case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
h : (f '' s).encard = s.encard
hne : Nonempty α
⊢ InjOn f s

Proof state:
case inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
h : (f '' s).encard = s.encard
h' : IsEmpty α
⊢ InjOn f s

Tactic:
rw [s.eq_empty_of_isEmpty]

Result:
case inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
h : (f '' s).encard = s.encard
h' : IsEmpty α
⊢ InjOn f ∅
-- Mathlib/Algebra/Lie/Submodule.lean
theorem toSubmodule_mk (p : Submodule R M) (h) :
    (({ p with lie_mem := h } : LieSubmodule R L M) : Submodule R M) = p

Proof state:
case mk
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
toAddSubmonoid✝ : AddSubmonoid M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h :
  ∀ {x : L} {m : M},
    m ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier →
      ⁅x, m⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier
⊢ ↑{ toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝, lie_mem := h } =
    { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ p.carrier → ⁅x, m⁆ ∈ p.carrier
⊢ ↑{ toSubmodule := p, lie_mem := h } = p

Tactic:
cases p

Result:
case mk
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
toAddSubmonoid✝ : AddSubmonoid M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h :
  ∀ {x : L} {m : M},
    m ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier →
      ⁅x, m⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier
⊢ ↑{ toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝, lie_mem := h } =
    { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem continuousAt_inv_infDist_pt (h : x ∉ closure s) :
    ContinuousAt (fun x ↦ (infDist x s)⁻¹) x

Proof state:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure s
hs : s.Nonempty
⊢ infDist x s ≠ 0

Tactic:
rwa [Ne, ← mem_closure_iff_infDist_zero hs]

Result:
no goals

Proof state:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure s
hs : s.Nonempty
⊢ ContinuousAt (fun x => (infDist x s)⁻¹) x

Tactic:
refine (continuous_infDist_pt s).continuousAt.inv₀ ?_

Result:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure s
hs : s.Nonempty
⊢ infDist x s ≠ 0

Proof state:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
x : α
h : x ∉ closure ∅
⊢ ContinuousAt (fun x => (infDist x ∅)⁻¹) x

Tactic:
simp only [infDist_empty, continuousAt_const]

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure s
⊢ ContinuousAt (fun x => (infDist x s)⁻¹) x

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs)

Result:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
x : α
h : x ∉ closure ∅
⊢ ContinuousAt (fun x => (infDist x ∅)⁻¹) x

case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure s
hs : s.Nonempty
⊢ ContinuousAt (fun x => (infDist x s)⁻¹) x
-- Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
theorem top_prod (s : NonUnitalSubsemiring S) :
    (⊤ : NonUnitalSubsemiring R).prod s = s.comap (NonUnitalRingHom.snd R S) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_snd]

Proof state:
R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
s : NonUnitalSubsemiring S
x : R × S
⊢ x ∈ ⊤.prod s ↔ x ∈ comap (NonUnitalRingHom.snd R S) s

Tactic:
simp [mem_prod, MonoidHom.coe_snd]

Result:
no goals