harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem symm_eq_on_of_inter_eq_of_eqOn {e' : PartialEquiv α β} (h : e.IsImage s t)
    (hs : e.source ∩ s = e'.source ∩ s) (heq : EqOn e e' (e.source ∩ s)) :
    EqOn e.symm e'.symm (e.target ∩ t)

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ EqOn (↑e.symm) (↑e'.symm) (↑e '' (e.source ∩ s))

Tactic:
rintro y ⟨x, hx, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
⊢ ↑e.symm (↑e x) = ↑e'.symm (↑e x)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
hx' : x ∈ e'.source ∩ s
⊢ ↑e.symm (↑e x) = ↑e'.symm (↑e x)

Tactic:
rw [e.left_inv hx.1, heq hx, e'.left_inv hx'.1]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ EqOn (↑e.symm) (↑e'.symm) (e.target ∩ t)

Tactic:
rw [← h.image_eq]

Result:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ EqOn (↑e.symm) (↑e'.symm) (↑e '' (e.source ∩ s))

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
⊢ ↑e.symm (↑e x) = ↑e'.symm (↑e x)

Tactic:
have hx' := hx

Result:
case intro.intro
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx hx' : x ∈ e.source ∩ s
⊢ ↑e.symm (↑e x) = ↑e'.symm (↑e x)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx hx' : x ∈ e.source ∩ s
⊢ ↑e.symm (↑e x) = ↑e'.symm (↑e x)

Tactic:
rw [hs] at hx'

Result:
case intro.intro
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
hx' : x ∈ e'.source ∩ s
⊢ ↑e.symm (↑e x) = ↑e'.symm (↑e x)
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem subseq_forall_of_frequently {ι : Type*} {x : ℕ → ι} {p : ι → Prop} {l : Filter ι}
    (h_tendsto : Tendsto x atTop l) (h : ∃ᶠ n in atTop, p (x n)) :
    ∃ ns : ℕ → ℕ, Tendsto (fun n => x (ns n)) atTop l ∧ ∀ n, p (x (ns n))

Proof state:
ι : Type u_6
x : ℕ → ι
p : ι → Prop
l : Filter ι
h_tendsto : Tendsto x atTop l
h : ∃ᶠ (n : ℕ) in atTop, p (x n)
ns : ℕ → ℕ
hge : ∀ (a : ℕ), ns a ≥ a
hns : ∀ (a : ℕ), p (x (ns a))
⊢ ∃ ns, Tendsto (fun n => x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))

Tactic:
exact ⟨ns, h_tendsto.comp (tendsto_atTop_mono hge tendsto_id), hns⟩

Result:
no goals

Proof state:
ι : Type u_6
x : ℕ → ι
p : ι → Prop
l : Filter ι
h_tendsto : Tendsto x atTop l
h : ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto (fun n => x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))

Tactic:
choose ns hge hns using frequently_atTop.1 h

Result:
ι : Type u_6
x : ℕ → ι
p : ι → Prop
l : Filter ι
h_tendsto : Tendsto x atTop l
h : ∃ᶠ (n : ℕ) in atTop, p (x n)
ns : ℕ → ℕ
hge : ∀ (a : ℕ), ns a ≥ a
hns : ∀ (a : ℕ), p (x (ns a))
⊢ ∃ ns, Tendsto (fun n => x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem isBounded_range_of_tendsto_cofinite_uniformity {f : β → α}
    (hf : Tendsto (Prod.map f f) (.cofinite ×ˢ .cofinite) (𝓤 α)) : IsBounded (range f)

Proof state:
case intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}
⊢ Bornology.IsBounded (f '' ?m.49269 ∪ f '' ?m.49269ᶜ)

α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}
⊢ Set β

Tactic:
refine (hsf.image f).isBounded.union (isBounded_image_iff.2 ⟨1, fun x hx y hy ↦ ?_⟩)

Result:
case intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}
x : β
hx : x ∈ sᶜ
y : β
hy : y ∈ sᶜ
⊢ dist (f x) (f y) ≤ 1

Proof state:
case intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}
⊢ Bornology.IsBounded (range f)

Tactic:
rw [← image_union_image_compl_eq_range]

Result:
case intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}
⊢ Bornology.IsBounded (f '' ?m.49269 ∪ f '' ?m.49269ᶜ)

α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}
⊢ Set β

Proof state:
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
⊢ Bornology.IsBounded (range f)

Tactic:
rcases (hasBasis_cofinite.prod_self.tendsto_iff uniformity_basis_dist).1 hf 1 zero_lt_one with
  ⟨s, hsf, hs1⟩

Result:
case intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}
⊢ Bornology.IsBounded (range f)

Proof state:
case intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}
x : β
hx : x ∈ sᶜ
y : β
hy : y ∈ sᶜ
⊢ dist (f x) (f y) ≤ 1

Tactic:
exact le_of_lt (hs1 (x, y) ⟨hx, hy⟩)

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/Seminorm.lean
/-- Equivalence of multiplicative ring norms is transitive. -/
@[deprecated "Use AbsoluteValue.isEquiv_trans instead" (since := "2025-01-07")]
lemma equiv_trans {f g k : MulRingNorm R} (hfg : equiv f g) (hgk : equiv g k) :
    equiv f k

Proof state:
case intro.intro
R : Type u_2
inst✝ : Ring R
f g k : MulRingNorm R
hgk : g.equiv k
c : ℝ
hcPos : 0 < c
hfg : (fun x => f x ^ c) = ⇑g
⊢ f.equiv k

Tactic:
rcases hgk with ⟨d, hdPos, hgk⟩

Result:
case intro.intro.intro.intro
R : Type u_2
inst✝ : Ring R
f g k : MulRingNorm R
c : ℝ
hcPos : 0 < c
hfg : (fun x => f x ^ c) = ⇑g
d : ℝ
hdPos : 0 < d
hgk : (fun x => g x ^ d) = ⇑k
⊢ f.equiv k

Proof state:
case intro.intro.intro.intro
R : Type u_2
inst✝ : Ring R
f g k : MulRingNorm R
c : ℝ
hcPos : 0 < c
hfg : (fun x => f x ^ c) = ⇑g
d : ℝ
hdPos : 0 < d
hgk : (fun x => g x ^ d) = ⇑k
⊢ (fun x => f x ^ (c * d)) = ⇑k

Tactic:
ext x

Result:
case intro.intro.intro.intro.h
R : Type u_2
inst✝ : Ring R
f g k : MulRingNorm R
c : ℝ
hcPos : 0 < c
hfg : (fun x => f x ^ c) = ⇑g
d : ℝ
hdPos : 0 < d
hgk : (fun x => g x ^ d) = ⇑k
x : R
⊢ f x ^ (c * d) = k x

Proof state:
R : Type u_2
inst✝ : Ring R
f g k : MulRingNorm R
hfg : f.equiv g
hgk : g.equiv k
⊢ f.equiv k

Tactic:
rcases hfg with ⟨c, hcPos, hfg⟩

Result:
case intro.intro
R : Type u_2
inst✝ : Ring R
f g k : MulRingNorm R
hgk : g.equiv k
c : ℝ
hcPos : 0 < c
hfg : (fun x => f x ^ c) = ⇑g
⊢ f.equiv k

Proof state:
case intro.intro.intro.intro.h
R : Type u_2
inst✝ : Ring R
f g k : MulRingNorm R
c : ℝ
hcPos : 0 < c
hfg : (fun x => f x ^ c) = ⇑g
d : ℝ
hdPos : 0 < d
hgk : (fun x => g x ^ d) = ⇑k
x : R
⊢ f x ^ (c * d) = k x

Tactic:
rw [Real.rpow_mul (apply_nonneg f x), congr_fun hfg x, congr_fun hgk x]

Result:
no goals

Proof state:
case intro.intro.intro.intro
R : Type u_2
inst✝ : Ring R
f g k : MulRingNorm R
c : ℝ
hcPos : 0 < c
hfg : (fun x => f x ^ c) = ⇑g
d : ℝ
hdPos : 0 < d
hgk : (fun x => g x ^ d) = ⇑k
⊢ f.equiv k

Tactic:
refine ⟨c*d, (mul_pos_iff_of_pos_left hcPos).mpr hdPos, ?_⟩

Result:
case intro.intro.intro.intro
R : Type u_2
inst✝ : Ring R
f g k : MulRingNorm R
c : ℝ
hcPos : 0 < c
hfg : (fun x => f x ^ c) = ⇑g
d : ℝ
hdPos : 0 < d
hgk : (fun x => g x ^ d) = ⇑k
⊢ (fun x => f x ^ (c * d)) = ⇑k
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.unitOfList_eq [BEq α] [Hashable α] {l : List α} :
    Raw.Const.unitOfList l = Raw₀.Const.insertManyIfNewUnit Raw₀.empty l

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
l : List α
⊢ Raw.Const.unitOfList l = (Raw₀.Const.insertManyIfNewUnit Raw₀.empty l).val.val

Tactic:
simp only [Raw.Const.unitOfList, Raw.Const.insertManyIfNewUnit, (Raw.WF.empty).size_buckets_pos ∅,
  ↓reduceDIte]

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
l : List α
⊢ (Raw₀.Const.insertManyIfNewUnit ⟨∅, ⋯⟩ l).val.val = (Raw₀.Const.insertManyIfNewUnit Raw₀.empty l).val.val

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
l : List α
⊢ (Raw₀.Const.insertManyIfNewUnit ⟨∅, ⋯⟩ l).val.val = (Raw₀.Const.insertManyIfNewUnit Raw₀.empty l).val.val

Tactic:
congr

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem abs_edgeDensity_sub_edgeDensity_le_one_sub_mul (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁)
    (hs₂ : s₂.Nonempty) (ht₂ : t₂.Nonempty) :
    |edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁| ≤ 1 - #s₂ / #s₁ * (#t₂ / #t₁)

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ edgeDensity (fun x y => ¬r x y) s₂ t₂ - edgeDensity (fun x y => ¬r x y) s₁ t₁ ≤
    1 - ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁))

Tactic:
exact edgeDensity_sub_edgeDensity_le_one_sub_mul _ hs ht hs₂ ht₂

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ |edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁| ≤ 1 - ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁))

Tactic:
refine abs_sub_le_iff.2 ⟨edgeDensity_sub_edgeDensity_le_one_sub_mul r hs ht hs₂ ht₂, ?_⟩

Result:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ edgeDensity r s₁ t₁ - edgeDensity r s₂ t₂ ≤ 1 - ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁))

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ edgeDensity r s₁ t₁ - edgeDensity r s₂ t₂ ≤ 1 - ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁))

Tactic:
rw [← add_sub_cancel_right (edgeDensity r s₁ t₁) (edgeDensity (fun x y ↦ ¬r x y) s₁ t₁),
  ← add_sub_cancel_right (edgeDensity r s₂ t₂) (edgeDensity (fun x y ↦ ¬r x y) s₂ t₂),
  edgeDensity_add_edgeDensity_compl _ (hs₂.mono hs) (ht₂.mono ht),
  edgeDensity_add_edgeDensity_compl _ hs₂ ht₂, sub_sub_sub_cancel_left]

Result:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ edgeDensity (fun x y => ¬r x y) s₂ t₂ - edgeDensity (fun x y => ¬r x y) s₁ t₁ ≤
    1 - ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁))
-- Mathlib/Order/Hom/Bounded.lean
theorem map_eq_top_iff [LE α] [OrderTop α] [PartialOrder β] [OrderTop β] [OrderIsoClass F α β]
    (f : F) {a : α} : f a = ⊤ ↔ a = ⊤

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : EquivLike F α β
inst✝⁴ : LE α
inst✝³ : OrderTop α
inst✝² : PartialOrder β
inst✝¹ : OrderTop β
inst✝ : OrderIsoClass F α β
f : F
a : α
this : TopHomClass F α β := OrderIsoClass.toTopHomClass
⊢ f a = ⊤ ↔ a = ⊤

Tactic:
rw [← map_top f, (EquivLike.injective f).eq_iff]

Result:
no goals

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : EquivLike F α β
inst✝⁴ : LE α
inst✝³ : OrderTop α
inst✝² : PartialOrder β
inst✝¹ : OrderTop β
inst✝ : OrderIsoClass F α β
f : F
a : α
⊢ f a = ⊤ ↔ a = ⊤

Tactic:
letI : TopHomClass F α β := OrderIsoClass.toTopHomClass

Result:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : EquivLike F α β
inst✝⁴ : LE α
inst✝³ : OrderTop α
inst✝² : PartialOrder β
inst✝¹ : OrderTop β
inst✝ : OrderIsoClass F α β
f : F
a : α
this : TopHomClass F α β := OrderIsoClass.toTopHomClass
⊢ f a = ⊤ ↔ a = ⊤
-- Mathlib/MeasureTheory/Measure/MutuallySingular.lean
theorem add_left_iff : μ₁ + μ₂ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ ν : Measure α
⊢ μ₁ + μ₂ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν

Tactic:
rw [← sum_cond, sum_left, Bool.forall_bool, cond, cond, and_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem HasStrictFDerivAt.cpow (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x)
    (h0 : f x ∈ slitPlane) : HasStrictFDerivAt (fun x => f x ^ g x)
      ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
f' g' : E →L[ℂ] ℂ
x : E
hf : HasStrictFDerivAt f f' x
hg : HasStrictFDerivAt g g' x
h0 : f x ∈ slitPlane
⊢ HasStrictFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x

Tactic:
convert (@hasStrictFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp x (hf.prod hg)

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
private lemma pairwiseDisjoint_fibers : Set.PairwiseDisjoint ↑t fun a ↦ s.filter (f · = a) :=
  fun x' hx y' hy hne ↦ by
    simp_rw [disjoint_left, mem_filter]; rintro i ⟨_, rfl⟩ ⟨_, rfl⟩; exact hne rfl

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
i : α
left✝¹ : i ∈ s
hx : f i ∈ ↑t
left✝ : i ∈ s
hy : f i ∈ ↑t
hne : f i ≠ f i
⊢ False

Tactic:
exact hne rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
x' : β
hx : x' ∈ ↑t
y' : β
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ ∀ ⦃a : α⦄, a ∈ s ∧ f a = x' → ¬(a ∈ s ∧ f a = y')

Tactic:
rintro i ⟨_, rfl⟩ ⟨_, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
i : α
left✝¹ : i ∈ s
hx : f i ∈ ↑t
left✝ : i ∈ s
hy : f i ∈ ↑t
hne : f i ≠ f i
⊢ False

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
x' : β
hx : x' ∈ ↑t
y' : β
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ Function.onFun Disjoint (fun a => filter (fun x => f x = a) s) x' y'

Tactic:
simp_rw [disjoint_left, mem_filter]

Result:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
x' : β
hx : x' ∈ ↑t
y' : β
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ ∀ ⦃a : α⦄, a ∈ s ∧ f a = x' → ¬(a ∈ s ∧ f a = y')
-- Mathlib/RingTheory/Idempotents.lean
lemma OrthogonalIdempotents.option (he : OrthogonalIdempotents e) [Fintype I] (x)
    (hx : IsIdempotentElem x) (hx₁ : x * ∑ i, e i = 0) (hx₂ : (∑ i, e i) * x = 0) :
    OrthogonalIdempotents (Option.elim · x e) where
  idem i := i.rec hx he.idem
  ortho i j ne

Proof state:
case some.some
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i : I, e i = 0
hx₂ : (∑ i : I, e i) * x = 0
i j : I
ne : some i ≠ some j
⊢ (some i).elim x e * (some j).elim x e = 0

Tactic:
exact he.ortho (Option.some_inj.ne.mp ne)

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i : I, e i = 0
hx₂ : (∑ i : I, e i) * x = 0
i j : Option I
ne : i ≠ j
⊢ (fun x1 x2 => x1.elim x e * x2.elim x e = 0) i j

Tactic:
rcases i with - | i <;> rcases j with - | j

Result:
case none.none
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i : I, e i = 0
hx₂ : (∑ i : I, e i) * x = 0
ne : none ≠ none
⊢ none.elim x e * none.elim x e = 0

case none.some
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i : I, e i = 0
hx₂ : (∑ i : I, e i) * x = 0
j : I
ne : none ≠ some j
⊢ none.elim x e * (some j).elim x e = 0

case some.none
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i : I, e i = 0
hx₂ : (∑ i : I, e i) * x = 0
i : I
ne : some i ≠ none
⊢ (some i).elim x e * none.elim x e = 0

case some.some
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i : I, e i = 0
hx₂ : (∑ i : I, e i) * x = 0
i j : I
ne : some i ≠ some j
⊢ (some i).elim x e * (some j).elim x e = 0

Proof state:
case none.none
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i : I, e i = 0
hx₂ : (∑ i : I, e i) * x = 0
ne : none ≠ none
⊢ none.elim x e * none.elim x e = 0

Tactic:
cases ne rfl

Result:
no goals
-- Mathlib/Topology/Sheaves/Stalks.lean
theorem app_injective_of_stalkFunctor_map_injective {F : Sheaf C X} {G : Presheaf C X} (f : F.1 ⟶ G)
    (U : Opens X) (h : ∀ x ∈ U, Function.Injective ((stalkFunctor C x).map f)) :
    Function.Injective (f.app (op U)) := fun s t hst =>
  section_ext F _ _ _ fun x hx =>
    h x hx <| by rw [stalkFunctor_map_germ_apply, stalkFunctor_map_germ_apply, hst]

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
G : Presheaf C X
f : F.val ⟶ G
U : Opens ↑X
h : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f))
s t : CC (F.val.obj (op U))
hst : (ConcreteCategory.hom (f.app (op U))) s = (ConcreteCategory.hom (f.app (op U))) t
x : ↑X
hx : x ∈ U
⊢ (ConcreteCategory.hom ((stalkFunctor C x).map f)) ((ConcreteCategory.hom (F.presheaf.germ U x hx)) s) =
    (ConcreteCategory.hom ((stalkFunctor C x).map f)) ((ConcreteCategory.hom (F.presheaf.germ U x hx)) t)

Tactic:
rw [stalkFunctor_map_germ_apply, stalkFunctor_map_germ_apply, hst]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem oangle_rotation (x y : V) (θ : Real.Angle) :
    o.oangle (o.rotation θ x) (o.rotation θ y) = o.oangle x y

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
⊢ o.oangle ((o.rotation θ) x) ((o.rotation θ) y) = o.oangle x y

Tactic:
by_cases hx : x = 0 <;> by_cases hy : y = 0 <;> simp [hx, hy]

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
@[simp]
lemma π_single (g : relations.G) :
    solution.π (Finsupp.single g 1) = solution.var g

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
g : relations.G
⊢ solution.π (Finsupp.single g 1) = solution.var g

Tactic:
simp [π]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem set_set (a b : α) : ∀ (l : List α) (n : Nat), (l.set n a).set n b = l.set n b
  | [], _ => by simp
  | _ :: _, 0 => by simp [set]
  | _ :: _, _+1 => by simp [set, set_set]

Proof state:
α : Type u_1
a b head✝ : α
tail✝ : List α
⊢ ((head✝ :: tail✝).set 0 a).set 0 b = (head✝ :: tail✝).set 0 b

Tactic:
simp [set]

Result:
no goals

Proof state:
α : Type u_1
a b head✝ : α
tail✝ : List α
n✝ : Nat
⊢ ((head✝ :: tail✝).set (n✝ + 1) a).set (n✝ + 1) b = (head✝ :: tail✝).set (n✝ + 1) b

Tactic:
simp [set, set_set]

Result:
no goals

Proof state:
α : Type u_1
a b : α
x✝ : Nat
⊢ ([].set x✝ a).set x✝ b = [].set x✝ b

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem update_eq_erase_add_single (f : α →₀ M) (a : α) (b : M) :
    f.update a b = f.erase a + single a b

Proof state:
case h.inr
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
h : a ≠ j
⊢ (f.update a b) j = (erase a f + single a b) j

Tactic:
simp [Function.update_of_ne h.symm, single_apply, h, erase_ne, h.symm]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
⊢ f.update a b = erase a f + single a b

Tactic:
ext j

Result:
case h
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
⊢ (f.update a b) j = (erase a f + single a b) j

Proof state:
case h.inl
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
⊢ (f.update a b) a = (erase a f + single a b) a

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
⊢ (f.update a b) j = (erase a f + single a b) j

Tactic:
rcases eq_or_ne a j with (rfl | h)

Result:
case h.inl
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
⊢ (f.update a b) a = (erase a f + single a b) a

case h.inr
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
h : a ≠ j
⊢ (f.update a b) j = (erase a f + single a b) j
-- Mathlib/Order/Basic.lean
theorem min_def' [LinearOrder α] (a b : α) : min a b = if b ≤ a then b else a

Proof state:
α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a

Tactic:
rcases lt_trichotomy a b with (lt | eq | gt)

Result:
case inl
α : Type u_2
inst✝ : LinearOrder α
a b : α
lt : a < b
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a

case inr.inl
α : Type u_2
inst✝ : LinearOrder α
a b : α
eq : a = b
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a

case inr.inr
α : Type u_2
inst✝ : LinearOrder α
a b : α
gt : b < a
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a

Proof state:
case inr.inr
α : Type u_2
inst✝ : LinearOrder α
a b : α
gt : b < a
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a

Tactic:
rw [if_neg (not_le.mpr gt.gt), if_pos gt.le]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ a ⊓ b = if b ≤ a then b else a

Tactic:
rw [min_def]

Result:
α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a

Proof state:
case inr.inl
α : Type u_2
inst✝ : LinearOrder α
a b : α
eq : a = b
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a

Tactic:
rw [if_pos eq.le, if_pos eq.ge, eq]

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝ : LinearOrder α
a b : α
lt : a < b
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a

Tactic:
rw [if_pos lt.le, if_neg (not_le.mpr lt)]

Result:
no goals