harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem aeval_comp_bind₁ [Algebra R S] (f : τ → S) (g : σ → MvPolynomial τ R) :
    (aeval f).comp (bind₁ g) = aeval fun i => aeval f (g i)

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : τ → S
g : σ → MvPolynomial τ R
⊢ (aeval f).comp (bind₁ g) = aeval fun i => (aeval f) (g i)

Tactic:
ext1

Result:
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : τ → S
g : σ → MvPolynomial τ R
i✝ : σ
⊢ ((aeval f).comp (bind₁ g)) (X i✝) = (aeval fun i => (aeval f) (g i)) (X i✝)

Proof state:
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : τ → S
g : σ → MvPolynomial τ R
i✝ : σ
⊢ ((aeval f).comp (bind₁ g)) (X i✝) = (aeval fun i => (aeval f) (g i)) (X i✝)

Tactic:
apply aeval_bind₁

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem edge_other_ne {e : Sym2 V} (he : e ∈ G.edgeSet) {v : V} (h : v ∈ e) :
    Sym2.Mem.other h ≠ v

Proof state:
V : Type u
G : SimpleGraph V
e : Sym2 V
v : V
h : v ∈ e
he : s(Sym2.Mem.other h, v) ∈ G.edgeSet
⊢ Sym2.Mem.other h ≠ v

Tactic:
exact G.ne_of_adj he

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
e : Sym2 V
he : e ∈ G.edgeSet
v : V
h : v ∈ e
⊢ Sym2.Mem.other h ≠ v

Tactic:
rw [← Sym2.other_spec h, Sym2.eq_swap] at he

Result:
V : Type u
G : SimpleGraph V
e : Sym2 V
v : V
h : v ∈ e
he : s(Sym2.Mem.other h, v) ∈ G.edgeSet
⊢ Sym2.Mem.other h ≠ v
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_eq_range_sigma (s : α → Set β) : ⋃ i, s i = range fun a : Σi, s i => a.2

Proof state:
α : Type u_1
β : Type u_2
s : α → Set β
⊢ ⋃ i, s i = range fun a => ↑a.snd

Tactic:
simp [Set.ext_iff]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iio_union_Ico' (h₁ : c ≤ b) : Iio b ∪ Ico c d = Iio (max b d)

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
hc : c ≤ x
⊢ x < b ∨ c ≤ x ∧ x < d ↔ x < b ∨ x < d

Tactic:
simp only [hc, true_and]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
⊢ x < b ∨ c ≤ x ∧ x < d ↔ x < b ∨ x < d

Tactic:
by_cases hc : c ≤ x

Result:
case pos
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
hc : c ≤ x
⊢ x < b ∨ c ≤ x ∧ x < d ↔ x < b ∨ x < d

case neg
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
⊢ x < b ∨ c ≤ x ∧ x < d ↔ x < b ∨ x < d

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
⊢ x < b ∨ c ≤ x ∧ x < d ↔ x < b ∨ x < d

Tactic:
have hxb : x < b := (lt_of_not_ge hc).trans_le h₁

Result:
case neg
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
hxb : x < b
⊢ x < b ∨ c ≤ x ∧ x < d ↔ x < b ∨ x < d

Proof state:
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
⊢ Iio b ∪ Ico c d = Iio (b ⊔ d)

Tactic:
ext1 x

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
⊢ x ∈ Iio b ∪ Ico c d ↔ x ∈ Iio (b ⊔ d)

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
hxb : x < b
⊢ x < b ∨ c ≤ x ∧ x < d ↔ x < b ∨ x < d

Tactic:
simp only [hxb, true_or]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
⊢ x ∈ Iio b ∪ Ico c d ↔ x ∈ Iio (b ⊔ d)

Tactic:
simp_rw [mem_union, mem_Iio, mem_Ico, lt_max_iff]

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
⊢ x < b ∨ c ≤ x ∧ x < d ↔ x < b ∨ x < d
-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem lcm_ndinsert (a : α) (s : Multiset α) : (ndinsert a s).lcm = GCDMonoid.lcm a s.lcm

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (ndinsert a s).lcm = GCDMonoid.lcm a s.lcm

Tactic:
rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_cons]

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem eq_push_append_of_mem {xs : Vector α n} {x : α} (h : x ∈ xs) :
    ∃ (n₁ n₂ : Nat) (as : Vector α n₁) (bs : Vector α n₂) (h : n₁ + 1 + n₂ = n),
      xs = (as.push x ++ bs).cast h ∧ x ∉ as

Proof state:
case mk.intro.intro.intro
α : Type u_1
x : α
xs : Array α
h✝ : x ∈ { toArray := xs, size_toArray := ⋯ }
as bs : Array α
h : xs = as.push x ++ bs
w : ¬x ∈ as
⊢ ∃ n₁ n₂ as bs h, { toArray := xs, size_toArray := ⋯ } = Vector.cast h (as.push x ++ bs) ∧ ¬x ∈ as

Tactic:
obtain rfl := h

Result:
case mk.intro.intro.intro
α : Type u_1
x : α
as bs : Array α
w : ¬x ∈ as
h : x ∈ { toArray := as.push x ++ bs, size_toArray := ⋯ }
⊢ ∃ n₁ n₂ as_1 bs_1 h,
    { toArray := as.push x ++ bs, size_toArray := ⋯ } = Vector.cast h (as_1.push x ++ bs_1) ∧ ¬x ∈ as_1

Proof state:
case mk.intro.intro.intro
α : Type u_1
x : α
as bs : Array α
w : ¬x ∈ as
h : x ∈ { toArray := as.push x ++ bs, size_toArray := ⋯ }
⊢ ∃ n₁ n₂ as_1 bs_1 h,
    { toArray := as.push x ++ bs, size_toArray := ⋯ } = Vector.cast h (as_1.push x ++ bs_1) ∧ ¬x ∈ as_1

Tactic:
exact ⟨_, _, as.toVector, bs.toVector, by simp, by simp, by simpa using w⟩

Result:
no goals

Proof state:
α : Type u_1
x : α
as bs : Array α
w : ¬x ∈ as
h : x ∈ { toArray := as.push x ++ bs, size_toArray := ⋯ }
⊢ ¬x ∈ as.toVector

Tactic:
simpa using w

Result:
no goals

Proof state:
case mk
α : Type u_1
x : α
xs : Array α
h : x ∈ { toArray := xs, size_toArray := ⋯ }
⊢ ∃ n₁ n₂ as bs h, { toArray := xs, size_toArray := ⋯ } = Vector.cast h (as.push x ++ bs) ∧ ¬x ∈ as

Tactic:
obtain ⟨as, bs, h, w⟩ := Array.eq_push_append_of_mem (by simpa using h)

Result:
case mk.intro.intro.intro
α : Type u_1
x : α
xs : Array α
h✝ : x ∈ { toArray := xs, size_toArray := ⋯ }
as bs : Array α
h : xs = as.push x ++ bs
w : ¬x ∈ as
⊢ ∃ n₁ n₂ as bs h, { toArray := xs, size_toArray := ⋯ } = Vector.cast h (as.push x ++ bs) ∧ ¬x ∈ as

Proof state:
α : Type u_1
n : Nat
xs : Vector α n
x : α
h : x ∈ xs
⊢ ∃ n₁ n₂ as bs h, xs = Vector.cast h (as.push x ++ bs) ∧ ¬x ∈ as

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
α : Type u_1
x : α
xs : Array α
h : x ∈ { toArray := xs, size_toArray := ⋯ }
⊢ ∃ n₁ n₂ as bs h, { toArray := xs, size_toArray := ⋯ } = Vector.cast h (as.push x ++ bs) ∧ ¬x ∈ as

Proof state:
α : Type u_1
x : α
xs : Array α
h : x ∈ { toArray := xs, size_toArray := ⋯ }
⊢ ?m.95827 ∈ ?m.95826

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
x : α
as bs : Array α
w : ¬x ∈ as
h : x ∈ { toArray := as.push x ++ bs, size_toArray := ⋯ }
⊢ { toArray := as.push x ++ bs, size_toArray := ⋯ } = Vector.cast ⋯ (as.toVector.push x ++ bs.toVector)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
x : α
as bs : Array α
w : ¬x ∈ as
h : x ∈ { toArray := as.push x ++ bs, size_toArray := ⋯ }
⊢ as.size + 1 + bs.size = (as.push x ++ bs).size

Tactic:
simp

Result:
no goals
-- Mathlib/Order/BooleanGenerators.lean
lemma complementedLattice_of_sSup_eq_top (hS : BooleanGenerators S) (h : sSup S = ⊤) :
    ComplementedLattice α

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ ComplementedLattice α

Tactic:
let _i := hS.distribLattice_of_sSup_eq_top h

Result:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
_i : DistribLattice α := hS.distribLattice_of_sSup_eq_top h
⊢ ComplementedLattice α

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
_i : DistribLattice α := hS.distribLattice_of_sSup_eq_top h
⊢ ComplementedLattice α

Tactic:
have _i₁ := isAtomistic_of_sSup_eq_top hS h

Result:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
_i : DistribLattice α := hS.distribLattice_of_sSup_eq_top h
_i₁ : IsAtomistic α
⊢ ComplementedLattice α

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
_i : DistribLattice α := hS.distribLattice_of_sSup_eq_top h
_i₁ : IsAtomistic α
⊢ ComplementedLattice α

Tactic:
apply complementedLattice_of_isAtomistic

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem NFBelow.snd {e n a b} (h : NFBelow (ONote.oadd e n a) b) : NFBelow a (repr e)

Proof state:
case oadd'
e : ONote
n : ℕ+
a : ONote
b eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b
⊢ a.NFBelow e.repr

Tactic:
exact h₂

Result:
no goals

Proof state:
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
h : (e.oadd n a).NFBelow b
⊢ a.NFBelow e.repr

Tactic:
obtain - | ⟨h₁, h₂, h₃⟩ := h

Result:
case oadd'
e : ONote
n : ℕ+
a : ONote
b eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b
⊢ a.NFBelow e.repr
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem get?_eq_getValueCast? [BEq α] [Hashable α] [LawfulBEq α]
    {m : Raw₀ α β} (hm : Raw.WFImp m.1) {a : α} :
    m.get? a = getValueCast? a (toListModel m.1.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
⊢ m.get? a = getValueCast? a (toListModel m.val.buckets)

Tactic:
rw [get?_eq_get?ₘ, get?ₘ_eq_getValueCast? hm]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem lt_add_one_iff_lt {x y : PartENat} (hx : x ≠ ⊤) : x < y + 1 ↔ x ≤ y

Proof state:
x y : PartENat
hx : x ≠ ⊤
h : x ≤ y
⊢ x < y + 1

Tactic:
rcases ne_top_iff.mp hx with ⟨m, rfl⟩

Result:
case intro
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h : ↑m ≤ y
⊢ ↑m < y + 1

Proof state:
case intro.a.a
m : ℕ
hx : ↑m ≠ ⊤
n : ℕ
h : ↑m ≤ ↑n
⊢ m ≤ n

Tactic:
norm_cast at h

Result:
no goals

Proof state:
case intro.a
m : ℕ
hx : ↑m ≠ ⊤
h : ↑m ≤ ⊤
⊢ ↑m < ⊤

Tactic:
apply natCast_lt_top

Result:
no goals

Proof state:
case intro.a
m : ℕ
hx : ↑m ≠ ⊤
h : ↑m ≤ ⊤
⊢ ↑m < ⊤ + 1

Tactic:
rw [top_add]

Result:
case intro.a
m : ℕ
hx : ↑m ≠ ⊤
h : ↑m ≤ ⊤
⊢ ↑m < ⊤

Proof state:
x y : PartENat
hx : x ≠ ⊤
⊢ x < y + 1 ↔ x ≤ y

Tactic:
refine ⟨le_of_lt_add_one, fun h => ?_⟩

Result:
x y : PartENat
hx : x ≠ ⊤
h : x ≤ y
⊢ x < y + 1

Proof state:
case intro.a
m : ℕ
hx : ↑m ≠ ⊤
n : ℕ
h : ↑m ≤ ↑n
⊢ ↑m < ↑n + 1

Tactic:
norm_cast

Result:
case intro.a
m : ℕ
hx : ↑m ≠ ⊤
n : ℕ
h : ↑m ≤ ↑n
⊢ m < n + 1

Proof state:
case intro
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h : ↑m ≤ y
⊢ ↑m < y + 1

Tactic:
induction' y using PartENat.casesOn with n

Result:
case intro.a
m : ℕ
hx : ↑m ≠ ⊤
h : ↑m ≤ ⊤
⊢ ↑m < ⊤ + 1

case intro.a
m : ℕ
hx : ↑m ≠ ⊤
n : ℕ
h : ↑m ≤ ↑n
⊢ ↑m < ↑n + 1

Proof state:
case intro.a
m : ℕ
hx : ↑m ≠ ⊤
n : ℕ
h : ↑m ≤ ↑n
⊢ m < n + 1

Tactic:
apply Nat.lt_succ_of_le

Result:
case intro.a.a
m : ℕ
hx : ↑m ≠ ⊤
n : ℕ
h : ↑m ≤ ↑n
⊢ m ≤ n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem get_ite {p : Prop} [Decidable p] (h) :
    (if p then some b else none).get h = b

Proof state:
α✝ : Type u_1
b : α✝
p : Prop
inst✝ : Decidable p
h : (if p then some b else none).isSome = true
⊢ (if h : p then some ((fun x => b) h) else none).isSome = true

Tactic:
simpa using h

Result:
no goals

Proof state:
α✝ : Type u_1
b : α✝
p : Prop
inst✝ : Decidable p
h : (if p then some b else none).isSome = true
⊢ (if p then some b else none).get h = b

Tactic:
simpa using get_dite (p := p) (fun _ => b) (by simpa using h)

Result:
no goals
-- Mathlib/Algebra/Module/Equiv/Defs.lean
theorem self_trans_symm (f : M₁ ≃ₛₗ[σ₁₂] M₂) : f.trans f.symm = LinearEquiv.refl R₁ M₁

Proof state:
case h
R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_7
M₂ : Type u_8
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₁
inst✝ : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M₁ ≃ₛₗ[σ₁₂] M₂
x : M₁
⊢ (f.trans f.symm) x = (refl R₁ M₁) x

Tactic:
simp

Result:
no goals

Proof state:
R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_7
M₂ : Type u_8
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₁
inst✝ : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M₁ ≃ₛₗ[σ₁₂] M₂
⊢ f.trans f.symm = refl R₁ M₁

Tactic:
ext x

Result:
case h
R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_7
M₂ : Type u_8
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₁
inst✝ : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M₁ ≃ₛₗ[σ₁₂] M₂
x : M₁
⊢ (f.trans f.symm) x = (refl R₁ M₁) x
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
lemma logb_self_eq_one_iff : logb b b = 1 ↔ b ≠ 0 ∧ b ≠ 1 ∧ b ≠ -1 :=
  Iff.trans ⟨fun h h' => by simp [logb, h'] at h, div_self⟩ log_ne_zero

Proof state:
b : ℝ
h : logb b b = 1
h' : log b = 0
⊢ False

Tactic:
simp [logb, h'] at h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_log : ∫ s in a..b, log s = b * log b - a * log a - b + a

Proof state:
a b : ℝ
⊢ (∫ (x : ℝ) in a..0, log x) + ∫ (x : ℝ) in 0 ..b, log x = b * log b - a * log a - b + a

Tactic:
rw [intervalIntegral.integral_symm, integral_log_from_zero, integral_log_from_zero]

Result:
a b : ℝ
⊢ -(a * log a - a) + (b * log b - b) = b * log b - a * log a - b + a

Proof state:
a b : ℝ
⊢ ∫ (s : ℝ) in a..b, log s = b * log b - a * log a - b + a

Tactic:
rw [← intervalIntegral.integral_add_adjacent_intervals (b := 0)]

Result:
a b : ℝ
⊢ (∫ (x : ℝ) in a..0, log x) + ∫ (x : ℝ) in 0 ..b, log x = b * log b - a * log a - b + a

case hab
a b : ℝ
⊢ IntervalIntegrable log MeasureTheory.volume a 0

case hbc
a b : ℝ
⊢ IntervalIntegrable log MeasureTheory.volume 0 b

Proof state:
case hbc
a b : ℝ
⊢ IntervalIntegrable log MeasureTheory.volume 0 b

Tactic:
exact intervalIntegrable_log'

Result:
no goals

Proof state:
case hab
a b : ℝ
⊢ IntervalIntegrable log MeasureTheory.volume a 0

case hbc
a b : ℝ
⊢ IntervalIntegrable log MeasureTheory.volume 0 b

Tactic:
all_goals exact intervalIntegrable_log'

Result:
no goals

Proof state:
a b : ℝ
⊢ -(a * log a - a) + (b * log b - b) = b * log b - a * log a - b + a

Tactic:
ring

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsCycle.transfer {q : G.Walk u u} (qc : q.IsCycle) (hq) :
    (q.transfer H hq).IsCycle

Proof state:
case cons
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
v✝ : V
h✝ : G.Adj u v✝
q : G.Walk v✝ u
hq✝ : ∀ e ∈ (cons h✝ q).edges, e ∈ H.edgeSet
hq : H.Adj u v✝ ∧ ∀ a ∈ q.edges, a ∈ H.edgeSet
qc : q.IsPath ∧ s(u, v✝) ∉ q.edges
⊢ (q.transfer H ⋯).IsPath ∧ s(u, v✝) ∉ q.edges

Tactic:
exact ⟨qc.1.transfer hq.2, qc.2⟩

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
v✝ : V
h✝ : G.Adj u v✝
q : G.Walk v✝ u
qc : (cons h✝ q).IsCycle
hq : ∀ e ∈ (cons h✝ q).edges, e ∈ H.edgeSet
⊢ ((cons h✝ q).transfer H hq).IsCycle

Tactic:
simp only [edges_cons, List.find?, List.mem_cons, forall_eq_or_imp, mem_edgeSet] at hq

Result:
case cons
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
v✝ : V
h✝ : G.Adj u v✝
q : G.Walk v✝ u
qc : (cons h✝ q).IsCycle
hq✝ : ∀ e ∈ (cons h✝ q).edges, e ∈ H.edgeSet
hq : H.Adj u v✝ ∧ ∀ a ∈ q.edges, a ∈ H.edgeSet
⊢ ((cons h✝ q).transfer H hq✝).IsCycle

Proof state:
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
q : G.Walk u u
qc : q.IsCycle
hq : ∀ e ∈ q.edges, e ∈ H.edgeSet
⊢ (q.transfer H hq).IsCycle

Tactic:
cases q with
| nil => simp at qc
| cons _ q =>
  simp only [edges_cons, List.find?, List.mem_cons, forall_eq_or_imp, mem_edgeSet] at hq
  simp only [Walk.transfer, cons_isCycle_iff, edges_transfer q hq.2] at qc ⊢
  exact ⟨qc.1.transfer hq.2, qc.2⟩

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
qc : nil.IsCycle
hq : ∀ e ∈ nil.edges, e ∈ H.edgeSet
⊢ (nil.transfer H hq).IsCycle

Tactic:
simp at qc

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
v✝ : V
h✝ : G.Adj u v✝
q : G.Walk v✝ u
qc : (cons h✝ q).IsCycle
hq✝ : ∀ e ∈ (cons h✝ q).edges, e ∈ H.edgeSet
hq : H.Adj u v✝ ∧ ∀ a ∈ q.edges, a ∈ H.edgeSet
⊢ ((cons h✝ q).transfer H hq✝).IsCycle

Tactic:
simp only [Walk.transfer, cons_isCycle_iff, edges_transfer q hq.2] at qc ⊢

Result:
case cons
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
v✝ : V
h✝ : G.Adj u v✝
q : G.Walk v✝ u
hq✝ : ∀ e ∈ (cons h✝ q).edges, e ∈ H.edgeSet
hq : H.Adj u v✝ ∧ ∀ a ∈ q.edges, a ∈ H.edgeSet
qc : q.IsPath ∧ s(u, v✝) ∉ q.edges
⊢ (q.transfer H ⋯).IsPath ∧ s(u, v✝) ∉ q.edges
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem all_eq_true_iff_forall_mem {xs : Vector α n} : xs.all p ↔ ∀ x, x ∈ xs → p x

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ { toArray := xs, size_toArray := ⋯ }.all p = true ↔ ∀ (x : α), x ∈ { toArray := xs, size_toArray := ⋯ } → p x = true

Tactic:
simp only [all_mk, Array.all_eq_true_iff_forall_mem]

Result:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ (∀ (x : α), x ∈ xs → p x = true) ↔ ∀ (x : α), x ∈ { toArray := xs, size_toArray := ⋯ } → p x = true

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ (∀ (x : α), x ∈ xs → p x = true) ↔ ∀ (x : α), x ∈ { toArray := xs, size_toArray := ⋯ } → p x = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
p : α → Bool
xs : Vector α n
⊢ xs.all p = true ↔ ∀ (x : α), x ∈ xs → p x = true

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ { toArray := xs, size_toArray := ⋯ }.all p = true ↔ ∀ (x : α), x ∈ { toArray := xs, size_toArray := ⋯ } → p x = true
-- Mathlib/Topology/Basic.lean
theorem clusterPt_principal {x : X} {C : Set X} :
    ClusterPt x (𝓟 C) ↔ x ∈ C ∨ AccPt x (𝓟 C)

Proof state:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : ClusterPt x (𝓟 C)
⊢ x ∈ C ∨ AccPt x (𝓟 C)

Tactic:
by_contra! hc

Result:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : ClusterPt x (𝓟 C)
hc : x ∉ C ∧ ¬AccPt x (𝓟 C)
⊢ False

Proof state:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : ClusterPt x (𝓟 C)
hc : x ∉ C ∧ ¬ClusterPt x (𝓟 (C \ {x}))
⊢ False

Tactic:
simp_all only [not_false_eq_true, diff_singleton_eq_self, not_true_eq_false, hc.1]

Result:
no goals

Proof state:
case mpr.inr
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : AccPt x (𝓟 C)
⊢ ClusterPt x (𝓟 C)

Tactic:
exact h.clusterPt

Result:
no goals

Proof state:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ ClusterPt x (𝓟 C) → x ∈ C ∨ AccPt x (𝓟 C)

Tactic:
intro h

Result:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : ClusterPt x (𝓟 C)
⊢ x ∈ C ∨ AccPt x (𝓟 C)

Proof state:
case mpr.inl
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : x ∈ C
⊢ ClusterPt x (𝓟 C)

Tactic:
exact clusterPt_principal_iff.mpr fun _ mem ↦ ⟨x, ⟨mem_of_mem_nhds mem, h⟩⟩

Result:
no goals

Proof state:
case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ x ∈ C ∨ AccPt x (𝓟 C) → ClusterPt x (𝓟 C)

Tactic:
rintro (h | h)

Result:
case mpr.inl
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : x ∈ C
⊢ ClusterPt x (𝓟 C)

case mpr.inr
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : AccPt x (𝓟 C)
⊢ ClusterPt x (𝓟 C)

Proof state:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : ClusterPt x (𝓟 C)
hc : x ∉ C ∧ ¬AccPt x (𝓟 C)
⊢ False

Tactic:
rw [acc_principal_iff_cluster] at hc

Result:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : ClusterPt x (𝓟 C)
hc : x ∉ C ∧ ¬ClusterPt x (𝓟 (C \ {x}))
⊢ False

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ ClusterPt x (𝓟 C) ↔ x ∈ C ∨ AccPt x (𝓟 C)

Tactic:
constructor

Result:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ ClusterPt x (𝓟 C) → x ∈ C ∨ AccPt x (𝓟 C)

case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ x ∈ C ∨ AccPt x (𝓟 C) → ClusterPt x (𝓟 C)
-- Mathlib/Data/Set/NAry.lean
/-- If `a` is a left identity for `f : α → β → β`, then `{a}` is a left identity for
`Set.image2 f`. -/
lemma image2_left_identity {f : α → β → β} {a : α} (h : ∀ b, f a b = b) (t : Set β) :
    image2 f {a} t = t

Proof state:
α : Type u_1
β : Type u_3
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
t : Set β
⊢ image2 f {a} t = t

Tactic:
rw [image2_singleton_left, show f a = id from funext h, image_id]

Result:
no goals
-- Mathlib/Algebra/Star/Subalgebra.lean
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : A →⋆ₐ[R] B) (hf : Function.Injective f)
    (s : ι → StarSubalgebra R A) : map f (iInf s) = ⨅ (i : ι), map f (s i)

Proof state:
R : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : StarRing R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : StarRing A
inst✝⁵ : StarModule R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R B
ι : Sort u_5
inst✝ : Nonempty ι
f : A →⋆ₐ[R] B
hf : Function.Injective ⇑f
s : ι → StarSubalgebra R A
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective

Result:
case a
R : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : StarRing R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : StarRing A
inst✝⁵ : StarModule R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R B
ι : Sort u_5
inst✝ : Nonempty ι
f : A →⋆ₐ[R] B
hf : Function.Injective ⇑f
s : ι → StarSubalgebra R A
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Proof state:
case a
R : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : StarRing R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : StarRing A
inst✝⁵ : StarModule R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R B
ι : Sort u_5
inst✝ : Nonempty ι
f : A →⋆ₐ[R] B
hf : Function.Injective ⇑f
s : ι → StarSubalgebra R A
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem mem_restrict_range {r : β} {s : Set α} {f : α →ₛ β} (hs : MeasurableSet s) :
    r ∈ (restrict f s).range ↔ r = 0 ∧ s ≠ univ ∨ r ∈ f '' s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hs : MeasurableSet s
⊢ r ∈ (f.restrict s).range ↔ r = 0 ∧ s ≠ univ ∨ r ∈ ⇑f '' s

Tactic:
rw [← Finset.mem_coe, coe_range, coe_restrict _ hs, mem_range_indicator]

Result:
no goals