harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Monoidal/Mon_.lean
theorem mul_rightUnitor {M : Mon_ C} :
    (tensorμ M.X (𝟙_ C) M.X (𝟙_ C) ≫ (M.mul ⊗ (λ_ (𝟙_ C)).hom)) ≫ (ρ_ M.X).hom =
      ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ M.mul

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ (tensorμ M.X (𝟙_ C) M.X (𝟙_ C) ≫ (𝟙 (M.X ⊗ M.X) ⊗ (λ_ (𝟙_ C)).hom) ≫ (M.mul ⊗ 𝟙 (𝟙_ C))) ≫ (ρ_ M.X).hom =
    ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul

Tactic:
simp only [tensorHom_id, id_tensorHom]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ (tensorμ M.X (𝟙_ C) M.X (𝟙_ C) ≫ (M.X ⊗ M.X) ◁ (λ_ (𝟙_ C)).hom ≫ M.mul ▷ 𝟙_ C) ≫ (ρ_ M.X).hom =
    ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ (tensorμ M.X (𝟙_ C) M.X (𝟙_ C) ≫ (M.mul ⊗ (λ_ (𝟙_ C)).hom)) ≫ (ρ_ M.X).hom = ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ M.mul

Tactic:
rw [← Category.id_comp M.mul, ← Category.comp_id (λ_ (𝟙_ C)).hom, tensor_comp]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ (tensorμ M.X (𝟙_ C) M.X (𝟙_ C) ≫ (𝟙 (M.X ⊗ M.X) ⊗ (λ_ (𝟙_ C)).hom) ≫ (M.mul ⊗ 𝟙 (𝟙_ C))) ≫ (ρ_ M.X).hom =
    ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ (tensorμ M.X (𝟙_ C) M.X (𝟙_ C) ≫ (M.X ⊗ M.X) ◁ (λ_ (𝟙_ C)).hom ≫ M.mul ▷ 𝟙_ C) ≫ (ρ_ M.X).hom =
    ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul

Tactic:
slice_lhs 3 4 => rw [rightUnitor_naturality]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ tensorμ M.X (𝟙_ C) M.X (𝟙_ C) ≫ (M.X ⊗ M.X) ◁ (λ_ (𝟙_ C)).hom ≫ (ρ_ (M.X ⊗ M.X)).hom ≫ M.mul =
    ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ tensorμ M.X (𝟙_ C) M.X (𝟙_ C) ≫ (M.X ⊗ M.X) ◁ (λ_ (𝟙_ C)).hom ≫ (ρ_ (M.X ⊗ M.X)).hom ≫ M.mul =
    ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul

Tactic:
slice_lhs 1 3 => rw [← rightUnitor_monoidal]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ M.mul = ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ M.mul = ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul

Tactic:
simp only [Category.assoc, Category.id_comp]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem erase_diff_erase_sublist_of_sublist {a : α} :
    ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → (l₂.erase a).diff (l₁.erase a) <+ l₂.diff l₁
  | [], _, _ => erase_sublist _ _
  | b :: l₁, l₂, h =>
    if heq : b = a then by simp only [heq, erase_cons_head, diff_cons]; rfl
    else by
      simp only [erase_cons_head b l₁, erase_cons_tail (not_beq_of_ne heq),
        diff_cons ((List.erase l₂ a)) (List.erase l₁ a) b, diff_cons l₂ l₁ b, erase_comm a b l₂]
      have h' := h.erase b
      rw [erase_cons_head] at h'
      exact @erase_diff_erase_sublist_of_sublist _ l₁ (l₂.erase b) h'

Proof state:
α : Type u
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
heq : ¬b = a
h' : (b :: l₁).erase b <+ l₂.erase b
⊢ ((l₂.erase b).erase a).diff (l₁.erase a) <+ (l₂.erase b).diff l₁

Tactic:
rw [erase_cons_head] at h'

Result:
α : Type u
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
heq : ¬b = a
h' : l₁ <+ l₂.erase b
⊢ ((l₂.erase b).erase a).diff (l₁.erase a) <+ (l₂.erase b).diff l₁

Proof state:
α : Type u
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
heq : ¬b = a
h' : l₁ <+ l₂.erase b
⊢ ((l₂.erase b).erase a).diff (l₁.erase a) <+ (l₂.erase b).diff l₁

Tactic:
exact @erase_diff_erase_sublist_of_sublist _ l₁ (l₂.erase b) h'

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
heq : b = a
⊢ (l₂.erase a).diff l₁ <+ (l₂.erase a).diff l₁

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
heq : ¬b = a
⊢ ((l₂.erase b).erase a).diff (l₁.erase a) <+ (l₂.erase b).diff l₁

Tactic:
have h' := h.erase b

Result:
α : Type u
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
heq : ¬b = a
h' : (b :: l₁).erase b <+ l₂.erase b
⊢ ((l₂.erase b).erase a).diff (l₁.erase a) <+ (l₂.erase b).diff l₁

Proof state:
α : Type u
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
heq : b = a
⊢ (l₂.erase a).diff ((b :: l₁).erase a) <+ l₂.diff (b :: l₁)

Tactic:
simp only [heq, erase_cons_head, diff_cons]

Result:
α : Type u
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
heq : b = a
⊢ (l₂.erase a).diff l₁ <+ (l₂.erase a).diff l₁

Proof state:
α : Type u
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
heq : ¬b = a
⊢ (l₂.erase a).diff ((b :: l₁).erase a) <+ l₂.diff (b :: l₁)

Tactic:
simp only [erase_cons_head b l₁, erase_cons_tail (not_beq_of_ne heq),
  diff_cons ((List.erase l₂ a)) (List.erase l₁ a) b, diff_cons l₂ l₁ b, erase_comm a b l₂]

Result:
α : Type u
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
heq : ¬b = a
⊢ ((l₂.erase b).erase a).diff (l₁.erase a) <+ (l₂.erase b).diff l₁
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_add_of_nonneg_left {a b : Int} (h : 0 ≤ b) : a ≤ b + a

Proof state:
a b : Int
h : 0 ≤ b
this : 0 + a ≤ b + a
⊢ a ≤ b + a

Tactic:
rwa [Int.zero_add] at this

Result:
no goals

Proof state:
a b : Int
h : 0 ≤ b
⊢ a ≤ b + a

Tactic:
have : 0 + a ≤ b + a := Int.add_le_add_right h a

Result:
a b : Int
h : 0 ≤ b
this : 0 + a ≤ b + a
⊢ a ≤ b + a
-- Mathlib/LinearAlgebra/Reflection.lean
lemma infinite_range_reflection_reflection_iterate_iff [NoZeroSMulDivisors ℤ M]
    (hfx : f x = 2) (hgy : g y = 2) (hgxfy : f y * g x = 4) :
    (range <| fun n ↦ ((reflection hgy).trans (reflection hfx))^[n] y).Infinite ↔
    f y • x ≠ (2 : R) • y

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst✝ : NoZeroSMulDivisors ℤ M
hfx : f x = 2
hgy : g y = 2
hgxfy : f y * g x = 4
⊢ (range fun n => (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y).Infinite ↔ f y • x ≠ 2 • y

Tactic:
simp only [reflection_reflection_iterate hfx hgy hgxfy, infinite_range_add_nsmul_iff, sub_ne_zero]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma equiv_some_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) : P ≈ ![P x / P z, P y / P z, 1] :=
  equiv_of_X_eq_of_Y_eq hPz one_ne_zero
    (by linear_combination (norm := (matrix_simp; ring1)) -P x * div_self hPz)
    (by linear_combination (norm := (matrix_simp; ring1)) -P y * div_self hPz)

Proof state:
case a.a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P y * 1 + -P y * 1 - (P y / P z * P z + -P y * (P z / P z)) = 0

Tactic:
ring1

Result:
no goals

Proof state:
case a.a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P y * ![P x / P z, P y / P z, 1] z + -P y * 1 - (![P x / P z, P y / P z, 1] y * P z + -P y * (P z / P z)) = 0

Tactic:
matrix_simp

Result:
case a.a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P y * 1 + -P y * 1 - (P y / P z * P z + -P y * (P z / P z)) = 0

Proof state:
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P x * ![P x / P z, P y / P z, 1] z = ![P x / P z, P y / P z, 1] x * P z

Tactic:
linear_combination (norm := (matrix_simp; ring1)) -P x * div_self hPz

Result:
no goals

Proof state:
case a.a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P x * ![P x / P z, P y / P z, 1] z + -P x * 1 - (![P x / P z, P y / P z, 1] x * P z + -P x * (P z / P z)) = 0

Tactic:
matrix_simp

Result:
case a.a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P x * 1 + -P x * 1 - (P x / P z * P z + -P x * (P z / P z)) = 0

Proof state:
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P y * ![P x / P z, P y / P z, 1] z = ![P x / P z, P y / P z, 1] y * P z

Tactic:
linear_combination (norm := (matrix_simp; ring1)) -P y * div_self hPz

Result:
no goals

Proof state:
case a.a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P x * 1 + -P x * 1 - (P x / P z * P z + -P x * (P z / P z)) = 0

Tactic:
ring1

Result:
no goals
-- Mathlib/NumberTheory/Multiplicity.lean
theorem Int.sq_mod_four_eq_one_of_odd {x : ℤ} : Odd x → x ^ 2 % 4 = 1

Proof state:
x : ℤ
⊢ Odd x → x ^ 2 % 4 = 1

Tactic:
intro hx

Result:
x : ℤ
hx : Odd x
⊢ x ^ 2 % 4 = 1

Proof state:
case intro
w✝ : ℤ
⊢ (2 * w✝ + 1) ^ 2 % 4 = 1

Tactic:
ring_nf

Result:
case intro
w✝ : ℤ
⊢ (1 + w✝ * 4 + w✝ ^ 2 * 4) % 4 = 1

Proof state:
case intro
w✝ : ℤ
⊢ 1 % 4 = 1

Tactic:
decide

Result:
no goals

Proof state:
case intro
w✝ : ℤ
⊢ (1 + w✝ * 4 + w✝ ^ 2 * 4) % 4 = 1

Tactic:
rw [add_assoc, ← add_mul, Int.add_mul_emod_self]

Result:
case intro
w✝ : ℤ
⊢ 1 % 4 = 1

Proof state:
x : ℤ
hx : ∃ k, x = 2 * k + 1
⊢ x ^ 2 % 4 = 1

Tactic:
rcases hx with ⟨_, rfl⟩

Result:
case intro
w✝ : ℤ
⊢ (2 * w✝ + 1) ^ 2 % 4 = 1

Proof state:
x : ℤ
hx : Odd x
⊢ x ^ 2 % 4 = 1

Tactic:
unfold Odd at hx

Result:
x : ℤ
hx : ∃ k, x = 2 * k + 1
⊢ x ^ 2 % 4 = 1
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem uniformity_hasBasis_open_symmetric :
    HasBasis (𝓤 α) (fun V : Set (α × α) => V ∈ 𝓤 α ∧ IsOpen V ∧ SymmetricRel V) id

Proof state:
α : Type ua
inst✝ : UniformSpace α
⊢ (𝓤 α).HasBasis (fun V => (V ∈ 𝓤 α ∧ IsOpen V) ∧ SymmetricRel V) id

Tactic:
refine uniformity_hasBasis_open.restrict fun s hs => ⟨symmetrizeRel s, ?_⟩

Result:
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α ∧ IsOpen s
⊢ (symmetrizeRel s ∈ 𝓤 α ∧ IsOpen (symmetrizeRel s)) ∧ SymmetricRel (symmetrizeRel s) ∧ id (symmetrizeRel s) ⊆ id s

Proof state:
α : Type ua
inst✝ : UniformSpace α
⊢ (𝓤 α).HasBasis (fun V => V ∈ 𝓤 α ∧ IsOpen V ∧ SymmetricRel V) id

Tactic:
simp only [← and_assoc]

Result:
α : Type ua
inst✝ : UniformSpace α
⊢ (𝓤 α).HasBasis (fun V => (V ∈ 𝓤 α ∧ IsOpen V) ∧ SymmetricRel V) id

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α ∧ IsOpen s
⊢ (symmetrizeRel s ∈ 𝓤 α ∧ IsOpen (symmetrizeRel s)) ∧ SymmetricRel (symmetrizeRel s) ∧ id (symmetrizeRel s) ⊆ id s

Tactic:
exact
  ⟨⟨symmetrize_mem_uniformity hs.1, IsOpen.inter hs.2 (hs.2.preimage continuous_swap)⟩,
    symmetric_symmetrizeRel s, symmetrizeRel_subset_self s⟩

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem map.unique (g : FreeGroup α →* FreeGroup β)
    (hg : ∀ x, g (FreeGroup.of x) = FreeGroup.of (f x)) :
    ∀ {x}, g x = map f x

Proof state:
α : Type u
β : Type v
f : α → β
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), g (FreeGroup.of x) = FreeGroup.of (f x)
⊢ ∀ {x : FreeGroup α}, g x = (map f) x

Tactic:
rintro ⟨L⟩

Result:
case mk
α : Type u
β : Type v
f : α → β
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), g (FreeGroup.of x) = FreeGroup.of (f x)
x✝ : FreeGroup α
L : List (α × Bool)
⊢ g (Quot.mk Red.Step L) = (map f) (Quot.mk Red.Step L)

Proof state:
case mk
α : Type u
β : Type v
f : α → β
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), g (FreeGroup.of x) = FreeGroup.of (f x)
x✝ : FreeGroup α
L : List (α × Bool)
⊢ g (Quot.mk Red.Step L) = (map f) (Quot.mk Red.Step L)

Tactic:
exact List.recOn L g.map_one fun ⟨x, b⟩ t (ih : g (FreeGroup.mk t) = map f (FreeGroup.mk t)) =>
  Bool.recOn b
    (show g ((FreeGroup.of x)⁻¹ * FreeGroup.mk t) =
        FreeGroup.map f ((FreeGroup.of x)⁻¹ * FreeGroup.mk t) by
      simp [g.map_mul, g.map_inv, hg, ih])
    (show g (FreeGroup.of x * FreeGroup.mk t) =
        FreeGroup.map f (FreeGroup.of x * FreeGroup.mk t) by simp [g.map_mul, hg, ih])

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), g (FreeGroup.of x) = FreeGroup.of (f x)
x✝¹ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
t : List (α × Bool)
ih : g (FreeGroup.mk t) = (map f) (FreeGroup.mk t)
x : α
b : Bool
⊢ g ((FreeGroup.of x)⁻¹ * FreeGroup.mk t) = (map f) ((FreeGroup.of x)⁻¹ * FreeGroup.mk t)

Tactic:
simp [g.map_mul, g.map_inv, hg, ih]

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), g (FreeGroup.of x) = FreeGroup.of (f x)
x✝¹ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
t : List (α × Bool)
ih : g (FreeGroup.mk t) = (map f) (FreeGroup.mk t)
x : α
b : Bool
⊢ g (FreeGroup.of x * FreeGroup.mk t) = (map f) (FreeGroup.of x * FreeGroup.mk t)

Tactic:
simp [g.map_mul, hg, ih]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem braiding_inv_tensor_left (X Y Z : C) :
    (β_ (X ⊗ Y) Z).inv  =
      (α_ Z X Y).inv ≫ (β_ X Z).inv ▷ Y ≫ (α_ X Z Y).hom ≫
        X ◁ (β_ Y Z).inv ≫ (α_ X Y Z).inv :=
  eq_of_inv_eq_inv (by simp)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ inv (β_ (X ⊗ Y) Z).inv = inv ((α_ Z X Y).inv ≫ (β_ X Z).inv ▷ Y ≫ (α_ X Z Y).hom ≫ X ◁ (β_ Y Z).inv ≫ (α_ X Y Z).inv)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Defs/Unbundled.lean
theorem trans_trichotomous_left [IsTrans α r] [IsTrichotomous α r] {a b c : α}
    (h₁ : ¬r b a) (h₂ : r b c) : r a c

Proof state:
case inl
α : Type u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r a b
⊢ r a c

Tactic:
exact _root_.trans h₃ h₂

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a c : α
h₁ : ¬r a a
h₂ : r a c
⊢ r a c

Tactic:
exact h₂

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r b a
⊢ r a c

Tactic:
exact absurd h₃ h₁

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : ¬r b a
h₂ : r b c
⊢ r a c

Tactic:
rcases trichotomous_of r a b with (h₃ | rfl | h₃)

Result:
case inl
α : Type u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r a b
⊢ r a c

case inr.inl
α : Type u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a c : α
h₁ : ¬r a a
h₂ : r a c
⊢ r a c

case inr.inr
α : Type u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r b a
⊢ r a c
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_sub_natCast (hx : x ≠ 0) (y : ℝ) (n : ℕ) : x ^ (y - n) = x ^ y / x ^ n

Proof state:
case a
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ ↑(x ^ (y - ↑n)) = ↑(x ^ y / x ^ n)

Tactic:
exact Real.rpow_sub_natCast (mod_cast hx) _ _

Result:
no goals

Proof state:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y - ↑n) = x ^ y / x ^ n

Tactic:
ext

Result:
case a
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ ↑(x ^ (y - ↑n)) = ↑(x ^ y / x ^ n)
-- Mathlib/Algebra/Lie/Submodule.lean
@[simp]
lemma map_le_range {M' : Type*}
    [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') :
    N.map f ≤ f.range

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
N : LieSubmodule R L M
M' : Type u_1
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
⊢ map f N ≤ f.range

Tactic:
rw [← LieModuleHom.map_top]

Result:
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
N : LieSubmodule R L M
M' : Type u_1
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
⊢ map f N ≤ map f ⊤

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
N : LieSubmodule R L M
M' : Type u_1
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
⊢ map f N ≤ map f ⊤

Tactic:
exact LieSubmodule.map_mono le_top

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem splitUpper_eq_bot {i x} : I.splitUpper i x = ⊥ ↔ I.upper i ≤ x

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ I.splitUpper i x = ⊥ ↔ I.upper i ≤ x

Tactic:
rw [splitUpper, mk'_eq_bot, exists_update_iff I.lower fun j y => I.upper j ≤ y]

Result:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (I.upper i ≤ x ⊔ I.lower i ∨ ∃ x, x ≠ i ∧ I.upper x ≤ I.lower x) ↔ I.upper i ≤ x

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ I.splitUpper i x = ⊥ ↔ I.upper i ≤ x

Tactic:
classical
rw [splitUpper, mk'_eq_bot, exists_update_iff I.lower fun j y => I.upper j ≤ y]
simp [(I.lower_lt_upper _).not_le]

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (I.upper i ≤ x ⊔ I.lower i ∨ ∃ x, x ≠ i ∧ I.upper x ≤ I.lower x) ↔ I.upper i ≤ x

Tactic:
simp [(I.lower_lt_upper _).not_le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem xor_left_inj {x y : BitVec w} (z : BitVec w) : (x ^^^ z = y ^^^ z) ↔ x = y

Proof state:
case mpr
w : Nat
x y z : BitVec w
h : x = y
⊢ x ^^^ z = y ^^^ z

Tactic:
rw [h]

Result:
no goals

Proof state:
w : Nat
x y z : BitVec w
⊢ x ^^^ z = y ^^^ z ↔ x = y

Tactic:
constructor

Result:
case mp
w : Nat
x y z : BitVec w
⊢ x ^^^ z = y ^^^ z → x = y

case mpr
w : Nat
x y z : BitVec w
⊢ x = y → x ^^^ z = y ^^^ z

Proof state:
case mp
w : Nat
x y z : BitVec w
⊢ x ^^^ z = y ^^^ z → x = y

Tactic:
intro h

Result:
case mp
w : Nat
x y z : BitVec w
h : x ^^^ z = y ^^^ z
⊢ x = y

Proof state:
case mp.pred
w : Nat
x y z : BitVec w
h : x ^^^ z = y ^^^ z
i : Nat
ih : i < w
⊢ x.getLsbD i = y.getLsbD i

Tactic:
have := BitVec.eq_of_getLsbD_eq_iff.mp h i

Result:
case mp.pred
w : Nat
x y z : BitVec w
h : x ^^^ z = y ^^^ z
i : Nat
ih : i < w
this : i < w → (x ^^^ z).getLsbD i = (y ^^^ z).getLsbD i
⊢ x.getLsbD i = y.getLsbD i

Proof state:
case mpr
w : Nat
x y z : BitVec w
⊢ x = y → x ^^^ z = y ^^^ z

Tactic:
intro h

Result:
case mpr
w : Nat
x y z : BitVec w
h : x = y
⊢ x ^^^ z = y ^^^ z

Proof state:
case mp
w : Nat
x y z : BitVec w
h : x ^^^ z = y ^^^ z
⊢ x = y

Tactic:
ext i ih

Result:
case mp.pred
w : Nat
x y z : BitVec w
h : x ^^^ z = y ^^^ z
i : Nat
ih : i < w
⊢ x.getLsbD i = y.getLsbD i

Proof state:
case mp.pred
w : Nat
x y z : BitVec w
h : x ^^^ z = y ^^^ z
i : Nat
ih : i < w
this : i < w → (x ^^^ z).getLsbD i = (y ^^^ z).getLsbD i
⊢ x.getLsbD i = y.getLsbD i

Tactic:
simp only [getLsbD_xor, Bool.xor_left_inj] at this

Result:
case mp.pred
w : Nat
x y z : BitVec w
h : x ^^^ z = y ^^^ z
i : Nat
ih : i < w
this : i < w → x.getLsbD i = y.getLsbD i
⊢ x.getLsbD i = y.getLsbD i

Proof state:
case mp.pred
w : Nat
x y z : BitVec w
h : x ^^^ z = y ^^^ z
i : Nat
ih : i < w
this : i < w → x.getLsbD i = y.getLsbD i
⊢ x.getLsbD i = y.getLsbD i

Tactic:
exact this ih

Result:
no goals
-- Mathlib/Algebra/Group/Ext.lean
@[to_additive]
lemma CommGroup.toGroup_injective {G : Type*} : Injective (@CommGroup.toGroup G)

Proof state:
G : Type u_1
⊢ Injective (@toGroup G)

Tactic:
rintro ⟨⟩ ⟨⟩ ⟨⟩

Result:
case mk.mk.refl
G : Type u_1
toGroup✝ : Group G
mul_comm✝¹ mul_comm✝ : ∀ (a b : G), a * b = b * a
⊢ mk mul_comm✝¹ = mk mul_comm✝

Proof state:
case mk.mk.refl
G : Type u_1
toGroup✝ : Group G
mul_comm✝¹ mul_comm✝ : ∀ (a b : G), a * b = b * a
⊢ mk mul_comm✝¹ = mk mul_comm✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem sum_C_mul_X_pow_eq (p : R[X]) : (p.sum fun n a => C a * X ^ n) = p

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p.sum fun n a => C a * X ^ n) = p

Tactic:
simp_rw [C_mul_X_pow_eq_monomial, sum_monomial_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
theorem pi_condition : Pi.lift K.ι ≫ I.fstPiMap = Pi.lift K.ι ≫ I.sndPiMap

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
⊢ Pi.lift K.ι ≫ I.fstPiMap = Pi.lift K.ι ≫ I.sndPiMap

Tactic:
ext

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
b✝ : J.R
⊢ (Pi.lift K.ι ≫ I.fstPiMap) ≫ Pi.π I.right b✝ = (Pi.lift K.ι ≫ I.sndPiMap) ≫ Pi.π I.right b✝

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
b✝ : J.R
⊢ (Pi.lift K.ι ≫ I.fstPiMap) ≫ Pi.π I.right b✝ = (Pi.lift K.ι ≫ I.sndPiMap) ≫ Pi.π I.right b✝

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Pointwise.lean
theorem NeBot.one_le_div (h : f.NeBot) : 1 ≤ f / f

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
f : Filter α
h : f.NeBot
s t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ f
hs : t₁ / t₂ ⊆ s
a : α
ha₁ : a ∈ t₁
ha₂ : a ∈ t₂
⊢ s ∈ 1

Tactic:
rw [mem_one, ← div_self' a]

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
f : Filter α
h : f.NeBot
s t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ f
hs : t₁ / t₂ ⊆ s
a : α
ha₁ : a ∈ t₁
ha₂ : a ∈ t₂
⊢ a / a ∈ s

Proof state:
case intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
f : Filter α
h : f.NeBot
s t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ f
hs : t₁ / t₂ ⊆ s
⊢ s ∈ 1

Tactic:
obtain ⟨a, ha₁, ha₂⟩ := Set.not_disjoint_iff.1 (h.not_disjoint h₁ h₂)

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
f : Filter α
h : f.NeBot
s t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ f
hs : t₁ / t₂ ⊆ s
a : α
ha₁ : a ∈ t₁
ha₂ : a ∈ t₂
⊢ s ∈ 1

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
f : Filter α
h : f.NeBot
s t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ f
hs : t₁ / t₂ ⊆ s
a : α
ha₁ : a ∈ t₁
ha₂ : a ∈ t₂
⊢ a / a ∈ s

Tactic:
exact hs (Set.div_mem_div ha₁ ha₂)

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Group α
f : Filter α
h : f.NeBot
⊢ 1 ≤ f / f

Tactic:
rintro s ⟨t₁, h₁, t₂, h₂, hs⟩

Result:
case intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
f : Filter α
h : f.NeBot
s t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ f
hs : t₁ / t₂ ⊆ s
⊢ s ∈ 1
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
@[simp]
lemma coverEntropyEntourage_empty {T : X → X} {U : Set (X × X)} :
    coverEntropyEntourage T ∅ U = ⊥

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
h : ∀ᶠ (n : ℕ) in atTop, (↑(coverMincard T ∅ U n)).log / ↑n = ⊥
⊢ coverEntropyEntourage T ∅ U = ⊥

Tactic:
rw [coverEntropyEntourage]

Result:
X : Type u_1
T : X → X
U : Set (X × X)
h : ∀ᶠ (n : ℕ) in atTop, (↑(coverMincard T ∅ U n)).log / ↑n = ⊥
⊢ limsup (fun n => (↑(coverMincard T ∅ U n)).log / ↑n) atTop = ⊥

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
⊢ coverEntropyEntourage T ∅ U = ⊥

Tactic:
suffices h : ∀ᶠ n : ℕ in atTop, log (coverMincard T ∅ U n) / n = ⊥ by
  rw [coverEntropyEntourage]
  exact limsup_congr h ▸ limsup_const ⊥

Result:
X : Type u_1
T : X → X
U : Set (X × X)
⊢ ∀ᶠ (n : ℕ) in atTop, (↑(coverMincard T ∅ U n)).log / ↑n = ⊥

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
⊢ ∃ a, ∀ b ≥ a, ⊥ / ↑b = ⊥

Tactic:
exact ⟨1, fun n n_pos ↦ bot_div_of_pos_ne_top (Nat.cast_pos'.2 n_pos) (natCast_ne_top n)⟩

Result:
no goals

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
⊢ ∀ᶠ (n : ℕ) in atTop, (↑(coverMincard T ∅ U n)).log / ↑n = ⊥

Tactic:
simp only [coverMincard_empty, ENat.toENNReal_zero, log_zero, eventually_atTop]

Result:
X : Type u_1
T : X → X
U : Set (X × X)
⊢ ∃ a, ∀ b ≥ a, ⊥ / ↑b = ⊥

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
h : ∀ᶠ (n : ℕ) in atTop, (↑(coverMincard T ∅ U n)).log / ↑n = ⊥
⊢ limsup (fun n => (↑(coverMincard T ∅ U n)).log / ↑n) atTop = ⊥

Tactic:
exact limsup_congr h ▸ limsup_const ⊥

Result:
no goals