harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Tactic/Ring/Basic.lean
theorem inv_mul {R} [DivisionRing R] {a₁ a₂ a₃ b₁ b₃ c}
    (_ : (a₁⁻¹ : R) = b₁) (_ : (a₃⁻¹ : R) = b₃)
    (_ : b₃ * (b₁ ^ a₂ * (nat_lit 1).rawCast) = c) :
    (a₁ ^ a₂ * a₃ : R)⁻¹ = c

Proof state:
R : Type u_2
inst✝ : DivisionRing R
a₁ : R
a₂ : ℕ
a₃ b₁ b₃ c : R
x✝² : a₁⁻¹ = b₁
x✝¹ : a₃⁻¹ = b₃
x✝ : b₃ * (b₁ ^ a₂ * Nat.rawCast 1) = c
⊢ (a₁ ^ a₂ * a₃)⁻¹ = c

Tactic:
subst_vars

Result:
R : Type u_2
inst✝ : DivisionRing R
a₁ : R
a₂ : ℕ
a₃ : R
⊢ (a₁ ^ a₂ * a₃)⁻¹ = a₃⁻¹ * (a₁⁻¹ ^ a₂ * Nat.rawCast 1)

Proof state:
R : Type u_2
inst✝ : DivisionRing R
a₁ : R
a₂ : ℕ
a₃ : R
⊢ (a₁ ^ a₂ * a₃)⁻¹ = a₃⁻¹ * (a₁⁻¹ ^ a₂ * Nat.rawCast 1)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_insertMany_empty_list_of_mem [LawfulBEq α]
    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} {fallback : β}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    getD (insertMany (empty : Raw₀ α (fun _ => β)) l) k' fallback = v

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
inst✝ : LawfulBEq α
l : List (α × β)
k k' : α
k_beq : (k == k') = true
v fallback : β
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : (k, v) ∈ l
⊢ getD (insertMany empty l).val k' fallback = v

Tactic:
rw [getD_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean
theorem map_eq_zero_iff (F : C ⥤ D) [PreservesZeroMorphisms F] [Faithful F] {X Y : C} {f : X ⟶ Y} :
    F.map f = 0 ↔ f = 0 :=
  ⟨F.zero_of_map_zero _, by
    rintro rfl
    exact F.map_zero _ _⟩

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
X Y : C
f : X ⟶ Y
⊢ f = 0 → F.map f = 0

Tactic:
rintro rfl

Result:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
X Y : C
⊢ F.map 0 = 0

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
X Y : C
⊢ F.map 0 = 0

Tactic:
exact F.map_zero _ _

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem dotProduct_neg : v ⬝ᵥ -w = -(v ⬝ᵥ w)

Proof state:
m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocRing α
v w : m → α
⊢ v ⬝ᵥ -w = -(v ⬝ᵥ w)

Tactic:
simp [dotProduct]

Result:
no goals
-- Mathlib/SetTheory/Game/Short.lean
theorem short_birthday (x : PGame.{u}) : [Short x] → x.birthday < Ordinal.omega0

Proof state:
case mk.mk.right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → (xL i).Short
sR : (j : xr) → (xR j).Short
i : xr
⊢ (xR i).birthday < Cardinal.aleph0.ord

Tactic:
rw [Cardinal.ord_aleph0]

Result:
case mk.mk.right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → (xL i).Short
sR : (j : xr) → (xR j).Short
i : xr
⊢ (xR i).birthday < Ordinal.omega0
-- Mathlib/Data/Set/Pointwise/SMul.lean
@[simp] protected lemma inv_zero : (0 : Set α)⁻¹ = 0

Proof state:
case h
α : Type u_2
inst✝ : GroupWithZero α
x✝ : α
⊢ x✝ ∈ 0⁻¹ ↔ x✝ ∈ 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝ : GroupWithZero α
⊢ 0⁻¹ = 0

Tactic:
ext

Result:
case h
α : Type u_2
inst✝ : GroupWithZero α
x✝ : α
⊢ x✝ ∈ 0⁻¹ ↔ x✝ ∈ 0
-- Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
lemma invMulSubgroup_eq_mul_inv (A : Finset G) (h) : (invMulSubgroup A h : Set G) = A * A⁻¹

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ ↑(#(A * A)) < 2 * ↑(#A)

Tactic:
linarith

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ ↑A * ↑A⁻¹ = ↑A⁻¹ * ↑A

Tactic:
norm_cast

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ A * A⁻¹ = A⁻¹ * A

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ ↑(A.invMulSubgroup h) = ↑A * ↑A⁻¹

Tactic:
rw [invMulSubgroup_eq_inv_mul, eq_comm]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ ↑A * ↑A⁻¹ = ↑A⁻¹ * ↑A

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ #(A * A) < 2 * #A

Tactic:
qify at h ⊢

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ ↑(#(A * A)) < 2 * ↑(#A)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ A * A⁻¹ = A⁻¹ * A

Tactic:
exact mul_inv_eq_inv_mul_of_doubling_lt_two (by qify at h ⊢; linarith)

Result:
no goals
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
theorem toOpen_toSpecΓ_app {X : Scheme.{u}} (U) :
    StructureSheaf.toOpen _ _ ≫ X.toSpecΓ.app U =
      X.presheaf.map (homOfLE (by exact le_top)).op

Proof state:
X : Scheme
U : (Spec Γ(X, ⊤)).Opens
⊢ (𝟙 (Scheme.Γ.rightOp.obj X)).unop ≫ ((pushforward CommRingCat X.toSpecΓ.base).obj X.presheaf).map (homOfLE ⋯).op =
    X.presheaf.map (homOfLE ⋯).op

Tactic:
dsimp

Result:
X : Scheme
U : (Spec Γ(X, ⊤)).Opens
⊢ 𝟙 Γ(X, ⊤) ≫ X.presheaf.map (homOfLE ⋯).op = X.presheaf.map (homOfLE ⋯).op

Proof state:
X : Scheme
U : (Spec Γ(X, ⊤)).Opens
⊢ 𝟙 Γ(X, ⊤) ≫ X.presheaf.map (homOfLE ⋯).op = X.presheaf.map (homOfLE ⋯).op

Tactic:
exact Category.id_comp _

Result:
no goals

Proof state:
X : Scheme
U : (Spec Γ(X, ⊤)).Opens
⊢ X.toSpecΓ ⁻¹ᵁ U ≤ ⊤

Tactic:
exact le_top

Result:
no goals

Proof state:
X : Scheme
U : (Spec Γ(X, ⊤)).Opens
⊢ toOpen ↑Γ(X, ⊤) ⊤ ≫
      X.toSpecΓ.c.app (op ⊤) ≫ ((pushforward CommRingCat X.toSpecΓ.base).obj X.presheaf).map (homOfLE ⋯).op =
    X.presheaf.map (homOfLE ⋯).op

Tactic:
show (ΓSpec.adjunction.counit.app (Scheme.Γ.rightOp.obj X)).unop ≫
  (Scheme.Γ.rightOp.map (ΓSpec.adjunction.unit.app X)).unop ≫ _ = _

Result:
X : Scheme
U : (Spec Γ(X, ⊤)).Opens
⊢ (ΓSpec.adjunction.counit.app (Scheme.Γ.rightOp.obj X)).unop ≫
      (Scheme.Γ.rightOp.map (ΓSpec.adjunction.unit.app X)).unop ≫
        ((pushforward CommRingCat X.toSpecΓ.base).obj X.presheaf).map (homOfLE ⋯).op =
    X.presheaf.map (homOfLE ⋯).op

Proof state:
X : Scheme
U : (Spec Γ(X, ⊤)).Opens
⊢ toOpen (↑Γ(X, ⊤)) U ≫ Scheme.Hom.app X.toSpecΓ U = X.presheaf.map (homOfLE ⋯).op

Tactic:
rw [← StructureSheaf.toOpen_res _ _ _ (homOfLE le_top), Category.assoc,
  NatTrans.naturality _ (homOfLE (le_top (a := U))).op]

Result:
X : Scheme
U : (Spec Γ(X, ⊤)).Opens
⊢ toOpen ↑Γ(X, ⊤) ⊤ ≫
      X.toSpecΓ.c.app (op ⊤) ≫ ((pushforward CommRingCat X.toSpecΓ.base).obj X.presheaf).map (homOfLE ⋯).op =
    X.presheaf.map (homOfLE ⋯).op

Proof state:
X : Scheme
U : (Spec Γ(X, ⊤)).Opens
⊢ (ΓSpec.adjunction.counit.app (Scheme.Γ.rightOp.obj X)).unop ≫
      (Scheme.Γ.rightOp.map (ΓSpec.adjunction.unit.app X)).unop ≫
        ((pushforward CommRingCat X.toSpecΓ.base).obj X.presheaf).map (homOfLE ⋯).op =
    X.presheaf.map (homOfLE ⋯).op

Tactic:
rw [← Category.assoc, ← unop_comp, ΓSpec.adjunction.left_triangle_components]

Result:
X : Scheme
U : (Spec Γ(X, ⊤)).Opens
⊢ (𝟙 (Scheme.Γ.rightOp.obj X)).unop ≫ ((pushforward CommRingCat X.toSpecΓ.base).obj X.presheaf).map (homOfLE ⋯).op =
    X.presheaf.map (homOfLE ⋯).op
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma neg_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    W.neg P = P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.neg P = P z • ![P x / P z, (toAffine W).negY (P x / P z) (P y / P z), 1]

Tactic:
erw [neg, smul_fin3, mul_div_cancel₀ _ hPz, ← negY_of_Z_ne_zero hPz, mul_div_cancel₀ _ hPz,
  mul_one]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem add_limZero {f g : CauSeq β abv} (hf : LimZero f) (hg : LimZero g) : LimZero (f + g)
  | ε, ε0 =>
    (exists_forall_ge_and (hf _ <| half_pos ε0) (hg _ <| half_pos ε0)).imp fun _ H j ij => by
      let ⟨H₁, H₂⟩ := H _ ij
      simpa [add_halves ε] using lt_of_le_of_lt (abv_add abv _ _) (add_lt_add H₁ H₂)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑f j) < ε / 2 ∧ abv (↑g j) < ε / 2
j : ℕ
ij : j ≥ x✝
H₁ : abv (↑f j) < ε / 2
H₂ : abv (↑g j) < ε / 2
⊢ abv (↑(f + g) j) < ε

Tactic:
simpa [add_halves ε] using lt_of_le_of_lt (abv_add abv _ _) (add_lt_add H₁ H₂)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑f j) < ε / 2 ∧ abv (↑g j) < ε / 2
j : ℕ
ij : j ≥ x✝
⊢ abv (↑(f + g) j) < ε

Tactic:
let ⟨H₁, H₂⟩ := H _ ij

Result:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑f j) < ε / 2 ∧ abv (↑g j) < ε / 2
j : ℕ
ij : j ≥ x✝
H₁ : abv (↑f j) < ε / 2
H₂ : abv (↑g j) < ε / 2
⊢ abv (↑(f + g) j) < ε
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem coe_algebraMap_mem (r : R) : ↑((algebraMap R K) r) ∈ adicCompletionIntegers K v

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ ↑((algebraMap R K) r) ∈ adicCompletionIntegers K v

Tactic:
rw [mem_adicCompletionIntegers]

Result:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ Valued.v ↑((algebraMap R K) r) ≤ 1

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ Valued.v ↑((algebraMap R K) r) ≤ 1

Tactic:
letI : Valued K ℤₘ₀ := adicValued v

Result:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
this : Valued K ℤₘ₀ := v.adicValued
⊢ Valued.v ↑((algebraMap R K) r) ≤ 1

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
this : Valued K ℤₘ₀ := v.adicValued
⊢ Valued.v ↑((algebraMap R K) r) ≤ 1

Tactic:
rw [Valued.valuedCompletion_apply]

Result:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
this : Valued K ℤₘ₀ := v.adicValued
⊢ Valued.v ((algebraMap R K) r) ≤ 1

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
this : Valued K ℤₘ₀ := v.adicValued
⊢ Valued.v ((algebraMap R K) r) ≤ 1

Tactic:
exact v.valuation_le_one _

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
theorem toComplex_involute (c : CliffordAlgebra Q) :
    toComplex (involute c) = conj (toComplex c)

Proof state:
c : CliffordAlgebra Q
⊢ toComplex (involute c) = (starRingEnd ℂ) (toComplex c)

Tactic:
have : toComplex (involute (ι Q 1)) = conj (toComplex (ι Q 1)) := by
  simp only [involute_ι, toComplex_ι, map_neg, one_smul, Complex.conj_I]

Result:
c : CliffordAlgebra Q
this : toComplex (involute ((ι Q) 1)) = (starRingEnd ℂ) (toComplex ((ι Q) 1))
⊢ toComplex (involute c) = (starRingEnd ℂ) (toComplex c)

Proof state:
c : CliffordAlgebra Q
this✝ : toComplex (involute ((ι Q) 1)) = (starRingEnd ℂ) (toComplex ((ι Q) 1))
this : toComplex.comp involute = (↑Complex.conjAe).comp toComplex
⊢ toComplex (involute c) = (starRingEnd ℂ) (toComplex c)

Tactic:
exact AlgHom.congr_fun this c

Result:
no goals

Proof state:
c : CliffordAlgebra Q
this : toComplex (involute ((ι Q) 1)) = (starRingEnd ℂ) (toComplex ((ι Q) 1))
⊢ toComplex (involute c) = (starRingEnd ℂ) (toComplex c)

Tactic:
suffices toComplex.comp involute = Complex.conjAe.toAlgHom.comp toComplex by
  exact AlgHom.congr_fun this c

Result:
c : CliffordAlgebra Q
this : toComplex (involute ((ι Q) 1)) = (starRingEnd ℂ) (toComplex ((ι Q) 1))
⊢ toComplex.comp involute = (↑Complex.conjAe).comp toComplex

Proof state:
c : CliffordAlgebra Q
⊢ toComplex (involute ((ι Q) 1)) = (starRingEnd ℂ) (toComplex ((ι Q) 1))

Tactic:
simp only [involute_ι, toComplex_ι, map_neg, one_smul, Complex.conj_I]

Result:
no goals

Proof state:
case a.h
c : CliffordAlgebra Q
this : toComplex (involute ((ι Q) 1)) = (starRingEnd ℂ) (toComplex ((ι Q) 1))
⊢ ((toComplex.comp involute).toLinearMap ∘ₗ ι Q) 1 = (((↑Complex.conjAe).comp toComplex).toLinearMap ∘ₗ ι Q) 1

Tactic:
exact this

Result:
no goals

Proof state:
c : CliffordAlgebra Q
this : toComplex (involute ((ι Q) 1)) = (starRingEnd ℂ) (toComplex ((ι Q) 1))
⊢ toComplex.comp involute = (↑Complex.conjAe).comp toComplex

Tactic:
ext : 2

Result:
case a.h
c : CliffordAlgebra Q
this : toComplex (involute ((ι Q) 1)) = (starRingEnd ℂ) (toComplex ((ι Q) 1))
⊢ ((toComplex.comp involute).toLinearMap ∘ₗ ι Q) 1 = (((↑Complex.conjAe).comp toComplex).toLinearMap ∘ₗ ι Q) 1
-- Mathlib/Data/Sym/Sym2/Order.lean
theorem inf_le_sup [Lattice α] (s : Sym2 α) : s.inf ≤ s.sup

Proof state:
case h
α : Type u_1
inst✝ : Lattice α
x✝ y✝ : α
⊢ s(x✝, y✝).inf ≤ s(x✝, y✝).sup

Tactic:
simp [_root_.inf_le_sup]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Lattice α
s : Sym2 α
⊢ s.inf ≤ s.sup

Tactic:
cases s using Sym2.ind

Result:
case h
α : Type u_1
inst✝ : Lattice α
x✝ y✝ : α
⊢ s(x✝, y✝).inf ≤ s(x✝, y✝).sup
-- Mathlib/Order/Compare.lean
theorem le_iff_le_of_cmp_eq_cmp (h : cmp x y = cmp x' y') : x ≤ y ↔ x' ≤ y'

Proof state:
case h.h
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ cmp y x = cmp y' x'

Tactic:
rwa [cmp_eq_cmp_symm]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ y < x ↔ y' < x'

Tactic:
apply lt_iff_lt_of_cmp_eq_cmp

Result:
case h.h
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ cmp y x = cmp y' x'

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ ¬y < x ↔ ¬y' < x'

Tactic:
apply not_congr

Result:
case h
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ y < x ↔ y' < x'

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x ≤ y ↔ x' ≤ y'

Tactic:
rw [← not_lt, ← not_lt]

Result:
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ ¬y < x ↔ ¬y' < x'
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem exists_frequently_lt_of_liminf_ne_top {ι : Type*} {l : Filter ι} {x : ι → ℝ}
    (hx : liminf (fun n => (Real.nnabs (x n) : ℝ≥0∞)) l ≠ ∞) : ∃ R, ∃ᶠ n in l, x n < R

Proof state:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x_1 ≤ x x_2
r : ℝ≥0
⊢ ∀ᶠ (n : ℝ≥0∞) in map (fun n => ↑(Real.nnabs (x n))) l, ↑r ≤ n

Tactic:
simp only [eventually_map, ENNReal.coe_le_coe]

Result:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x_1 ≤ x x_2
r : ℝ≥0
⊢ ∀ᶠ (a : ι) in l, r ≤ Real.nnabs (x a)

Proof state:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x_1 ≤ x x_2
⊢ False

Tactic:
refine hx (ENNReal.eq_top_of_forall_nnreal_le fun r => le_limsInf_of_le (by isBoundedDefault) ?_)

Result:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x_1 ≤ x x_2
r : ℝ≥0
⊢ ∀ᶠ (n : ℝ≥0∞) in map (fun n => ↑(Real.nnabs (x n))) l, ↑r ≤ n

Proof state:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x_1 ≤ x x_2
r : ℝ≥0
⊢ IsCobounded (fun x1 x2 => x1 ≥ x2) (map (fun n => ↑(Real.nnabs (x n))) l)

Tactic:
isBoundedDefault

Result:
no goals

Proof state:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
⊢ ∃ R, ∃ᶠ (n : ι) in l, x n < R

Tactic:
by_contra h

Result:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
h : ¬∃ R, ∃ᶠ (n : ι) in l, x n < R
⊢ False

Proof state:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
h : ¬∃ R, ∃ᶠ (n : ι) in l, x n < R
⊢ False

Tactic:
simp_rw [not_exists, not_frequently, not_lt] at h

Result:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x_1 ≤ x x_2
⊢ False

Proof state:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x_1 ≤ x x_2
r : ℝ≥0
⊢ ∀ᶠ (a : ι) in l, r ≤ Real.nnabs (x a)

Tactic:
filter_upwards [h r] with i hi using hi.trans (le_abs_self (x i))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_append {a : α} {s : Vector α n} {t : Vector α m} :
    a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t

Proof state:
case mk
α : Type u_1
n m : Nat
a : α
t : Vector α m
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } ++ t ↔
    a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } ∨ a ∈ t

Tactic:
cases t

Result:
case mk.mk
α : Type u_1
n m : Nat
a : α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = m
⊢ a ∈
      { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
        { toArray := toArray✝, size_toArray := size_toArray✝ } ↔
    a ∈ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ∨
      a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk.mk
α : Type u_1
n m : Nat
a : α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = m
⊢ a ∈
      { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
        { toArray := toArray✝, size_toArray := size_toArray✝ } ↔
    a ∈ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ∨
      a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
a : α
s : Vector α n
t : Vector α m
⊢ a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t

Tactic:
cases s

Result:
case mk
α : Type u_1
n m : Nat
a : α
t : Vector α m
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } ++ t ↔
    a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } ∨ a ∈ t
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_mono_ae_restrict (h : f ≤ᵐ[μ.restrict (Icc a b)] g) :
    (∫ u in a..b, f u ∂μ) ≤ ∫ u in a..b, g u ∂μ

Proof state:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : f ≤ᶠ[ae (μ.restrict (Icc a b))] g
H : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioc a b), f x ≤ g x :=
  Eventually.filter_mono (ae_mono (Measure.restrict_mono Ioc_subset_Icc_self (le_refl μ))) h
⊢ ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ

Tactic:
simpa only [integral_of_le hab] using setIntegral_mono_ae_restrict hf.1 hg.1 H

Result:
no goals

Proof state:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : f ≤ᶠ[ae (μ.restrict (Icc a b))] g
⊢ ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ

Tactic:
let H := h.filter_mono <| ae_mono <| Measure.restrict_mono Ioc_subset_Icc_self <| le_refl μ

Result:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : f ≤ᶠ[ae (μ.restrict (Icc a b))] g
H : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioc a b), f x ≤ g x :=
  Eventually.filter_mono (ae_mono (Measure.restrict_mono Ioc_subset_Icc_self (le_refl μ))) h
⊢ ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ
-- Mathlib/Order/Defs/LinearOrder.lean
lemma max_def (a b : α) : max a b = if a ≤ b then b else a

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

Tactic:
rw [LinearOrder.max_def a]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem size_eq {t : RBNode α} : t.size = t.toList.length

Proof state:
α : Type u_1
t : RBNode α
⊢ t.size = t.toList.length

Tactic:
induction t <;> simp [*, size]

Result:
case node
α : Type u_1
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : l✝.size = l✝.toList.length
r_ih✝ : r✝.size = r✝.toList.length
⊢ l✝.toList.length + r✝.toList.length + 1 = l✝.toList.length + (r✝.toList.length + 1)

Proof state:
case node
α : Type u_1
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : l✝.size = l✝.toList.length
r_ih✝ : r✝.size = r✝.toList.length
⊢ l✝.toList.length + r✝.toList.length + 1 = l✝.toList.length + (r✝.toList.length + 1)

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Ideal.lean
theorem jacobson_matricesOver (I : TwoSidedIdeal R) :
    (I.matricesOver n).jacobson = I.jacobson.matricesOver n

Proof state:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ (matricesOver n I).jacobson = matricesOver n I.jacobson

Tactic:
apply le_antisymm

Result:
case a
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ (matricesOver n I).jacobson ≤ matricesOver n I.jacobson

case a
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ matricesOver n I.jacobson ≤ (matricesOver n I).jacobson

Proof state:
case a
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ matricesOver n I.jacobson ≤ (matricesOver n I).jacobson

Tactic:
show asIdeal (I.matricesOver n).jacobson ≥ asIdeal (I.jacobson.matricesOver n)

Result:
case a
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ asIdeal (matricesOver n I).jacobson ≥ asIdeal (matricesOver n I.jacobson)

Proof state:
case a
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ (matricesOver n I).jacobson ≤ matricesOver n I.jacobson

Tactic:
apply jacobson_matricesOver_le

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ asIdeal (matricesOver n I).jacobson ≥ asIdeal (matricesOver n I.jacobson)

Tactic:
simp [asIdeal_jacobson, asIdeal_matricesOver, Ideal.matricesOver_jacobson_le]

Result:
no goals