harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem gcd_union (s₁ s₂ : Multiset α) : (s₁ ∪ s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

Tactic:
rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add]

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem reverse_ins [inst : @OrientedCmp α cmp] {t : RBNode α} :
    (ins cmp x t).reverse = ins (flip cmp) x t.reverse

Proof state:
case node
α : Type u_1
cmp : α → α → Ordering
x : α
inst : OrientedCmp cmp
c : RBColor
a : RBNode α
y : α
b : RBNode α
iha : (ins cmp x a).reverse = ins (flip cmp) x a.reverse
ihb : (ins cmp x b).reverse = ins (flip cmp) x b.reverse
⊢ (ins cmp x (node c a y b)).reverse = ins (flip cmp) x (node c a y b).reverse

Tactic:
cases c

Result:
case node.red
α : Type u_1
cmp : α → α → Ordering
x : α
inst : OrientedCmp cmp
a : RBNode α
y : α
b : RBNode α
iha : (ins cmp x a).reverse = ins (flip cmp) x a.reverse
ihb : (ins cmp x b).reverse = ins (flip cmp) x b.reverse
⊢ (ins cmp x (node red a y b)).reverse = ins (flip cmp) x (node red a y b).reverse

case node.black
α : Type u_1
cmp : α → α → Ordering
x : α
inst : OrientedCmp cmp
a : RBNode α
y : α
b : RBNode α
iha : (ins cmp x a).reverse = ins (flip cmp) x a.reverse
ihb : (ins cmp x b).reverse = ins (flip cmp) x b.reverse
⊢ (ins cmp x (node black a y b)).reverse = ins (flip cmp) x (node black a y b).reverse

Proof state:
α : Type u_1
cmp : α → α → Ordering
x : α
inst : OrientedCmp cmp
t : RBNode α
⊢ (ins cmp x t).reverse = ins (flip cmp) x t.reverse

Tactic:
induction t <;> [skip; (rename_i c a y b iha ihb; cases c)] <;> simp [ins, flip]
  <;> rw [← inst.symm x y] <;> split <;> simp [*, Ordering.swap, iha, ihb]

Result:
no goals

Proof state:
case node
α : Type u_1
cmp : α → α → Ordering
x : α
inst : OrientedCmp cmp
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : (ins cmp x l✝).reverse = ins (flip cmp) x l✝.reverse
r_ih✝ : (ins cmp x r✝).reverse = ins (flip cmp) x r✝.reverse
⊢ (ins cmp x (node c✝ l✝ v✝ r✝)).reverse = ins (flip cmp) x (node c✝ l✝ v✝ r✝).reverse

Tactic:
rename_i c a y b iha ihb

Result:
case node
α : Type u_1
cmp : α → α → Ordering
x : α
inst : OrientedCmp cmp
c : RBColor
a : RBNode α
y : α
b : RBNode α
iha : (ins cmp x a).reverse = ins (flip cmp) x a.reverse
ihb : (ins cmp x b).reverse = ins (flip cmp) x b.reverse
⊢ (ins cmp x (node c a y b)).reverse = ins (flip cmp) x (node c a y b).reverse
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_append_right {as bs : Array α} {i : Nat} (h : as.size ≤ i) :
    (as ++ bs)[i]? = bs[i - as.size]?

Proof state:
case mk.mk
α : Type u_1
i : Nat
toList✝¹ : List α
h : { toList := toList✝¹ }.size ≤ i
toList✝ : List α
⊢ ({ toList := toList✝¹ } ++ { toList := toList✝ })[i]? = { toList := toList✝ }[i - { toList := toList✝¹ }.size]?

Tactic:
simp at h

Result:
case mk.mk
α : Type u_1
i : Nat
toList✝¹ toList✝ : List α
h : toList✝¹.length ≤ i
⊢ ({ toList := toList✝¹ } ++ { toList := toList✝ })[i]? = { toList := toList✝ }[i - { toList := toList✝¹ }.size]?

Proof state:
case mk.mk
α : Type u_1
i : Nat
toList✝¹ toList✝ : List α
h : toList✝¹.length ≤ i
⊢ ({ toList := toList✝¹ } ++ { toList := toList✝ })[i]? = { toList := toList✝ }[i - { toList := toList✝¹ }.size]?

Tactic:
simp [List.getElem?_append_right, h]

Result:
no goals

Proof state:
case mk
α : Type u_1
bs : Array α
i : Nat
toList✝ : List α
h : { toList := toList✝ }.size ≤ i
⊢ ({ toList := toList✝ } ++ bs)[i]? = bs[i - { toList := toList✝ }.size]?

Tactic:
cases bs

Result:
case mk.mk
α : Type u_1
i : Nat
toList✝¹ : List α
h : { toList := toList✝¹ }.size ≤ i
toList✝ : List α
⊢ ({ toList := toList✝¹ } ++ { toList := toList✝ })[i]? = { toList := toList✝ }[i - { toList := toList✝¹ }.size]?

Proof state:
α : Type u_1
as bs : Array α
i : Nat
h : as.size ≤ i
⊢ (as ++ bs)[i]? = bs[i - as.size]?

Tactic:
cases as

Result:
case mk
α : Type u_1
bs : Array α
i : Nat
toList✝ : List α
h : { toList := toList✝ }.size ≤ i
⊢ ({ toList := toList✝ } ++ bs)[i]? = bs[i - { toList := toList✝ }.size]?
-- Mathlib/Algebra/Star/Pi.lean
theorem star_sumElim {I J α : Type*} (x : I → α) (y : J → α) [Star α] :
    star (Sum.elim x y) = Sum.elim (star x) (star y)

Proof state:
case h
I : Type u_1
J : Type u_2
α : Type u_3
x✝ : I → α
y : J → α
inst✝ : Star α
x : I ⊕ J
⊢ star (Sum.elim x✝ y) x = Sum.elim (star x✝) (star y) x

Tactic:
cases x <;> simp only [Pi.star_apply, Sum.elim_inl, Sum.elim_inr]

Result:
no goals

Proof state:
I : Type u_1
J : Type u_2
α : Type u_3
x : I → α
y : J → α
inst✝ : Star α
⊢ star (Sum.elim x y) = Sum.elim (star x) (star y)

Tactic:
ext x

Result:
case h
I : Type u_1
J : Type u_2
α : Type u_3
x✝ : I → α
y : J → α
inst✝ : Star α
x : I ⊕ J
⊢ star (Sum.elim x✝ y) x = Sum.elim (star x✝) (star y) x
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_self_im (x : F) : im ⟪x, x⟫ = 0

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ I * ((starRingEnd 𝕜) ⟪x, x⟫_𝕜 - ⟪x, x⟫_𝕜) / 2 = ↑0

Tactic:
simp [inner_conj_symm]

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ im ⟪x, x⟫_𝕜 = 0

Tactic:
rw [← @ofReal_inj 𝕜, im_eq_conj_sub]

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ I * ((starRingEnd 𝕜) ⟪x, x⟫_𝕜 - ⟪x, x⟫_𝕜) / 2 = ↑0
-- Mathlib/Combinatorics/Additive/Energy.lean
@[to_additive (attr := simp)]
lemma mulEnergy_univ_left : Eₘ[univ, t] = Fintype.card α * t.card ^ 2

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
⊢ Eₘ[univ, t] = Fintype.card α * #t ^ 2

Tactic:
simp only [mulEnergy, univ_product_univ, Fintype.card, sq, ← card_product]

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
⊢ #(filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) (univ ×ˢ t ×ˢ t)) = #(univ ×ˢ t ×ˢ t)

Proof state:
case e_s.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
a : (α × α) × α × α
⊢ (a.2.1 ∈ t ∧ a.2.2 ∈ t) ∧ a.1.1 * a.2.1 = a.1.2 * a.2.2 ↔ ∃ a_1 a_2 b, (a_2 ∈ t ∧ b ∈ t) ∧ f (a_1, a_2, b) = a

Tactic:
refine ⟨fun h => ⟨a.1.1 * a.2.2⁻¹, _, _, h.1, by simp [f, mul_right_comm, h.2]⟩, ?_⟩

Result:
case e_s.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
a : (α × α) × α × α
⊢ (∃ a_1 a_2 b, (a_2 ∈ t ∧ b ∈ t) ∧ f (a_1, a_2, b) = a) → (a.2.1 ∈ t ∧ a.2.2 ∈ t) ∧ a.1.1 * a.2.1 = a.1.2 * a.2.2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mem_mapIdx {b : β} {l : Array α} :
    b ∈ mapIdx f l ↔ ∃ (i : Nat) (h : i < l.size), f i l[i] = b

Proof state:
case mpr.intro.intro
β : Type u_1
α : Type u_2
f : Nat → α → β
l : Array α
i : Nat
h : i < l.size
⊢ f i l[i] ∈ mapIdx f l

Tactic:
rw [mem_iff_getElem]

Result:
case mpr.intro.intro
β : Type u_1
α : Type u_2
f : Nat → α → β
l : Array α
i : Nat
h : i < l.size
⊢ ∃ i_1 h_1, (mapIdx f l)[i_1] = f i l[i]

Proof state:
case mpr
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : Array α
⊢ (∃ i h, f i l[i] = b) → b ∈ mapIdx f l

Tactic:
rintro ⟨i, h, rfl⟩

Result:
case mpr.intro.intro
β : Type u_1
α : Type u_2
f : Nat → α → β
l : Array α
i : Nat
h : i < l.size
⊢ f i l[i] ∈ mapIdx f l

Proof state:
β : Type u_1
α : Type u_2
f : Nat → α → β
l : Array α
i : Nat
h : i < l.size
⊢ (mapIdx f l)[i] = f i l[i]

Tactic:
simp

Result:
no goals

Proof state:
case mp
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : Array α
h : b ∈ mapIdx f l
⊢ ∃ i h, f i l[i] = b

Tactic:
exact exists_of_mem_mapIdx h

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : Array α
⊢ b ∈ mapIdx f l ↔ ∃ i h, f i l[i] = b

Tactic:
constructor

Result:
case mp
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : Array α
⊢ b ∈ mapIdx f l → ∃ i h, f i l[i] = b

case mpr
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : Array α
⊢ (∃ i h, f i l[i] = b) → b ∈ mapIdx f l

Proof state:
case mp
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : Array α
⊢ b ∈ mapIdx f l → ∃ i h, f i l[i] = b

Tactic:
intro h

Result:
case mp
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : Array α
h : b ∈ mapIdx f l
⊢ ∃ i h, f i l[i] = b

Proof state:
case mpr.intro.intro
β : Type u_1
α : Type u_2
f : Nat → α → β
l : Array α
i : Nat
h : i < l.size
⊢ ∃ i_1 h_1, (mapIdx f l)[i_1] = f i l[i]

Tactic:
exact ⟨i, by simpa using h, by simp⟩

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
f : Nat → α → β
l : Array α
i : Nat
h : i < l.size
⊢ i < (mapIdx f l).size

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Topology/VectorBundle/Basic.lean
theorem symmₗ_linearMapAt (e : Pretrivialization F (π F E)) [e.IsLinear R] {b : B}
    (hb : b ∈ e.baseSet) (y : E b) : e.symmₗ R b (e.linearMapAt R b y) = y

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
y : E b
⊢ (Pretrivialization.symmₗ R e b) ((Pretrivialization.linearMapAt R e b) y) = y

Tactic:
rw [e.linearMapAt_def_of_mem hb]

Result:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
y : E b
⊢ (Pretrivialization.symmₗ R e b) (↑(linearEquivAt R e b hb) y) = y

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
y : E b
⊢ (Pretrivialization.symmₗ R e b) (↑(linearEquivAt R e b hb) y) = y

Tactic:
exact (e.linearEquivAt R b hb).left_inv y

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem eventually_homothety_image_subset_of_finite_subset_interior (x : Q) {s : Set Q} {t : Set Q}
    (ht : t.Finite) (h : t ⊆ interior s) : ∀ᶠ δ in 𝓝 (1 : 𝕜), homothety x δ '' t ⊆ s

Proof state:
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : t.Finite
h : t ⊆ interior s
this : ∀ y ∈ t, ∀ᶠ (δ : 𝕜) in 𝓝 1, (homothety x δ) y ∈ s
⊢ ∀ᶠ (δ : 𝕜) in 𝓝 1, t ⊆ ⇑(homothety x δ) ⁻¹' s

Tactic:
exact (Filter.eventually_all_finite ht).mpr this

Result:
no goals

Proof state:
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : t.Finite
h : t ⊆ interior s
y : Q
hy : y ∈ t
⊢ ∀ᶠ (δ : 𝕜) in 𝓝 1, (homothety x δ) y ∈ s

Tactic:
exact eventually_homothety_mem_of_mem_interior 𝕜 x (h hy)

Result:
no goals

Proof state:
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : t.Finite
h : t ⊆ interior s
⊢ ∀ y ∈ t, ∀ᶠ (δ : 𝕜) in 𝓝 1, (homothety x δ) y ∈ s

Tactic:
intro y hy

Result:
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : t.Finite
h : t ⊆ interior s
y : Q
hy : y ∈ t
⊢ ∀ᶠ (δ : 𝕜) in 𝓝 1, (homothety x δ) y ∈ s

Proof state:
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : t.Finite
h : t ⊆ interior s
this : ∀ y ∈ t, ∀ᶠ (δ : 𝕜) in 𝓝 1, (homothety x δ) y ∈ s
⊢ ∀ᶠ (δ : 𝕜) in 𝓝 1, ⇑(homothety x δ) '' t ⊆ s

Tactic:
simp_rw [Set.image_subset_iff]

Result:
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : t.Finite
h : t ⊆ interior s
this : ∀ y ∈ t, ∀ᶠ (δ : 𝕜) in 𝓝 1, (homothety x δ) y ∈ s
⊢ ∀ᶠ (δ : 𝕜) in 𝓝 1, t ⊆ ⇑(homothety x δ) ⁻¹' s

Proof state:
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : t.Finite
h : t ⊆ interior s
⊢ ∀ᶠ (δ : 𝕜) in 𝓝 1, ⇑(homothety x δ) '' t ⊆ s

Tactic:
suffices ∀ y ∈ t, ∀ᶠ δ in 𝓝 (1 : 𝕜), homothety x δ y ∈ s by
  simp_rw [Set.image_subset_iff]
  exact (Filter.eventually_all_finite ht).mpr this

Result:
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : t.Finite
h : t ⊆ interior s
⊢ ∀ y ∈ t, ∀ᶠ (δ : 𝕜) in 𝓝 1, (homothety x δ) y ∈ s
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem extract_zero_endPos : ∀ (s : String), s.extract 0 (endPos s) = s
  | ⟨[]⟩ => rfl
  | ⟨c :: cs⟩ => by
    simp only [extract, Pos.byteIdx_zero, endPos_eq, utf8Len_cons, ge_iff_le, Nat.le_zero_eq,
      Nat.ne_of_gt add_utf8Size_pos, ↓reduceIte]
    congr
    apply extract.go₁_zero_utf8Len

Proof state:
case e_data
c : Char
cs : List Char
⊢ extract.go₁ (c :: cs) 0 0 { byteIdx := utf8Len cs + c.utf8Size } = c :: cs

Tactic:
apply extract.go₁_zero_utf8Len

Result:
no goals

Proof state:
c : Char
cs : List Char
⊢ { data := extract.go₁ (c :: cs) 0 0 { byteIdx := utf8Len cs + c.utf8Size } } = { data := c :: cs }

Tactic:
congr

Result:
case e_data
c : Char
cs : List Char
⊢ extract.go₁ (c :: cs) 0 0 { byteIdx := utf8Len cs + c.utf8Size } = c :: cs

Proof state:
c : Char
cs : List Char
⊢ { data := c :: cs }.extract 0 { data := c :: cs }.endPos = { data := c :: cs }

Tactic:
simp only [extract, Pos.byteIdx_zero, endPos_eq, utf8Len_cons, ge_iff_le, Nat.le_zero_eq,
  Nat.ne_of_gt add_utf8Size_pos, ↓reduceIte]

Result:
c : Char
cs : List Char
⊢ { data := extract.go₁ (c :: cs) 0 0 { byteIdx := utf8Len cs + c.utf8Size } } = { data := c :: cs }
-- Mathlib/Order/Birkhoff.lean
@[simp] lemma supIrred_Iic (a : α) : SupIrred (Iic a)

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ SupIrred (Iic a)

Tactic:
refine ⟨fun h ↦ Iic_ne_bot h.eq_bot, fun s t hst ↦ ?_⟩

Result:
α : Type u_1
inst✝ : PartialOrder α
a : α
s t : LowerSet α
hst : s ⊔ t = Iic a
⊢ s = Iic a ∨ t = Iic a

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a : α
s t : LowerSet α
hst : s ⊔ t = Iic a
this : a ∈ s ⊔ t
⊢ s = Iic a ∨ t = Iic a

Tactic:
exact this.imp (fun ha ↦ (le_sup_left.trans_eq hst).antisymm <| Iic_le.2 ha) fun ha ↦
  (le_sup_right.trans_eq hst).antisymm <| Iic_le.2 ha

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a : α
s t : LowerSet α
hst : s ⊔ t = Iic a
⊢ s = Iic a ∨ t = Iic a

Tactic:
have := mem_Iic_iff.2 (le_refl a)

Result:
α : Type u_1
inst✝ : PartialOrder α
a : α
s t : LowerSet α
hst : s ⊔ t = Iic a
this : a ∈ Iic a
⊢ s = Iic a ∨ t = Iic a

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a : α
s t : LowerSet α
hst : s ⊔ t = Iic a
this : a ∈ Iic a
⊢ s = Iic a ∨ t = Iic a

Tactic:
rw [← hst] at this

Result:
α : Type u_1
inst✝ : PartialOrder α
a : α
s t : LowerSet α
hst : s ⊔ t = Iic a
this : a ∈ s ⊔ t
⊢ s = Iic a ∨ t = Iic a
-- Mathlib/Order/Filter/Prod.lean
theorem Tendsto.prod_map {δ : Type*} {f : α → γ} {g : β → δ} {a : Filter α} {b : Filter β}
    {c : Filter γ} {d : Filter δ} (hf : Tendsto f a c) (hg : Tendsto g b d) :
    Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_6
f : α → γ
g : β → δ
a : Filter α
b : Filter β
c : Filter γ
d : Filter δ
hf : Tendsto f a c
hg : Tendsto g b d
⊢ Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d)

Tactic:
rw [Tendsto, Prod.map_def, ← prod_map_map_eq]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_6
f : α → γ
g : β → δ
a : Filter α
b : Filter β
c : Filter γ
d : Filter δ
hf : Tendsto f a c
hg : Tendsto g b d
⊢ map f a ×ˢ map g b ≤ c ×ˢ d

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_6
f : α → γ
g : β → δ
a : Filter α
b : Filter β
c : Filter γ
d : Filter δ
hf : Tendsto f a c
hg : Tendsto g b d
⊢ map f a ×ˢ map g b ≤ c ×ˢ d

Tactic:
exact Filter.prod_mono hf hg

Result:
no goals
-- Mathlib/ModelTheory/Basic.lean
theorem self_comp_symm_toEmbedding (f : M ≃[L] N) :
    f.toEmbedding.comp f.symm.toEmbedding = Embedding.refl L N

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ f.toEmbedding.comp f.symm.toEmbedding = Embedding.refl L N

Tactic:
rw [← comp_toEmbedding, self_comp_symm, refl_toEmbedding]

Result:
no goals
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_add (s t : Multiset α) (comm) :
    noncommProd (s + t) comm =
      noncommProd s (comm.mono <| subset_of_le <| s.le_add_right t) *
        noncommProd t (comm.mono <| subset_of_le <| t.le_add_left s)

Proof state:
case mk
α : Type u_3
inst✝ : Monoid α
s t : Multiset α
a✝ : List α
comm : {x | x ∈ Quot.mk (⇑(List.isSetoid α)) a✝ + t}.Pairwise Commute
⊢ (Quot.mk (⇑(List.isSetoid α)) a✝ + t).noncommProd comm =
    noncommProd (Quot.mk (⇑(List.isSetoid α)) a✝) ⋯ * t.noncommProd ⋯

Tactic:
rcases t with ⟨⟩

Result:
case mk.mk
α : Type u_3
inst✝ : Monoid α
s t : Multiset α
a✝¹ a✝ : List α
comm : {x | x ∈ Quot.mk (⇑(List.isSetoid α)) a✝¹ + Quot.mk (⇑(List.isSetoid α)) a✝}.Pairwise Commute
⊢ (Quot.mk (⇑(List.isSetoid α)) a✝¹ + Quot.mk (⇑(List.isSetoid α)) a✝).noncommProd comm =
    noncommProd (Quot.mk (⇑(List.isSetoid α)) a✝¹) ⋯ * noncommProd (Quot.mk (⇑(List.isSetoid α)) a✝) ⋯

Proof state:
case mk.mk
α : Type u_3
inst✝ : Monoid α
s t : Multiset α
a✝¹ a✝ : List α
comm : {x | x ∈ Quot.mk (⇑(List.isSetoid α)) a✝¹ + Quot.mk (⇑(List.isSetoid α)) a✝}.Pairwise Commute
⊢ (Quot.mk (⇑(List.isSetoid α)) a✝¹ + Quot.mk (⇑(List.isSetoid α)) a✝).noncommProd comm =
    noncommProd (Quot.mk (⇑(List.isSetoid α)) a✝¹) ⋯ * noncommProd (Quot.mk (⇑(List.isSetoid α)) a✝) ⋯

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_3
inst✝ : Monoid α
s t : Multiset α
comm : {x | x ∈ s + t}.Pairwise Commute
⊢ (s + t).noncommProd comm = s.noncommProd ⋯ * t.noncommProd ⋯

Tactic:
rcases s with ⟨⟩

Result:
case mk
α : Type u_3
inst✝ : Monoid α
s t : Multiset α
a✝ : List α
comm : {x | x ∈ Quot.mk (⇑(List.isSetoid α)) a✝ + t}.Pairwise Commute
⊢ (Quot.mk (⇑(List.isSetoid α)) a✝ + t).noncommProd comm =
    noncommProd (Quot.mk (⇑(List.isSetoid α)) a✝) ⋯ * t.noncommProd ⋯
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
/-- If the affine span of an affine independent finset is strictly contained in the affine span of
another finset, then its cardinality is strictly less than the cardinality of that finset. -/
lemma AffineIndependent.card_lt_card_of_affineSpan_lt_affineSpan {s t : Finset V}
    (hs : AffineIndependent k ((↑) : s → V))
    (hst : affineSpan k (s : Set V) < affineSpan k (t : Set V)) : #s < #t

Proof state:
case inr.inl
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hs : AffineIndependent k Subtype.val
hs' : s.Nonempty
hst : affineSpan k ↑s < affineSpan k ↑∅
⊢ #s < #∅

Tactic:
simp [Set.subset_empty_iff] at hst

Result:
no goals
-- Mathlib/Analysis/ODE/PicardLindelof.lean
theorem vComp_apply_coe (t : Icc v.tMin v.tMax) : f.vComp t = v t (f t)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
t : ↑(Icc v.tMin v.tMax)
⊢ f.vComp ↑t = v.toFun (↑t) (f.toFun t)

Tactic:
simp only [vComp, proj_coe]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Finset.lean
/-- Also see `Finset.sup'_add` that works for ordered groups. -/
lemma sup'_add' (s : Finset ι) (f : ι → M) (a : M) (hs : s.Nonempty) :
    s.sup' hs f + a = s.sup' hs fun i ↦ f i + a

Proof state:
case a
ι : Type u_1
M : Type u_3
inst✝⁴ : LinearOrderedAddCommMonoid M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f + a ≤ s.sup' hs fun i => f i + a

Tactic:
apply add_le_of_le_tsub_right_of_le

Result:
case a.h
ι : Type u_1
M : Type u_3
inst✝⁴ : LinearOrderedAddCommMonoid M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ a ≤ s.sup' hs fun i => f i + a

case a.h2
ι : Type u_1
M : Type u_3
inst✝⁴ : LinearOrderedAddCommMonoid M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f ≤ (s.sup' hs fun i => f i + a) - a

Proof state:
case a
ι : Type u_1
M : Type u_3
inst✝⁴ : LinearOrderedAddCommMonoid M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ (s.sup' hs fun i => f i + a) ≤ s.sup' hs f + a

Tactic:
exact Finset.sup'_le _ _ fun i hi ↦ add_le_add_right (Finset.le_sup' _ hi) _

Result:
no goals

Proof state:
case a.h
ι : Type u_1
M : Type u_3
inst✝⁴ : LinearOrderedAddCommMonoid M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ a ≤ s.sup' hs fun i => f i + a

Tactic:
exact Finset.le_sup'_of_le _ hs.choose_spec le_add_self

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
inst✝⁴ : LinearOrderedAddCommMonoid M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f + a = s.sup' hs fun i => f i + a

Tactic:
apply le_antisymm

Result:
case a
ι : Type u_1
M : Type u_3
inst✝⁴ : LinearOrderedAddCommMonoid M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f + a ≤ s.sup' hs fun i => f i + a

case a
ι : Type u_1
M : Type u_3
inst✝⁴ : LinearOrderedAddCommMonoid M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ (s.sup' hs fun i => f i + a) ≤ s.sup' hs f + a
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_ne_zero (h : 0 ≤ x) : √x ≠ 0 ↔ x ≠ 0

Proof state:
x : ℝ
h : 0 ≤ x
⊢ √x ≠ 0 ↔ x ≠ 0

Tactic:
rw [not_iff_not, sqrt_eq_zero h]

Result:
no goals