harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Monotone/MonovaryOrder.lean
lemma antivaryOn_iff_exists_monotoneOn_antitoneOn :
    AntivaryOn f g s ↔ ∃ (_ : LinearOrder ι), MonotoneOn f s ∧ AntitoneOn g s

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
⊢ AntivaryOn f g s ↔ ∃ x, MonotoneOn f s ∧ AntitoneOn g s

Tactic:
simp_rw [← monovaryOn_toDual_right, monovaryOn_iff_exists_monotoneOn, monotoneOn_toDual_comp_iff]

Result:
no goals
-- Mathlib/Topology/Category/Compactum.lean
theorem str_hom_commute (X Y : Compactum) (f : X ⟶ Y) (xs : Ultrafilter X) :
    f (X.str xs) = Y.str (map f xs)

Proof state:
X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ (β.map f.f ≫ Y.a) xs = Y.str (Ultrafilter.map (⇑(ConcreteCategory.hom f)) xs)

Tactic:
rfl

Result:
no goals

Proof state:
X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ (X.a ≫ f.f) xs = Y.str (Ultrafilter.map (⇑(ConcreteCategory.hom f)) xs)

Tactic:
rw [← f.h]

Result:
X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ (β.map f.f ≫ Y.a) xs = Y.str (Ultrafilter.map (⇑(ConcreteCategory.hom f)) xs)

Proof state:
X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ (ConcreteCategory.hom f) (X.str xs) = Y.str (Ultrafilter.map (⇑(ConcreteCategory.hom f)) xs)

Tactic:
change (X.a ≫ f.f) _ = _

Result:
X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ (X.a ≫ f.f) xs = Y.str (Ultrafilter.map (⇑(ConcreteCategory.hom f)) xs)
-- Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
@[reassoc (attr := simp)]
lemma ranCounit_app_whiskerLeft_ranAdjunction_unit_app (G : D ⥤ H) :
    whiskerLeft L ((L.ranAdjunction H).unit.app G) ≫ L.ranCounit.app (L ⋙ G) = 𝟙 (L ⋙ G)

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{u_5, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
G : D ⥤ H
⊢ whiskerLeft L ((L.ranAdjunction H).unit.app G) ≫ L.ranCounit.app (L ⋙ G) = 𝟙 (L ⋙ G)

Tactic:
simp [ranAdjunction_unit_app]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Countable.lean
theorem sequentialFunctor_final_aux (j : J) : ∃ (n : ℕ), j ≤ sequentialFunctor_obj J n

Proof state:
case intro
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
j : J
m : ℕ
h : ⋯.choose m = j
⊢ j ≤ sequentialFunctor_obj J (m + 1)

Tactic:
simpa only [h] using leOfHom (IsFilteredOrEmpty.cocone_objs ((exists_surjective_nat _).choose m)
  (sequentialFunctor_obj J m)).choose_spec.choose

Result:
no goals

Proof state:
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
j : J
⊢ ∃ n, j ≤ sequentialFunctor_obj J n

Tactic:
obtain ⟨m, h⟩ := (exists_surjective_nat _).choose_spec j

Result:
case intro
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
j : J
m : ℕ
h : ⋯.choose m = j
⊢ ∃ n, j ≤ sequentialFunctor_obj J n

Proof state:
case intro
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
j : J
m : ℕ
h : ⋯.choose m = j
⊢ ∃ n, j ≤ sequentialFunctor_obj J n

Tactic:
refine ⟨m + 1, ?_⟩

Result:
case intro
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
j : J
m : ℕ
h : ⋯.choose m = j
⊢ j ≤ sequentialFunctor_obj J (m + 1)
-- Mathlib/Topology/MetricSpace/Pseudo/Real.lean
lemma dist_le_of_mem_uIcc {x y x' y' : ℝ} (hx : x ∈ uIcc x' y') (hy : y ∈ uIcc x' y') :
    dist x y ≤ dist x' y' :=
  abs_sub_le_of_uIcc_subset_uIcc <| uIcc_subset_uIcc (by rwa [uIcc_comm]) (by rwa [uIcc_comm])

Proof state:
x y x' y' : ℝ
hx : x ∈ uIcc x' y'
hy : y ∈ uIcc x' y'
⊢ y ∈ uIcc y' x'

Tactic:
rwa [uIcc_comm]

Result:
no goals

Proof state:
x y x' y' : ℝ
hx : x ∈ uIcc x' y'
hy : y ∈ uIcc x' y'
⊢ x ∈ uIcc y' x'

Tactic:
rwa [uIcc_comm]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
lemma comp_v {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ : Cochain G K n₂) (h : n₁ + n₂ = n₁₂)
    (p₁ p₂ p₃ : ℤ) (h₁ : p₁ + n₁ = p₂) (h₂ : p₂ + n₂ = p₃) :
    (z₁.comp z₂ h).v p₁ p₃ (by rw [← h₂, ← h₁, ← h, add_assoc]) =
      z₁.v p₁ p₂ h₁ ≫ z₂.v p₂ p₃ h₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p₁ p₃ : ℤ
h₂ : p₁ + n₁ + n₂ = p₃
⊢ (z₁.comp z₂ h).v p₁ p₃ ⋯ = z₁.v p₁ (p₁ + n₁) ⋯ ≫ z₂.v (p₁ + n₁) p₃ h₂

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p₁ p₂ p₃ : ℤ
h₁ : p₁ + n₁ = p₂
h₂ : p₂ + n₂ = p₃
⊢ p₁ + n₁₂ = p₃

Tactic:
rw [← h₂, ← h₁, ← h, add_assoc]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p₁ p₂ p₃ : ℤ
h₁ : p₁ + n₁ = p₂
h₂ : p₂ + n₂ = p₃
⊢ (z₁.comp z₂ h).v p₁ p₃ ⋯ = z₁.v p₁ p₂ h₁ ≫ z₂.v p₂ p₃ h₂

Tactic:
subst h₁

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p₁ p₃ : ℤ
h₂ : p₁ + n₁ + n₂ = p₃
⊢ (z₁.comp z₂ h).v p₁ p₃ ⋯ = z₁.v p₁ (p₁ + n₁) ⋯ ≫ z₂.v (p₁ + n₁) p₃ h₂
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
@[simp]
lemma leftHomologyMap_nullHomotopic [S₁.HasLeftHomology] [S₂.HasLeftHomology]
    (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : h₀ ≫ S₂.f = 0)
    (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : S₁.g ≫ h₃ = 0) :
    leftHomologyMap (nullHomotopic _ _ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ leftHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

Tactic:
apply leftHomologyMap'_nullHomotopic

Result:
no goals
-- Mathlib/Data/Nat/Squarefree.lean
theorem sum_divisors_filter_squarefree {n : ℕ} (h0 : n ≠ 0) {α : Type*} [AddCommMonoid α]
    {f : ℕ → α} :
    ∑ d ∈ n.divisors with Squarefree d, f d =
      ∑ i ∈ (UniqueFactorizationMonoid.normalizedFactors n).toFinset.powerset, f i.val.prod

Proof state:
n : ℕ
h0 : n ≠ 0
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ → α
⊢ ∑ d ∈ filter (fun d => Squarefree d) n.divisors, f d = ∑ i ∈ (normalizedFactors n).toFinset.powerset, f i.val.prod

Tactic:
rw [Finset.sum_eq_multiset_sum, divisors_filter_squarefree h0, Multiset.map_map,
  Finset.sum_eq_multiset_sum]

Result:
n : ℕ
h0 : n ≠ 0
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ → α
⊢ (Multiset.map (f ∘ fun x => x.val.prod) (normalizedFactors n).toFinset.powerset.val).sum =
    (Multiset.map (fun i => f i.val.prod) (normalizedFactors n).toFinset.powerset.val).sum

Proof state:
n : ℕ
h0 : n ≠ 0
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ → α
⊢ (Multiset.map (f ∘ fun x => x.val.prod) (normalizedFactors n).toFinset.powerset.val).sum =
    (Multiset.map (fun i => f i.val.prod) (normalizedFactors n).toFinset.powerset.val).sum

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem whiskerRight_id_symm {f g : a ⟶ b} (η : f ⟶ g) : η = (ρ_ f).inv ≫ η ▷ 𝟙 b ≫ (ρ_ g).hom

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η = (ρ_ f).inv ≫ η ▷ 𝟙 b ≫ (ρ_ g).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma uIoo_self : uIoo a a = ∅

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ uIoo a a = ∅

Tactic:
simp [uIoo]

Result:
no goals
-- Mathlib/Data/List/AList.lean
theorem perm_insert {a} {b : β a} {s₁ s₂ : AList β} (p : s₁.entries ~ s₂.entries) :
    (insert a b s₁).entries ~ (insert a b s₂).entries

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
p : s₁.entries ~ s₂.entries
⊢ (insert a b s₁).entries ~ (insert a b s₂).entries

Tactic:
simp only [entries_insert]

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
p : s₁.entries ~ s₂.entries
⊢ ⟨a, b⟩ :: kerase a s₁.entries ~ ⟨a, b⟩ :: kerase a s₂.entries

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
p : s₁.entries ~ s₂.entries
⊢ ⟨a, b⟩ :: kerase a s₁.entries ~ ⟨a, b⟩ :: kerase a s₂.entries

Tactic:
exact p.kinsert s₁.nodupKeys

Result:
no goals
-- Mathlib/Order/Category/FinPartOrd.lean
lemma comp_apply {X Y Z : FinPartOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (f ≫ g) x = g (f x)

Proof state:
X Y Z : FinPartOrd
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X.toPartOrd
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/CharP/Defs.lean
lemma nontrivial_of_char_ne_one {v : ℕ} (hv : v ≠ 1) [hr : CharP R v] : Nontrivial R :=
  ⟨⟨(1 : ℕ), 0, fun h =>
      hv <| by rwa [CharP.cast_eq_zero_iff _ v, Nat.dvd_one] at h⟩⟩

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
v : ℕ
hv : v ≠ 1
hr : CharP R v
h : ↑1 = 0
⊢ v = 1

Tactic:
rwa [CharP.cast_eq_zero_iff _ v, Nat.dvd_one] at h

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coeff_add_monomial_mul (a : R) :
    coeff R (m + n) (monomial R m a * φ) = a * coeff R n φ

Proof state:
case hc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ m ≤ m + n

Tactic:
exact le_add_right le_rfl

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff R (m + n)) ((monomial R m) a * φ) = a * (coeff R n) φ

Tactic:
rw [coeff_monomial_mul, if_pos, add_tsub_cancel_left]

Result:
case hc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ m ≤ m + n
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Bounded.dual :
    ∀ {t : Ordnode α} {o₁ o₂}, Bounded t o₁ o₂ → @Bounded αᵒᵈ _ (dual t) o₂ o₁
  | nil, o₁, o₂, h => by cases o₁ <;> cases o₂ <;> trivial
  | node _ _ _ _, _, _, ⟨ol, Or⟩ => ⟨Or.dual, ol.dual⟩

Proof state:
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
h : nil.Bounded o₁ o₂
⊢ nil.dual.Bounded o₂ o₁

Tactic:
cases o₁ <;> cases o₂ <;> trivial

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
theorem ext_num_den_iff : p = q ↔ p.num = q.num ∧ p.den = q.den :=
  ⟨by rintro rfl; exact ⟨rfl, rfl⟩, fun h ↦ ext_num_den h.1 h.2⟩

Proof state:
p : ℚ≥0
⊢ p.num = p.num ∧ p.den = p.den

Tactic:
exact ⟨rfl, rfl⟩

Result:
no goals

Proof state:
p q : ℚ≥0
⊢ p = q → p.num = q.num ∧ p.den = q.den

Tactic:
rintro rfl

Result:
p : ℚ≥0
⊢ p.num = p.num ∧ p.den = p.den
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem foldRev_cons_key {l : Raw α β} {acc : List α} :
    l.foldRev (fun acc k _ => k :: acc) acc = List.keys (toListModel l.buckets) ++ acc

Proof state:
α : Type u
β : α → Type v
l : Raw α β
acc : List α
⊢ Raw.foldRev (fun acc k x => k :: acc) acc l = List.keys (toListModel l.buckets) ++ acc

Tactic:
rw [foldRev_cons_apply, keys_eq_map]

Result:
no goals
-- Mathlib/Logic/IsEmpty.lean
theorem leftTotal_empty [IsEmpty α] : LeftTotal R

Proof state:
α : Type u_4
β : Type u_5
R : α → β → Prop
inst✝ : IsEmpty α
⊢ LeftTotal R

Tactic:
simp only [LeftTotal, IsEmpty.forall_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem max_comm (a b : Int) : max a b = max b a

Proof state:
a b : Int
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b

Tactic:
by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]

Result:
case pos
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
⊢ b = a

case neg
a b : Int
h₁ : ¬a ≤ b
h₂ : ¬b ≤ a
⊢ a = b

Proof state:
case pos
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
⊢ b = a

Tactic:
exact Int.le_antisymm h₂ h₁

Result:
no goals

Proof state:
a b : Int
⊢ max a b = max b a

Tactic:
simp only [Int.max_def]

Result:
a b : Int
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b

Proof state:
case neg
a b : Int
h₁ : ¬a ≤ b
h₂ : ¬b ≤ a
⊢ a = b

Tactic:
cases not_or_intro h₁ h₂ <| Int.le_total ..

Result:
no goals
-- Mathlib/Data/List/Lemmas.lean
theorem foldl_range_subset_of_range_subset {f : α → β → α} {g : α → γ → α}
    (hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b) (a : α) :
    Set.range (foldl f a) ⊆ Set.range (foldl g a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ Set.range (foldr (fun z w => f w z) a ∘ reverse) ⊆ Set.range (foldr (fun z w => g w z) a ∘ reverse)

Tactic:
simp_rw [Set.range_comp _ reverse, reverse_involutive.bijective.surjective.range_eq,
  Set.image_univ]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ Set.range (foldr (fun z w => f w z) a) ⊆ Set.range (foldr (fun z w => g w z) a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ Set.range (foldr (fun z w => f w z) a) ⊆ Set.range (foldr (fun z w => g w z) a)

Tactic:
exact foldr_range_subset_of_range_subset hfg a

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ (Set.range fun l => foldl f a l) ⊆ Set.range fun l => foldl g a l

Tactic:
simp_rw [← foldr_reverse _ (fun z w => g w z), ← foldr_reverse _ (fun z w => f w z)]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ (Set.range fun l => foldr (fun z w => f w z) a l.reverse) ⊆ Set.range fun l => foldr (fun z w => g w z) a l.reverse

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ Set.range (foldl f a) ⊆ Set.range (foldl g a)

Tactic:
change (Set.range fun l => _) ⊆ Set.range fun l => _

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ (Set.range fun l => foldl f a l) ⊆ Set.range fun l => foldl g a l

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ (Set.range fun l => foldr (fun z w => f w z) a l.reverse) ⊆ Set.range fun l => foldr (fun z w => g w z) a l.reverse

Tactic:
change (Set.range (foldr (fun z w => f w z) a ∘ reverse)) ⊆
  Set.range (foldr (fun z w => g w z) a ∘ reverse)

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ Set.range (foldr (fun z w => f w z) a ∘ reverse) ⊆ Set.range (foldr (fun z w => g w z) a ∘ reverse)
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioo_inter_Ioi : Ioo a b ∩ Ioi c = Ioo (max a c) b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ioo a b ∩ Ioi c = Ioo (a ⊔ c) b

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c x✝ : α
⊢ x✝ ∈ Ioo a b ∩ Ioi c ↔ x✝ ∈ Ioo (a ⊔ c) b

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c x✝ : α
⊢ x✝ ∈ Ioo a b ∩ Ioi c ↔ x✝ ∈ Ioo (a ⊔ c) b

Tactic:
simp_rw [mem_inter_iff, mem_Ioo, mem_Ioi, max_lt_iff, and_assoc, and_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
/-- Compositional version of `Finset.measurable_prod` for use by `fun_prop`. -/
@[to_additive (attr := measurability, fun_prop)
"Compositional version of `Finset.measurable_sum` for use by `fun_prop`."]
lemma Finset.measurable_prod' {f : ι → α → β → M} {g : α → β} {s : Finset ι}
    (hf : ∀ i, Measurable ↿(f i)) (hg : Measurable g) :
    Measurable fun a ↦ (∏ i ∈ s, f i a) (g a)

Proof state:
M : Type u_2
ι : Type u_3
α : Type u_4
β : Type u_5
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
mβ : MeasurableSpace β
f : ι → α → β → M
g : α → β
s : Finset ι
hf : ∀ (i : ι), Measurable ↿(f i)
hg : Measurable g
⊢ Measurable fun a => ∏ c ∈ s, f c a (g a)

Tactic:
fun_prop

Result:
no goals

Proof state:
M : Type u_2
ι : Type u_3
α : Type u_4
β : Type u_5
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
mβ : MeasurableSpace β
f : ι → α → β → M
g : α → β
s : Finset ι
hf : ∀ (i : ι), Measurable ↿(f i)
hg : Measurable g
⊢ Measurable fun a => (∏ i ∈ s, f i a) (g a)

Tactic:
simp

Result:
M : Type u_2
ι : Type u_3
α : Type u_4
β : Type u_5
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
mβ : MeasurableSpace β
f : ι → α → β → M
g : α → β
s : Finset ι
hf : ∀ (i : ι), Measurable ↿(f i)
hg : Measurable g
⊢ Measurable fun a => ∏ c ∈ s, f c a (g a)
-- Mathlib/Data/Nat/Bitwise.lean
theorem xor_left_injective {n : ℕ} : Function.Injective fun m => m ^^^ n :=
  fun m m' (h : m ^^^ n = m' ^^^ n) => by
  rw [← xor_cancel_right n m, ← xor_cancel_right n m', h]

Proof state:
n m m' : ℕ
h : m ^^^ n = m' ^^^ n
⊢ m = m'

Tactic:
rw [← xor_cancel_right n m, ← xor_cancel_right n m', h]

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem isSimpleModule_iff_isAtom : IsSimpleModule R m ↔ IsAtom m

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : Submodule R M
⊢ IsSimpleModule R ↥m ↔ IsAtom m

Tactic:
rw [← Set.isSimpleOrder_Iic_iff_isAtom]

Result:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : Submodule R M
⊢ IsSimpleModule R ↥m ↔ IsSimpleOrder ↑(Set.Iic m)

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : Submodule R M
⊢ IsSimpleModule R ↥m ↔ IsSimpleOrder ↑(Set.Iic m)

Tactic:
exact m.mapIic.isSimpleOrder_iff

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem epic_of_localizationMap {j k : N →* P} (h : ∀ a, j.comp f.toMap a = k.comp f.toMap a) :
    j = k

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
j k : N →* P
h : ∀ (a : M), (j.comp f.toMap) a = (k.comp f.toMap) a
⊢ f.lift ⋯ = f.lift ⋯

Tactic:
congr 1 with x

Result:
case e_g.h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
j k : N →* P
h : ∀ (a : M), (j.comp f.toMap) a = (k.comp f.toMap) a
x : M
⊢ (j.comp f.toMap) x = (k.comp f.toMap) x

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
j k : N →* P
h : ∀ (a : M), (j.comp f.toMap) a = (k.comp f.toMap) a
⊢ j = k

Tactic:
rw [← f.lift_of_comp j, ← f.lift_of_comp k]

Result:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
j k : N →* P
h : ∀ (a : M), (j.comp f.toMap) a = (k.comp f.toMap) a
⊢ f.lift ⋯ = f.lift ⋯

Proof state:
case e_g.h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
j k : N →* P
h : ∀ (a : M), (j.comp f.toMap) a = (k.comp f.toMap) a
x : M
⊢ (j.comp f.toMap) x = (k.comp f.toMap) x

Tactic:
exact h x

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem union_zeroLocus (s s' : Set R) :
    zeroLocus s ∪ zeroLocus s' = zeroLocus (Ideal.span s ⊓ Ideal.span s' : Ideal R)

Proof state:
R : Type u
inst✝ : CommSemiring R
s s' : Set R
⊢ zeroLocus s ∪ zeroLocus s' = zeroLocus ↑(Ideal.span s ⊓ Ideal.span s')

Tactic:
rw [zeroLocus_inf]

Result:
R : Type u
inst✝ : CommSemiring R
s s' : Set R
⊢ zeroLocus s ∪ zeroLocus s' = zeroLocus ↑(Ideal.span s) ∪ zeroLocus ↑(Ideal.span s')

Proof state:
R : Type u
inst✝ : CommSemiring R
s s' : Set R
⊢ zeroLocus s ∪ zeroLocus s' = zeroLocus ↑(Ideal.span s) ∪ zeroLocus ↑(Ideal.span s')

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Mod.lean
theorem mul_lt_mul_right (a0 : 0 < a) : b * a < c * a ↔ b < c

Proof state:
a b c : Nat
a0 : 0 < a
⊢ b * a < c * a ↔ b < c

Tactic:
rw [Nat.mul_comm b a, Nat.mul_comm c a, Nat.mul_lt_mul_left a0]

Result:
no goals
-- Mathlib/Data/Finsupp/Interval.lean
theorem card_Ioc : #(Ioc f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 1

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ #(Ioc f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 1

Tactic:
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem sign_cycleRange {n : ℕ} (i : Fin n) : Perm.sign (cycleRange i) = (-1) ^ (i : ℕ)

Proof state:
n : ℕ
i : Fin n
⊢ sign i.cycleRange = (-1) ^ ↑i

Tactic:
simp [cycleRange]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem map_eq_nil_iff {p : G.Walk u u} : p.map f = nil ↔ p = nil

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
⊢ Walk.map f p = nil ↔ p = nil

Tactic:
cases p <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Adjunction.lean
@[reassoc (attr := simp)]
lemma commShiftIso_hom_app_counit_app_shift [adj.CommShift A] (a : A) (Y : D) :
    ((G ⋙ F).commShiftIso a).hom.app Y ≫ (adj.counit.app Y)⟦a⟧' = adj.counit.app (Y⟦a⟧)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
inst✝ : adj.CommShift A
a : A
Y : D
⊢ ((G ⋙ F).commShiftIso a).hom.app Y ≫ (shiftFunctor D a).map (adj.counit.app Y) =
    adj.counit.app ((shiftFunctor D a).obj Y)

Tactic:
simpa using (NatTrans.shift_app_comm adj.counit a Y)

Result:
no goals
-- Mathlib/Computability/ContextFreeGrammar.lean
@[simp] lemma reverse_reverse (r : ContextFreeRule T N) : r.reverse.reverse = r

Proof state:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
⊢ r.reverse.reverse = r

Tactic:
simp [reverse]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem length_tail (l : List α) : length (tail l) = length l - 1

Proof state:
α : Type u_1
l : List α
⊢ l.tail.length = l.length - 1

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem withTopEquiv_ofNat (n : Nat) [n.AtLeastTwo] :
    withTopEquiv ofNat(n) = OfNat.ofNat n

Proof state:
n : ℕ
inst✝ : n.AtLeastTwo
⊢ withTopEquiv (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_le_iff : ⌊a⌋ ≤ z ↔ a < z + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ⌊a⌋ ≤ z ↔ a < ↑z + 1

Tactic:
rw [← lt_add_one_iff, floor_lt]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ a < ↑(z + 1) ↔ a < ↑z + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ a < ↑(z + 1) ↔ a < ↑z + 1

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem inv_mul_cancel_left₀ (h : a ≠ 0) (b : G₀) : a⁻¹ * (a * b) = b :=
  calc
    a⁻¹ * (a * b) = a⁻¹ * a * b := (mul_assoc _ _ _).symm
    _ = b

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
b : G₀
⊢ a⁻¹ * a * b = b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Tactic/NormNum/PowMod.lean
theorem natPow_one_natMod : Nat.mod (Nat.pow a (nat_lit 1)) m = Nat.mod a m

Proof state:
a m : ℕ
⊢ (a.pow 1).mod m = a.mod m

Tactic:
rw [natPow_one]

Result:
no goals