harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma IsCycle.isPath_of_append_right {p : G.Walk u v} {q : G.Walk v u} (h : ¬ p.Nil)
    (hcyc : (p.append q).IsCycle) : q.IsPath

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail
⊢ v ∉ q.support.tail ∧ q.support.tail.Nodup

Tactic:
exact ⟨this.2.2 (p.end_mem_tail_support h), this.2.1⟩

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : (p.append q).support.tail.Nodup
⊢ q.IsPath

Tactic:
rw [tail_support_append, List.nodup_append] at this

Result:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail
⊢ q.IsPath

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail
⊢ q.IsPath

Tactic:
rw [isPath_def, support_eq_cons, List.nodup_cons]

Result:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail
⊢ v ∉ q.support.tail ∧ q.support.tail.Nodup

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
⊢ q.IsPath

Tactic:
have := hcyc.2

Result:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : (p.append q).support.tail.Nodup
⊢ q.IsPath
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem nfp_lt_ord_of_isRegular {f : Ordinal → Ordinal} {c} (hc : IsRegular c) (hc' : c ≠ ℵ₀)
    (hf : ∀ i < c.ord, f i < c.ord) {a} : a < c.ord → nfp f a < c.ord :=
  nfp_lt_ord
    (by
      rw [hc.cof_eq]
      exact lt_of_le_of_ne hc.1 hc'.symm)
    hf

Proof state:
f : Ordinal.{u_1} → Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hc' : c ≠ ℵ₀
hf : ∀ i < c.ord, f i < c.ord
a : Ordinal.{u_1}
⊢ ℵ₀ < c.ord.cof

Tactic:
rw [hc.cof_eq]

Result:
f : Ordinal.{u_1} → Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hc' : c ≠ ℵ₀
hf : ∀ i < c.ord, f i < c.ord
a : Ordinal.{u_1}
⊢ ℵ₀ < c

Proof state:
f : Ordinal.{u_1} → Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hc' : c ≠ ℵ₀
hf : ∀ i < c.ord, f i < c.ord
a : Ordinal.{u_1}
⊢ ℵ₀ < c

Tactic:
exact lt_of_le_of_ne hc.1 hc'.symm

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem compl_compl_himp_distrib (a b : α) : (a ⇨ b)ᶜᶜ = aᶜᶜ ⇨ bᶜᶜ

Proof state:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ (a ⇨ b)ᶜᶜ = aᶜᶜ ⇨ bᶜᶜ

Tactic:
apply le_antisymm

Result:
case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ (a ⇨ b)ᶜᶜ ≤ aᶜᶜ ⇨ bᶜᶜ

case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ aᶜᶜ ⇨ bᶜᶜ ≤ (a ⇨ b)ᶜᶜ

Proof state:
case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ aᶜᶜ ⊓ (aᶜᶜ ⇨ bᶜᶜ) ≤ bᶜᶜ

Tactic:
exact inf_himp_le

Result:
no goals

Proof state:
case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ (aᶜ ⊔ b)ᶜ ≤ (aᶜᶜ ⇨ bᶜᶜ)ᶜ

Tactic:
rw [compl_sup_distrib, le_compl_iff_disjoint_right, disjoint_right_comm, ←
  le_compl_iff_disjoint_right]

Result:
case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ aᶜᶜ ⊓ (aᶜᶜ ⇨ bᶜᶜ) ≤ bᶜᶜ

Proof state:
case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ ((a ⇨ b) ⊓ a)ᶜᶜ ≤ bᶜᶜ

Tactic:
exact compl_anti (compl_anti himp_inf_le)

Result:
no goals

Proof state:
case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ aᶜᶜ ⇨ bᶜᶜ ≤ (a ⇨ b)ᶜᶜ

Tactic:
refine le_compl_comm.1 ((compl_anti compl_sup_le_himp).trans ?_)

Result:
case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ (aᶜ ⊔ b)ᶜ ≤ (aᶜᶜ ⇨ bᶜᶜ)ᶜ

Proof state:
case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ (a ⇨ b)ᶜᶜ ≤ aᶜᶜ ⇨ bᶜᶜ

Tactic:
rw [le_himp_iff, ← compl_compl_inf_distrib]

Result:
case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ ((a ⇨ b) ⊓ a)ᶜᶜ ≤ bᶜᶜ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseIdx_ne_empty_iff {l : Array α} {i : Nat} {h} : eraseIdx l i ≠ #[] ↔ 2 ≤ l.size

Proof state:
case mk.nil
α : Type u_1
i : Nat
h : i < { toList := [] }.size
⊢ { toList := [] }.eraseIdx i h ≠ #[] ↔ 2 ≤ { toList := [] }.size

Tactic:
simp

Result:
no goals

Proof state:
case mk.cons.nil
α : Type u_1
i : Nat
a : α
h✝ : i < { toList := [a] }.size
h : i = 0
⊢ { toList := [a] }.eraseIdx i h✝ ≠ #[] ↔ 2 ≤ { toList := [a] }.size

Tactic:
simp [h]

Result:
no goals

Proof state:
case mk.cons.cons
α : Type u_1
i : Nat
a b : α
l : List α
h : i < { toList := a :: b :: l }.size
⊢ { toList := a :: b :: l }.eraseIdx i h ≠ #[] ↔ 2 ≤ { toList := a :: b :: l }.size

Tactic:
simp

Result:
no goals

Proof state:
case mk.cons.nil
α : Type u_1
i : Nat
a : α
h : i < { toList := [a] }.size
⊢ { toList := [a] }.eraseIdx i h ≠ #[] ↔ 2 ≤ { toList := [a] }.size

Tactic:
simp at h

Result:
case mk.cons.nil
α : Type u_1
i : Nat
a : α
h✝ : i < { toList := [a] }.size
h : i = 0
⊢ { toList := [a] }.eraseIdx i h✝ ≠ #[] ↔ 2 ≤ { toList := [a] }.size

Proof state:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
⊢ l.eraseIdx i h ≠ #[] ↔ 2 ≤ l.size

Tactic:
rcases l with ⟨_ | ⟨a, (_ | ⟨b, l⟩)⟩⟩

Result:
case mk.nil
α : Type u_1
i : Nat
h : i < { toList := [] }.size
⊢ { toList := [] }.eraseIdx i h ≠ #[] ↔ 2 ≤ { toList := [] }.size

case mk.cons.nil
α : Type u_1
i : Nat
a : α
h : i < { toList := [a] }.size
⊢ { toList := [a] }.eraseIdx i h ≠ #[] ↔ 2 ≤ { toList := [a] }.size

case mk.cons.cons
α : Type u_1
i : Nat
a b : α
l : List α
h : i < { toList := a :: b :: l }.size
⊢ { toList := a :: b :: l }.eraseIdx i h ≠ #[] ↔ 2 ≤ { toList := a :: b :: l }.size
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_sub_cancel (x y : Int): (x - y) % y = x % y

Proof state:
x y : Int
⊢ (x - y) % y = x % y

Tactic:
by_cases h : y = 0

Result:
case pos
x y : Int
h : y = 0
⊢ (x - y) % y = x % y

case neg
x y : Int
h : ¬y = 0
⊢ (x - y) % y = x % y

Proof state:
case neg
x y : Int
h : ¬y = 0
⊢ (x - y) % y = x % y

Tactic:
simp only [Int.emod_def, Int.sub_ediv_of_dvd, Int.dvd_refl, Int.ediv_self h, Int.mul_sub]

Result:
case neg
x y : Int
h : ¬y = 0
⊢ x - y - (y * (x / y) - y * 1) = x - y * (x / y)

Proof state:
case neg
x y : Int
h : ¬y = 0
⊢ x - y - (y * (x / y) - y * 1) = x - y * (x / y)

Tactic:
simp [Int.mul_one, Int.sub_sub, Int.add_comm y]

Result:
no goals

Proof state:
case pos
x y : Int
h : y = 0
⊢ (x - y) % y = x % y

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Group/Nat/Even.lean
@[parity_simps] lemma even_mul : Even (m * n) ↔ Even m ∨ Even n

Proof state:
m n : ℕ
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
rcases mod_two_eq_zero_or_one m with h₁ | h₁ <;> rcases mod_two_eq_zero_or_one n with h₂ | h₂ <;>
  simp [even_iff, h₁, h₂, Nat.mul_mod]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem setParentBump_rankD_lt {arr : Array UFNode} {x y : Fin arr.size}
    (hroot : arr[x.1].rank < arr[y.1].rank ∨ arr[y.1].parent = y)
    (H : arr[x.1].rank ≤ arr[y.1].rank) {i : Nat}
    (rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i))
    (hP : parentD arr' i = if x.1 = i then y.1 else parentD arr i)
    (hR : ∀ {i}, rankD arr' i =
      if y.1 = i ∧ arr[x.1].rank = arr[y.1].rank then
        arr[y.1].rank + 1
      else rankD arr i) :
    ¬parentD arr' i = i → rankD arr' i < rankD arr' (parentD arr' i)

Proof state:
case isTrue.isFalse
arr' arr : Array UFNode
x y : Fin arr.size
hroot : arr[↑x].rank < arr[↑y].rank ∨ arr[↑y].parent = ↑y
H : arr[↑x].rank ≤ arr[↑y].rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ¬(↑y = ↑x ∧ arr[↑x].rank = arr[↑y].rank)
h : ¬↑y = ↑x
⊢ rankD arr ↑x < if arr[↑x].rank = arr[↑y].rank then arr[↑y].rank + 1 else rankD arr ↑y

Tactic:
simp only [rankD_eq, x.2, y.2, Array.get_eq_getElem]

Result:
case isTrue.isFalse
arr' arr : Array UFNode
x y : Fin arr.size
hroot : arr[↑x].rank < arr[↑y].rank ∨ arr[↑y].parent = ↑y
H : arr[↑x].rank ≤ arr[↑y].rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ¬(↑y = ↑x ∧ arr[↑x].rank = arr[↑y].rank)
h : ¬↑y = ↑x
⊢ arr[↑x].rank < if arr[↑x].rank = arr[↑y].rank then arr[↑y].rank + 1 else arr[↑y].rank

Proof state:
case isTrue.isFalse.isTrue
arr' arr : Array UFNode
x y : Fin arr.size
hroot : arr[↑x].rank < arr[↑y].rank ∨ arr[↑y].parent = ↑y
H : arr[↑x].rank ≤ arr[↑y].rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ¬(↑y = ↑x ∧ arr[↑x].rank = arr[↑y].rank)
h : ¬↑y = ↑x
h₃ : arr[↑x].rank = arr[↑y].rank
⊢ arr[↑x].rank < arr[↑x].rank + 1

Tactic:
apply Nat.lt_succ_self

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
/-- If `φ : a ⟶ b` lifts `𝟙 T` and `ψ : b ⟶ c` lifts `f`, then `φ  ≫ ψ` lifts `f` -/
lemma comp_lift_id_left' {a b c : 𝒳} (R : 𝒮) (φ : a ⟶ b) [p.IsHomLift (𝟙 R) φ]
    {S T : 𝒮} (f : S ⟶ T) (ψ : b ⟶ c) [p.IsHomLift f ψ] : p.IsHomLift f (φ ≫ ψ)

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b c : 𝒳
R : 𝒮
φ : a ⟶ b
inst✝¹ : p.IsHomLift (𝟙 R) φ
S T : 𝒮
f : S ⟶ T
ψ : b ⟶ c
inst✝ : p.IsHomLift f ψ
⊢ p.IsHomLift f (φ ≫ ψ)

Tactic:
obtain rfl : R = S := by rw [← codomain_eq p (𝟙 R) φ, domain_eq p f ψ]

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b c : 𝒳
R : 𝒮
φ : a ⟶ b
inst✝¹ : p.IsHomLift (𝟙 R) φ
T : 𝒮
ψ : b ⟶ c
f : R ⟶ T
inst✝ : p.IsHomLift f ψ
⊢ p.IsHomLift f (φ ≫ ψ)

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b c : 𝒳
R : 𝒮
φ : a ⟶ b
inst✝¹ : p.IsHomLift (𝟙 R) φ
T : 𝒮
ψ : b ⟶ c
f : R ⟶ T
inst✝ : p.IsHomLift f ψ
⊢ p.IsHomLift f (φ ≫ ψ)

Tactic:
infer_instance

Result:
no goals

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b c : 𝒳
R : 𝒮
φ : a ⟶ b
inst✝¹ : p.IsHomLift (𝟙 R) φ
S T : 𝒮
f : S ⟶ T
ψ : b ⟶ c
inst✝ : p.IsHomLift f ψ
⊢ R = S

Tactic:
rw [← codomain_eq p (𝟙 R) φ, domain_eq p f ψ]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
/-- Binary entropy is continuous everywhere.
This is due to definition of `Real.log` for negative numbers. -/
@[fun_prop] lemma binEntropy_continuous : Continuous binEntropy

Proof state:
⊢ Continuous binEntropy

Tactic:
rw [binEntropy_eq_negMulLog_add_negMulLog_one_sub']

Result:
⊢ Continuous fun p => p.negMulLog + (1 - p).negMulLog

Proof state:
⊢ Continuous fun p => p.negMulLog + (1 - p).negMulLog

Tactic:
fun_prop

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Hom.lean
@[simp]
lemma id_comp {ι₂ M₂ N₂ : Type*}
    [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
    (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : RootPairing.Equiv P Q) :
    comp f (id P) = f

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
⊢ f.comp (id P) = f

Tactic:
ext x <;> simp

Result:
no goals
-- Mathlib/Algebra/Group/Subsemigroup/Basic.lean
theorem mem_iSup {ι : Sort*} (p : ι → Subsemigroup M) {m : M} :
    (m ∈ ⨆ i, p i) ↔ ∀ N, (∀ i, p i ≤ N) → m ∈ N

Proof state:
M : Type u_1
inst✝ : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
m : M
⊢ (∀ (b : Subsemigroup M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔
    ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
simp only [closure_singleton_le_iff_mem]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
m : M
⊢ m ∈ ⨆ i, p i ↔ ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
rw [← closure_singleton_le_iff_mem, le_iSup_iff]

Result:
M : Type u_1
inst✝ : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
m : M
⊢ (∀ (b : Subsemigroup M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔
    ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N
-- Mathlib/Order/Interval/Set/OrdConnected.lean
theorem ordConnected_of_Ioo {α : Type*} [PartialOrder α] {s : Set α}
    (hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s) : OrdConnected s

Proof state:
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
⊢ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → Icc x y ⊆ s

Tactic:
intro x hx y hy hxy

Result:
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ Icc x y ⊆ s

Proof state:
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
⊢ s.OrdConnected

Tactic:
rw [ordConnected_iff]

Result:
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
⊢ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → Icc x y ⊆ s

Proof state:
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ Icc x y ⊆ s

Tactic:
rcases eq_or_lt_of_le hxy with (rfl | hxy')

Result:
case inl
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx hy : x ∈ s
hxy : x ≤ x
⊢ Icc x x ⊆ s

case inr
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
⊢ Icc x y ⊆ s

Proof state:
case inl
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx hy : x ∈ s
hxy : x ≤ x
⊢ Icc x x ⊆ s

Tactic:
simpa

Result:
no goals

Proof state:
case inr
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
⊢ insert x (insert y (Ioo x y)) ⊆ s

Tactic:
exact insert_subset_iff.2 ⟨hx, insert_subset_iff.2 ⟨hy, hs x hx y hy hxy'⟩⟩

Result:
no goals

Proof state:
case inr
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
⊢ Icc x y ⊆ s

Tactic:
rw [← Ioc_insert_left hxy, ← Ioo_insert_right hxy']

Result:
case inr
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
⊢ insert x (insert y (Ioo x y)) ⊆ s
-- Mathlib/RingTheory/Kaehler/CotangentComplex.lean
lemma H1Cotangent.map_comp
    (f : Hom P P') (g : Hom P' P'') :
    map (g.comp f) = (map g).restrictScalars S ∘ₗ map f

Proof state:
R : Type u
S : Type v
inst✝²² : CommRing R
inst✝²¹ : CommRing S
inst✝²⁰ : Algebra R S
R' : Type u'
S' : Type v'
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁶ : Algebra R R'
inst✝¹⁵ : Algebra S S'
inst✝¹⁴ : Algebra R S'
inst✝¹³ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Extension R'' S''
inst✝⁹ : Algebra R R''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S''
inst✝⁶ : IsScalarTower R R'' S''
inst✝⁵ : Algebra R' R''
inst✝⁴ : Algebra S' S''
inst✝³ : Algebra R' S''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R R' R''
inst✝ : IsScalarTower S S' S''
P : Extension R S
f : P.Hom P'
g : P'.Hom P''
⊢ map (g.comp f) = ↑S (map g) ∘ₗ map f

Tactic:
ext

Result:
case h.e.e
R : Type u
S : Type v
inst✝²² : CommRing R
inst✝²¹ : CommRing S
inst✝²⁰ : Algebra R S
R' : Type u'
S' : Type v'
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁶ : Algebra R R'
inst✝¹⁵ : Algebra S S'
inst✝¹⁴ : Algebra R S'
inst✝¹³ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Extension R'' S''
inst✝⁹ : Algebra R R''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S''
inst✝⁶ : IsScalarTower R R'' S''
inst✝⁵ : Algebra R' R''
inst✝⁴ : Algebra S' S''
inst✝³ : Algebra R' S''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R R' R''
inst✝ : IsScalarTower S S' S''
P : Extension R S
f : P.Hom P'
g : P'.Hom P''
x✝ : P.H1Cotangent
⊢ (↑((map (g.comp f)) x✝)).val = (↑((↑S (map g) ∘ₗ map f) x✝)).val

Proof state:
case h.e.e
R : Type u
S : Type v
inst✝²² : CommRing R
inst✝²¹ : CommRing S
inst✝²⁰ : Algebra R S
R' : Type u'
S' : Type v'
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁶ : Algebra R R'
inst✝¹⁵ : Algebra S S'
inst✝¹⁴ : Algebra R S'
inst✝¹³ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Extension R'' S''
inst✝⁹ : Algebra R R''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S''
inst✝⁶ : IsScalarTower R R'' S''
inst✝⁵ : Algebra R' R''
inst✝⁴ : Algebra S' S''
inst✝³ : Algebra R' S''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R R' R''
inst✝ : IsScalarTower S S' S''
P : Extension R S
f : P.Hom P'
g : P'.Hom P''
x✝ : P.H1Cotangent
⊢ (↑((map (g.comp f)) x✝)).val = (↑((↑S (map g) ∘ₗ map f) x✝)).val

Tactic:
simp [Cotangent.map_comp]

Result:
no goals
-- Mathlib/GroupTheory/Commutator/Basic.lean
theorem map_commutator (f : G →* G') : map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆

Proof state:
case left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅f g₁, f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆

Tactic:
intro p hp q hq

Result:
case left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ ⁅f p, f q⁆ ∈ ⁅map f H₁, map f H₂⁆

Proof state:
case right.intro.intro.intro.intro
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ ↑H₁
q : G
hq : q ∈ ↑H₂
⊢ ⁅f p, f q⁆ ∈ map f ⁅H₁, H₂⁆

Tactic:
rw [← map_commutatorElement]

Result:
case right.intro.intro.intro.intro
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ ↑H₁
q : G
hq : q ∈ ↑H₂
⊢ f ⁅p, q⁆ ∈ map f ⁅H₁, H₂⁆

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆

Tactic:
simp_rw [le_antisymm_iff, map_le_iff_le_comap, commutator_le, mem_comap, map_commutatorElement]

Result:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ (∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅f g₁, f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆) ∧
    ∀ g₁ ∈ map f H₁, ∀ g₂ ∈ map f H₂, ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆

Proof state:
case right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ ∀ g₁ ∈ map f H₁, ∀ g₂ ∈ map f H₂, ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆

Tactic:
rintro _ ⟨p, hp, rfl⟩ _ ⟨q, hq, rfl⟩

Result:
case right.intro.intro.intro.intro
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ ↑H₁
q : G
hq : q ∈ ↑H₂
⊢ ⁅f p, f q⁆ ∈ map f ⁅H₁, H₂⁆

Proof state:
case right.intro.intro.intro.intro
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ ↑H₁
q : G
hq : q ∈ ↑H₂
⊢ f ⁅p, q⁆ ∈ map f ⁅H₁, H₂⁆

Tactic:
exact mem_map_of_mem _ (commutator_mem_commutator hp hq)

Result:
no goals

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ (∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅f g₁, f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆) ∧
    ∀ g₁ ∈ map f H₁, ∀ g₂ ∈ map f H₂, ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆

Tactic:
constructor

Result:
case left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅f g₁, f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆

case right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ ∀ g₁ ∈ map f H₁, ∀ g₂ ∈ map f H₂, ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆

Proof state:
case left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ ⁅f p, f q⁆ ∈ ⁅map f H₁, map f H₂⁆

Tactic:
exact commutator_mem_commutator (mem_map_of_mem _ hp) (mem_map_of_mem _ hq)

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean
lemma dynEntourage_eq_inter_Ico (T : X → X) (U : Set (X × X)) (n : ℕ) :
    dynEntourage T U n = ⋂ k : Ico 0 n, (map T T)^[k] ⁻¹' U

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
n : ℕ
⊢ dynEntourage T U n = ⋂ k, (map T T)^[↑k] ⁻¹' U

Tactic:
simp [dynEntourage]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem inf_map_atTop_neBot_iff [Nonempty α] :
    NeBot (F ⊓ map u atTop) ↔ ∀ U ∈ F, ∀ N, ∃ n ≥ N, u n ∈ U

Proof state:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
F : Filter β
u : α → β
inst✝ : Nonempty α
⊢ (∀ {p : β → Prop}, (∀ᶠ (x : β) in F, p x) → ∀ (a : α), ∃ b ≥ a, p (u b)) ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≥ N, u n ∈ U

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
F : Filter β
u : α → β
inst✝ : Nonempty α
⊢ (F ⊓ map u atTop).NeBot ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≥ N, u n ∈ U

Tactic:
simp_rw [inf_neBot_iff_frequently_left, frequently_map, frequently_atTop]

Result:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
F : Filter β
u : α → β
inst✝ : Nonempty α
⊢ (∀ {p : β → Prop}, (∀ᶠ (x : β) in F, p x) → ∀ (a : α), ∃ b ≥ a, p (u b)) ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≥ N, u n ∈ U
-- Mathlib/Data/Multiset/Filter.lean
theorem count_eq_card_filter_eq [DecidableEq α] (s : Multiset α) (a : α) :
    s.count a = card (s.filter (a = ·))

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ count a s = (filter (fun x => a = x) s).card

Tactic:
rw [count, countP_eq_card_filter]

Result:
no goals
-- Mathlib/GroupTheory/Nilpotent.lean
theorem nilpotencyClass_prod [IsNilpotent G₁] [IsNilpotent G₂] :
    Group.nilpotencyClass (G₁ × G₂) =
    max (Group.nilpotencyClass G₁) (Group.nilpotencyClass G₂)

Proof state:
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsNilpotent G₁
inst✝ : IsNilpotent G₂
⊢ nilpotencyClass (G₁ × G₂) = nilpotencyClass G₁ ⊔ nilpotencyClass G₂

Tactic:
refine eq_of_forall_ge_iff fun k => ?_

Result:
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsNilpotent G₁
inst✝ : IsNilpotent G₂
k : ℕ
⊢ nilpotencyClass (G₁ × G₂) ≤ k ↔ nilpotencyClass G₁ ⊔ nilpotencyClass G₂ ≤ k

Proof state:
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsNilpotent G₁
inst✝ : IsNilpotent G₂
k : ℕ
⊢ nilpotencyClass (G₁ × G₂) ≤ k ↔ nilpotencyClass G₁ ⊔ nilpotencyClass G₂ ≤ k

Tactic:
simp only [max_le_iff, ← lowerCentralSeries_eq_bot_iff_nilpotencyClass_le,
  lowerCentralSeries_prod, prod_eq_bot_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
theorem inclusion_map {X Y : N C} (f : X ⟶ Y) :
    inclusion.map f = eqToHom (congr_arg _ (Discrete.ext (Discrete.eq_of_hom f)))

Proof state:
case up.up
C : Type u
X Y : (Discrete ∘ NormalMonoidalObject) C
down✝ : X.as = Y.as
⊢ inclusion.map { down := { down := down✝ } } = eqToHom ⋯

Tactic:
cases Discrete.ext (by assumption)

Result:
case up.up.refl
C : Type u
X : (Discrete ∘ NormalMonoidalObject) C
down✝ : X.as = X.as
⊢ inclusion.map { down := { down := down✝ } } = eqToHom ⋯

Proof state:
C : Type u
X Y : (Discrete ∘ NormalMonoidalObject) C
down✝ : X.as = Y.as
⊢ Discrete.as ?m.5556 = Discrete.as ?m.5557

Tactic:
assumption

Result:
no goals

Proof state:
case up.up.refl
C : Type u
X : (Discrete ∘ NormalMonoidalObject) C
down✝ : X.as = X.as
⊢ inclusion.map { down := { down := down✝ } } = eqToHom ⋯

Tactic:
apply inclusion.map_id

Result:
no goals

Proof state:
C : Type u
X Y : (Discrete ∘ NormalMonoidalObject) C
f : X ⟶ Y
⊢ inclusion.map f = eqToHom ⋯

Tactic:
rcases f with ⟨⟨⟩⟩

Result:
case up.up
C : Type u
X Y : (Discrete ∘ NormalMonoidalObject) C
down✝ : X.as = Y.as
⊢ inclusion.map { down := { down := down✝ } } = eqToHom ⋯