harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem eq_none_iff_forall_not_mem : o = none ↔ ∀ a, a ∉ o :=
  ⟨fun e a h => by rw [e] at h; (cases h), fun h => ext <| by simp; exact h⟩

Proof state:
α✝ : Type u_1
o : Option α✝
e : o = none
a : α✝
h : a ∈ none
⊢ False

Tactic:
cases h

Result:
no goals

Proof state:
α✝ : Type u_1
o : Option α✝
e : o = none
a : α✝
h : a ∈ o
⊢ False

Tactic:
rw [e] at h

Result:
α✝ : Type u_1
o : Option α✝
e : o = none
a : α✝
h : a ∈ none
⊢ False

Proof state:
α✝ : Type u_1
o : Option α✝
h : ∀ (a : α✝), ¬a ∈ o
⊢ ∀ (a : α✝), ¬o = some a

Tactic:
exact h

Result:
no goals

Proof state:
α✝ : Type u_1
o : Option α✝
h : ∀ (a : α✝), ¬a ∈ o
⊢ ∀ (a : α✝), a ∈ o ↔ a ∈ none

Tactic:
simp

Result:
α✝ : Type u_1
o : Option α✝
h : ∀ (a : α✝), ¬a ∈ o
⊢ ∀ (a : α✝), ¬o = some a

Proof state:
α✝ : Type u_1
o : Option α✝
e : o = none
a : α✝
h : a ∈ none
⊢ False

Tactic:
(cases h)

Result:
no goals
-- Mathlib/Data/FP/Basic.lean
theorem Float.Zero.valid : ValidFinite emin 0 :=
  ⟨by
    rw [add_sub_assoc]
    apply le_add_of_nonneg_right
    apply sub_nonneg_of_le
    apply Int.ofNat_le_ofNat_of_le
    exact C.precPos,
    suffices prec ≤ 2 * emax by
      rw [← Int.ofNat_le] at this
      rw [← sub_nonneg] at *
      simp only [emin, emax] at *
      omega
    le_trans C.precMax (Nat.le_mul_of_pos_left _ Nat.zero_lt_two),
    by (rw [max_eq_right]; simp [sub_eq_add_neg, Int.ofNat_zero_le])⟩

Proof state:
C : FloatCfg
⊢ emin = (emin + ↑(Nat.size 0) - ↑prec) ⊔ emin

Tactic:
rw [max_eq_right]

Result:
C : FloatCfg
⊢ emin + ↑(Nat.size 0) - ↑prec ≤ emin

Proof state:
case h.a.a
C : FloatCfg
⊢ 1 ≤ prec

Tactic:
exact C.precPos

Result:
no goals

Proof state:
C : FloatCfg
⊢ emin = (emin + ↑(Nat.size 0) - ↑prec) ⊔ emin

Tactic:
(rw [max_eq_right]; simp [sub_eq_add_neg, Int.ofNat_zero_le])

Result:
no goals

Proof state:
C : FloatCfg
⊢ emin ≤ emin + (↑prec - 1)

Tactic:
apply le_add_of_nonneg_right

Result:
case h
C : FloatCfg
⊢ 0 ≤ ↑prec - 1

Proof state:
case h.a
C : FloatCfg
⊢ 1 ≤ ↑prec

Tactic:
apply Int.ofNat_le_ofNat_of_le

Result:
case h.a.a
C : FloatCfg
⊢ 1 ≤ prec

Proof state:
C : FloatCfg
this : 0 ≤ ↑(2 * FloatCfg.emax) - ↑prec
⊢ 0 ≤ ↑FloatCfg.emax - (1 - ↑FloatCfg.emax + ↑prec - 1)

Tactic:
omega

Result:
no goals

Proof state:
case h
C : FloatCfg
⊢ 0 ≤ ↑prec - 1

Tactic:
apply sub_nonneg_of_le

Result:
case h.a
C : FloatCfg
⊢ 1 ≤ ↑prec

Proof state:
C : FloatCfg
⊢ emin ≤ emin + ↑prec - 1

Tactic:
rw [add_sub_assoc]

Result:
C : FloatCfg
⊢ emin ≤ emin + (↑prec - 1)

Proof state:
C : FloatCfg
this : ↑prec ≤ ↑(2 * emax)
⊢ emin + ↑prec - 1 ≤ ↑emax

Tactic:
rw [← sub_nonneg] at *

Result:
C : FloatCfg
this : 0 ≤ ↑(2 * emax) - ↑prec
⊢ 0 ≤ ↑emax - (emin + ↑prec - 1)

Proof state:
C : FloatCfg
this : 0 ≤ ↑(2 * emax) - ↑prec
⊢ 0 ≤ ↑emax - (emin + ↑prec - 1)

Tactic:
simp only [emin, emax] at *

Result:
C : FloatCfg
this : 0 ≤ ↑(2 * FloatCfg.emax) - ↑prec
⊢ 0 ≤ ↑FloatCfg.emax - (1 - ↑FloatCfg.emax + ↑prec - 1)

Proof state:
C : FloatCfg
⊢ emin + ↑(Nat.size 0) - ↑prec ≤ emin

Tactic:
simp [sub_eq_add_neg, Int.ofNat_zero_le]

Result:
no goals

Proof state:
C : FloatCfg
this : prec ≤ 2 * emax
⊢ emin + ↑prec - 1 ≤ ↑emax

Tactic:
rw [← Int.ofNat_le] at this

Result:
C : FloatCfg
this : ↑prec ≤ ↑(2 * emax)
⊢ emin + ↑prec - 1 ≤ ↑emax
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem isConj_swap {w x y z : α} (hwx : w ≠ x) (hyz : y ≠ z) : IsConj (swap w x) (swap y z) :=
  isConj_iff.2
    (have h :
      ∀ {y z : α},
        y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z :=
      fun {y z} hyz hwz => by
      rw [mul_inv_rev, swap_inv, swap_inv, mul_assoc (swap w y), mul_assoc (swap w y), ←
        mul_assoc _ (swap x z), swap_mul_swap_mul_swap hwx hwz, ← mul_assoc,
        swap_mul_swap_mul_swap hwz.symm hyz.symm]
    if hwz : w = z then
      have hwy : w ≠ y

Proof state:
α : Type u
inst✝ : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
hwy : w ≠ y
⊢ swap w z * swap x y * swap w x * (swap w z * swap x y)⁻¹ = swap y z

Tactic:
rw [swap_comm y z, h hyz.symm hwy]

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
⊢ w ≠ y

Tactic:
rw [hwz]

Result:
α : Type u
inst✝ : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
⊢ z ≠ y

Proof state:
α : Type u
inst✝ : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
⊢ z ≠ y

Tactic:
exact hyz.symm

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
w x y✝ z✝ : α
hwx : w ≠ x
hyz✝ : y✝ ≠ z✝
y z : α
hyz : y ≠ z
hwz : w ≠ z
⊢ swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z

Tactic:
rw [mul_inv_rev, swap_inv, swap_inv, mul_assoc (swap w y), mul_assoc (swap w y), ←
  mul_assoc _ (swap x z), swap_mul_swap_mul_swap hwx hwz, ← mul_assoc,
  swap_mul_swap_mul_swap hwz.symm hyz.symm]

Result:
no goals
-- Mathlib/Data/Nat/Find.lean
@[simp] lemma find_eq_zero (h : ∃ n : ℕ, p n) : Nat.find h = 0 ↔ p 0

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ Nat.find h = 0 ↔ p 0

Tactic:
simp [find_eq_iff]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem Associated.pow_pow [CommMonoid M] {a b : M} {n : ℕ} (h : a ~ᵤ b) : a ^ n ~ᵤ b ^ n

Proof state:
case zero
M : Type u_1
inst✝ : CommMonoid M
a b : M
h : a ~ᵤ b
⊢ a ^ 0 ~ᵤ b ^ 0

Tactic:
simp [Associated.refl]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a b : M
n : ℕ
h : a ~ᵤ b
⊢ a ^ n ~ᵤ b ^ n

Tactic:
induction n with
| zero => simp [Associated.refl]
| succ n ih => convert h.mul_mul ih <;> rw [pow_succ']

Result:
no goals

Proof state:
case succ
M : Type u_1
inst✝ : CommMonoid M
a b : M
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
⊢ a ^ (n + 1) ~ᵤ b ^ (n + 1)

Tactic:
convert h.mul_mul ih <;> rw [pow_succ']

Result:
no goals
-- Mathlib/Computability/TMToPartrec.lean
theorem head_supports {S k q} (H : (q : Λ').Supports S) : (head k q).Supports S := fun _ => by
  dsimp only; split_ifs <;> exact H

Proof state:
S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x✝ : Option Γ'
⊢ Λ'.Supports S ((if x✝ = some Γ'.consₗ then id else Λ'.clear (fun x => decide (x = Γ'.consₗ)) k) (unrev q))

Tactic:
split_ifs <;> exact H

Result:
no goals

Proof state:
S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x✝ : Option Γ'
⊢ Λ'.Supports S
    ((fun s => (if s = some Γ'.consₗ then id else Λ'.clear (fun x => decide (x = Γ'.consₗ)) k) (unrev q)) x✝)

Tactic:
dsimp only

Result:
S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x✝ : Option Γ'
⊢ Λ'.Supports S ((if x✝ = some Γ'.consₗ then id else Λ'.clear (fun x => decide (x = Γ'.consₗ)) k) (unrev q))
-- Mathlib/CategoryTheory/Sites/Equivalence.lean
lemma W_inverseImage_whiskeringLeft :
    K.W.inverseImage ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) = J.W

Proof state:
case h.h.a.mpr
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P✝ Q : Cᵒᵖ ⥤ A
f : P✝ ⟶ Q
P : Dᵒᵖ ⥤ A
⊢ ObjectProperty.isoClosure (fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj) P →
    ObjectProperty.isoClosure (fun x => x ∈ Set.range (sheafToPresheaf K A).obj) P

Tactic:
rintro ⟨_, ⟨R, rfl⟩, ⟨e⟩⟩

Result:
case h.h.a.mpr.intro.intro.intro.intro
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P✝ Q : Cᵒᵖ ⥤ A
f : P✝ ⟶ Q
P : Dᵒᵖ ⥤ A
R : Sheaf J A
e : P ≅ (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj R
⊢ ObjectProperty.isoClosure (fun x => x ∈ Set.range (sheafToPresheaf K A).obj) P

Proof state:
case h
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ (ObjectProperty.isoClosure fun x => x ∈ Set.range (sheafToPresheaf K A).obj) =
    ObjectProperty.isoClosure fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj

Tactic:
ext P

Result:
case h.h.a
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P✝ Q : Cᵒᵖ ⥤ A
f : P✝ ⟶ Q
P : Dᵒᵖ ⥤ A
⊢ ObjectProperty.isoClosure (fun x => x ∈ Set.range (sheafToPresheaf K A).obj) P ↔
    ObjectProperty.isoClosure (fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj) P
-- Mathlib/Computability/PartrecCode.lean
theorem encode_lt_prec (cf cg) :
    encode cf < encode (prec cf cg) ∧ encode cg < encode (prec cf cg)

Proof state:
cf cg : Code
⊢ encode cf < encode (cf.prec cg) ∧ encode cg < encode (cf.prec cg)

Tactic:
have : encode (pair cf cg) < encode (prec cf cg) := by simp [encodeCode_eq, encodeCode]

Result:
cf cg : Code
this : encode (cf.pair cg) < encode (cf.prec cg)
⊢ encode cf < encode (cf.prec cg) ∧ encode cg < encode (cf.prec cg)

Proof state:
cf cg : Code
this : encode (cf.pair cg) < encode (cf.prec cg)
⊢ encode cf < encode (cf.prec cg) ∧ encode cg < encode (cf.prec cg)

Tactic:
exact (encode_lt_pair cf cg).imp (fun h => lt_trans h this) fun h => lt_trans h this

Result:
no goals

Proof state:
cf cg : Code
⊢ encode (cf.pair cg) < encode (cf.prec cg)

Tactic:
simp [encodeCode_eq, encodeCode]

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Archimedean.lean
theorem dense_or_cyclic (S : AddSubgroup G) : Dense (S : Set G) ∨ ∃ a : G, S = closure {a}

Proof state:
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
h : ∃ ε > 0, ∀ g ∈ S, g ∉ Ioo 0 ε
⊢ ∃ a, S = closure {a}

Tactic:
rcases h with ⟨ε, ε0, hε⟩

Result:
case intro.intro
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
ε : G
ε0 : ε > 0
hε : ∀ g ∈ S, g ∉ Ioo 0 ε
⊢ ∃ a, S = closure {a}

Proof state:
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
h : ¬∀ ε > 0, ∃ g ∈ S, g ∈ Ioo 0 ε
⊢ ∃ a, S = closure {a}

Tactic:
push_neg at h

Result:
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
h : ∃ ε > 0, ∀ g ∈ S, g ∉ Ioo 0 ε
⊢ ∃ a, S = closure {a}

Proof state:
case intro.intro
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
ε : G
ε0 : ε > 0
hε : ∀ g ∈ S, g ∉ Ioo 0 ε
⊢ ∃ a, S = closure {a}

Tactic:
exact cyclic_of_isolated_zero ε0 (disjoint_left.2 hε)

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
⊢ Dense ↑S ∨ ∃ a, S = closure {a}

Tactic:
refine (em _).imp (dense_of_not_isolated_zero S) fun h => ?_

Result:
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
h : ¬∀ ε > 0, ∃ g ∈ S, g ∈ Ioo 0 ε
⊢ ∃ a, S = closure {a}
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorAdd_add_zero_hom_app (a : A) (X : C) : (shiftFunctorAdd C a 0).hom.app X =
    eqToHom (by dsimp; rw [add_zero]) ≫ (shiftFunctorZero C A).inv.app (X⟦a⟧)

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C (a + 0)).obj X = (𝟭 C).obj ((shiftFunctor C a).obj X)

Tactic:
dsimp

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C (a + 0)).obj X = (shiftFunctor C a).obj X

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C (a + 0)).obj X = (shiftFunctor C a).obj X

Tactic:
rw [add_zero]

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctorAdd C a 0).hom.app X = eqToHom ⋯ ≫ (shiftFunctorZero C A).inv.app ((shiftFunctor C a).obj X)

Tactic:
simp [← shiftFunctorAdd'_add_zero_hom_app, shiftFunctorAdd']

Result:
no goals
-- Mathlib/Data/Setoid/Basic.lean
theorem sSup_def {s : Set (Setoid α)} : sSup s = EqvGen.setoid (sSup ((⇑) '' s))

Proof state:
α : Type u_1
s : Set (Setoid α)
⊢ sSup s = EqvGen.setoid (sSup (@r α '' s))

Tactic:
rw [sSup_eq_eqvGen, sSup_image]

Result:
α : Type u_1
s : Set (Setoid α)
⊢ (EqvGen.setoid fun x y => ∃ r ∈ s, r x y) = EqvGen.setoid (⨆ a ∈ s, ⇑a)

Proof state:
α : Type u_1
s : Set (Setoid α)
⊢ (EqvGen.setoid fun x y => ∃ r ∈ s, r x y) = EqvGen.setoid (⨆ a ∈ s, ⇑a)

Tactic:
congr with (x y)

Result:
case e_r.h.h.a
α : Type u_1
s : Set (Setoid α)
x y : α
⊢ (∃ r ∈ s, r x y) ↔ (⨆ a ∈ s, ⇑a) x y

Proof state:
case e_r.h.h.a
α : Type u_1
s : Set (Setoid α)
x y : α
⊢ (∃ r ∈ s, r x y) ↔ (⨆ a ∈ s, ⇑a) x y

Tactic:
simp only [iSup_apply, iSup_Prop_eq, exists_prop]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallyInjective.lean
lemma mono_of_isLocallyInjective [IsLocallyInjective φ] : Mono φ

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Sheaf J D
φ : F₁ ⟶ F₂
inst✝¹ : J.HasSheafCompose (forget D)
inst✝ : IsLocallyInjective φ
⊢ Mono φ

Tactic:
apply mono_of_injective

Result:
case hφ
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Sheaf J D
φ : F₁ ⟶ F₂
inst✝¹ : J.HasSheafCompose (forget D)
inst✝ : IsLocallyInjective φ
⊢ ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.val.app X))

Proof state:
case hφ
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Sheaf J D
φ : F₁ ⟶ F₂
inst✝¹ : J.HasSheafCompose (forget D)
inst✝ : IsLocallyInjective φ
⊢ ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.val.app X))

Tactic:
rw [← isLocallyInjective_iff_injective]

Result:
case hφ
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Sheaf J D
φ : F₁ ⟶ F₂
inst✝¹ : J.HasSheafCompose (forget D)
inst✝ : IsLocallyInjective φ
⊢ IsLocallyInjective φ

Proof state:
case hφ
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Sheaf J D
φ : F₁ ⟶ F₂
inst✝¹ : J.HasSheafCompose (forget D)
inst✝ : IsLocallyInjective φ
⊢ IsLocallyInjective φ

Tactic:
infer_instance

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem chain_iterates {f : α → α} (hf : monotone f) : chain (iterates f)

Proof state:
case neg
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih : ∀ (x : α), c x → ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
hy : iterates f y
h : ¬∃ z, c z ∧ y ⊑ z
⊢ csup c ⊑ y ∨ y ⊑ csup c

Tactic:
left

Result:
case neg.h
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih : ∀ (x : α), c x → ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
hy : iterates f y
h : ¬∃ z, c z ∧ y ⊑ z
⊢ csup c ⊑ y

Proof state:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih2 : ∀ (x_1 : α), c x_1 → f x ⊑ x_1 ∨ x_1 ⊑ f x
z : α
hz : c z
h : ¬f x ⊑ z
⊢ z ⊑ f x

Tactic:
cases ih2 z hz

Result:
case inl
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih2 : ∀ (x_1 : α), c x_1 → f x ⊑ x_1 ∨ x_1 ⊑ f x
z : α
hz : c z
h : ¬f x ⊑ z
h✝ : f x ⊑ z
⊢ z ⊑ f x

case inr
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih2 : ∀ (x_1 : α), c x_1 → f x ⊑ x_1 ∨ x_1 ⊑ f x
z : α
hz : c z
h : ¬f x ⊑ z
h✝ : z ⊑ f x
⊢ z ⊑ f x

Proof state:
case pos.h.intro.intro
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih2 : ∀ (x_1 : α), c x_1 → f x ⊑ x_1 ∨ x_1 ⊑ f x
z : α
hz : c z
hfz : f x ⊑ z
⊢ f x ⊑ csup c

Tactic:
apply rel_trans hfz

Result:
case pos.h.intro.intro
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih2 : ∀ (x_1 : α), c x_1 → f x ⊑ x_1 ∨ x_1 ⊑ f x
z : α
hz : c z
hfz : f x ⊑ z
⊢ z ⊑ csup c
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma norm_le_one_iff_of_nonneg (a : A) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ ‖a‖ ≤ 1 ↔ a ≤ 1

Tactic:
simpa using norm_le_iff_le_algebraMap a zero_le_one

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nadd_comm (a b) : a ♯ b = b ♯ a

Proof state:
a b : Ordinal.{u_1}
⊢ (⨆ x, succ (a ♯ ↑x)) ⊔ ⨆ x, succ (↑x ♯ b) = (⨆ x, succ (↑x ♯ a)) ⊔ ⨆ x, succ (b ♯ ↑x)

Tactic:
congr <;> ext x <;> cases x <;> apply congr_arg _ (nadd_comm _ _)

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
⊢ a ♯ b = b ♯ a

Tactic:
rw [nadd, nadd, max_comm]

Result:
a b : Ordinal.{u_1}
⊢ (⨆ x, succ (a ♯ ↑x)) ⊔ ⨆ x, succ (↑x ♯ b) = (⨆ x, succ (↑x ♯ a)) ⊔ ⨆ x, succ (b ♯ ↑x)
-- Mathlib/Computability/TMToPartrec.lean
theorem trList_ne_consₗ : ∀ (l), ∀ x ∈ trList l, x ≠ Γ'.consₗ
  | a :: l, x, h => by
    simp only [trList, List.mem_append, List.mem_cons] at h
    obtain h | rfl | h := h
    · rintro rfl
      cases trNat_natEnd _ _ h
    · rintro ⟨⟩
    · exact trList_ne_consₗ l _ h

Proof state:
case inr.inr
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList l
⊢ x ≠ Γ'.consₗ

Tactic:
exact trList_ne_consₗ l _ h

Result:
no goals

Proof state:
case inr.inl
a : ℕ
l : List ℕ
⊢ Γ'.cons ≠ Γ'.consₗ

Tactic:
rintro ⟨⟩

Result:
no goals

Proof state:
case inl
a : ℕ
l : List ℕ
h : Γ'.consₗ ∈ trNat a
⊢ False

Tactic:
cases trNat_natEnd _ _ h

Result:
no goals

Proof state:
case inl
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trNat a
⊢ x ≠ Γ'.consₗ

Tactic:
rintro rfl

Result:
case inl
a : ℕ
l : List ℕ
h : Γ'.consₗ ∈ trNat a
⊢ False

Proof state:
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList (a :: l)
⊢ x ≠ Γ'.consₗ

Tactic:
simp only [trList, List.mem_append, List.mem_cons] at h

Result:
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trNat a ∨ x = Γ'.cons ∨ x ∈ trList l
⊢ x ≠ Γ'.consₗ

Proof state:
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trNat a ∨ x = Γ'.cons ∨ x ∈ trList l
⊢ x ≠ Γ'.consₗ

Tactic:
obtain h | rfl | h := h

Result:
case inl
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trNat a
⊢ x ≠ Γ'.consₗ

case inr.inl
a : ℕ
l : List ℕ
⊢ Γ'.cons ≠ Γ'.consₗ

case inr.inr
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList l
⊢ x ≠ Γ'.consₗ
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma adj_spanningCoe_induce_supp {v w : V} (c : G.ConnectedComponent) :
    (G.induce c.supp).spanningCoe.Adj v w ↔ v ∈ c.supp ∧ G.Adj v w

Proof state:
case pos
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
h : v ∈ c.supp
⊢ (induce c.supp G).spanningCoe.Adj v w ↔ v ∈ c.supp ∧ G.Adj v w

Tactic:
refine ⟨by aesop, ?_⟩

Result:
case pos
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
h : v ∈ c.supp
⊢ v ∈ c.supp ∧ G.Adj v w → (induce c.supp G).spanningCoe.Adj v w

Proof state:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
h : v ∈ c.supp
h' : v ∈ c.supp ∧ G.Adj v w
⊢ w ∈ c.supp

Tactic:
rwa [c.mem_supp_congr_adj h'.2] at h

Result:
no goals

Proof state:
case pos
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
h : v ∈ c.supp
h' : v ∈ c.supp ∧ G.Adj v w
⊢ (induce c.supp G).spanningCoe.Adj v w

Tactic:
have : w ∈ c.supp := by rwa [c.mem_supp_congr_adj h'.2] at h

Result:
case pos
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
h : v ∈ c.supp
h' : v ∈ c.supp ∧ G.Adj v w
this : w ∈ c.supp
⊢ (induce c.supp G).spanningCoe.Adj v w

Proof state:
case neg
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
h : v ∉ c.supp
⊢ (induce c.supp G).spanningCoe.Adj v w ↔ v ∈ c.supp ∧ G.Adj v w

Tactic:
aesop

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
⊢ (induce c.supp G).spanningCoe.Adj v w ↔ v ∈ c.supp ∧ G.Adj v w

Tactic:
by_cases h : v ∈ c.supp

Result:
case pos
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
h : v ∈ c.supp
⊢ (induce c.supp G).spanningCoe.Adj v w ↔ v ∈ c.supp ∧ G.Adj v w

case neg
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
h : v ∉ c.supp
⊢ (induce c.supp G).spanningCoe.Adj v w ↔ v ∈ c.supp ∧ G.Adj v w

Proof state:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
h : v ∈ c.supp
⊢ (induce c.supp G).spanningCoe.Adj v w → v ∈ c.supp ∧ G.Adj v w

Tactic:
aesop

Result:
no goals

Proof state:
case pos
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
h : v ∈ c.supp
h' : v ∈ c.supp ∧ G.Adj v w
this : w ∈ c.supp
⊢ (induce c.supp G).spanningCoe.Adj v w

Tactic:
aesop

Result:
no goals

Proof state:
case pos
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
h : v ∈ c.supp
⊢ v ∈ c.supp ∧ G.Adj v w → (induce c.supp G).spanningCoe.Adj v w

Tactic:
intro h'

Result:
case pos
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
h : v ∈ c.supp
h' : v ∈ c.supp ∧ G.Adj v w
⊢ (induce c.supp G).spanningCoe.Adj v w