harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/Sheaf.lean
theorem isSheaf_of_isSheaf_comp (s : A ⥤ B) [ReflectsLimitsOfSize.{v₁, max v₁ u₁} s]
    (h : IsSheaf J (P ⋙ s)) : IsSheaf J P

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
B : Type u₃
inst✝¹ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝ : ReflectsLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : IsSheaf J (P ⋙ s)
⊢ IsSheaf J P

Tactic:
rw [isSheaf_iff_isLimit] at h ⊢

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
B : Type u₃
inst✝¹ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝ : ReflectsLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit ((P ⋙ s).mapCone S.arrows.cocone.op))
⊢ ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit (P.mapCone S.arrows.cocone.op))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
B : Type u₃
inst✝¹ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝ : ReflectsLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit ((P ⋙ s).mapCone S.arrows.cocone.op))
⊢ ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit (P.mapCone S.arrows.cocone.op))

Tactic:
exact fun X S hS ↦ (h S hS).map fun t ↦ isLimitOfReflects s t

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Zip.lean
theorem denote_zip {aig : AIG α} (target : ZipTarget aig len) :
    ∀ (idx : Nat) (hidx : idx < len),
      ⟦(zip aig target).aig, (zip aig target).vec.get idx hidx, assign⟧
        =
      ⟦target.func aig ⟨target.input.lhs.get idx hidx, target.input.rhs.get idx hidx⟩, assign⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
target : ZipTarget aig len
⊢ ∀ (idx : Nat) (hidx : idx < len),
    ⟦assign, { aig := (zip aig target).aig, ref := (zip aig target).vec.get idx hidx }⟧ =
      ⟦assign, target.func aig { lhs := target.input.lhs.get idx hidx, rhs := target.input.rhs.get idx hidx }⟧

Tactic:
intros

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
target : ZipTarget aig len
idx✝ : Nat
hidx✝ : idx✝ < len
⊢ ⟦assign, { aig := (zip aig target).aig, ref := (zip aig target).vec.get idx✝ hidx✝ }⟧ =
    ⟦assign, target.func aig { lhs := target.input.lhs.get idx✝ hidx✝, rhs := target.input.rhs.get idx✝ hidx✝ }⟧

Proof state:
case a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
target : ZipTarget aig len
idx✝ : Nat
hidx✝ : idx✝ < len
⊢ 0 ≤ idx✝

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
target : ZipTarget aig len
idx✝ : Nat
hidx✝ : idx✝ < len
⊢ ⟦assign, { aig := (zip aig target).aig, ref := (zip aig target).vec.get idx✝ hidx✝ }⟧ =
    ⟦assign, target.func aig { lhs := target.input.lhs.get idx✝ hidx✝, rhs := target.input.rhs.get idx✝ hidx✝ }⟧

Tactic:
apply zip.denote_go

Result:
case a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
target : ZipTarget aig len
idx✝ : Nat
hidx✝ : idx✝ < len
⊢ 0 ≤ idx✝
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffEdist_ne_top_of_nonempty_of_bounded (hs : s.Nonempty) (ht : t.Nonempty)
    (bs : IsBounded s) (bt : IsBounded t) : hausdorffEdist s t ≠ ⊤

Proof state:
case intro.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
⊢ hausdorffEdist s t ≠ ⊤

Tactic:
rcases bt.subset_closedBall cs with ⟨rt, hrt⟩

Result:
case intro.intro.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
⊢ hausdorffEdist s t ≠ ⊤

Proof state:
case H2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xt : x ∈ t
this : dist x cs ≤ rs ⊔ rt
⊢ 0 ≤ rs ⊔ rt

Tactic:
exact le_trans dist_nonneg this

Result:
no goals

Proof state:
case intro
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
ht : t.Nonempty
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
⊢ hausdorffEdist s t ≠ ⊤

Tactic:
rcases ht with ⟨ct, hct⟩

Result:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
⊢ hausdorffEdist s t ≠ ⊤
-- Mathlib/Data/Vector/Basic.lean
theorem ofFn_get (v : Vector α n) : ofFn (get v) = v

Proof state:
case mk.a
α : Type u_1
l : List α
⊢ (ofFn (get ⟨l, ⋯⟩)).toList = toList ⟨l, ⋯⟩

Tactic:
dsimp

Result:
case mk.a
α : Type u_1
l : List α
⊢ (ofFn (get ⟨l, ⋯⟩)).toList = l

Proof state:
case mk.a
α : Type u_1
l : List α
⊢ (ofFn (get ⟨l, ⋯⟩)).toList = l

Tactic:
simpa only [toList_ofFn] using List.ofFn_get _

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
v : Vector α n
⊢ ofFn v.get = v

Tactic:
rcases v with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
l : List α
⊢ ofFn (get ⟨l, ⋯⟩) = ⟨l, ⋯⟩

Proof state:
case mk
α : Type u_1
l : List α
⊢ ofFn (get ⟨l, ⋯⟩) = ⟨l, ⋯⟩

Tactic:
apply toList_injective

Result:
case mk.a
α : Type u_1
l : List α
⊢ (ofFn (get ⟨l, ⋯⟩)).toList = toList ⟨l, ⋯⟩
-- Mathlib/GroupTheory/EckmannHilton.lean
theorem mul_comm : Std.Commutative m₂ :=
  ⟨fun a b => by simpa [mul h₁ h₂ distrib, h₂.left_id, h₂.right_id] using distrib e₂ a b e₂⟩

Proof state:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₂ a b = m₂ b a

Tactic:
simpa [mul h₁ h₂ distrib, h₂.left_id, h₂.right_id] using distrib e₂ a b e₂

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Lemmas.lean
theorem testBit_ofBits (f : Fin n → Bool) :
    (ofBits f).testBit i = if h : i < n then f ⟨i, h⟩ else false

Proof state:
case inr
n i : Nat
f : Fin n → Bool
h : i ≥ n
⊢ (ofBits f).testBit i = if h : i < n then f ⟨i, h⟩ else false

Tactic:
simp [h, Nat.not_lt_of_ge h]

Result:
no goals

Proof state:
case inl
n i : Nat
f : Fin n → Bool
h : i < n
⊢ (ofBits f).testBit i = if h : i < n then f ⟨i, h⟩ else false

Tactic:
simp [h]

Result:
no goals

Proof state:
n i : Nat
f : Fin n → Bool
⊢ (ofBits f).testBit i = if h : i < n then f ⟨i, h⟩ else false

Tactic:
cases Nat.lt_or_ge i n with
| inl h => simp [h]
| inr h => simp [h, Nat.not_lt_of_ge h]

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem idealOfLE_le_of_le (R S : ValuationSubring K) (hR : A ≤ R) (hS : A ≤ S) (h : R ≤ S) :
    idealOfLE A S hS ≤ idealOfLE A R hR := fun x hx =>
  (valuation_lt_one_iff R _).2
    (by
      by_contra c; push_neg at c; replace c := monotone_mapOfLE R S h c
      rw [(mapOfLE _ _ _).map_one, mapOfLE_valuation_apply] at c
      apply not_le_of_lt ((valuation_lt_one_iff S _).1 hx) c)

Proof state:
K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : (R.mapOfLE S h) 1 ≤ (R.mapOfLE S h) (R.valuation ↑((A.inclusion R hR) x))
⊢ False

Tactic:
rw [(mapOfLE _ _ _).map_one, mapOfLE_valuation_apply] at c

Result:
K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : 1 ≤ S.valuation ↑((A.inclusion R hR) x)
⊢ False

Proof state:
K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : 1 ≤ R.valuation ↑((A.inclusion R hR) x)
⊢ False

Tactic:
replace c := monotone_mapOfLE R S h c

Result:
K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : (R.mapOfLE S h) 1 ≤ (R.mapOfLE S h) (R.valuation ↑((A.inclusion R hR) x))
⊢ False

Proof state:
K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : 1 ≤ S.valuation ↑((A.inclusion R hR) x)
⊢ False

Tactic:
apply not_le_of_lt ((valuation_lt_one_iff S _).1 hx) c

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : ¬R.valuation ↑((A.inclusion R hR) x) < 1
⊢ False

Tactic:
push_neg at c

Result:
K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : 1 ≤ R.valuation ↑((A.inclusion R hR) x)
⊢ False

Proof state:
K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
⊢ R.valuation ↑((A.inclusion R hR) x) < 1

Tactic:
by_contra c

Result:
K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : ¬R.valuation ↑((A.inclusion R hR) x) < 1
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem lt_of_getLsbD {x : BitVec w} {i : Nat} : getLsbD x i = true → i < w

Proof state:
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ x.getLsbD i = true → i < w

Tactic:
simp [h]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ x.getLsbD i = true → i < w

Tactic:
if h : i < w then
  simp [h]
else
  simp [Nat.ge_of_not_lt h]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
h : ¬i < w
⊢ x.getLsbD i = true → i < w

Tactic:
simp [Nat.ge_of_not_lt h]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Field.lean
theorem dvd {p : A[X]} (hp : Polynomial.aeval x p = 0) : minpoly A x ∣ p

Proof state:
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
⊢ minpoly A x ∣ p

Tactic:
rw [← modByMonic_eq_zero_iff_dvd (monic hx)]

Result:
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
⊢ p %ₘ minpoly A x = 0

Proof state:
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
hnz : ¬p %ₘ minpoly A x = 0
⊢ (p %ₘ minpoly A x).degree < (minpoly A x).degree

Tactic:
exact degree_modByMonic_lt _ (monic hx)

Result:
no goals

Proof state:
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
hnz : ¬p %ₘ minpoly A x = 0
⊢ False

Tactic:
apply degree_le_of_ne_zero A x hnz
  ((aeval_modByMonic_eq_self_of_root (monic hx) (aeval _ _)).trans hp) |>.not_lt

Result:
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
hnz : ¬p %ₘ minpoly A x = 0
⊢ (p %ₘ minpoly A x).degree < (minpoly A x).degree

Proof state:
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
⊢ minpoly A x ∣ p

Tactic:
by_cases hp0 : p = 0

Result:
case pos
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
hp0 : p = 0
⊢ minpoly A x ∣ p

case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
hp0 : ¬p = 0
⊢ minpoly A x ∣ p

Proof state:
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
⊢ p %ₘ minpoly A x = 0

Tactic:
by_contra hnz

Result:
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
hnz : ¬p %ₘ minpoly A x = 0
⊢ False

Proof state:
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
hp0 : ¬p = 0
⊢ minpoly A x ∣ p

Tactic:
have hx : IsIntegral A x := IsAlgebraic.isIntegral ⟨p, hp0, hp⟩

Result:
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
⊢ minpoly A x ∣ p

Proof state:
case pos
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
hp0 : p = 0
⊢ minpoly A x ∣ p

Tactic:
simp only [hp0, dvd_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/PartialAdjoint.lean
lemma isRightAdjoint_iff_leftAdjointObjIsDefined_eq_top :
    F.IsRightAdjoint ↔ F.LeftAdjointObjIsDefined = ⊤

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
⊢ F.IsRightAdjoint ↔ F.LeftAdjointObjIsDefined = ⊤

Tactic:
refine ⟨fun h ↦ ?_, isRightAdjoint_of_leftAdjointObjIsDefined_eq_top⟩

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
h : F.IsRightAdjoint
⊢ F.LeftAdjointObjIsDefined = ⊤

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
h : F.IsRightAdjoint
⊢ F.LeftAdjointObjIsDefined = ⊤

Tactic:
ext X

Result:
case h.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
h : F.IsRightAdjoint
X : C
⊢ F.LeftAdjointObjIsDefined X ↔ ⊤ X

Proof state:
case h.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
h : F.IsRightAdjoint
X : C
⊢ F.LeftAdjointObjIsDefined X ↔ ⊤ X

Tactic:
simpa only [Pi.top_apply, Prop.top_eq_true, iff_true]
  using leftAdjointObjIsDefined_of_adjunction (Adjunction.ofIsRightAdjoint F) X

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem one_apply_coe (a : Rˣ) : (1 : MulChar R R') a = 1

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
a : Rˣ
⊢ 1 ↑a = 1

Tactic:
classical exact dif_pos a.isUnit

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
a : Rˣ
⊢ 1 ↑a = 1

Tactic:
exact dif_pos a.isUnit

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem index_eq_two_iff : H.index = 2 ↔ ∃ a, ∀ b, Xor' (b * a ∈ H) (b ∈ H)

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ x ∉ H, ∀ x_1 ∉ H, x_1⁻¹ * x ∈ H) ↔ ∃ a, ∀ (b : G), b * a ∈ H ↔ b ∉ H

Tactic:
refine exists_congr fun a =>
  ⟨fun ha b => ⟨fun hba hb => ?_, fun hb => ?_⟩, fun ha => ⟨?_, fun b hb => ?_⟩⟩

Result:
case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H
b : G
hba : b * a ∈ H
hb : b ∈ H
⊢ False

case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H
b : G
hb : b ∉ H
⊢ b * a ∈ H

case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ a ∉ H

case refine_4
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
b : G
hb : b ∉ H
⊢ b⁻¹ * a ∈ H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.index = 2 ↔ ∃ a, ∀ (b : G), Xor' (b * a ∈ H) (b ∈ H)

Tactic:
simp only [index, Nat.card_eq_two_iff' ((1 : G) : G ⧸ H), ExistsUnique, inv_mem_iff,
  QuotientGroup.exists_mk, QuotientGroup.forall_mk, Ne, QuotientGroup.eq, mul_one,
  xor_iff_iff_not]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ x ∉ H, ∀ x_1 ∉ H, x_1⁻¹ * x ∈ H) ↔ ∃ a, ∀ (b : G), b * a ∈ H ↔ b ∉ H

Proof state:
case refine_4
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
b : G
hb : b ∉ H
⊢ b⁻¹ * a ∈ H

Tactic:
rwa [ha, inv_mem_iff (x := b)]

Result:
no goals

Proof state:
case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ 1 ∈ H

Tactic:
exact one_mem _

Result:
no goals

Proof state:
case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H
b : G
hb : b ∉ H
⊢ b * a ∈ H

Tactic:
exact inv_inv b ▸ ha.2 _ (mt (inv_mem_iff (x := b)).1 hb)

Result:
no goals

Proof state:
case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ a ∉ H

Tactic:
rw [← inv_mem_iff (x := a), ← ha, inv_mul_cancel]

Result:
case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ 1 ∈ H

Proof state:
case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H
b : G
hba : b * a ∈ H
hb : b ∈ H
⊢ False

Tactic:
exact ha.1 ((mul_mem_cancel_left hb).1 hba)

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem continuousOn_lift {hf : ∀ x y, (x ~ᵢ y) → f x = f y} {s : Set (SeparationQuotient X)} :
    ContinuousOn (lift f hf) s ↔ ContinuousOn f (mk ⁻¹' s)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
s : Set (SeparationQuotient X)
⊢ ContinuousOn (lift f hf) s ↔ ContinuousOn f (mk ⁻¹' s)

Tactic:
simp only [ContinuousOn, surjective_mk.forall, continuousWithinAt_lift, mem_preimage]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem Nat.cauchy_induction_mul (h : ∀ (n : ℕ), P (n + 1) → P n) (k seed : ℕ) (hk : 1 < k)
    (hs : P seed.succ) (hm : ∀ x, seed < x → P x → P (k * x)) (n : ℕ) : P n

Proof state:
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x✝ : ℕ
hl : seed.succ ≤ x✝
hP✝ : P x✝
⊢ x✝ < (fun x => k * x) x✝

Tactic:
convert (Nat.mul_lt_mul_right <| seed.succ_pos.trans_le hl).2 hk

Result:
case h.e'_3
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x✝ : ℕ
hl : seed.succ ≤ x✝
hP✝ : P x✝
⊢ x✝ = 1 * x✝

Proof state:
case h.e'_3
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x✝ : ℕ
hl : seed.succ ≤ x✝
hP✝ : P x✝
⊢ x✝ = 1 * x✝

Tactic:
rw [one_mul]

Result:
no goals

Proof state:
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n : ℕ
⊢ ∀ (x : ℕ), seed.succ ≤ x → P x → x < (fun x => k * x) x

Tactic:
intro _ hl _

Result:
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x✝ : ℕ
hl : seed.succ ≤ x✝
hP✝ : P x✝
⊢ x✝ < (fun x => k * x) x✝
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem isAlgebraic_algebraMap [Nontrivial R] (x : R) : IsAlgebraic R (algebraMap R A x) :=
  ⟨_, X_sub_C_ne_zero x, by rw [map_sub, aeval_X, aeval_C, sub_self]⟩

Proof state:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : R
⊢ (aeval ((algebraMap R A) x)) (X - C x) = 0

Tactic:
rw [map_sub, aeval_X, aeval_C, sub_self]

Result:
no goals
-- Mathlib/Algebra/Divisibility/Basic.lean
theorem dvd_mul [DecompositionMonoid α] {k m n : α} :
    k ∣ m * n ↔ ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommSemigroup α
inst✝ : DecompositionMonoid α
m n d₁ d₂ : α
hy : d₁ ∣ m
hz : d₂ ∣ n
⊢ d₁ * d₂ ∣ m * n

Tactic:
exact mul_dvd_mul hy hz

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CommSemigroup α
inst✝ : DecompositionMonoid α
k m n : α
⊢ (∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂) → k ∣ m * n

Tactic:
rintro ⟨d₁, d₂, hy, hz, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommSemigroup α
inst✝ : DecompositionMonoid α
m n d₁ d₂ : α
hy : d₁ ∣ m
hz : d₂ ∣ n
⊢ d₁ * d₂ ∣ m * n

Proof state:
α : Type u_1
inst✝¹ : CommSemigroup α
inst✝ : DecompositionMonoid α
k m n : α
⊢ k ∣ m * n ↔ ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂

Tactic:
refine ⟨exists_dvd_and_dvd_of_dvd_mul, ?_⟩

Result:
α : Type u_1
inst✝¹ : CommSemigroup α
inst✝ : DecompositionMonoid α
k m n : α
⊢ (∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂) → k ∣ m * n
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_lt_rpow_of_exponent_gt (hx0 : 0 < x) (hx1 : x < 1) (hyz : z < y) : x ^ y < x ^ z

Proof state:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ rexp (log x * y) < x ^ z

Tactic:
rw [rpow_def_of_pos hx0]

Result:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ rexp (log x * y) < rexp (log x * z)

Proof state:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ log x * y < log x * z

Tactic:
exact mul_lt_mul_of_neg_left hyz (log_neg hx0 hx1)

Result:
no goals

Proof state:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ x ^ y < x ^ z

Tactic:
repeat' rw [rpow_def_of_pos hx0]

Result:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ rexp (log x * y) < rexp (log x * z)

Proof state:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ rexp (log x * y) < rexp (log x * z)

Tactic:
rw [exp_lt_exp]

Result:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ log x * y < log x * z
-- Mathlib/Control/Functor.lean
theorem id_map : ∀ x : Comp F G α, Comp.map id x = x
  | Comp.mk x => by simp only [Comp.map, id_map, id_map']; rfl

Proof state:
F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α : Type v
x : F (G α)
⊢ Comp.map id (mk x) = mk x

Tactic:
simp only [Comp.map, id_map, id_map']

Result:
F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α : Type v
x : F (G α)
⊢ mk (mk x) = mk x

Proof state:
F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α : Type v
x : F (G α)
⊢ mk (mk x) = mk x

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
/-- (Pseudo) metric space has discrete `UniformSpace` structure
iff the distances between distinct points are uniformly bounded away from zero. -/
protected lemma uniformSpace_eq_bot :
    ‹PseudoMetricSpace α›.toUniformSpace = ⊥ ↔
      ∃ r : ℝ, 0 < r ∧ Pairwise (r ≤ dist · · : α → α → Prop)

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
⊢ PseudoMetricSpace.toUniformSpace = ⊥ ↔ ∃ r, 0 < r ∧ Pairwise fun x1 x2 => r ≤ dist x1 x2

Tactic:
simp only [uniformity_basis_dist.uniformSpace_eq_bot, mem_setOf_eq, not_lt]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_coe_le_of_lintegral_coe_le {f : α → ℝ≥0} {b : ℝ≥0} (h : ∫⁻ a, f a ∂μ ≤ b) :
    ∫ a, (f a : ℝ) ∂μ ≤ b

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b
⊢ ∫ (a : α), ↑(f a) ∂μ ≤ ↑b

Tactic:
by_cases hf : Integrable (fun a => (f a : ℝ)) μ

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b
hf : Integrable (fun a => ↑(f a)) μ
⊢ ∫ (a : α), ↑(f a) ∂μ ≤ ↑b

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b
hf : ¬Integrable (fun a => ↑(f a)) μ
⊢ ∫ (a : α), ↑(f a) ∂μ ≤ ↑b

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b
hf : Integrable (fun a => ↑(f a)) μ
⊢ ∫ (a : α), ↑(f a) ∂μ ≤ ↑b

Tactic:
exact (lintegral_coe_le_coe_iff_integral_le hf).1 h

Result:
no goals

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b
hf : ¬Integrable (fun a => ↑(f a)) μ
⊢ 0 ≤ ↑b

Tactic:
exact b.2

Result:
no goals

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b
hf : ¬Integrable (fun a => ↑(f a)) μ
⊢ ∫ (a : α), ↑(f a) ∂μ ≤ ↑b

Tactic:
rw [integral_undef hf]

Result:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b
hf : ¬Integrable (fun a => ↑(f a)) μ
⊢ 0 ≤ ↑b