harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/IntegralDomain.lean
theorem isCyclic_of_subgroup_isDomain [Finite G] (f : G →* R) (hf : Injective f) : IsCyclic G

Proof state:
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ⇑f
⊢ IsCyclic G

Tactic:
cases nonempty_fintype G

Result:
case intro
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ⇑f
val✝ : Fintype G
⊢ IsCyclic G

Proof state:
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ⇑f
⊢ IsCyclic G

Tactic:
classical
  cases nonempty_fintype G
  apply isCyclic_of_card_pow_eq_one_le
  intro n hn
  exact le_trans (card_nthRoots_subgroup_units f hf hn 1) (card_nthRoots n (f 1))

Result:
no goals

Proof state:
case intro
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ⇑f
val✝ : Fintype G
⊢ IsCyclic G

Tactic:
apply isCyclic_of_card_pow_eq_one_le

Result:
case intro.hn
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ⇑f
val✝ : Fintype G
⊢ ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n

Proof state:
case intro.hn
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ⇑f
val✝ : Fintype G
n : ℕ
hn : 0 < n
⊢ #(filter (fun a => a ^ n = 1) univ) ≤ n

Tactic:
exact le_trans (card_nthRoots_subgroup_units f hf hn 1) (card_nthRoots n (f 1))

Result:
no goals

Proof state:
case intro.hn
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ⇑f
val✝ : Fintype G
⊢ ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n

Tactic:
intro n hn

Result:
case intro.hn
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ⇑f
val✝ : Fintype G
n : ℕ
hn : 0 < n
⊢ #(filter (fun a => a ^ n = 1) univ) ≤ n
-- Mathlib/RingTheory/TwoSidedIdeal/BigOperators.lean
lemma listSum_mem {ι : Type*} (l : List ι) (f : ι → R) (hl : ∀ x ∈ l, f x ∈ I) :
    (l.map f).sum ∈ I

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ (List.map f l).sum ∈ I

Tactic:
rw [mem_iff, ← List.sum_map_zero]

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ I.ringCon (List.map f l).sum (List.map (fun x => 0) ?m.356).sum

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ Type ?u.352

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ List ?m.353

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ I.ringCon (List.map f l).sum (List.map (fun x => 0) ?m.356).sum

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ Type ?u.352

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ List ?m.353

Tactic:
exact I.ringCon.listSum l hl

Result:
no goals
-- Mathlib/Algebra/Ring/NegOnePow.lean
lemma negOnePow_odd (n : ℤ) (hn : Odd n) : n.negOnePow = -1

Proof state:
case intro
k : ℤ
⊢ (2 * k + 1).negOnePow = -1

Tactic:
simp only [negOnePow_add, negOnePow_two_mul, negOnePow_one, mul_neg, mul_one]

Result:
no goals

Proof state:
n : ℤ
hn : Odd n
⊢ n.negOnePow = -1

Tactic:
obtain ⟨k, rfl⟩ := hn

Result:
case intro
k : ℤ
⊢ (2 * k + 1).negOnePow = -1
-- Mathlib/Data/Rel.lean
theorem comp_right_bot (r : Rel α β) : r • (⊥ : Rel β γ) = ⊥

Proof state:
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x : α
y : γ
⊢ (r • ⊥) x y ↔ ⊥ x y

Tactic:
simp [comp, Bot.bot]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
⊢ r • ⊥ = ⊥

Tactic:
ext x y

Result:
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x : α
y : γ
⊢ (r • ⊥) x y ↔ ⊥ x y
-- Mathlib/Data/Real/EReal.lean
lemma inv_pos_of_pos_ne_top {a : EReal} (h : 0 < a) (h' : a ≠ ⊤) : 0 < a⁻¹

Proof state:
case h_real
a : ℝ
h : 0 < ↑a
h' : ↑a ≠ ⊤
⊢ 0 < ↑a⁻¹

Tactic:
norm_cast at *

Result:
case h_real
a : ℝ
h' : ¬↑a = ⊤
h : 0 < a
⊢ 0 < a⁻¹

Proof state:
case h_real
a : ℝ
h' : ¬↑a = ⊤
h : 0 < a
⊢ 0 < a⁻¹

Tactic:
exact inv_pos_of_pos h

Result:
no goals

Proof state:
case h_real
a : ℝ
h : 0 < ↑a
h' : ↑a ≠ ⊤
⊢ 0 < (↑a)⁻¹

Tactic:
rw [← coe_inv a]

Result:
case h_real
a : ℝ
h : 0 < ↑a
h' : ↑a ≠ ⊤
⊢ 0 < ↑a⁻¹

Proof state:
case h_top
h : 0 < ⊤
h' : ⊤ ≠ ⊤
⊢ 0 < ⊤⁻¹

Tactic:
exact (h' (Eq.refl ⊤)).rec

Result:
no goals

Proof state:
case h_bot
h : 0 < ⊥
h' : ⊥ ≠ ⊤
⊢ 0 < ⊥⁻¹

Tactic:
exact (not_lt_bot h).rec

Result:
no goals

Proof state:
a : EReal
h : 0 < a
h' : a ≠ ⊤
⊢ 0 < a⁻¹

Tactic:
cases a with
| h_bot => exact (not_lt_bot h).rec
| h_real a =>  rw [← coe_inv a]; norm_cast at *; exact inv_pos_of_pos h
| h_top => exact (h' (Eq.refl ⊤)).rec

Result:
no goals
-- Mathlib/Control/Lawful.lean
theorem run_map (f : α → β) [LawfulMonad m] : (f <$> x).run = Option.map f <$> x.run

Proof state:
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
⊢ (f <$> x).run = Option.map f <$> x.run

Tactic:
rw [← bind_pure_comp _ x.run]

Result:
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
⊢ (f <$> x).run = do
    let a ← x.run
    pure (Option.map f a)

Proof state:
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
⊢ (do
      let x ← x.run
      match x with
        | some a => (pure (f a)).run
        | none => pure none) =
    do
    let a ← x.run
    pure (Option.map f a)

Tactic:
apply bind_congr

Result:
case h
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
⊢ ∀ (a : Option α),
    (match a with
      | some a => (pure (f a)).run
      | none => pure none) =
      pure (Option.map f a)

Proof state:
case h
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
⊢ ∀ (a : Option α),
    (match a with
      | some a => (pure (f a)).run
      | none => pure none) =
      pure (Option.map f a)

Tactic:
intro a

Result:
case h
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
a : Option α
⊢ (match a with
    | some a => (pure (f a)).run
    | none => pure none) =
    pure (Option.map f a)

Proof state:
case h
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
a : Option α
⊢ (match a with
    | some a => (pure (f a)).run
    | none => pure none) =
    pure (Option.map f a)

Tactic:
cases a <;> simp [Option.map, Option.bind]

Result:
no goals

Proof state:
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
⊢ (f <$> x).run = do
    let a ← x.run
    pure (Option.map f a)

Tactic:
change x.run >>= (fun
                   | some a => OptionT.run (pure (f a))
                   | none   => pure none) = _

Result:
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
⊢ (do
      let x ← x.run
      match x with
        | some a => (pure (f a)).run
        | none => pure none) =
    do
    let a ← x.run
    pure (Option.map f a)
-- Mathlib/AlgebraicTopology/SimplicialObject/Split.lean
theorem eqId_iff_len_eq : A.EqId ↔ A.1.unop.len = Δ.unop.len

Proof state:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop A.fst).len = (unop Δ).len
⊢ unop A.fst = unop Δ

Tactic:
ext

Result:
case mpr.a
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop A.fst).len = (unop Δ).len
⊢ (unop A.fst).len = (unop Δ).len

Proof state:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId ↔ (unop A.fst).len = (unop Δ).len

Tactic:
rw [eqId_iff_eq]

Result:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ ↔ (unop A.fst).len = (unop Δ).len

Proof state:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst = Δ
⊢ (unop A.fst).len = (unop Δ).len

Tactic:
rw [h]

Result:
no goals

Proof state:
case mpr.a
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop A.fst).len = (unop Δ).len
⊢ (unop A.fst).len = (unop Δ).len

Tactic:
exact h

Result:
no goals

Proof state:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ ↔ (unop A.fst).len = (unop Δ).len

Tactic:
constructor

Result:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ → (unop A.fst).len = (unop Δ).len

case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (unop A.fst).len = (unop Δ).len → A.fst = Δ

Proof state:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop A.fst).len = (unop Δ).len
⊢ A.fst = Δ

Tactic:
rw [← unop_inj_iff]

Result:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop A.fst).len = (unop Δ).len
⊢ unop A.fst = unop Δ

Proof state:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ → (unop A.fst).len = (unop Δ).len

Tactic:
intro h

Result:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst = Δ
⊢ (unop A.fst).len = (unop Δ).len

Proof state:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (unop A.fst).len = (unop Δ).len → A.fst = Δ

Tactic:
intro h

Result:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop A.fst).len = (unop Δ).len
⊢ A.fst = Δ
-- Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
theorem rightUnitor_naturality {M N : ModuleCat R} (f : M ⟶ N) :
    tensorHom f (𝟙 (ModuleCat.of R R)) ≫ (rightUnitor N).hom = (rightUnitor M).hom ≫ f

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ (mk R ↑M ↑(of R R)).compr₂ (Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) =
    (mk R ↑M ↑(of R R)).compr₂ (Hom.hom ((rightUnitor M).hom ≫ f))

Tactic:
ext x

Result:
case hf.H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ (((mk R ↑M ↑(of R R)).compr₂ (Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom))) x) 1 =
    (((mk R ↑M ↑(of R R)).compr₂ (Hom.hom ((rightUnitor M).hom ≫ f))) x) 1

Proof state:
case hf.H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ (((mk R ↑M ↑(of R R)).compr₂ (Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom))) x) 1 =
    (((mk R ↑M ↑(of R R)).compr₂ (Hom.hom ((rightUnitor M).hom ≫ f))) x) 1

Tactic:
dsimp

Result:
case hf.H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ (Hom.hom (rightUnitor N).hom) ((Hom.hom (tensorHom f (𝟙 (of R R)))) (x ⊗ₜ[R] 1)) =
    (Hom.hom f) ((Hom.hom (rightUnitor M).hom) (x ⊗ₜ[R] 1))

Proof state:
case hf.H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ (Hom.hom (rightUnitor N).hom) ((Hom.hom (tensorHom f (𝟙 (of R R)))) (x ⊗ₜ[R] 1)) =
    (Hom.hom f) ((Hom.hom (rightUnitor M).hom) (x ⊗ₜ[R] 1))

Tactic:
erw [TensorProduct.rid_tmul, TensorProduct.rid_tmul]

Result:
case hf.H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ (Hom.hom (𝟙 (of R R))) (x, 1).2 • (Hom.hom f) (x, 1).1 = (Hom.hom f) (1 • x)

Proof state:
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom = (rightUnitor M).hom ≫ f

Tactic:
ext : 1

Result:
case hf
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom) = Hom.hom ((rightUnitor M).hom ≫ f)

Proof state:
case hf.H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ (Hom.hom (𝟙 (of R R))) (x, 1).2 • (Hom.hom f) (x, 1).1 = (Hom.hom f) (1 • x)

Tactic:
rw [LinearMap.map_smul]

Result:
case hf.H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ (Hom.hom (𝟙 (of R R))) (x, 1).2 • (Hom.hom f) (x, 1).1 = 1 • (Hom.hom f) x

Proof state:
case hf.H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ (Hom.hom (𝟙 (of R R))) (x, 1).2 • (Hom.hom f) (x, 1).1 = 1 • (Hom.hom f) x

Tactic:
rfl

Result:
no goals

Proof state:
case hf
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom) = Hom.hom ((rightUnitor M).hom ≫ f)

Tactic:
apply TensorProduct.ext

Result:
case hf.H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ (mk R ↑M ↑(of R R)).compr₂ (Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) =
    (mk R ↑M ↑(of R R)).compr₂ (Hom.hom ((rightUnitor M).hom ≫ f))
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodyLT'_convex : Convex ℝ (convexBodyLT' K f w₀)

Proof state:
case pos
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
h✝ : x✝¹ = w₀
⊢ Convex ℝ {x | (-1 < x.re ∧ x.re < 1) ∧ -↑(f ↑x✝¹) ^ 2 < x.im ∧ x.im < ↑(f ↑x✝¹) ^ 2}

Tactic:
refine Convex.inter ((convex_halfSpace_re_gt _).inter (convex_halfSpace_re_lt _))
  ((convex_halfSpace_im_gt _).inter (convex_halfSpace_im_lt _))

Result:
no goals

Proof state:
case pos
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
h✝ : x✝¹ = w₀
⊢ Convex ℝ {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑x✝¹) ^ 2}

Tactic:
simp_rw [abs_lt]

Result:
case pos
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
h✝ : x✝¹ = w₀
⊢ Convex ℝ {x | (-1 < x.re ∧ x.re < 1) ∧ -↑(f ↑x✝¹) ^ 2 < x.im ∧ x.im < ↑(f ↑x✝¹) ^ 2}

Proof state:
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
⊢ Convex ℝ (if x✝¹ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑x✝¹) ^ 2} else ball 0 ↑(f ↑x✝¹))

Tactic:
split_ifs

Result:
case pos
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
h✝ : x✝¹ = w₀
⊢ Convex ℝ {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑x✝¹) ^ 2}

case neg
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
h✝ : ¬x✝¹ = w₀
⊢ Convex ℝ (ball 0 ↑(f ↑x✝¹))

Proof state:
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
⊢ Convex ℝ (convexBodyLT' K f w₀)

Tactic:
refine Convex.prod (convex_pi (fun _ _ => convex_ball _ _)) (convex_pi (fun _ _ => ?_))

Result:
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
⊢ Convex ℝ (if x✝¹ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑x✝¹) ^ 2} else ball 0 ↑(f ↑x✝¹))

Proof state:
case neg
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
h✝ : ¬x✝¹ = w₀
⊢ Convex ℝ (ball 0 ↑(f ↑x✝¹))

Tactic:
exact convex_ball _ _

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem add_le_add' : ∀ {a b c d : Cardinal}, a ≤ b → c ≤ d → a + c ≤ b + d

Proof state:
case mk.mk.mk.mk.intro.intro
a✝ : Cardinal.{u_1}
α : Type u_1
b✝ : Cardinal.{u_1}
β : Type u_1
c✝ : Cardinal.{u_1}
γ : Type u_1
d✝ : Cardinal.{u_1}
δ : Type u_1
e₁ : α ↪ β
e₂ : γ ↪ δ
⊢ Quot.mk (⇑isEquivalent) α + Quot.mk (⇑isEquivalent) γ ≤ Quot.mk (⇑isEquivalent) β + Quot.mk (⇑isEquivalent) δ

Tactic:
exact ⟨e₁.sumMap e₂⟩

Result:
no goals

Proof state:
⊢ ∀ {a b c d : Cardinal.{u_1}}, a ≤ b → c ≤ d → a + c ≤ b + d

Tactic:
rintro ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨δ⟩ ⟨e₁⟩ ⟨e₂⟩

Result:
case mk.mk.mk.mk.intro.intro
a✝ : Cardinal.{u_1}
α : Type u_1
b✝ : Cardinal.{u_1}
β : Type u_1
c✝ : Cardinal.{u_1}
γ : Type u_1
d✝ : Cardinal.{u_1}
δ : Type u_1
e₁ : α ↪ β
e₂ : γ ↪ δ
⊢ Quot.mk (⇑isEquivalent) α + Quot.mk (⇑isEquivalent) γ ≤ Quot.mk (⇑isEquivalent) β + Quot.mk (⇑isEquivalent) δ
-- Mathlib/Data/Ordering/Lemmas.lean
theorem ite_eq_lt_distrib (c : Prop) [Decidable c] (a b : Ordering) :
    ((if c then a else b) = Ordering.lt) = if c then a = Ordering.lt else b = Ordering.lt

Proof state:
c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt

Tactic:
by_cases c <;> simp [*]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsCycles.reachable_sdiff_toSubgraph_spanningCoe [Finite V] {v w : V} (hcyc : G.IsCycles)
    (p : G.Walk v w) (hp : p.IsPath) : (G \ p.toSubgraph.spanningCoe).Reachable w v

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
this : Fintype V
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
exact reachable_sdiff_toSubgraph_spanningCoe_aux hcyc p hp

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
have : Fintype V := Fintype.ofFinite V

Result:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
this : Fintype V
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma strictMonoOn_one_sub_smoothingFn :
    StrictMonoOn (fun (x : ℝ) => (1 : ℝ) - ε x) (Set.Ioi 1)

Proof state:
⊢ StrictMonoOn (fun x => 1 - ε x) (Set.Ioi 1)

Tactic:
simp_rw [sub_eq_add_neg]

Result:
⊢ StrictMonoOn (fun x => 1 + -ε x) (Set.Ioi 1)

Proof state:
⊢ StrictMonoOn (fun x => 1 + -ε x) (Set.Ioi 1)

Tactic:
exact StrictMonoOn.const_add (StrictAntiOn.neg <| strictAntiOn_smoothingFn) 1

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Positive.lean
theorem IsPositive.inner_nonneg_right {T : E →L[𝕜] E} (hT : IsPositive T) (x : E) :
    0 ≤ re ⟪x, T x⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : T.IsPositive
x : E
⊢ 0 ≤ re ⟪x, T x⟫_𝕜

Tactic:
rw [inner_re_symm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : T.IsPositive
x : E
⊢ 0 ≤ re ⟪T x, x⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : T.IsPositive
x : E
⊢ 0 ≤ re ⟪T x, x⟫_𝕜

Tactic:
exact hT.inner_nonneg_left x

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem nonneg_of_neg_nonpos {a : Int} (h : -a ≤ 0) : 0 ≤ a :=
  Int.le_of_neg_le_neg <| by rwa [Int.neg_zero]

Proof state:
a : Int
h : -a ≤ 0
⊢ -a ≤ -0

Tactic:
rwa [Int.neg_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.not_eq_not {a b : Bool} : ¬a = !b ↔ a = b

Proof state:
a b : Bool
⊢ ¬a = !b ↔ a = b

Tactic:
cases a <;> cases b <;> simp

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
/-- A strictly convex function admits at most one global minimum. -/
lemma StrictConvexOn.eq_of_isMinOn (hf : StrictConvexOn 𝕜 s f) (hfx : IsMinOn f s x)
    (hfy : IsMinOn f s y) (hx : x ∈ s) (hy : y ∈ s) : x = y

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : OrderedAddCommMonoid β
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := 2⁻¹ • x + 2⁻¹ • y
hz : z ∈ s
⊢ 2⁻¹ • f z + 2⁻¹ • f z = f z

Tactic:
rw [← _root_.add_smul]

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : OrderedAddCommMonoid β
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := 2⁻¹ • x + 2⁻¹ • y
hz : z ∈ s
⊢ (2⁻¹ + 2⁻¹) • f z = f z

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : OrderedAddCommMonoid β
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := 2⁻¹ • x + 2⁻¹ • y
⊢ False

Tactic:
have hz : z ∈ s := hf.1 hx hy (by norm_num) (by norm_num) <| by norm_num

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : OrderedAddCommMonoid β
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := 2⁻¹ • x + 2⁻¹ • y
hz : z ∈ s
⊢ False
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem atTop_basis' (a : α) : atTop.HasBasis (a ≤ ·) Ici

Proof state:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
this : Nonempty α
⊢ atTop.HasBasis (fun x => a ≤ x) Ici

Tactic:
refine atTop_basis.to_hasBasis (fun b _ ↦ ?_) fun b _ ↦ ⟨b, trivial, Subset.rfl⟩

Result:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
this : Nonempty α
b : α
x✝ : True
⊢ ∃ i', a ≤ i' ∧ Ici i' ⊆ Ici b

Proof state:
case intro.intro
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
this : Nonempty α
b : α
x✝ : True
c : α
hac : a ≤ c
hbc : b ≤ c
⊢ ∃ i', a ≤ i' ∧ Ici i' ⊆ Ici b

Tactic:
exact ⟨c, hac, Ici_subset_Ici.2 hbc⟩

Result:
no goals

Proof state:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
⊢ atTop.HasBasis (fun x => a ≤ x) Ici

Tactic:
have : Nonempty α := ⟨a⟩

Result:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
this : Nonempty α
⊢ atTop.HasBasis (fun x => a ≤ x) Ici

Proof state:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
this : Nonempty α
b : α
x✝ : True
⊢ ∃ i', a ≤ i' ∧ Ici i' ⊆ Ici b

Tactic:
obtain ⟨c, hac, hbc⟩ := exists_ge_ge a b

Result:
case intro.intro
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
this : Nonempty α
b : α
x✝ : True
c : α
hac : a ≤ c
hbc : b ≤ c
⊢ ∃ i', a ≤ i' ∧ Ici i' ⊆ Ici b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem head_modifyHead (f : α → α) (l : List α) (h) :
    (l.modifyHead f).head h = f (l.head (by simpa using h))

Proof state:
α : Type u_1
f : α → α
l : List α
h : modifyHead f l ≠ []
⊢ (modifyHead f l).head h = f (l.head ⋯)

Tactic:
cases l with
| nil => simp at h
| cons hd tl => simp

Result:
no goals

Proof state:
case cons
α : Type u_1
f : α → α
hd : α
tl : List α
h : modifyHead f (hd :: tl) ≠ []
⊢ (modifyHead f (hd :: tl)).head h = f ((hd :: tl).head ⋯)

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u_1
f : α → α
h : modifyHead f [] ≠ []
⊢ (modifyHead f []).head h = f ([].head ⋯)

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type ?u.7751
f : α → α
l : List α
h : modifyHead f l ≠ []
⊢ l ≠ []

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Ideals.lean
theorem idealOfEmpty_eq_bot : idealOfSet R (∅ : Set X) = ⊥ :=
  Ideal.ext fun f => by
    simp only [mem_idealOfSet, Set.compl_empty, Set.mem_univ, forall_true_left, Ideal.mem_bot,
      DFunLike.ext_iff, zero_apply]

Proof state:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
f : C(X, R)
⊢ f ∈ idealOfSet R ∅ ↔ f ∈ ⊥

Tactic:
simp only [mem_idealOfSet, Set.compl_empty, Set.mem_univ, forall_true_left, Ideal.mem_bot,
  DFunLike.ext_iff, zero_apply]

Result:
no goals