harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Int/GCD.lean
theorem gcd_dvd_iff {a b : ℤ} {n : ℕ} : gcd a b ∣ n ↔ ∃ x y : ℤ, ↑n = a * x + b * y

Proof state:
a b : ℤ
n : ℕ
⊢ a.gcd b ∣ n ↔ ∃ x y, ↑n = a * x + b * y

Tactic:
constructor

Result:
case mp
a b : ℤ
n : ℕ
⊢ a.gcd b ∣ n → ∃ x y, ↑n = a * x + b * y

case mpr
a b : ℤ
n : ℕ
⊢ (∃ x y, ↑n = a * x + b * y) → a.gcd b ∣ n

Proof state:
case mpr.intro.intro
a b : ℤ
n : ℕ
x y : ℤ
h : ↑n = a * x + b * y
⊢ ↑(a.gcd b) ∣ a * x + b * y

Tactic:
exact Int.dvd_add (dvd_mul_of_dvd_left gcd_dvd_left _) (dvd_mul_of_dvd_left gcd_dvd_right y)

Result:
no goals

Proof state:
case mp
a b : ℤ
n : ℕ
⊢ a.gcd b ∣ n → ∃ x y, ↑n = a * x + b * y

Tactic:
intro h

Result:
case mp
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ x y, ↑n = a * x + b * y

Proof state:
case mpr.intro.intro
a b : ℤ
n : ℕ
x y : ℤ
h : ↑n = a * x + b * y
⊢ a.gcd b ∣ n

Tactic:
rw [← Int.natCast_dvd_natCast, h]

Result:
case mpr.intro.intro
a b : ℤ
n : ℕ
x y : ℤ
h : ↑n = a * x + b * y
⊢ ↑(a.gcd b) ∣ a * x + b * y

Proof state:
case mp
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ x y, a * (a.gcdA b * ↑(n / a.gcd b)) + b * (a.gcdB b * ↑(n / a.gcd b)) = a * x + b * y

Tactic:
exact ⟨_, _, rfl⟩

Result:
no goals

Proof state:
case mpr
a b : ℤ
n : ℕ
⊢ (∃ x y, ↑n = a * x + b * y) → a.gcd b ∣ n

Tactic:
rintro ⟨x, y, h⟩

Result:
case mpr.intro.intro
a b : ℤ
n : ℕ
x y : ℤ
h : ↑n = a * x + b * y
⊢ a.gcd b ∣ n

Proof state:
case mp
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ x y, ↑n = a * x + b * y

Tactic:
rw [← Nat.mul_div_cancel' h, Int.ofNat_mul, gcd_eq_gcd_ab, Int.add_mul, mul_assoc, mul_assoc]

Result:
case mp
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ x y, a * (a.gcdA b * ↑(n / a.gcd b)) + b * (a.gcdB b * ↑(n / a.gcd b)) = a * x + b * y
-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem separableClosure_le (L : IntermediateField F E)
    [h : IsPurelyInseparable L E] : separableClosure F E ≤ L := fun x hx ↦ by
  obtain ⟨y, rfl⟩ := h.inseparable' _ <|
    IsSeparable.tower_top L (mem_separableClosure_iff.1 hx)
  exact y.2

Proof state:
case intro
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : IsPurelyInseparable (↥L) E
y : ↥L
hx : (algebraMap (↥L) E) y ∈ separableClosure F E
⊢ (algebraMap (↥L) E) y ∈ L

Tactic:
exact y.2

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : IsPurelyInseparable (↥L) E
x : E
hx : x ∈ separableClosure F E
⊢ x ∈ L

Tactic:
obtain ⟨y, rfl⟩ := h.inseparable' _ <|
  IsSeparable.tower_top L (mem_separableClosure_iff.1 hx)

Result:
case intro
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : IsPurelyInseparable (↥L) E
y : ↥L
hx : (algebraMap (↥L) E) y ∈ separableClosure F E
⊢ (algebraMap (↥L) E) y ∈ L
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma eLpNorm_indicator_const' (hs : MeasurableSet s) (hμs : μ s ≠ 0) (hp : p ≠ 0) :
    eLpNorm (s.indicator fun _ => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal)

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
c : F
hs : MeasurableSet s
hμs : μ s ≠ 0
hp : p ≠ 0
hp_top : p = ⊤
⊢ eLpNorm (s.indicator fun x => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal)

Tactic:
simp [hp_top, eLpNormEssSup_indicator_const_eq s c hμs]

Result:
no goals

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
c : F
hs : MeasurableSet s
hμs : μ s ≠ 0
hp : p ≠ 0
hp_top : ¬p = ⊤
⊢ eLpNorm (s.indicator fun x => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal)

Tactic:
exact eLpNorm_indicator_const hs hp hp_top

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
c : F
hs : MeasurableSet s
hμs : μ s ≠ 0
hp : p ≠ 0
⊢ eLpNorm (s.indicator fun x => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal)

Tactic:
by_cases hp_top : p = ∞

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
c : F
hs : MeasurableSet s
hμs : μ s ≠ 0
hp : p ≠ 0
hp_top : p = ⊤
⊢ eLpNorm (s.indicator fun x => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal)

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
c : F
hs : MeasurableSet s
hμs : μ s ≠ 0
hp : p ≠ 0
hp_top : ¬p = ⊤
⊢ eLpNorm (s.indicator fun x => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal)
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem deriv_mul_eq_opow_omega0_mul {a : Ordinal.{u}} (ha : 0 < a) (b) :
    deriv (a * ·) b = a ^ ω * b

Proof state:
a : Ordinal.{u}
ha : 0 < a
b : Ordinal.{u}
⊢ deriv (fun x => a * x) b = a ^ ω * b

Tactic:
revert b

Result:
a : Ordinal.{u}
ha : 0 < a
⊢ ∀ (b : Ordinal.{u}), deriv (fun x => a * x) b = a ^ ω * b

Proof state:
a : Ordinal.{u}
ha : 0 < a
⊢ ∀ (b : Ordinal.{u}), deriv (fun x => a * x) b = a ^ ω * b

Tactic:
rw [← funext_iff,
  IsNormal.eq_iff_zero_and_succ (isNormal_deriv _) (isNormal_mul_right (opow_pos ω ha))]

Result:
a : Ordinal.{u}
ha : 0 < a
⊢ deriv (fun x => a * x) 0 = a ^ ω * 0 ∧
    ∀ (a_1 : Ordinal.{u}),
      deriv (fun x => a * x) a_1 = a ^ ω * a_1 → deriv (fun x => a * x) (succ a_1) = a ^ ω * succ a_1

Proof state:
a : Ordinal.{u}
ha : 0 < a
⊢ deriv (fun x => a * x) 0 = a ^ ω * 0 ∧
    ∀ (a_1 : Ordinal.{u}),
      deriv (fun x => a * x) a_1 = a ^ ω * a_1 → deriv (fun x => a * x) (succ a_1) = a ^ ω * succ a_1

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

Result:
case refine_1
a : Ordinal.{u}
ha : 0 < a
⊢ deriv (fun x => a * x) 0 = a ^ ω * 0

case refine_2
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun x => a * x) c = a ^ ω * c
⊢ deriv (fun x => a * x) (succ c) = a ^ ω * succ c

Proof state:
case refine_2
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun x => a * x) c = a ^ ω * c
⊢ deriv (fun x => a * x) (succ c) = a ^ ω * succ c

Tactic:
rw [deriv_succ, h]

Result:
case refine_2
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun x => a * x) c = a ^ ω * c
⊢ nfp (fun x => a * x) (succ (a ^ ω * c)) = a ^ ω * succ c

Proof state:
case refine_1
a : Ordinal.{u}
ha : 0 < a
⊢ deriv (fun x => a * x) 0 = a ^ ω * 0

Tactic:
rw [deriv_zero_right, nfp_mul_zero, mul_zero]

Result:
no goals

Proof state:
case refine_2
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun x => a * x) c = a ^ ω * c
⊢ nfp (fun x => a * x) (succ (a ^ ω * c)) = a ^ ω * succ c

Tactic:
exact nfp_mul_opow_omega0_add c ha zero_lt_one (one_le_iff_pos.2 (opow_pos _ ha))

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem map_direction (s : AffineSubspace k P₁) :
    (s.map f).direction = s.direction.map f.linear

Proof state:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
⊢ (map f s).direction = Submodule.map f.linear s.direction

Tactic:
rw [direction_eq_vectorSpan, direction_eq_vectorSpan, coe_map,
  AffineMap.vectorSpan_image_eq_submodule_map]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup'_le_iff {a : α} : s.sup' H f ≤ a ↔ ∀ b ∈ s, f b ≤ a

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
a : α
⊢ s.sup' H f ≤ a ↔ ∀ b ∈ s, f b ≤ a

Tactic:
simp_rw [← @WithBot.coe_le_coe α, coe_sup', Finset.sup_le_iff]

Result:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
a : α
⊢ (∀ b ∈ s, (WithBot.some ∘ f) b ≤ ↑a) ↔ ∀ b ∈ s, ↑(f b) ≤ ↑a

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
a : α
⊢ (∀ b ∈ s, (WithBot.some ∘ f) b ≤ ↑a) ↔ ∀ b ∈ s, ↑(f b) ≤ ↑a

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurableSet_pi {s : Set δ} {t : ∀ i, Set (π i)} (hs : s.Countable) :
    MeasurableSet (pi s t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ pi s t = ∅

Proof state:
case inl
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
s : Set δ
t : (i : δ) → Set (π i)
hs : s.Countable
h : s.pi t = ∅
⊢ MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅

Tactic:
simp [h]

Result:
no goals

Proof state:
case inr
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
s : Set δ
t : (i : δ) → Set (π i)
hs : s.Countable
h : (s.pi t).Nonempty
⊢ MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅

Tactic:
simp [measurableSet_pi_of_nonempty hs, h, ← not_nonempty_iff_eq_empty]

Result:
no goals

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
s : Set δ
t : (i : δ) → Set (π i)
hs : s.Countable
⊢ MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅

Tactic:
rcases (pi s t).eq_empty_or_nonempty with h | h

Result:
case inl
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
s : Set δ
t : (i : δ) → Set (π i)
hs : s.Countable
h : s.pi t = ∅
⊢ MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅

case inr
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
s : Set δ
t : (i : δ) → Set (π i)
hs : s.Countable
h : (s.pi t).Nonempty
⊢ MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅
-- Mathlib/Data/Finset/Lattice/Pi.lean
theorem inf_sup {κ : ι → Type*} (s : Finset ι) (t : ∀ i, Finset (κ i)) (f : ∀ i, κ i → α) :
    (s.inf fun i => (t i).sup (f i)) =
      (s.pi t).sup fun g => s.attach.inf fun i => f _ <| g _ i.2

Proof state:
case insert
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i => (t i).sup (f i)) = (s.pi t).sup fun g => s.attach.inf fun i => f (↑i) (g ↑i ⋯)
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 => f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x => ⟨↑x, ⋯⟩) ≤ c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
⊢ (f i a ⊓ s.attach.inf fun i => f (↑i) (g ↑i ⋯)) ≤ c

Tactic:
have aux : ∀ j : { x // x ∈ s }, ↑j ≠ i := fun j : s => ne_of_mem_of_not_mem j.2 hi

Result:
case insert
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i => (t i).sup (f i)) = (s.pi t).sup fun g => s.attach.inf fun i => f (↑i) (g ↑i ⋯)
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 => f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x => ⟨↑x, ⋯⟩) ≤ c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : { x // x ∈ s }), ↑j ≠ i
⊢ (f i a ⊓ s.attach.inf fun i => f (↑i) (g ↑i ⋯)) ≤ c

Proof state:
case insert
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i => (t i).sup (f i)) = (s.pi t).sup fun g => s.attach.inf fun i => f (↑i) (g ↑i ⋯)
c : α
⊢ ((t i ×ˢ s.pi t).sup fun i_1 => f i i_1.1 ⊓ s.attach.inf fun i_2 => f (↑i_2) (i_1.2 ↑i_2 ⋯)) ≤ c ↔
    (((insert i s).pi t).sup fun g =>
        (insert ⟨i, ⋯⟩ (image (fun x => ⟨↑x, ⋯⟩) s.attach)).inf fun i_1 => f (↑i_1) (g ↑i_1 ⋯)) ≤
      c

Tactic:
simp only [Finset.sup_le_iff, mem_product, mem_pi, and_imp, Prod.forall,
  inf_insert, inf_image]

Result:
case insert
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i => (t i).sup (f i)) = (s.pi t).sup fun g => s.attach.inf fun i => f (↑i) (g ↑i ⋯)
c : α
⊢ (∀ (a : κ i) (b : (a : ι) → a ∈ s → κ a),
      a ∈ t i → (∀ (a : ι) (h : a ∈ s), b a h ∈ t a) → (f i a ⊓ s.attach.inf fun i => f (↑i) (b ↑i ⋯)) ≤ c) ↔
    ∀ (b : (a : ι) → a ∈ insert i s → κ a),
      (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
        f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 => f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x => ⟨↑x, ⋯⟩) ≤ c
-- Mathlib/Data/Finset/NatAntidiagonal.lean
@[simp] lemma antidiagonal_filter_snd_le_of_le {n k : ℕ} (h : k ≤ n) :
    (antidiagonal n).filter (fun a ↦ a.snd ≤ k) = (antidiagonal k).map
      (Embedding.prodMap ⟨_, add_left_injective (n - k)⟩ (Embedding.refl ℕ))

Proof state:
case h.mk.refine_2
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (∃ a, a + j = k ∧ a + (n - k) = i) → i + j = n ∧ j ≤ k

Tactic:
rintro ⟨l, hl, rfl⟩

Result:
case h.mk.refine_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ l + (n - k) + j = n ∧ j ≤ k

Proof state:
case h.mk.refine_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ l + (n - k) + j = n

Tactic:
rw [add_assoc, add_comm, add_assoc, add_comm j l, hl]

Result:
case h.mk.refine_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ n - k + k = n

Proof state:
case h.mk.refine_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ n - k + k = n

Tactic:
exact Nat.sub_add_cancel h

Result:
no goals

Proof state:
n k : ℕ
h : k ≤ n
i j : ℕ
this : i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i
⊢ (i, j) ∈ filter (fun a => a.2 ≤ k) (antidiagonal n) ↔
    (i, j) ∈ map ({ toFun := fun x => x + (n - k), inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal k)

Tactic:
simpa

Result:
no goals

Proof state:
n k : ℕ
h : k ≤ n
⊢ filter (fun a => a.2 ≤ k) (antidiagonal n) =
    map ({ toFun := fun x => x + (n - k), inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal k)

Tactic:
ext ⟨i, j⟩

Result:
case h.mk
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (i, j) ∈ filter (fun a => a.2 ≤ k) (antidiagonal n) ↔
    (i, j) ∈ map ({ toFun := fun x => x + (n - k), inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal k)

Proof state:
case h.mk
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (i, j) ∈ filter (fun a => a.2 ≤ k) (antidiagonal n) ↔
    (i, j) ∈ map ({ toFun := fun x => x + (n - k), inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal k)

Tactic:
suffices i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i by simpa

Result:
case h.mk
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i

Proof state:
case h.mk.refine_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ l + (n - k) + j = n ∧ j ≤ k

Tactic:
refine ⟨?_, hl ▸ Nat.le_add_left j l⟩

Result:
case h.mk.refine_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ l + (n - k) + j = n

Proof state:
case h.mk.refine_1
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ j ≤ k
⊢ k - j + (n - k) = i

Tactic:
rw [add_comm, tsub_add_eq_add_tsub h, ← hi.1, add_assoc, Nat.add_sub_of_le hi.2,
  add_tsub_cancel_right]

Result:
no goals

Proof state:
case h.mk
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i

Tactic:
refine ⟨fun hi ↦ ⟨k - j, tsub_add_cancel_of_le hi.2, ?_⟩, ?_⟩

Result:
case h.mk.refine_1
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ j ≤ k
⊢ k - j + (n - k) = i

case h.mk.refine_2
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (∃ a, a + j = k ∧ a + (n - k) = i) → i + j = n ∧ j ≤ k
-- Mathlib/Data/Fin/VecNotation.lean
theorem cons_val_fin_one (x : α) (u : Fin 0 → α) : ∀ (i : Fin 1), vecCons x u i = x

Proof state:
α : Type u
x : α
u : Fin 0 → α
⊢ ∀ (i : Fin 1), vecCons x u i = x

Tactic:
rw [Fin.forall_fin_one]

Result:
α : Type u
x : α
u : Fin 0 → α
⊢ vecCons x u 0 = x

Proof state:
α : Type u
x : α
u : Fin 0 → α
⊢ vecCons x u 0 = x

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem subset_singleton_iff_eq {s : Set α} {x : α} : s ⊆ {x} ↔ s = ∅ ∨ s = {x}

Proof state:
α : Type u
s : Set α
x : α
⊢ s ⊆ {x} ↔ s = ∅ ∨ s = {x}

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Result:
case inl
α : Type u
x : α
⊢ ∅ ⊆ {x} ↔ ∅ = ∅ ∨ ∅ = {x}

case inr
α : Type u
s : Set α
x : α
hs : s.Nonempty
⊢ s ⊆ {x} ↔ s = ∅ ∨ s = {x}

Proof state:
case inl
α : Type u
x : α
⊢ ∅ ⊆ {x} ↔ ∅ = ∅ ∨ ∅ = {x}

Tactic:
exact ⟨fun _ => Or.inl rfl, fun _ => empty_subset _⟩

Result:
no goals

Proof state:
case inr
α : Type u
s : Set α
x : α
hs : s.Nonempty
⊢ s ⊆ {x} ↔ s = ∅ ∨ s = {x}

Tactic:
simp [eq_singleton_iff_nonempty_unique_mem, hs, hs.ne_empty]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem equivMapDomain_trans (f : α ≃ β) (g : β ≃ γ) (l : α →₀ M) :
    equivMapDomain (f.trans g) l = equivMapDomain g (equivMapDomain f l)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : Zero M
f : α ≃ β
g : β ≃ γ
l : α →₀ M
⊢ equivMapDomain (f.trans g) l = equivMapDomain g (equivMapDomain f l)

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : Zero M
f : α ≃ β
g : β ≃ γ
l : α →₀ M
x : γ
⊢ (equivMapDomain (f.trans g) l) x = (equivMapDomain g (equivMapDomain f l)) x

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : Zero M
f : α ≃ β
g : β ≃ γ
l : α →₀ M
x : γ
⊢ (equivMapDomain (f.trans g) l) x = (equivMapDomain g (equivMapDomain f l)) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/SmoothingSeminorm.lean
theorem μ_bddAbove' (hμ1 : μ 1 ≤ 1) {s : ℕ → ℕ} (hs : ∀ n : ℕ, s n ≤ n) (x : R)
    (ψ : ℕ → ℕ) : BddAbove ((fun n : ℕ => μ (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ))) '' Set.univ)

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ BddAbove (Set.range fun x_1 => μ (x ^ s (ψ ↑x_1)) ^ (1 / ↑(ψ ↑x_1)))

Tactic:
convert μ_bddAbove μ hμ1 hs x ψ

Result:
case h.e'_3
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ (Set.range fun x_1 => μ (x ^ s (ψ ↑x_1)) ^ (1 / ↑(ψ ↑x_1))) = Set.range fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))

Proof state:
case h.e'_3.h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
x✝ : ℝ
⊢ (x✝ ∈ Set.range fun x_1 => μ (x ^ s (ψ ↑x_1)) ^ (1 / ↑(ψ ↑x_1))) ↔
    x✝ ∈ Set.range fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))

Tactic:
simp [one_div, Set.mem_range, Subtype.exists, Set.mem_univ, exists_const]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ BddAbove ((fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) '' Set.univ)

Tactic:
rw [Set.image_eq_range]

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ BddAbove (Set.range fun x_1 => μ (x ^ s (ψ ↑x_1)) ^ (1 / ↑(ψ ↑x_1)))

Proof state:
case h.e'_3
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ (Set.range fun x_1 => μ (x ^ s (ψ ↑x_1)) ^ (1 / ↑(ψ ↑x_1))) = Set.range fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))

Tactic:
ext

Result:
case h.e'_3.h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
x✝ : ℝ
⊢ (x✝ ∈ Set.range fun x_1 => μ (x ^ s (ψ ↑x_1)) ^ (1 / ↑(ψ ↑x_1))) ↔
    x✝ ∈ Set.range fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_signExtend_of_le (x : BitVec w) {v : Nat} (hv : w ≤ v) :
    (x.signExtend v).toNat = x.toNat + if x.msb then 2^v - 2^w else 0

Proof state:
case pred
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i : Nat
⊢ (signExtend v x).toNat.testBit i = (x.toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0).testBit i

Tactic:
have ⟨k, hk⟩ := Nat.exists_eq_add_of_le hv

Result:
case pred
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
⊢ (signExtend v x).toNat.testBit i = (x.toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0).testBit i

Proof state:
case pos.inl
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
hi : i < w
⊢ x.getLsbD i = true → i < w + k

Tactic:
omega

Result:
no goals

Proof state:
case pred
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
⊢ ∀ (i : Nat), (signExtend v x).toNat.testBit i = (x.toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0).testBit i

Tactic:
intro i

Result:
case pred
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i : Nat
⊢ (signExtend v x).toNat.testBit i = (x.toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0).testBit i

Proof state:
case neg
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : ¬x.msb = true
hi : i < w ∨ w ≤ i ∧ i < w + k ∨ w + k ≤ i
⊢ (decide (i < w + k) && (decide (i < w) && x.getLsbD i)) = x.getLsbD i

Tactic:
rcases hi with hi | hi | hi

Result:
case neg.inl
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : ¬x.msb = true
hi : i < w
⊢ (decide (i < w + k) && (decide (i < w) && x.getLsbD i)) = x.getLsbD i

case neg.inr.inl
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : ¬x.msb = true
hi : w ≤ i ∧ i < w + k
⊢ (decide (i < w + k) && (decide (i < w) && x.getLsbD i)) = x.getLsbD i

case neg.inr.inr
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : ¬x.msb = true
hi : w + k ≤ i
⊢ (decide (i < w + k) && (decide (i < w) && x.getLsbD i)) = x.getLsbD i

Proof state:
case pos.inr.inl
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
hi : w ≤ i ∧ i < w + k
⊢ (decide (i < w + k) && (!decide (i < w) || x.getLsbD i)) = if i < w then x.getLsbD i else decide (i - w < k)

Tactic:
simp [hi]

Result:
case pos.inr.inl
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
hi : w ≤ i ∧ i < w + k
⊢ i - w < k

Proof state:
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
⊢ (signExtend v x).toNat = x.toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
⊢ ∀ (i : Nat), (signExtend v x).toNat.testBit i = (x.toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0).testBit i

Proof state:
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
hi : w + k ≤ i
⊢ ¬i < w + k

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : ¬x.msb = true
hi : w + k ≤ i
⊢ ¬i < w + k

Tactic:
omega

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem interedges_disjoint_right (s : Finset α) {t t' : Finset β} (ht : Disjoint t t') :
    Disjoint (interedges r s t) (interedges r s t')

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'
⊢ ∀ ⦃a : α × β⦄, a ∈ interedges r s t → a ∉ interedges r s t'

Tactic:
intro _ hx hy

Result:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'
a✝ : α × β
hx : a✝ ∈ interedges r s t
hy : a✝ ∈ interedges r s t'
⊢ False

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'
a✝ : α × β
hx : a✝.1 ∈ s ∧ a✝.2 ∈ t ∧ r a✝.1 a✝.2
hy : a✝.1 ∈ s ∧ a✝.2 ∈ t' ∧ r a✝.1 a✝.2
⊢ False

Tactic:
exact ht hx.2.1 hy.2.1

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t t' : Finset β
ht : Disjoint t t'
⊢ Disjoint (interedges r s t) (interedges r s t')

Tactic:
rw [Finset.disjoint_left] at ht ⊢

Result:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'
⊢ ∀ ⦃a : α × β⦄, a ∈ interedges r s t → a ∉ interedges r s t'

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'
a✝ : α × β
hx : a✝ ∈ interedges r s t
hy : a✝ ∈ interedges r s t'
⊢ False

Tactic:
rw [mem_interedges_iff] at hx hy

Result:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'
a✝ : α × β
hx : a✝.1 ∈ s ∧ a✝.2 ∈ t ∧ r a✝.1 a✝.2
hy : a✝.1 ∈ s ∧ a✝.2 ∈ t' ∧ r a✝.1 a✝.2
⊢ False