harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/MulChar/Duality.lean
lemma exists_apply_ne_one_iff_exists_monoidHom (a : Mˣ) :
    (∃ χ : MulChar M R, χ a ≠ 1) ↔ ∃ φ : Mˣ →* Rˣ, φ a ≠ 1

Proof state:
case refine_2
M : Type u_1
R : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommRing R
a : Mˣ
x✝ : ∃ φ, φ a ≠ 1
φ : Mˣ →* Rˣ
hφ : φ a ≠ 1
⊢ (ofUnitHom φ) ↑a ≠ 1

Tactic:
contrapose! hφ

Result:
case refine_2
M : Type u_1
R : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommRing R
a : Mˣ
x✝ : ∃ φ, φ a ≠ 1
φ : Mˣ →* Rˣ
hφ : (ofUnitHom φ) ↑a = 1
⊢ φ a = 1

Proof state:
case refine_1
M : Type u_1
R : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommRing R
a : Mˣ
x✝ : ∃ χ, χ ↑a ≠ 1
χ : MulChar M R
hχ : χ ↑a ≠ 1
⊢ χ.toUnitHom a ≠ 1

Tactic:
contrapose! hχ

Result:
case refine_1
M : Type u_1
R : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommRing R
a : Mˣ
x✝ : ∃ χ, χ ↑a ≠ 1
χ : MulChar M R
hχ : χ.toUnitHom a = 1
⊢ χ ↑a = 1

Proof state:
M : Type u_1
R : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommRing R
a : Mˣ
⊢ (∃ χ, χ ↑a ≠ 1) ↔ ∃ φ, φ a ≠ 1

Tactic:
refine ⟨fun ⟨χ, hχ⟩ ↦ ⟨χ.toUnitHom, ?_⟩, fun ⟨φ, hφ⟩ ↦ ⟨ofUnitHom φ, ?_⟩⟩

Result:
case refine_1
M : Type u_1
R : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommRing R
a : Mˣ
x✝ : ∃ χ, χ ↑a ≠ 1
χ : MulChar M R
hχ : χ ↑a ≠ 1
⊢ χ.toUnitHom a ≠ 1

case refine_2
M : Type u_1
R : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommRing R
a : Mˣ
x✝ : ∃ φ, φ a ≠ 1
φ : Mˣ →* Rˣ
hφ : φ a ≠ 1
⊢ (ofUnitHom φ) ↑a ≠ 1

Proof state:
case refine_1
M : Type u_1
R : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommRing R
a : Mˣ
x✝ : ∃ χ, χ ↑a ≠ 1
χ : MulChar M R
hχ : χ.toUnitHom a = 1
⊢ χ ↑a = 1

Tactic:
rwa [Units.ext_iff, coe_toUnitHom] at hχ

Result:
no goals

Proof state:
case refine_2
M : Type u_1
R : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommRing R
a : Mˣ
x✝ : ∃ φ, φ a ≠ 1
φ : Mˣ →* Rˣ
hφ : (ofUnitHom φ) ↑a = 1
⊢ φ a = 1

Tactic:
simpa only [ofUnitHom_eq, equivToUnitHom_symm_coe, Units.val_eq_one] using hφ

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma Exact.epi_f_iff (hS : S.Exact) : Epi S.f ↔ S.g = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ Epi S.f ↔ S.g = 0

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ Epi S.f → S.g = 0

case mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ S.g = 0 → Epi S.f

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ Epi S.f → S.g = 0

Tactic:
intro

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
a✝ : Epi S.f
⊢ S.g = 0

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
a✝ : Epi S.f
⊢ S.g = 0

Tactic:
rw [← cancel_epi S.f, zero, comp_zero]

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ S.g = 0 → Epi S.f

Tactic:
exact hS.epi_f

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Defs.lean
theorem atTop_eq_generate_Ici [Preorder α] : atTop = generate (range (Ici (α := α)))

Proof state:
α : Type u_3
inst✝ : Preorder α
⊢ atTop = generate (range Ici)

Tactic:
simp only [generate_eq_biInf, atTop, iInf_range]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
lemma LocallyLinear.map (f : α ↪ β) (hG : G.LocallyLinear) : (G.map f).LocallyLinear

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.LocallyLinear
⊢ ∀ ⦃x y : β⦄, (SimpleGraph.map f G).Adj x y → ∃ s, (SimpleGraph.map f G).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s

Tactic:
rintro _ _ ⟨a, b, h, rfl, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.LocallyLinear
a b : α
h : G.Adj a b
⊢ ∃ s, (SimpleGraph.map f G).IsNClique 3 s ∧ f a ∈ s ∧ f b ∈ s

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.LocallyLinear
a b : α
h : G.Adj a b
⊢ ∃ s, (SimpleGraph.map f G).IsNClique 3 s ∧ f a ∈ s ∧ f b ∈ s

Tactic:
obtain ⟨s, hs, ha, hb⟩ := hG.2 h

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.LocallyLinear
a b : α
h : G.Adj a b
s : Finset α
hs : G.IsNClique 3 s
ha : a ∈ s
hb : b ∈ s
⊢ ∃ s, (SimpleGraph.map f G).IsNClique 3 s ∧ f a ∈ s ∧ f b ∈ s

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.LocallyLinear
a b : α
h : G.Adj a b
s : Finset α
hs : G.IsNClique 3 s
ha : a ∈ s
hb : b ∈ s
⊢ ∃ s, (SimpleGraph.map f G).IsNClique 3 s ∧ f a ∈ s ∧ f b ∈ s

Tactic:
exact ⟨s.map f, hs.map, mem_map_of_mem _ ha, mem_map_of_mem _ hb⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.LocallyLinear
⊢ (SimpleGraph.map f G).LocallyLinear

Tactic:
refine ⟨hG.1.map _, ?_⟩

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.LocallyLinear
⊢ ∀ ⦃x y : β⦄, (SimpleGraph.map f G).Adj x y → ∃ s, (SimpleGraph.map f G).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s
-- Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
theorem rank_le_rankOfDiscrBdd :
    finrank ℚ K ≤ rankOfDiscrBdd N

Proof state:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ ↑↑N
⊢ ↑(finrank ℚ K) ≤ Real.log (9 / 4 * ↑N) / Real.log (3 * π / 4)

Tactic:
contrapose! h

Result:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : Real.log (9 / 4 * ↑N) / Real.log (3 * π / 4) < ↑(finrank ℚ K)
⊢ ↑↑N < 4 / 9 * (3 * π / 4) ^ finrank ℚ K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h : N = 0
⊢ discr K = 0

Tactic:
rwa [h, Nat.cast_zero, abs_nonpos_iff] at hK

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * ↑N) < ↑(finrank ℚ K)
⊢ 0 < 9 / 4 * ↑N

Tactic:
positivity

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
⊢ N ≠ 0

Tactic:
refine fun h ↦ discr_ne_zero K ?_

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h : N = 0
⊢ discr K = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
⊢ 1 < 3 * π / 4

Tactic:
rw [_root_.lt_div_iff₀ (by positivity), ← _root_.div_lt_iff₀' (by positivity), one_mul]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
⊢ 4 / 3 < π

Proof state:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ finrank ℚ K ≤ ⌊Real.log (9 / 4 * ↑N) / Real.log (3 * π / 4)⌋₊

Tactic:
rw [Nat.le_floor_iff]

Result:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ ↑(finrank ℚ K) ≤ Real.log (9 / 4 * ↑N) / Real.log (3 * π / 4)

case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ 0 ≤ Real.log (9 / 4 * ↑N) / Real.log (3 * π / 4)
-- Mathlib/CategoryTheory/Subpresheaf/Image.lean
@[simp]
lemma preimage_image_of_epi (G : Subpresheaf F) (p : F' ⟶ F) [hp : Epi p] :
    (G.preimage p).image p = G

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
p : F' ⟶ F
hp : Epi p
i : Cᵒᵖ
x : F.obj i
hx : x ∈ G.obj i
⊢ x ∈ ((G.preimage p).image p).obj i

Tactic:
simp only [NatTrans.epi_iff_epi_app, epi_iff_surjective] at hp

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
p : F' ⟶ F
i : Cᵒᵖ
x : F.obj i
hx : x ∈ G.obj i
hp : ∀ (k : Cᵒᵖ), Function.Surjective (p.app k)
⊢ x ∈ ((G.preimage p).image p).obj i

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
p : F' ⟶ F
i : Cᵒᵖ
x : F.obj i
hx : x ∈ G.obj i
hp : ∀ (k : Cᵒᵖ), Function.Surjective (p.app k)
⊢ x ∈ ((G.preimage p).image p).obj i

Tactic:
obtain ⟨y, rfl⟩ := hp _ x

Result:
case a.intro
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
p : F' ⟶ F
i : Cᵒᵖ
hp : ∀ (k : Cᵒᵖ), Function.Surjective (p.app k)
y : F'.obj i
hx : p.app i y ∈ G.obj i
⊢ p.app i y ∈ ((G.preimage p).image p).obj i

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
p : F' ⟶ F
hp : Epi p
⊢ G ≤ (G.preimage p).image p

Tactic:
intro i x hx

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
p : F' ⟶ F
hp : Epi p
i : Cᵒᵖ
x : F.obj i
hx : x ∈ G.obj i
⊢ x ∈ ((G.preimage p).image p).obj i

Proof state:
case a.intro
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
p : F' ⟶ F
i : Cᵒᵖ
hp : ∀ (k : Cᵒᵖ), Function.Surjective (p.app k)
y : F'.obj i
hx : p.app i y ∈ G.obj i
⊢ p.app i y ∈ ((G.preimage p).image p).obj i

Tactic:
exact ⟨y, hx, rfl⟩

Result:
no goals

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
p : F' ⟶ F
hp : Epi p
⊢ (G.preimage p).image p ≤ G

Tactic:
rw [image_le_iff]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
p : F' ⟶ F
hp : Epi p
⊢ (G.preimage p).image p = G

Tactic:
apply le_antisymm

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
p : F' ⟶ F
hp : Epi p
⊢ (G.preimage p).image p ≤ G

case a
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
p : F' ⟶ F
hp : Epi p
⊢ G ≤ (G.preimage p).image p
-- Mathlib/RingTheory/NonUnitalSubring/Basic.lean
theorem mem_closure_iff {s : Set R} {x} :
    x ∈ closure s ↔ x ∈ AddSubgroup.closure (Subsemigroup.closure s : Set R) :=
  ⟨fun h => by
    induction h using closure_induction with
    | mem _ hx => exact AddSubgroup.subset_closure (Subsemigroup.subset_closure hx)
    | zero => exact zero_mem _
    | add _ _ _ _ hx hy => exact add_mem hx hy
    | neg x _ hx => exact neg_mem hx
    | mul _ _ _hx _hy hx hy =>
      clear _hx _hy
      induction hx, hy using AddSubgroup.closure_induction₂ with
      | mem _ _ hx hy => exact AddSubgroup.subset_closure (mul_mem hx hy)
      | one_left => simpa using zero_mem _
      | one_right => simpa using zero_mem _
      | mul_left _ _ _ _ _ _ h₁ h₂ => simpa [add_mul] using add_mem h₁ h₂
      | mul_right _ _ _ _ _ _ h₁ h₂ => simpa [mul_add] using add_mem h₁ h₂
      | inv_left _ _ _ _ h => simpa [neg_mul] using neg_mem h
      | inv_right _ _ _ _ h => simpa [mul_neg] using neg_mem h,
  fun h => by
    induction h using AddSubgroup.closure_induction with
    | mem _ hx => induction hx using Subsemigroup.closure_induction with
      | mem _ h => exact subset_closure h
      | mul _ _ _ _ h₁ h₂ => exact mul_mem h₁ h₂
    | one => exact zero_mem _
    | mul _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
    | inv _ _ h => exact neg_mem h⟩

Proof state:
case mul.one_right
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝ x✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * 0 ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
simpa using zero_mem _

Result:
no goals

Proof state:
case mul
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ y✝ : R
hx : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
induction hx, hy using AddSubgroup.closure_induction₂ with
| mem _ _ hx hy => exact AddSubgroup.subset_closure (mul_mem hx hy)
| one_left => simpa using zero_mem _
| one_right => simpa using zero_mem _
| mul_left _ _ _ _ _ _ h₁ h₂ => simpa [add_mul] using add_mem h₁ h₂
| mul_right _ _ _ _ _ _ h₁ h₂ => simpa [mul_add] using add_mem h₁ h₂
| inv_left _ _ _ _ h => simpa [neg_mul] using neg_mem h
| inv_right _ _ _ _ h => simpa [mul_neg] using neg_mem h

Result:
no goals

Proof state:
case mem.mem
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ x✝ : R
h : x✝ ∈ s
⊢ x✝ ∈ closure s

Tactic:
exact subset_closure h

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_approx_end (n m : ℕ) (x : ℝ) (e₁ : n + 1 = m) (h : |x| ≤ 1) :
    |exp x - expNear m x 0| ≤ |x| ^ m / m.factorial * ((m + 1) / m)

Proof state:
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ |rexp x - expNear m x 0| ≤ |x| ^ m / ↑m.factorial * ((↑m + 1) / ↑m)

Tactic:
simp only [expNear, mul_zero, add_zero]

Result:
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ |rexp x - ∑ m ∈ range m, x ^ m / ↑m.factorial| ≤ |x| ^ m / ↑m.factorial * ((↑m + 1) / ↑m)

Proof state:
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ 0 < m

Tactic:
omega

Result:
no goals

Proof state:
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ |rexp x - ∑ m ∈ range m, x ^ m / ↑m.factorial| ≤ |x| ^ m / ↑m.factorial * ((↑m + 1) / ↑m)

Tactic:
convert exp_bound (n := m) h ?_ using 1

Result:
case h.e'_4
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ |x| ^ m / ↑m.factorial * ((↑m + 1) / ↑m) = |x| ^ m * (↑m.succ / (↑m.factorial * ↑m))

n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ 0 < m

Proof state:
case h.e'_4
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ |x| ^ m / ↑m.factorial * ((↑m + 1) / ↑m) = |x| ^ m * (↑m.succ / (↑m.factorial * ↑m))

Tactic:
field_simp [mul_comm]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem isUnit_iff_mulRight_bijective {a : M} :
    IsUnit a ↔ Function.Bijective (· * a) :=
  ⟨fun h ↦ ⟨h.mul_left_injective, fun y ↦ ⟨y * h.unit⁻¹, by simp [mul_assoc]⟩⟩,
    fun h ↦ ⟨⟨a, _, h.1 (by simpa [mul_assoc] using congr_arg (a * ·) (h.2 1).choose_spec),
      (h.2 1).choose_spec⟩, rfl⟩⟩

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
y : M
⊢ (fun x => x * a) (y * ↑h.unit⁻¹) = y

Tactic:
simp [mul_assoc]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem isEquiv_iff_val_lt_val [LinearOrderedCommGroupWithZero Γ₀]
    [LinearOrderedCommGroupWithZero Γ'₀] {v : Valuation K Γ₀} {v' : Valuation K Γ'₀} :
    v.IsEquiv v' ↔ ∀ {x y : K}, v x < v y ↔ v' x < v' y

Proof state:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ (∀ (r s : K), v s < v r ↔ v' s < v' r) ↔ ∀ {x y : K}, v x < v y ↔ v' x < v' y

Tactic:
exact forall_comm

Result:
no goals

Proof state:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ v.IsEquiv v' ↔ ∀ {x y : K}, v x < v y ↔ v' x < v' y

Tactic:
simp only [IsEquiv, le_iff_le_iff_lt_iff_lt]

Result:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ (∀ (r s : K), v s < v r ↔ v' s < v' r) ↔ ∀ {x y : K}, v x < v y ↔ v' x < v' y
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem exists_ne_zero_mem_ideal_lt (h : minkowskiBound K I < volume (convexBodyLT K f)) :
    ∃ a ∈ (I : FractionalIdeal (𝓞 K)⁰ K), a ≠ 0 ∧ ∀ w : InfinitePlace K, w a < f w

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
h : minkowskiBound K I < volume (convexBodyLT K f)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ∀ (w : InfinitePlace K), w a < ↑(f w)

Tactic:
have : Countable (span ℤ (Set.range (fractionalIdealLatticeBasis K I))).toAddSubgroup := by
  change Countable (span ℤ (Set.range (fractionalIdealLatticeBasis K I)))
  infer_instance

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
h : minkowskiBound K I < volume (convexBodyLT K f)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ∀ (w : InfinitePlace K), w a < ↑(f w)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
h : minkowskiBound K I < volume (convexBodyLT K f)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodyLT K f
⊢ a ≠ 0

Tactic:
simpa using h_nz

Result:
no goals
-- Mathlib/Algebra/Order/Nonneg/Field.lean
lemma NNRat.cast_nonneg (q : ℚ≥0) : 0 ≤ (q : α)

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
q : ℚ≥0
⊢ 0 ≤ ↑q.num / ↑q.den

Tactic:
exact div_nonneg q.num.cast_nonneg q.den.cast_nonneg

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
q : ℚ≥0
⊢ 0 ≤ ↑q

Tactic:
rw [cast_def]

Result:
α : Type u_1
inst✝ : LinearOrderedSemifield α
q : ℚ≥0
⊢ 0 ≤ ↑q.num / ↑q.den
-- Mathlib/Data/Finsupp/Basic.lean
theorem equivMapDomain_refl (l : α →₀ M) : equivMapDomain (Equiv.refl _) l = l

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
l : α →₀ M
⊢ equivMapDomain (Equiv.refl α) l = l

Tactic:
ext x

Result:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
l : α →₀ M
x : α
⊢ (equivMapDomain (Equiv.refl α) l) x = l x

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
l : α →₀ M
x : α
⊢ (equivMapDomain (Equiv.refl α) l) x = l x

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem reverse_reverse (as : Vector α n) : as.reverse.reverse = as

Proof state:
α : Type u_1
n : Nat
as : Vector α n
⊢ as.reverse.reverse = as

Tactic:
rcases as with ⟨as, rfl⟩

Result:
case mk
α : Type u_1
as : Array α
⊢ { toArray := as, size_toArray := ⋯ }.reverse.reverse = { toArray := as, size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
as : Array α
⊢ { toArray := as, size_toArray := ⋯ }.reverse.reverse = { toArray := as, size_toArray := ⋯ }

Tactic:
simp [Array.reverse_reverse]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Height.lean
lemma Ideal.primeHeight_lt_top (I : Ideal R) [I.FiniteHeight] [h : I.IsPrime] :
    I.primeHeight < ⊤

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.FiniteHeight
h : I.IsPrime
⊢ I.height < ⊤

Tactic:
exact Ideal.height_lt_top h.ne_top

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.FiniteHeight
h : I.IsPrime
⊢ I.primeHeight < ⊤

Tactic:
rw [← I.height_eq_primeHeight]

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.FiniteHeight
h : I.IsPrime
⊢ I.height < ⊤
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem AffineSubspace.isClosed_direction_iff (s : AffineSubspace 𝕜 Q) :
    IsClosed (s.direction : Set W) ↔ IsClosed (s : Set Q)

Proof state:
case inr.intro
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
s : AffineSubspace 𝕜 Q
x : Q
hx : x ∈ ↑s
⊢ IsClosed ((fun x_1 => x_1 -ᵥ x) '' ↑s) ↔ IsClosed (⇑(IsometryEquiv.vaddConst x).toHomeomorph.symm '' ↑s)

Tactic:
rfl

Result:
no goals

Proof state:
case inr.intro
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
s : AffineSubspace 𝕜 Q
x : Q
hx : x ∈ ↑s
⊢ IsClosed ↑s.direction ↔ IsClosed ↑s

Tactic:
rw [← (IsometryEquiv.vaddConst x).toHomeomorph.symm.isClosed_image,
  AffineSubspace.coe_direction_eq_vsub_set_right hx]

Result:
case inr.intro
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
s : AffineSubspace 𝕜 Q
x : Q
hx : x ∈ ↑s
⊢ IsClosed ((fun x_1 => x_1 -ᵥ x) '' ↑s) ↔ IsClosed (⇑(IsometryEquiv.vaddConst x).toHomeomorph.symm '' ↑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
s : AffineSubspace 𝕜 Q
⊢ IsClosed ↑s.direction ↔ IsClosed ↑s

Tactic:
rcases s.eq_bot_or_nonempty with (rfl | ⟨x, hx⟩)

Result:
case inl
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
⊢ IsClosed ↑⊥.direction ↔ IsClosed ↑⊥

case inr.intro
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
s : AffineSubspace 𝕜 Q
x : Q
hx : x ∈ ↑s
⊢ IsClosed ↑s.direction ↔ IsClosed ↑s

Proof state:
case inl
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
⊢ IsClosed ↑⊥.direction ↔ IsClosed ↑⊥

Tactic:
simp [isClosed_singleton]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
/-- Adding a gift horse left option does not change the value of `x`. A gift horse left option is
 a game `x'` with `x' ⧏ x`. It is called "gift horse" because it seems like Left has gotten the
 "gift" of a new option, but actually the value of the game did not change. -/
lemma insertLeft_equiv_of_lf {x x' : PGame} (h : x' ⧏ x) : insertLeft x x' ≈ x

Proof state:
case left.left
x x' : PGame
h : x' ⧏ x
i : (x.insertLeft x').LeftMoves
⊢ (∃ i', (x.insertLeft x').moveLeft i ≤ x.moveLeft i') ∨ ∃ j, ((x.insertLeft x').moveLeft i).moveRight j ≤ x

Tactic:
rcases x with ⟨xl, xr, xL, xR⟩

Result:
case left.left.mk
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : x' ⧏ mk xl xr xL xR
i : ((mk xl xr xL xR).insertLeft x').LeftMoves
⊢ (∃ i', ((mk xl xr xL xR).insertLeft x').moveLeft i ≤ (mk xl xr xL xR).moveLeft i') ∨
    ∃ j, (((mk xl xr xL xR).insertLeft x').moveLeft i).moveRight j ≤ mk xl xr xL xR

Proof state:
case left.left.mk
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : x' ⧏ mk xl xr xL xR
i : ((mk xl xr xL xR).insertLeft x').LeftMoves
⊢ (∃ i', ((mk xl xr xL xR).insertLeft x').moveLeft i ≤ (mk xl xr xL xR).moveLeft i') ∨
    ∃ j, (((mk xl xr xL xR).insertLeft x').moveLeft i).moveRight j ≤ mk xl xr xL xR

Tactic:
simp only [insertLeft, leftMoves_mk, moveLeft_mk] at i ⊢

Result:
case left.left.mk
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : x' ⧏ mk xl xr xL xR
i : xl ⊕ PUnit.{u_1 + 1}
⊢ (∃ i', Sum.elim xL (fun x => x') i ≤ xL i') ∨ ∃ j, (Sum.elim xL (fun x => x') i).moveRight j ≤ mk xl xr xL xR