harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finsupp/Single.lean
theorem embDomain_single (f : α ↪ β) (a : α) (m : M) :
    embDomain f (single a m) = single (f a) m

Proof state:
case pos.intro
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
a' : α
⊢ (embDomain f (single a m)) (f a') = (single (f a) m) (f a')

Tactic:
simp [single_apply]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
b : β
⊢ (embDomain f (single a m)) b = (single (f a) m) b

Tactic:
by_cases h : b ∈ Set.range f

Result:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
b : β
h : b ∈ Set.range ⇑f
⊢ (embDomain f (single a m)) b = (single (f a) m) b

case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
b : β
h : b ∉ Set.range ⇑f
⊢ (embDomain f (single a m)) b = (single (f a) m) b

Proof state:
case neg.hnc
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
h : f a ∉ Set.range ⇑f
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
case neg.hnc
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
b : β
h : b ∉ Set.range ⇑f
⊢ ¬f a = b

Tactic:
rintro rfl

Result:
case neg.hnc
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
h : f a ∉ Set.range ⇑f
⊢ False

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
⊢ embDomain f (single a m) = single (f a) m

Tactic:
ext b

Result:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
b : β
⊢ (embDomain f (single a m)) b = (single (f a) m) b

Proof state:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
b : β
h : b ∈ Set.range ⇑f
⊢ (embDomain f (single a m)) b = (single (f a) m) b

Tactic:
rcases h with ⟨a', rfl⟩

Result:
case pos.intro
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
a' : α
⊢ (embDomain f (single a m)) (f a') = (single (f a) m) (f a')

Proof state:
case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
b : β
h : b ∉ Set.range ⇑f
⊢ (embDomain f (single a m)) b = (single (f a) m) b

Tactic:
simp only [embDomain_notin_range, h, single_apply, not_false_iff]

Result:
case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
b : β
h : b ∉ Set.range ⇑f
⊢ 0 = if f a = b then m else 0

Proof state:
case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
b : β
h : b ∉ Set.range ⇑f
⊢ 0 = if f a = b then m else 0

Tactic:
rw [if_neg]

Result:
case neg.hnc
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
b : β
h : b ∉ Set.range ⇑f
⊢ ¬f a = b
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
lemma norm_eq_zpow_neg_valuation {x : ℤ_[p]} (hx : x ≠ 0) : ‖x‖ = p ^ (-x.valuation : ℤ)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ‖x‖ = ↑p ^ (-↑x.valuation)

Tactic:
simp [norm_def, Padic.norm_eq_zpow_neg_valuation <| coe_ne_zero.2 hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_two_pow_of_ne {n m : Nat} (hm : n ≠ m) : testBit (2 ^ n) m = false

Proof state:
n m : Nat
hm : n ≠ m
⊢ (2 ^ n).testBit m = false

Tactic:
simp [testBit_two_pow]

Result:
n m : Nat
hm : n ≠ m
⊢ ¬n = m

Proof state:
n m : Nat
hm : n ≠ m
⊢ ¬n = m

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Extend.lean
lemma extendMap_id_f (i' : ι') : (extendMap (𝟙 K) e).f i' = 𝟙 _

Proof state:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = 𝟙 ((K.extend e).X i')

Tactic:
apply (K.isZero_extend_X e i' (fun i hi => hi' ⟨i, hi⟩)).eq_of_src

Result:
no goals

Proof state:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = 𝟙 ((K.extend e).X i')

Tactic:
obtain ⟨i, hi⟩ := hi'

Result:
case pos.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
i : ι
hi : e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = 𝟙 ((K.extend e).X i')

Proof state:
case pos.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
i : ι
hi : e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = 𝟙 ((K.extend e).X i')

Tactic:
simp [extendMap_f _ e hi]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
⊢ (extendMap (𝟙 K) e).f i' = 𝟙 ((K.extend e).X i')

Tactic:
by_cases hi' : ∃ i, e.f i = i'

Result:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = 𝟙 ((K.extend e).X i')

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = 𝟙 ((K.extend e).X i')
-- Mathlib/Data/Matroid/Circuit.lean
lemma fundCocircuit_inter_eq (M : Matroid α) {B : Set α} (he : e ∈ B) :
    (M.fundCocircuit e B) ∩ B = {e}

Proof state:
α : Type u_1
e : α
M : Matroid α
B : Set α
he : e ∈ B
⊢ insert e (M.E \ B) ∩ B ⊆ {e}

Tactic:
simp +contextual

Result:
no goals

Proof state:
α : Type u_1
e : α
M : Matroid α
B : Set α
he : e ∈ B
⊢ M.fundCocircuit e B ∩ B = {e}

Tactic:
refine subset_antisymm ?_ (singleton_subset_iff.2 ⟨M.mem_fundCocircuit _ _, he⟩)

Result:
α : Type u_1
e : α
M : Matroid α
B : Set α
he : e ∈ B
⊢ M.fundCocircuit e B ∩ B ⊆ {e}

Proof state:
α : Type u_1
e : α
M : Matroid α
B : Set α
he : e ∈ B
⊢ M.fundCocircuit e B ∩ B ⊆ {e}

Tactic:
refine (inter_subset_inter_left _ (M.fundCocircuit_subset_insert_compl _ _)).trans ?_

Result:
α : Type u_1
e : α
M : Matroid α
B : Set α
he : e ∈ B
⊢ insert e (M.E \ B) ∩ B ⊆ {e}
-- Mathlib/RingTheory/Congruence/Basic.lean
theorem sup_def {c d : RingCon R} : c ⊔ d = ringConGen (⇑c ⊔ ⇑d)

Proof state:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ c ⊔ d = ringConGen (⇑c ⊔ ⇑d)

Tactic:
rw [sup_eq_ringConGen]

Result:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ (ringConGen fun x y => c x y ∨ d x y) = ringConGen (⇑c ⊔ ⇑d)

Proof state:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ (ringConGen fun x y => c x y ∨ d x y) = ringConGen (⇑c ⊔ ⇑d)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem insert_singleton_eq {a : α} {b b' : β a} : insert a b (singleton a b') = singleton a b

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
⊢ insert a b (singleton a b') = singleton a b

Tactic:
simp only [singleton, Finmap.insert_toFinmap, AList.insert_singleton_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_flatten (l : List (List α)) :
    countP p l.flatten = (l.map (countP p)).sum

Proof state:
α : Type u_1
p : α → Bool
l : List (List α)
⊢ countP p l.flatten = (map (countP p) l).sum

Tactic:
simp only [countP_eq_length_filter, filter_flatten]

Result:
α : Type u_1
p : α → Bool
l : List (List α)
⊢ (map (filter p) l).flatten.length = (map (countP p) l).sum

Proof state:
α : Type u_1
p : α → Bool
l : List (List α)
⊢ (map (filter p) l).flatten.length = (map (countP p) l).sum

Tactic:
simp [countP_eq_length_filter']

Result:
no goals
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem restrict_inj {x₁ x₂ : FamilyOfElements P (generate R).arrows} (t₁ : x₁.Compatible)
    (t₂ : x₂.Compatible) : x₁.restrict (le_generate R) = x₂.restrict (le_generate R) → x₁ = x₂ :=
  fun h => by
  rw [← extend_restrict t₁, ← extend_restrict t₂]
  -- Porting note: congr fails to make progress
  apply congr_arg
  exact h

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : x₁.Compatible
t₂ : x₂.Compatible
h : FamilyOfElements.restrict ⋯ x₁ = FamilyOfElements.restrict ⋯ x₂
⊢ FamilyOfElements.restrict ⋯ x₁ = FamilyOfElements.restrict ⋯ x₂

Tactic:
exact h

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : x₁.Compatible
t₂ : x₂.Compatible
h : FamilyOfElements.restrict ⋯ x₁ = FamilyOfElements.restrict ⋯ x₂
⊢ x₁ = x₂

Tactic:
rw [← extend_restrict t₁, ← extend_restrict t₂]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : x₁.Compatible
t₂ : x₂.Compatible
h : FamilyOfElements.restrict ⋯ x₁ = FamilyOfElements.restrict ⋯ x₂
⊢ (FamilyOfElements.restrict ⋯ x₁).sieveExtend = (FamilyOfElements.restrict ⋯ x₂).sieveExtend

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : x₁.Compatible
t₂ : x₂.Compatible
h : FamilyOfElements.restrict ⋯ x₁ = FamilyOfElements.restrict ⋯ x₂
⊢ (FamilyOfElements.restrict ⋯ x₁).sieveExtend = (FamilyOfElements.restrict ⋯ x₂).sieveExtend

Tactic:
apply congr_arg

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : x₁.Compatible
t₂ : x₂.Compatible
h : FamilyOfElements.restrict ⋯ x₁ = FamilyOfElements.restrict ⋯ x₂
⊢ FamilyOfElements.restrict ⋯ x₁ = FamilyOfElements.restrict ⋯ x₂
-- Mathlib/Combinatorics/Additive/ETransform.lean
theorem mulDysonETransform.subset :
    (mulDysonETransform e x).1 * (mulDysonETransform e x).2 ⊆ x.1 * x.2

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ (mulDysonETransform e x).1 * (mulDysonETransform e x).2 ⊆ x.1 * x.2

Tactic:
refine union_mul_inter_subset_union.trans (union_subset Subset.rfl ?_)

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • x.2 * e⁻¹ • x.1 ⊆ x.1 * x.2

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • x.2 * e⁻¹ • x.1 ⊆ x.1 * x.2

Tactic:
rw [mul_smul_comm, smul_mul_assoc, inv_smul_smul, mul_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem smul [WeaklyRegular μ] {x : ℝ≥0∞} (hx : x ≠ ∞) : (x • μ).WeaklyRegular

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.WeaklyRegular
x : ℝ≥0∞
hx : x ≠ ⊤
⊢ (x • μ).WeaklyRegular

Tactic:
haveI := OuterRegular.smul μ hx

Result:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.WeaklyRegular
x : ℝ≥0∞
hx : x ≠ ⊤
this : (x • μ).OuterRegular
⊢ (x • μ).WeaklyRegular

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.WeaklyRegular
x : ℝ≥0∞
hx : x ≠ ⊤
this : (x • μ).OuterRegular
⊢ (x • μ).WeaklyRegular

Tactic:
exact ⟨WeaklyRegular.innerRegular.smul x⟩

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem support_coeff_finSuccEquiv {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {m : Fin n →₀ ℕ} :
    m ∈ ((finSuccEquiv R n f).coeff i).support ↔ m.cons i ∈ f.support

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ m ∈ (((finSuccEquiv R n) f).coeff i).support → cons i m ∈ f.support

Tactic:
intro h

Result:
case mp
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : m ∈ (((finSuccEquiv R n) f).coeff i).support
⊢ cons i m ∈ f.support

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : m ∈ (((finSuccEquiv R n) f).coeff i).support
⊢ cons i m ∈ f.support

Tactic:
simpa [← finSuccEquiv_coeff_coeff] using h

Result:
no goals

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : cons i m ∈ f.support
⊢ m ∈ (((finSuccEquiv R n) f).coeff i).support

Tactic:
simpa [mem_support_iff, ← finSuccEquiv_coeff_coeff m f i] using h

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ m ∈ (((finSuccEquiv R n) f).coeff i).support ↔ cons i m ∈ f.support

Tactic:
apply Iff.intro

Result:
case mp
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ m ∈ (((finSuccEquiv R n) f).coeff i).support → cons i m ∈ f.support

case mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ cons i m ∈ f.support → m ∈ (((finSuccEquiv R n) f).coeff i).support

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ cons i m ∈ f.support → m ∈ (((finSuccEquiv R n) f).coeff i).support

Tactic:
intro h

Result:
case mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : cons i m ∈ f.support
⊢ m ∈ (((finSuccEquiv R n) f).coeff i).support
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem push_inj_right {a b : α} {xs : Vector α n} : xs.push a = xs.push b ↔ a = b :=
  ⟨back_eq_of_push_eq, fun h => by simp [h]⟩

Proof state:
α : Type u_1
n : Nat
a b : α
xs : Vector α n
h : a = b
⊢ xs.push a = xs.push b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma isCircuit_iff_forall_ssubset : M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃I⦄, I ⊂ C → M.Indep I

Proof state:
α : Type u_1
M : Matroid α
C : Set α
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I

Tactic:
rw [IsCircuit, minimal_iff_forall_ssubset, and_congr_right_iff]

Result:
α : Type u_1
M : Matroid α
C : Set α
⊢ M.Dep C → ((∀ ⦃t : Set α⦄, t ⊂ C → ¬M.Dep t) ↔ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I)

Proof state:
α : Type u_1
M : Matroid α
C : Set α
⊢ M.Dep C → ((∀ ⦃t : Set α⦄, t ⊂ C → ¬M.Dep t) ↔ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I)

Tactic:
exact fun h ↦ ⟨fun h' I hIC ↦ ((not_dep_iff (hIC.subset.trans h.subset_ground)).1 (h' hIC)),
  fun h I hIC ↦ (h hIC).not_dep⟩

Result:
no goals
-- Mathlib/Data/Set/Pairwise/Basic.lean
theorem pairwise_iff_exists_forall [Nonempty ι] (s : Set α) (f : α → ι) {r : ι → ι → Prop}
    [IsEquiv ι r] : s.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ s, r (f x) z

Proof state:
α : Type u_1
ι : Type u_4
inst✝¹ : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
⊢ s.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ s, r (f x) z

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hne)

Result:
case inl
α : Type u_1
ι : Type u_4
inst✝¹ : Nonempty ι
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
⊢ ∅.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ ∅, r (f x) z

case inr
α : Type u_1
ι : Type u_4
inst✝¹ : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
hne : s.Nonempty
⊢ s.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ s, r (f x) z

Proof state:
case inl
α : Type u_1
ι : Type u_4
inst✝¹ : Nonempty ι
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
⊢ ∅.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ ∅, r (f x) z

Tactic:
simp

Result:
no goals

Proof state:
case inr
α : Type u_1
ι : Type u_4
inst✝¹ : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
hne : s.Nonempty
⊢ s.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ s, r (f x) z

Tactic:
exact hne.pairwise_iff_exists_forall

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Cartesian.lean
theorem uncurry_id_eq_ev (A X : C) [Exponentiable A] : uncurry (𝟙 (A ⟹ X)) = (exp.ev A).app X

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
A X : C
inst✝ : Exponentiable A
⊢ uncurry (𝟙 (A ⟹ X)) = (exp.ev A).app X

Tactic:
rw [uncurry_eq, whiskerLeft_id_assoc]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem self_diff_frontier (s : Set X) : s \ frontier s = interior s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s \ frontier s = interior s

Tactic:
rw [frontier, diff_diff_right, diff_eq_empty.2 subset_closure,
  inter_eq_self_of_subset_right interior_subset, empty_union]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Hom.lean
lemma of_injective {f : F} (hf : Injective f) [NeZero a] : NeZero (f a) :=
  ⟨by rw [← ZeroHomClass.map_zero f]; exact hf.ne NeZero.out⟩

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : FunLike F α β
inst✝¹ : ZeroHomClass F α β
a : α
f : F
hf : Injective ⇑f
inst✝ : NeZero a
⊢ f a ≠ 0

Tactic:
rw [← ZeroHomClass.map_zero f]

Result:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : FunLike F α β
inst✝¹ : ZeroHomClass F α β
a : α
f : F
hf : Injective ⇑f
inst✝ : NeZero a
⊢ f a ≠ f 0

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : FunLike F α β
inst✝¹ : ZeroHomClass F α β
a : α
f : F
hf : Injective ⇑f
inst✝ : NeZero a
⊢ f a ≠ f 0

Tactic:
exact hf.ne NeZero.out

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem support_single_subset : support (single a r) ⊆ {a}

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
⊢ ((single a) r).support ⊆ {a}

Tactic:
classical exact Pi.support_single_subset

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
⊢ ((single a) r).support ⊆ {a}

Tactic:
exact Pi.support_single_subset

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem biUnion_image_left : (s.biUnion fun a => t.image <| f a) = image₂ f s t :=
  coe_injective <| by
    push_cast
    exact Set.iUnion_image_left _

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ ⋃ x ∈ ↑s, f x '' ↑t = image2 f ↑s ↑t

Tactic:
exact Set.iUnion_image_left _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ ↑(s.biUnion fun a => image (f a) t) = ↑(image₂ f s t)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ ⋃ x ∈ ↑s, f x '' ↑t = image2 f ↑s ↑t
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
/-- See `le_expGrowthSup_mul` for a version with swapped argument `u` and `v`. -/
lemma le_expGrowthSup_mul' {u v : ℕ → ℝ≥0∞} :
    expGrowthInf u + expGrowthSup v ≤ expGrowthSup (u * v)

Proof state:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup v + expGrowthInf u ≤ expGrowthSup (v * u)

Tactic:
exact le_expGrowthSup_mul

Result:
no goals

Proof state:
u v : ℕ → ℝ≥0∞
⊢ expGrowthInf u + expGrowthSup v ≤ expGrowthSup (u * v)

Tactic:
rw [mul_comm, add_comm]

Result:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup v + expGrowthInf u ≤ expGrowthSup (v * u)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem pmap_eq_self {l : Array α} {p : α → Prop} {hp : ∀ (a : α), a ∈ l → p a}
    {f : (a : α) → p a → α} : l.pmap f hp = l ↔ ∀ a (h : a ∈ l), f a (hp a h) = a

Proof state:
α : Type u_1
l : Array α
p : α → Prop
hp : ∀ (a : α), a ∈ l → p a
f : (a : α) → p a → α
⊢ pmap f l hp = l ↔ ∀ (a : α) (h : a ∈ l), f a ⋯ = a

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Prop
f : (a : α) → p a → α
toList✝ : List α
hp : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ pmap f { toList := toList✝ } hp = { toList := toList✝ } ↔ ∀ (a : α) (h : a ∈ { toList := toList✝ }), f a ⋯ = a

Proof state:
case mk
α : Type u_1
p : α → Prop
f : (a : α) → p a → α
toList✝ : List α
hp : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ pmap f { toList := toList✝ } hp = { toList := toList✝ } ↔ ∀ (a : α) (h : a ∈ { toList := toList✝ }), f a ⋯ = a

Tactic:
simp [List.pmap_eq_self]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem insert_erase (h : a ∈ s) : insert a (erase s a) = s :=
  ext fun x => by
    simp only [mem_insert, mem_erase, or_and_left, dec_em, true_and]
    apply or_iff_right_of_imp
    rintro rfl
    exact h

Proof state:
case ha
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
h : x ∈ s
⊢ x ∈ s

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∈ s
x : α
⊢ x ∈ insert a (s.erase a) ↔ x ∈ s

Tactic:
simp only [mem_insert, mem_erase, or_and_left, dec_em, true_and]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∈ s
x : α
⊢ x = a ∨ x ∈ s ↔ x ∈ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∈ s
x : α
⊢ x = a ∨ x ∈ s ↔ x ∈ s

Tactic:
apply or_iff_right_of_imp

Result:
case ha
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∈ s
x : α
⊢ x = a → x ∈ s

Proof state:
case ha
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∈ s
x : α
⊢ x = a → x ∈ s

Tactic:
rintro rfl

Result:
case ha
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
h : x ∈ s
⊢ x ∈ s
-- Mathlib/CategoryTheory/Limits/IsConnected.lean
theorem isConnected_iff_colimit_constPUnitFunctor_iso_pUnit
    [HasColimit (constPUnitFunctor.{w} C)] :
    IsConnected C ↔ Nonempty (colimit (constPUnitFunctor.{w} C) ≅ PUnit)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimit (constPUnitFunctor C)
⊢ IsConnected C ↔ Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})

Tactic:
refine ⟨fun _ => ⟨colimitConstPUnitIsoPUnit.{w} C⟩, fun ⟨h⟩ => ?_⟩

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimit (constPUnitFunctor C)
x✝ : Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})
h : colimit (constPUnitFunctor C) ≅ PUnit.{w + 1}
⊢ IsConnected C

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimit (constPUnitFunctor C)
x✝ : Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})
h : colimit (constPUnitFunctor C) ≅ PUnit.{w + 1}
⊢ IsConnected C

Tactic:
have : Nonempty C := nonempty_of_nonempty_colimit <| Nonempty.map h.inv inferInstance

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimit (constPUnitFunctor C)
x✝ : Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})
h : colimit (constPUnitFunctor C) ≅ PUnit.{w + 1}
this : Nonempty C
⊢ IsConnected C

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimit (constPUnitFunctor C)
x✝ : Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})
h : colimit (constPUnitFunctor C) ≅ PUnit.{w + 1}
this : Nonempty C
c d : C
⊢ Zigzag c d

Tactic:
refine zigzag_of_eqvGen_quot_rel _ (constPUnitFunctor C) ⟨c, PUnit.unit⟩ ⟨d, PUnit.unit⟩ ?_

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimit (constPUnitFunctor C)
x✝ : Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})
h : colimit (constPUnitFunctor C) ≅ PUnit.{w + 1}
this : Nonempty C
c d : C
⊢ Relation.EqvGen (Quot.Rel (constPUnitFunctor C)) ⟨c, PUnit.unit⟩ ⟨d, PUnit.unit⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimit (constPUnitFunctor C)
x✝ : Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})
h : colimit (constPUnitFunctor C) ≅ PUnit.{w + 1}
this : Nonempty C
⊢ IsConnected C

Tactic:
refine zigzag_isConnected <| fun c d => ?_

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimit (constPUnitFunctor C)
x✝ : Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})
h : colimit (constPUnitFunctor C) ≅ PUnit.{w + 1}
this : Nonempty C
c d : C
⊢ Zigzag c d

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimit (constPUnitFunctor C)
x✝ : Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})
h : colimit (constPUnitFunctor C) ≅ PUnit.{w + 1}
this : Nonempty C
c d : C
⊢ Relation.EqvGen (Quot.Rel (constPUnitFunctor C)) ⟨c, PUnit.unit⟩ ⟨d, PUnit.unit⟩

Tactic:
exact colimit_eq <| h.toEquiv.injective rfl

Result:
no goals