harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem order_lt_order_of_eq_add_single {R} {Γ} [LinearOrder Γ] [Zero Γ] [AddCancelCommMonoid R]
    {x y : HahnSeries Γ R} (hxy : x = y + single x.order x.leadingCoeff) (hy : y ≠ 0) :
    x.order < y.order

Proof state:
case neg
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this✝ : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : ¬g = x.order
this : x.coeff g = (y + (single x.order) x.leadingCoeff).coeff g
⊢ g ∈ x.support

Tactic:
rw [coeff_add, coeff_single_of_ne hgx, add_zero] at this

Result:
case neg
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this✝ : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : ¬g = x.order
this : x.coeff g = y.coeff g
⊢ g ∈ x.support

Proof state:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
⊢ x.order ≠ y.order

Tactic:
intro h

Result:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
h : x.order = y.order
⊢ False

Proof state:
case pos
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this✝ : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g = x.order
this : x.coeff x.order ≠ 0
⊢ x.coeff g ≠ 0

Tactic:
rwa [← hgx] at this

Result:
no goals

Proof state:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : ¬g = x.order
⊢ x.coeff g = (y + (single x.order) x.leadingCoeff).coeff g

Tactic:
rw [← hxy]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_rpow {r : ℝ} (h : -1 < r ∨ r ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]]) :
    ∫ x in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)

Proof state:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ ↑r + 1 = ↑(r + 1)

Tactic:
push_cast

Result:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ ↑r + 1 = ↑r + 1

Proof state:
case inl
a b r : ℝ
h✝ : -1 < r
⊢ -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]

Tactic:
left

Result:
case inl.h
a b r : ℝ
h✝ : -1 < r
⊢ -1 < (↑r).re

Proof state:
case h.e'_2
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ⇑RCLike.re
⊢ IntervalIntegrable (fun x => ↑x ^ ↑r) MeasureTheory.volume a b

Tactic:
rcases h' with h' | h'

Result:
case h.e'_2.inl
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ⇑RCLike.re
h' : -1 < (↑r).re
⊢ IntervalIntegrable (fun x => ↑x ^ ↑r) MeasureTheory.volume a b

case h.e'_2.inr
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ⇑RCLike.re
h' : ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ IntervalIntegrable (fun x => ↑x ^ ↑r) MeasureTheory.volume a b

Proof state:
case h.e'_2
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ⇑RCLike.re
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, x ^ r ∂MeasureTheory.volume =
    (if a ≤ b then 1 else -1) * (∫ (x : ℝ) in Ι a b, ↑x ^ ↑r ∂MeasureTheory.volume).re

Tactic:
rw [this, ← integral_re]

Result:
case h.e'_2
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ⇑RCLike.re
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, x ^ r ∂MeasureTheory.volume =
    (if a ≤ b then 1 else -1) * ∫ (x : ℝ) in Ι a b, RCLike.re (↑x ^ ↑r) ∂MeasureTheory.volume

case h.e'_2
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ⇑RCLike.re
⊢ MeasureTheory.Integrable (fun x => ↑x ^ ↑r) (MeasureTheory.volume.restrict (Ι a b))

Proof state:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ ↑r + 1 = ↑r + 1

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
@[to_additive]
lemma isComplement_range_right {f : Quotient (QuotientGroup.rightRel H) → G}
    (hf : ∀ q, Quotient.mk'' (f q) = q) : IsComplement H (range f)

Proof state:
case mk.intro.mk.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
q₁ q₂ : Quotient (QuotientGroup.rightRel H)
h : (range f).restrict Quotient.mk'' ⟨f q₁, ⋯⟩ = (range f).restrict Quotient.mk'' ⟨f q₂, ⋯⟩
⊢ ⟨f q₁, ⋯⟩ = ⟨f q₂, ⋯⟩

Tactic:
exact Subtype.ext <| congr_arg f <| ((hf q₁).symm.trans h).trans (hf q₂)

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
⊢ Injective ((range f).restrict Quotient.mk'')

Tactic:
rintro ⟨-, q₁, rfl⟩ ⟨-, q₂, rfl⟩ h

Result:
case mk.intro.mk.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
q₁ q₂ : Quotient (QuotientGroup.rightRel H)
h : (range f).restrict Quotient.mk'' ⟨f q₁, ⋯⟩ = (range f).restrict Quotient.mk'' ⟨f q₂, ⋯⟩
⊢ ⟨f q₁, ⋯⟩ = ⟨f q₂, ⋯⟩

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
⊢ Bijective ((range f).restrict Quotient.mk'')

Tactic:
refine ⟨?_, fun q ↦ ⟨⟨f q, q, rfl⟩, hf q⟩⟩

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
⊢ Injective ((range f).restrict Quotient.mk'')

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
⊢ IsComplement (↑H) (range f)

Tactic:
rw [isComplement_subgroup_left_iff_bijective]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
⊢ Bijective ((range f).restrict Quotient.mk'')
-- Mathlib/SetTheory/Surreal/Basic.lean
theorem lt_def {x y : PGame} (ox : x.Numeric) (oy : y.Numeric) :
    x < y ↔
      (∃ i, (∀ i', x.moveLeft i' < y.moveLeft i) ∧ ∀ j, x < (y.moveLeft i).moveRight j) ∨
        ∃ j, (∀ i, (x.moveRight j).moveLeft i < y) ∧ ∀ j', x.moveRight j < y.moveRight j'

Proof state:
x y : PGame
ox : x.Numeric
oy : y.Numeric
⊢ x < y ↔
    (∃ i,
        (∀ (i' : x.LeftMoves), x.moveLeft i' < y.moveLeft i) ∧
          ∀ (j : (y.moveLeft i).RightMoves), x < (y.moveLeft i).moveRight j) ∨
      ∃ j,
        (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i < y) ∧
          ∀ (j' : y.RightMoves), x.moveRight j < y.moveRight j'

Tactic:
rw [← lf_iff_lt ox oy, lf_def]

Result:
x y : PGame
ox : x.Numeric
oy : y.Numeric
⊢ ((∃ i,
        (∀ (i' : x.LeftMoves), x.moveLeft i' ⧏ y.moveLeft i) ∧
          ∀ (j : (y.moveLeft i).RightMoves), x ⧏ (y.moveLeft i).moveRight j) ∨
      ∃ j,
        (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i ⧏ y) ∧
          ∀ (j' : y.RightMoves), x.moveRight j ⧏ y.moveRight j') ↔
    (∃ i,
        (∀ (i' : x.LeftMoves), x.moveLeft i' < y.moveLeft i) ∧
          ∀ (j : (y.moveLeft i).RightMoves), x < (y.moveLeft i).moveRight j) ∨
      ∃ j,
        (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i < y) ∧
          ∀ (j' : y.RightMoves), x.moveRight j < y.moveRight j'

Proof state:
x y : PGame
ox : x.Numeric
oy : y.Numeric
⊢ ((∃ i,
        (∀ (i' : x.LeftMoves), x.moveLeft i' ⧏ y.moveLeft i) ∧
          ∀ (j : (y.moveLeft i).RightMoves), x ⧏ (y.moveLeft i).moveRight j) ∨
      ∃ j,
        (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i ⧏ y) ∧
          ∀ (j' : y.RightMoves), x.moveRight j ⧏ y.moveRight j') ↔
    (∃ i,
        (∀ (i' : x.LeftMoves), x.moveLeft i' < y.moveLeft i) ∧
          ∀ (j : (y.moveLeft i).RightMoves), x < (y.moveLeft i).moveRight j) ∨
      ∃ j,
        (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i < y) ∧
          ∀ (j' : y.RightMoves), x.moveRight j < y.moveRight j'

Tactic:
refine or_congr ?_ ?_ <;> refine exists_congr fun x_1 => ?_ <;> refine and_congr ?_ ?_ <;>
    refine forall_congr' fun i => lf_iff_lt ?_ ?_ <;>
  apply_rules [Numeric.moveLeft, Numeric.moveRight]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem zero_zpow_eq (n : ℤ) : (0 : M) ^ n = if n = 0 then 1 else 0

Proof state:
case neg
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℤ
h : ¬n = 0
⊢ 0 ^ n = 0

Tactic:
rw [zero_zpow _ h]

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℤ
⊢ 0 ^ n = if n = 0 then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℤ
h : n = 0
⊢ 0 ^ n = 1

case neg
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℤ
h : ¬n = 0
⊢ 0 ^ n = 0

Proof state:
case pos
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℤ
h : n = 0
⊢ 0 ^ n = 1

Tactic:
rw [h, zpow_zero]

Result:
no goals
-- Mathlib/Combinatorics/Configuration.lean
theorem lineCount_eq_lineCount [Finite P] [Finite L] (p q : P) : lineCount L p = lineCount L q

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : p₁ ∉ l₂
h₁₃ : p₁ ∉ l₃
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
⊢ lineCount L p = lineCount L q

Tactic:
have hl₁ : pointCount P l₁ = n := (HasLines.lineCount_eq_pointCount h h₂₁).symm.trans hp₂

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : p₁ ∉ l₂
h₁₃ : p₁ ∉ l₃
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
⊢ lineCount L p = lineCount L q
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem toSpanSingleton_injective : Function.Injective (toSpanSingleton R M) :=
  fun _ _ eq ↦ by simpa using congr($eq 1)

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝¹ x✝ : M
eq : toSpanSingleton R M x✝¹ = toSpanSingleton R M x✝
⊢ x✝¹ = x✝

Tactic:
simpa using congr($eq 1)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem pbind_eq_some_iff {o : Option α} {f : (a : α) → a ∈ o → Option β} {b : β} :
    o.pbind f = some b ↔ ∃ a h, f a h = some b

Proof state:
case some
α : Type u_1
β : Type u_2
b : β
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ f a ⋯ = some b ↔ ∃ a_1 h, f a_1 ⋯ = some b

Tactic:
constructor

Result:
case some.mp
α : Type u_1
β : Type u_2
b : β
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ f a ⋯ = some b → ∃ a_2 h, f a_2 ⋯ = some b

case some.mpr
α : Type u_1
β : Type u_2
b : β
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ (∃ a_1 h, f a_1 ⋯ = some b) → f a ⋯ = some b

Proof state:
case some.mpr
α : Type u_1
β : Type u_2
b : β
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ (∃ a_1 h, f a_1 ⋯ = some b) → f a ⋯ = some b

Tactic:
rintro ⟨a, rfl, h⟩

Result:
case some.mpr.intro.intro
α : Type u_1
β : Type u_2
b : β
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
h : f a ⋯ = some b
⊢ f a ⋯ = some b

Proof state:
case some.mp
α : Type u_1
β : Type u_2
b : β
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ f a ⋯ = some b → ∃ a_2 h, f a_2 ⋯ = some b

Tactic:
intro h

Result:
case some.mp
α : Type u_1
β : Type u_2
b : β
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
h : f a ⋯ = some b
⊢ ∃ a_1 h, f a_1 ⋯ = some b

Proof state:
case some.mp
α : Type u_1
β : Type u_2
b : β
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
h : f a ⋯ = some b
⊢ ∃ a_1 h, f a_1 ⋯ = some b

Tactic:
exact ⟨a, rfl, h⟩

Result:
no goals

Proof state:
case some.mpr.intro.intro
α : Type u_1
β : Type u_2
b : β
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
h : f a ⋯ = some b
⊢ f a ⋯ = some b

Tactic:
exact h

Result:
no goals

Proof state:
case some
α : Type u_1
β : Type u_2
b : β
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ (some a).pbind f = some b ↔ ∃ a_1 h, f a_1 h = some b

Tactic:
simp only [pbind_some, mem_def, some.injEq]

Result:
case some
α : Type u_1
β : Type u_2
b : β
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ f a ⋯ = some b ↔ ∃ a_1 h, f a_1 ⋯ = some b

Proof state:
case none
α : Type u_1
β : Type u_2
b : β
f : (a : α) → a ∈ none → Option β
⊢ none.pbind f = some b ↔ ∃ a h, f a h = some b

Tactic:
simp

Result:
no goals
-- Mathlib/ModelTheory/Satisfiability.lean
theorem exists_elementaryEmbedding_card_eq_of_ge (M : Type w') [L.Structure M] [iM : Infinite M]
    (κ : Cardinal.{w}) (h1 : Cardinal.lift.{w} L.card ≤ Cardinal.lift.{max u v} κ)
    (h2 : Cardinal.lift.{w} #M ≤ Cardinal.lift.{w'} κ) :
    ∃ N : Bundled L.Structure, Nonempty (M ↪ₑ[L] N) ∧ #N = κ

Proof state:
case intro.intro.intro.intro
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
N : Bundled L[[M]].Structure
hN : #↑N = κ
NN0 : ↑N ↪ₑ[L[[M]]] ↑N0
this : L.Structure ↑N := (L.lhomWithConstants M).reduct ↑N
h : ↑N ⊨ L.elementaryDiagram M
⊢ M ↪ₑ[L] ↑(Bundled.of ↑N)

Tactic:
apply ElementaryEmbedding.ofModelsElementaryDiagram L M N

Result:
no goals

Proof state:
case intro.intro.intro.intro
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
N : Bundled L[[M]].Structure
hN : #↑N = κ
NN0 : ↑N ↪ₑ[L[[M]]] ↑N0
this : L.Structure ↑N := (L.lhomWithConstants M).reduct ↑N
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ

Tactic:
haveI h : N ⊨ L.elementaryDiagram M :=
  (NN0.theory_model_iff (L.elementaryDiagram M)).2 inferInstance

Result:
case intro.intro.intro.intro
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
N : Bundled L[[M]].Structure
hN : #↑N = κ
NN0 : ↑N ↪ₑ[L[[M]]] ↑N0
this : L.Structure ↑N := (L.lhomWithConstants M).reduct ↑N
h : ↑N ⊨ L.elementaryDiagram M
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ

Proof state:
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ lift.{w, max (max w' u) v} L[[M]].card ≤ lift.{max (max w' u) v, w} κ

Tactic:
simp only [card_withConstants, lift_add, lift_lift]

Result:
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ lift.{max w' w, max u v} L.card + lift.{max (max u v) w, w'} #M ≤ lift.{max (max w' u) v, w} κ
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
theorem insert_union_comm (s t : Finset α) (a : α) : insert a s ∪ t = s ∪ insert a t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ insert a s ∪ t = s ∪ insert a t

Tactic:
rw [insert_union, union_insert]

Result:
no goals
-- Mathlib/CategoryTheory/LiftingProperties/Adjunction.lean
theorem right_adjoint (sq : CommSq u (G.map i) p v) (adj : G ⊣ F) :
    CommSq (adj.homEquiv _ _ u) i (F.map p) (adj.homEquiv _ _ v) :=
  ⟨by
    simp only [Adjunction.homEquiv_unit, assoc, ← F.map_comp, sq.w]
    rw [F.map_comp, Adjunction.unit_naturality_assoc]⟩

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_3, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ (adj.homEquiv A X) u ≫ F.map p = i ≫ (adj.homEquiv B Y) v

Tactic:
simp only [Adjunction.homEquiv_unit, assoc, ← F.map_comp, sq.w]

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_3, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ adj.unit.app A ≫ F.map (G.map i ≫ v) = i ≫ adj.unit.app B ≫ F.map v

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_3, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ adj.unit.app A ≫ F.map (G.map i ≫ v) = i ≫ adj.unit.app B ≫ F.map v

Tactic:
rw [F.map_comp, Adjunction.unit_naturality_assoc]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_map_map {L : Type v} [Field L] (f : E →+* L) :
    relrank (A.map f) (B.map f) = relrank A B

Proof state:
E : Type v
inst✝¹ : Field E
A B : Subfield E
L : Type v
inst✝ : Field L
f : E →+* L
⊢ (map f A).relrank (map f B) = A.relrank B

Tactic:
simpa only [lift_id] using lift_relrank_map_map A B f

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp.lean
theorem isZero_of_subsingleton (V : SemiNormedGrp₁) [Subsingleton V] : Limits.IsZero V

Proof state:
case refine_1.hf.a.H
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
x : V.carrier
this : x = 0
⊢ ↑(Hom.hom f) x = ↑(Hom.hom default) x

Tactic:
simp only [this, map_zero]

Result:
no goals

Proof state:
case refine_2
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : X ⟶ V
⊢ f = default

Tactic:
ext

Result:
case refine_2.hf.a.H
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : X ⟶ V
x✝ : X.carrier
⊢ ↑(Hom.hom f) x✝ = ↑(Hom.hom default) x✝

Proof state:
case refine_1
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
⊢ f = default

Tactic:
ext x

Result:
case refine_1.hf.a.H
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
x : V.carrier
⊢ ↑(Hom.hom f) x = ↑(Hom.hom default) x

Proof state:
case refine_2.hf.a.H
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : X ⟶ V
x✝ : X.carrier
⊢ ↑(Hom.hom f) x✝ = ↑(Hom.hom default) x✝

Tactic:
apply Subsingleton.elim

Result:
no goals

Proof state:
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
⊢ Limits.IsZero V

Tactic:
refine ⟨fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩

Result:
case refine_1
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
⊢ f = default

case refine_2
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : X ⟶ V
⊢ f = default

Proof state:
case refine_1.hf.a.H
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
x : V.carrier
⊢ ↑(Hom.hom f) x = ↑(Hom.hom default) x

Tactic:
have : x = 0 := Subsingleton.elim _ _

Result:
case refine_1.hf.a.H
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
x : V.carrier
this : x = 0
⊢ ↑(Hom.hom f) x = ↑(Hom.hom default) x
-- Mathlib/RingTheory/ChainOfDivisors.lean
theorem eq_second_of_chain_of_prime_dvd {p q r : Associates M} {n : ℕ} (hn : n ≠ 0)
    {c : Fin (n + 1) → Associates M} (h₁ : StrictMono c)
    (h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i) (hp : Prime p) (hr : r ∣ q) (hp' : p ∣ r) :
    p = c 1

Proof state:
case succ.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (n + 1 + 1)
hp : Prime (c i)
hp' : c i ∣ r
⊢ c i = c 1

Tactic:
refine congr_arg c (eq_of_ge_of_not_gt ?_ fun hi => ?_)

Result:
case succ.intro.refine_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (n + 1 + 1)
hp : Prime (c i)
hp' : c i ∣ r
⊢ 1 ≤ i

case succ.intro.refine_2
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (n + 1 + 1)
hp : Prime (c i)
hp' : c i ∣ r
hi : 1 < i
⊢ False
-- Mathlib/Algebra/Star/Pointwise.lean
theorem star_singleton {β : Type*} [InvolutiveStar β] (x : β) : ({x} : Set β)⋆ = {x⋆}

Proof state:
case h
β : Type u_2
inst✝ : InvolutiveStar β
x y : β
⊢ y ∈ {x}⋆ ↔ y ∈ {x⋆}

Tactic:
rw [mem_star, mem_singleton_iff, mem_singleton_iff, star_eq_iff_star_eq, eq_comm]

Result:
no goals

Proof state:
β : Type u_2
inst✝ : InvolutiveStar β
x : β
⊢ {x}⋆ = {x⋆}

Tactic:
ext1 y

Result:
case h
β : Type u_2
inst✝ : InvolutiveStar β
x y : β
⊢ y ∈ {x}⋆ ↔ y ∈ {x⋆}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem any_eq_true' {p : α → Bool} {as : Array α} :
    as.any p = true ↔ (∃ x, x ∈ as ∧ p x)

Proof state:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ { toList := toList✝ }.any p = true ↔ ∃ x, x ∈ { toList := toList✝ } ∧ p x = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ as.any p = true ↔ ∃ x, x ∈ as ∧ p x = true

Tactic:
cases as

Result:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ { toList := toList✝ }.any p = true ↔ ∃ x, x ∈ { toList := toList✝ } ∧ p x = true
-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem isTrichotomous (h : x.IsOrdinal) : IsTrichotomous _ (Subrel (· ∈ ·) (· ∈ x)) :=
  ⟨fun ⟨a, ha⟩ ⟨b, hb⟩ ↦ by simpa using mem_trichotomous (h.mem ha) (h.mem hb)⟩

Proof state:
x : ZFSet.{u}
h : x.IsOrdinal
x✝¹ x✝ : { x_1 // x_1 ∈ x }
a : ZFSet.{u}
ha : a ∈ x
b : ZFSet.{u}
hb : b ∈ x
⊢ Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) ⟨a, ha⟩ ⟨b, hb⟩ ∨
    ⟨a, ha⟩ = ⟨b, hb⟩ ∨ Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) ⟨b, hb⟩ ⟨a, ha⟩

Tactic:
simpa using mem_trichotomous (h.mem ha) (h.mem hb)

Result:
no goals