harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
@[reassoc (attr := simp)]
lemma stalkMap_hom_inv (e : X ≅ Y) (y : Y) :
    e.hom.stalkMap (e.inv.base y) ≫ e.inv.stalkMap y =
      Y.presheaf.stalkSpecializes (specializes_of_eq <| by simp)

Proof state:
X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (𝟙 Y) y = Y.presheaf.stalkSpecializes ⋯

Tactic:
simp

Result:
no goals

Proof state:
X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ Hom.stalkMap e.hom ((ConcreteCategory.hom e.inv.base) y) ≫ Hom.stalkMap e.inv y = Y.presheaf.stalkSpecializes ⋯

Tactic:
rw [← stalkMap_comp, LocallyRingedSpace.stalkMap_congr_hom (e.inv ≫ e.hom) (𝟙 _) (by simp)]

Result:
X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (𝟙 Y) y = Y.presheaf.stalkSpecializes ⋯

Proof state:
X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ e.inv ≫ e.hom = 𝟙 Y

Tactic:
simp

Result:
no goals

Proof state:
X✝ X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
e : X ≅ Y
y : ↑Y.toTopCat
⊢ y = (ConcreteCategory.hom e.hom.base) ((ConcreteCategory.hom e.inv.base) y)

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/SubMulAction.lean
theorem smul_of_tower_mem (s : S) {x : M} (h : x ∈ p) : s • x ∈ p

Proof state:
S : Type u'
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
p : SubMulAction R M
s : S
x : M
h : x ∈ p
⊢ (s • 1) • x ∈ p

Tactic:
exact p.smul_mem _ h

Result:
no goals

Proof state:
S : Type u'
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
p : SubMulAction R M
s : S
x : M
h : x ∈ p
⊢ s • x ∈ p

Tactic:
rw [← one_smul R x, ← smul_assoc]

Result:
S : Type u'
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
p : SubMulAction R M
s : S
x : M
h : x ∈ p
⊢ (s • 1) • x ∈ p
-- Mathlib/Order/RelSeries.lean
lemma smash_castAdd {p q : RelSeries r} (connect : p.last = q.head) (i : Fin p.length) :
    p.smash q connect (Fin.castSucc <| i.castAdd q.length) = p (Fin.castSucc i)

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
⊢ { length := p.length + q.length,
          toFun := fun i => if H : ↑i < p.length then p.toFun ⟨↑i, ⋯⟩ else q.toFun ⟨↑i - p.length, ⋯⟩, step := ⋯ }.toFun
      (Fin.castAdd q.length i).castSucc =
    p.toFun i.castSucc

Tactic:
dsimp

Result:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
⊢ (if H : ↑i < p.length then p.toFun ⟨↑i, ⋯⟩ else q.toFun ⟨↑i - p.length, ⋯⟩) = p.toFun i.castSucc

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
⊢ (if H : ↑i < p.length then p.toFun ⟨↑i, ⋯⟩ else q.toFun ⟨↑i - p.length, ⋯⟩) = p.toFun i.castSucc

Tactic:
rw [dif_pos i.2]

Result:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
⊢ p.toFun ⟨↑i, ⋯⟩ = p.toFun i.castSucc

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
⊢ p.toFun ⟨↑i, ⋯⟩ = p.toFun i.castSucc

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
⊢ (p.smash q connect).toFun (Fin.castAdd q.length i).castSucc = p.toFun i.castSucc

Tactic:
unfold smash

Result:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
⊢ { length := p.length + q.length,
          toFun := fun i => if H : ↑i < p.length then p.toFun ⟨↑i, ⋯⟩ else q.toFun ⟨↑i - p.length, ⋯⟩, step := ⋯ }.toFun
      (Fin.castAdd q.length i).castSucc =
    p.toFun i.castSucc
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem archimedean_iff_int_lt : Archimedean α ↔ ∀ x : α, ∃ n : ℤ, x < n :=
  ⟨@exists_int_gt α _, by
    rw [archimedean_iff_nat_lt]
    intro h x
    obtain ⟨n, h⟩ := h x
    refine ⟨n.toNat, h.trans_le ?_⟩
    exact mod_cast Int.self_le_toNat _⟩

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
⊢ (∀ (x : α), ∃ n, x < ↑n) → Archimedean α

Tactic:
rw [archimedean_iff_nat_lt]

Result:
α : Type u_1
inst✝ : LinearOrderedField α
⊢ (∀ (x : α), ∃ n, x < ↑n) → ∀ (x : α), ∃ n, x < ↑n

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
⊢ (∀ (x : α), ∃ n, x < ↑n) → ∀ (x : α), ∃ n, x < ↑n

Tactic:
intro h x

Result:
α : Type u_1
inst✝ : LinearOrderedField α
h : ∀ (x : α), ∃ n, x < ↑n
x : α
⊢ ∃ n, x < ↑n

Proof state:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
h✝ : ∀ (x : α), ∃ n, x < ↑n
x : α
n : ℤ
h : x < ↑n
⊢ ∃ n, x < ↑n

Tactic:
refine ⟨n.toNat, h.trans_le ?_⟩

Result:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
h✝ : ∀ (x : α), ∃ n, x < ↑n
x : α
n : ℤ
h : x < ↑n
⊢ ↑n ≤ ↑n.toNat

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
h : ∀ (x : α), ∃ n, x < ↑n
x : α
⊢ ∃ n, x < ↑n

Tactic:
obtain ⟨n, h⟩ := h x

Result:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
h✝ : ∀ (x : α), ∃ n, x < ↑n
x : α
n : ℤ
h : x < ↑n
⊢ ∃ n, x < ↑n

Proof state:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
h✝ : ∀ (x : α), ∃ n, x < ↑n
x : α
n : ℤ
h : x < ↑n
⊢ ↑n ≤ ↑n.toNat

Tactic:
exact mod_cast Int.self_le_toNat _

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem IsAdjointPair.smul (c : R) (h : IsAdjointPair B B' f g) :
    IsAdjointPair B B' (c • f) (c • g) := fun _ _ ↦ by
  simp [h _]

Proof state:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B : M →ₗ[R] M →ₗ[R] M₂
B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂
f : M → M₁
g : M₁ → M
c : R
h : B.IsAdjointPair B' f g
x✝¹ : M
x✝ : M₁
⊢ (B' ((c • f) x✝¹)) x✝ = (B x✝¹) ((c • g) x✝)

Tactic:
simp [h _]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean
theorem Ioi_mul_Ici_subset' [LocallyFiniteOrderTop α] (a b : α) : Ioi a * Ici b ⊆ Ioi (a * b) :=
  Finset.coe_subset.mp <| by simpa using Set.Ioi_mul_Ici_subset' _ _

Proof state:
α : Type u_1
inst✝⁵ : Mul α
inst✝⁴ : PartialOrder α
inst✝³ : DecidableEq α
inst✝² : MulLeftStrictMono α
inst✝¹ : MulRightStrictMono α
inst✝ : LocallyFiniteOrderTop α
a b : α
⊢ ↑(Ioi a * Ici b) ⊆ ↑(Ioi (a * b))

Tactic:
simpa using Set.Ioi_mul_Ici_subset' _ _

Result:
no goals
-- Mathlib/Order/Sublattice.lean
@[simp] lemma prod_eq_top [Nonempty α] [Nonempty β] {M : Sublattice β} :
    L.prod M = ⊤ ↔ L = ⊤ ∧ M = ⊤

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : Lattice α
inst✝² : Lattice β
L : Sublattice α
inst✝¹ : Nonempty α
inst✝ : Nonempty β
M : Sublattice β
⊢ L.prod M = ⊤ ↔ L = ⊤ ∧ M = ⊤

Tactic:
simpa only [← coe_inj] using Set.prod_eq_univ

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
theorem of_h_eq_intFractPair_seq1_fst_b : (of v).h = (IntFractPair.seq1 v).fst.b

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ (of v).h = ↑(IntFractPair.seq1 v).1.b

Tactic:
cases aux_seq_eq : IntFractPair.seq1 v

Result:
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
fst✝ : IntFractPair K
snd✝ : Stream'.Seq (IntFractPair K)
aux_seq_eq : IntFractPair.seq1 v = (fst✝, snd✝)
⊢ (of v).h = ↑(fst✝, snd✝).1.b

Proof state:
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
fst✝ : IntFractPair K
snd✝ : Stream'.Seq (IntFractPair K)
aux_seq_eq : IntFractPair.seq1 v = (fst✝, snd✝)
⊢ (of v).h = ↑(fst✝, snd✝).1.b

Tactic:
simp [of, aux_seq_eq]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem idealFactorsFunOfQuotHom_id :
    idealFactorsFunOfQuotHom (RingHom.id (A ⧸ J)).surjective = OrderHom.id :=
  OrderHom.ext _ _
    (funext fun X => by
      simp only [idealFactorsFunOfQuotHom, map_id, OrderHom.coe_mk, OrderHom.id_coe, id,
        comap_map_of_surjective (Ideal.Quotient.mk J) Ideal.Quotient.mk_surjective, ←
        RingHom.ker_eq_comap_bot (Ideal.Quotient.mk J), mk_ker,
        sup_eq_left.mpr (dvd_iff_le.mp X.prop), Subtype.coe_eta])

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
J : Ideal A
X : { p // p ∣ J }
⊢ (idealFactorsFunOfQuotHom ⋯) X = OrderHom.id X

Tactic:
simp only [idealFactorsFunOfQuotHom, map_id, OrderHom.coe_mk, OrderHom.id_coe, id,
  comap_map_of_surjective (Ideal.Quotient.mk J) Ideal.Quotient.mk_surjective, ←
  RingHom.ker_eq_comap_bot (Ideal.Quotient.mk J), mk_ker,
  sup_eq_left.mpr (dvd_iff_le.mp X.prop), Subtype.coe_eta]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Basic.lean
lemma smul_naturality {M N : ModuleCat.{v} R} (f : M ⟶ N) (r : R) :
    (forget₂ (ModuleCat R) AddCommGrp).map f ≫ N.smul r =
      M.smul r ≫ (forget₂ (ModuleCat R) AddCommGrp).map f

Proof state:
case hf.h
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
r : R
x : ↑((forget₂ (ModuleCat R) AddCommGrp).obj M)
⊢ (AddCommGrp.Hom.hom ((forget₂ (ModuleCat R) AddCommGrp).map f ≫ N.smul r)) x =
    (AddCommGrp.Hom.hom (M.smul r ≫ (forget₂ (ModuleCat R) AddCommGrp).map f)) x

Tactic:
exact (f.hom.map_smul r x).symm

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
r : R
⊢ (forget₂ (ModuleCat R) AddCommGrp).map f ≫ N.smul r = M.smul r ≫ (forget₂ (ModuleCat R) AddCommGrp).map f

Tactic:
ext x

Result:
case hf.h
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
r : R
x : ↑((forget₂ (ModuleCat R) AddCommGrp).obj M)
⊢ (AddCommGrp.Hom.hom ((forget₂ (ModuleCat R) AddCommGrp).map f ≫ N.smul r)) x =
    (AddCommGrp.Hom.hom (M.smul r ≫ (forget₂ (ModuleCat R) AddCommGrp).map f)) x
-- Mathlib/Data/Seq/Computation.lean
theorem liftRel_map {δ} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : Computation α}
    {s2 : Computation β} {f1 : α → γ} {f2 : β → δ} (h1 : LiftRel R s1 s2)
    (h2 : ∀ {a b}, R a b → S (f1 a) (f2 b)) : LiftRel S (map f1 s1) (map f2 s2)

Proof state:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
⊢ ∀ {a : α} {b : β}, R a b → LiftRel S ((pure ∘ f1) a) ((pure ∘ f2) b)

Tactic:
simp only [comp_apply, liftRel_pure_right]

Result:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
⊢ ∀ {a : α} {b : β}, R a b → ∃ a_2, a_2 ∈ pure (f1 a) ∧ S a_2 (f2 b)

Proof state:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
⊢ LiftRel S (map f1 s1) (map f2 s2)

Tactic:
rw [← bind_pure, ← bind_pure]

Result:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
⊢ LiftRel S (s1.bind (pure ∘ f1)) (s2.bind (pure ∘ f2))

Proof state:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
⊢ LiftRel S (s1.bind (pure ∘ f1)) (s2.bind (pure ∘ f2))

Tactic:
apply liftRel_bind _ _ h1

Result:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
⊢ ∀ {a : α} {b : β}, R a b → LiftRel S ((pure ∘ f1) a) ((pure ∘ f2) b)

Proof state:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
⊢ ∀ {a : α} {b : β}, R a b → ∃ a_2, a_2 ∈ pure (f1 a) ∧ S a_2 (f2 b)

Tactic:
intros a b h

Result:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
a : α
b : β
h : R a b
⊢ ∃ a_1, a_1 ∈ pure (f1 a) ∧ S a_1 (f2 b)

Proof state:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
a : α
b : β
h : R a b
⊢ ∃ a_1, a_1 ∈ pure (f1 a) ∧ S a_1 (f2 b)

Tactic:
exact ⟨f1 a, ⟨ret_mem _, @h2 a b h⟩⟩

Result:
no goals
-- Mathlib/Data/Finsupp/Multiset.lean
theorem toFinsupp_inter (s t : Multiset α) : toFinsupp (s ∩ t) = toFinsupp s ⊓ toFinsupp t

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a✝ : α
⊢ (toFinsupp (s ∩ t)) a✝ = (toFinsupp s ⊓ toFinsupp t) a✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toFinsupp (s ∩ t) = toFinsupp s ⊓ toFinsupp t

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a✝ : α
⊢ (toFinsupp (s ∩ t)) a✝ = (toFinsupp s ⊓ toFinsupp t) a✝
-- Mathlib/MeasureTheory/SetAlgebra.lean
theorem generateSetAlgebra_mono {ℬ : Set (Set α)} (h : 𝒜 ⊆ ℬ) :
    generateSetAlgebra 𝒜 ⊆ generateSetAlgebra ℬ

Proof state:
case union
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s t u : Set α
hs✝ : generateSetAlgebra 𝒜 t
ht✝ : generateSetAlgebra 𝒜 u
t_mem : t ∈ generateSetAlgebra ℬ
u_mem : u ∈ generateSetAlgebra ℬ
⊢ t ∪ u ∈ generateSetAlgebra ℬ

Tactic:
exact isSetAlgebra_generateSetAlgebra.union_mem t_mem u_mem

Result:
no goals

Proof state:
case base
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s t : Set α
t_mem : t ∈ 𝒜
⊢ t ∈ generateSetAlgebra ℬ

Tactic:
exact self_subset_generateSetAlgebra (h t_mem)

Result:
no goals

Proof state:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s : Set α
hs : s ∈ generateSetAlgebra 𝒜
⊢ s ∈ generateSetAlgebra ℬ

Tactic:
induction hs with
| base t t_mem => exact self_subset_generateSetAlgebra (h t_mem)
| empty => exact isSetAlgebra_generateSetAlgebra.empty_mem
| compl t _ t_mem => exact isSetAlgebra_generateSetAlgebra.compl_mem t_mem
| union t u _ _ t_mem u_mem => exact isSetAlgebra_generateSetAlgebra.union_mem t_mem u_mem

Result:
no goals

Proof state:
case empty
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s : Set α
⊢ ∅ ∈ generateSetAlgebra ℬ

Tactic:
exact isSetAlgebra_generateSetAlgebra.empty_mem

Result:
no goals

Proof state:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
⊢ generateSetAlgebra 𝒜 ⊆ generateSetAlgebra ℬ

Tactic:
intro s hs

Result:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s : Set α
hs : s ∈ generateSetAlgebra 𝒜
⊢ s ∈ generateSetAlgebra ℬ

Proof state:
case compl
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s t : Set α
hs✝ : generateSetAlgebra 𝒜 t
t_mem : t ∈ generateSetAlgebra ℬ
⊢ tᶜ ∈ generateSetAlgebra ℬ

Tactic:
exact isSetAlgebra_generateSetAlgebra.compl_mem t_mem

Result:
no goals
-- Mathlib/Order/MinMax.lean
theorem min_cases (a b : α) : min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a

Proof state:
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ a ⊓ b = a ∧ a ≤ b ∨ a ⊓ b = b ∧ b < a

Tactic:
by_cases h : a ≤ b

Result:
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ a ⊓ b = a ∧ a ≤ b ∨ a ⊓ b = b ∧ b < a

case neg
α : Type u
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ a ⊓ b = a ∧ a ≤ b ∨ a ⊓ b = b ∧ b < a

Proof state:
case pos.h
α : Type u
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ a ⊓ b = a ∧ a ≤ b

Tactic:
exact ⟨min_eq_left h, h⟩

Result:
no goals

Proof state:
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ a ⊓ b = a ∧ a ≤ b ∨ a ⊓ b = b ∧ b < a

Tactic:
left

Result:
case pos.h
α : Type u
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ a ⊓ b = a ∧ a ≤ b

Proof state:
case neg
α : Type u
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ a ⊓ b = a ∧ a ≤ b ∨ a ⊓ b = b ∧ b < a

Tactic:
right

Result:
case neg.h
α : Type u
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ a ⊓ b = b ∧ b < a

Proof state:
case neg.h
α : Type u
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ a ⊓ b = b ∧ b < a

Tactic:
exact ⟨min_eq_right (le_of_lt (not_le.mp h)), not_le.mp h⟩

Result:
no goals
-- Mathlib/Topology/PartitionOfUnity.lean
theorem toPOUFun_eq_mul_prod (i : ι) (x : X) (t : Finset ι)
    (ht : ∀ j, WellOrderingRel j i → f j x ≠ 0 → j ∈ t) :
    f.toPOUFun i x = f i x * ∏ j ∈ t.filter fun j => WellOrderingRel j i, (1 - f j x)

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t
j : ι
hj : ¬(f j) x = 0
⊢ WellOrderingRel j i → j ∈ t

Tactic:
exact flip (ht j) hj

Result:
no goals

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t
⊢ f.toPOUFun i x = (f i) x * ∏ j ∈ Finset.filter (fun j => WellOrderingRel j i) t, (1 - (f j) x)

Tactic:
refine congr_arg _ (finprod_cond_eq_prod_of_cond_iff _ fun {j} hj => ?_)

Result:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t
j : ι
hj : 1 - (f j) x ≠ 1
⊢ WellOrderingRel j i ↔ j ∈ Finset.filter (fun j => WellOrderingRel j i) t

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t
j : ι
hj : ¬(f j) x = 0
⊢ WellOrderingRel j i ↔ j ∈ Finset.filter (fun j => WellOrderingRel j i) t

Tactic:
rw [Finset.mem_filter, Iff.comm, and_iff_right_iff_imp]

Result:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t
j : ι
hj : ¬(f j) x = 0
⊢ WellOrderingRel j i → j ∈ t

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t
j : ι
hj : 1 - (f j) x ≠ 1
⊢ WellOrderingRel j i ↔ j ∈ Finset.filter (fun j => WellOrderingRel j i) t

Tactic:
rw [Ne, sub_eq_self] at hj

Result:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t
j : ι
hj : ¬(f j) x = 0
⊢ WellOrderingRel j i ↔ j ∈ Finset.filter (fun j => WellOrderingRel j i) t
-- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
/-- As `x → 0`, we have `f x = x ^ (-P.k) • constant` up to a rapidly decaying error. -/
lemma hf_zero (P : WeakFEPair E) (r : ℝ) :
    (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) =O[𝓝[>] 0] (· ^ r)

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
x : ℝ
hC' : x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖

Tactic:
specialize hC' hx

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_filterMap (f : α → Option β) (p : β → Bool) (l : Array α) :
    filter p (filterMap f l) = filterMap (fun x => (f x).filter p) l

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
toList✝ : List α
⊢ filter p (filterMap f { toList := toList✝ }) = filterMap (fun x => Option.filter p (f x)) { toList := toList✝ }

Tactic:
simp [List.filter_filterMap]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
l : Array α
⊢ filter p (filterMap f l) = filterMap (fun x => Option.filter p (f x)) l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
toList✝ : List α
⊢ filter p (filterMap f { toList := toList✝ }) = filterMap (fun x => Option.filter p (f x)) { toList := toList✝ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem pmap_eq_map (p : α → Prop) (f : α → β) (l : List α) (H) :
    @pmap _ _ p (fun a _ => f a) l H = map f l

Proof state:
case nil
α : Type u_1
β : Type u_2
p : α → Prop
f : α → β
H : ∀ (a : α), a ∈ [] → p a
⊢ pmap (fun a x => f a) [] H = map f []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
p : α → Prop
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (H : ∀ (a : α), a ∈ tail✝ → p a), pmap (fun a x => f a) tail✝ H = map f tail✝
H : ∀ (a : α), a ∈ head✝ :: tail✝ → p a
⊢ pmap (fun a x => f a) (head✝ :: tail✝) H = map f (head✝ :: tail✝)

Tactic:
simp only [*, pmap, map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : α → β
l : List α
H : ∀ (a : α), a ∈ l → p a
⊢ pmap (fun a x => f a) l H = map f l

Tactic:
induction l

Result:
case nil
α : Type u_1
β : Type u_2
p : α → Prop
f : α → β
H : ∀ (a : α), a ∈ [] → p a
⊢ pmap (fun a x => f a) [] H = map f []

case cons
α : Type u_1
β : Type u_2
p : α → Prop
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (H : ∀ (a : α), a ∈ tail✝ → p a), pmap (fun a x => f a) tail✝ H = map f tail✝
H : ∀ (a : α), a ∈ head✝ :: tail✝ → p a
⊢ pmap (fun a x => f a) (head✝ :: tail✝) H = map f (head✝ :: tail✝)
-- Mathlib/CategoryTheory/Shift/CommShift.lean
@[simp]
lemma isoZero'_eq_isoZero : isoZero' F A 0 rfl = isoZero F A

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_7, u_1} C
inst✝³ : Category.{u_6, u_2} D
F : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
⊢ isoZero' F A 0 ⋯ = isoZero F A

Tactic:
ext

Result:
case w.w.h
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_7, u_1} C
inst✝³ : Category.{u_6, u_2} D
F : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
x✝ : C
⊢ (isoZero' F A 0 ⋯).hom.app x✝ = (isoZero F A).hom.app x✝

Proof state:
case w.w.h
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_7, u_1} C
inst✝³ : Category.{u_6, u_2} D
F : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
x✝ : C
⊢ (isoZero' F A 0 ⋯).hom.app x✝ = (isoZero F A).hom.app x✝

Tactic:
simp [isoZero', shiftFunctorZero']

Result:
no goals