harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/ResidueField.lean
@[reassoc]
lemma residue_residueFieldMap (x : X) :
    Y.residue (f.base x) ≫ f.residueFieldMap x = f.stalkMap x ≫ X.residue x

Proof state:
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
⊢ Y.residue ((ConcreteCategory.hom f.base) x) ≫ Hom.residueFieldMap f x = Hom.stalkMap f x ≫ X.residue x

Tactic:
simp [Hom.residueFieldMap]

Result:
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
⊢ Y.residue ((ConcreteCategory.hom f.base) x) ≫
      CommRingCat.ofHom (ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f x))) =
    Hom.stalkMap f x ≫ X.residue x

Proof state:
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
⊢ Y.residue ((ConcreteCategory.hom f.base) x) ≫
      CommRingCat.ofHom (ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f x))) =
    Hom.stalkMap f x ≫ X.residue x

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem mem_cons_iff (s : WSeq α) (b) {a} : a ∈ cons b s ↔ a = b ∨ a ∈ s :=
  eq_or_mem_iff_mem <| by simp [ret_mem]

Proof state:
α : Type u
s : WSeq α
b a : α
⊢ some (b, s) ∈ (cons b s).destruct

Tactic:
simp [ret_mem]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma lt_succ_self (a : ℤ) : a < succ a

Proof state:
a : ℤ
⊢ a < a.succ

Tactic:
unfold succ

Result:
a : ℤ
⊢ a < a + 1

Proof state:
a : ℤ
⊢ a < a + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Tactic/DeriveCountable.lean
theorem cons_eq_imp {p : Prop} {a b a' b' : ℕ}
    (h : a = a' → b = b' → p) : Nat.pair a b = Nat.pair a' b' → p

Proof state:
p : Prop
a b a' b' : ℕ
h : a = a' → b = b' → p
⊢ Nat.pair a b = Nat.pair a' b' → p

Tactic:
rwa [Nat.pair_eq_pair, and_imp]

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem irrational_nat_div_iff : Irrational (n / x) ↔ n ≠ 0 ∧ Irrational x

Proof state:
n : ℕ
x : ℝ
⊢ Irrational (↑n / x) ↔ n ≠ 0 ∧ Irrational x

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem C_injective : Function.Injective (C R)

Proof state:
R : Type u_1
inst✝ : Semiring R
⊢ Function.Injective ⇑(C R)

Tactic:
intro a b H

Result:
R : Type u_1
inst✝ : Semiring R
a b : R
H : (C R) a = (C R) b
⊢ a = b

Proof state:
R : Type u_1
inst✝ : Semiring R
a b : R
H : (C R) a = (C R) b
⊢ a = b

Tactic:
simp_rw [PowerSeries.ext_iff] at H

Result:
R : Type u_1
inst✝ : Semiring R
a b : R
H : ∀ (n : ℕ), (coeff R n) ((C R) a) = (coeff R n) ((C R) b)
⊢ a = b

Proof state:
R : Type u_1
inst✝ : Semiring R
a b : R
H : ∀ (n : ℕ), (coeff R n) ((C R) a) = (coeff R n) ((C R) b)
⊢ a = b

Tactic:
simpa only [coeff_zero_C] using H 0

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_nsmul_toReal_eq_two_mul_sub_two_pi {θ : Angle} :
    ((2 : ℕ) • θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal

Proof state:
θ : Angle
h : π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ 3 * π
⊢ π / 2 < θ.toReal

Tactic:
linarith

Result:
no goals

Proof state:
θ : Angle
⊢ π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ 3 * π ↔ π / 2 < θ.toReal

Tactic:
exact
  ⟨fun h => by linarith, fun h =>
    ⟨(div_lt_iff₀' (zero_lt_two' ℝ)).1 h, by linarith [pi_pos, toReal_le_pi θ]⟩⟩

Result:
no goals

Proof state:
θ : Angle
⊢ (2 • θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal

Tactic:
nth_rw 1 [← coe_toReal θ]

Result:
θ : Angle
⊢ (2 • ↑θ.toReal).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal

Proof state:
θ : Angle
h : π / 2 < θ.toReal
⊢ 2 * θ.toReal ≤ 3 * π

Tactic:
linarith [pi_pos, toReal_le_pi θ]

Result:
no goals

Proof state:
θ : Angle
⊢ (2 • ↑θ.toReal).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal

Tactic:
rw [← coe_nsmul, two_nsmul, ← two_mul, toReal_coe_eq_self_sub_two_pi_iff, Set.mem_Ioc]

Result:
θ : Angle
⊢ π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ 3 * π ↔ π / 2 < θ.toReal
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem mem_spanSingleton {x y : P} : x ∈ spanSingleton S y ↔ ∃ z : R, z • y = x

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x y : P
⊢ x ∈ spanSingleton S y ↔ ∃ z, z • y = x

Tactic:
rw [spanSingleton]

Result:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x y : P
⊢ x ∈ ⟨span R {y}, ⋯⟩ ↔ ∃ z, z • y = x

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x y : P
⊢ x ∈ ⟨span R {y}, ⋯⟩ ↔ ∃ z, z • y = x

Tactic:
exact Submodule.mem_span_singleton

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma density_mono_set (hκν : fst κ ≤ ν) (a : α) (x : γ) {s s' : Set β} (h : s ⊆ s') :
    density κ ν a x s ≤ density κ ν a x s'

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ (fun n => κ.densityProcess ν n a x s) ≤ᶠ[atTop] fun n => κ.densityProcess ν n a x s'

Tactic:
exact Eventually.of_forall (fun n ↦ densityProcess_mono_set hκν n a x h)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ κ.density ν a x s ≤ κ.density ν a x s'

Tactic:
refine limsup_le_limsup ?_ ?_ ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ (fun n => κ.densityProcess ν n a x s) ≤ᶠ[atTop] fun n => κ.densityProcess ν n a x s'

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) atTop fun n => κ.densityProcess ν n a x s

case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) atTop fun n => κ.densityProcess ν n a x s'

Proof state:
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) atTop fun n => κ.densityProcess ν n a x s'

Tactic:
exact isBoundedUnder_of ⟨1, fun n ↦ densityProcess_le_one hκν _ _ _ _⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) atTop fun n => κ.densityProcess ν n a x s

Tactic:
exact isCoboundedUnder_le_of_le atTop (fun i ↦ densityProcess_nonneg _ _ _ _ _ _)

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mul_lt_aleph0 {a b : Cardinal} (ha : a < ℵ₀) (hb : b < ℵ₀) : a * b < ℵ₀ :=
  match a, b, lt_aleph0.1 ha, lt_aleph0.1 hb with
  | _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ => by rw [← Nat.cast_mul]; apply nat_lt_aleph0

Proof state:
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m * n) < ℵ₀

Tactic:
apply nat_lt_aleph0

Result:
no goals

Proof state:
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑m * ↑n < ℵ₀

Tactic:
rw [← Nat.cast_mul]

Result:
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m * n) < ℵ₀
-- Mathlib/Data/Set/Image.lean
theorem range_ite_subset {p : α → Prop} [DecidablePred p] {f g : α → β} :
    (range fun x => if p x then f x else g x) ⊆ range f ∪ range g

Proof state:
case pos
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
x : α
h : p x
⊢ (if p x then f x else g x) ∈ range f ∪ range g

Tactic:
simp only [if_pos h, mem_union, mem_range, exists_apply_eq_apply, true_or]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
⊢ (range fun x => if p x then f x else g x) ⊆ range f ∪ range g

Tactic:
rw [range_subset_iff]

Result:
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
⊢ ∀ (y : α), (if p y then f y else g y) ∈ range f ∪ range g

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
⊢ ∀ (y : α), (if p y then f y else g y) ∈ range f ∪ range g

Tactic:
intro x

Result:
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
x : α
⊢ (if p x then f x else g x) ∈ range f ∪ range g

Proof state:
case neg
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
x : α
h : ¬p x
⊢ (if p x then f x else g x) ∈ range f ∪ range g

Tactic:
simp [if_neg h, mem_union, mem_range_self]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
x : α
⊢ (if p x then f x else g x) ∈ range f ∪ range g

Tactic:
by_cases h : p x

Result:
case pos
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
x : α
h : p x
⊢ (if p x then f x else g x) ∈ range f ∪ range g

case neg
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
x : α
h : ¬p x
⊢ (if p x then f x else g x) ∈ range f ∪ range g
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem valuation_le_one (r : R) : v.valuation 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
⊢ (valuation K v) ↑r ≤ 1

Tactic:
rw [valuation_of_algebraMap]

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
⊢ v.intValuation 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
⊢ v.intValuation r ≤ 1

Tactic:
exact v.intValuation_le_one r

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.lo_le (u w v k : Nat) : u + k ≤ w → w ≤ v → u + k ≤ v

Proof state:
u w v k : Nat
⊢ u + k ≤ w → w ≤ v → u + k ≤ v

Tactic:
omega

Result:
no goals
-- Mathlib/RingTheory/Valuation/Integers.lean
theorem isUnit_of_one' (hv : Integers v O) {x : O} (hvx : v (algebraMap O F x) = 1) : IsUnit x

Proof state:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
hvx : v ((algebraMap O F) x) = 1
⊢ IsUnit x

Tactic:
refine isUnit_of_one hv (IsUnit.mk0 _ ?_) hvx

Result:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
hvx : v ((algebraMap O F) x) = 1
⊢ (algebraMap O F) x ≠ 0

Proof state:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : O
hvx : v ((algebraMap O F) x) = 1
⊢ (algebraMap O F) x ≠ 0

Tactic:
simp only [← v.ne_zero_iff, hvx, ne_eq, one_ne_zero, not_false_eq_true]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
@[simp]
lemma mem_pmap_iff {P : α → Prop} (f : ∀ a, P a → β) (z : Sym2 α) (h : ∀ a ∈ z, P a) (b : β) :
    b ∈ z.pmap f h ↔ ∃ (a : α) (ha : a ∈ z), b = f a (h a ha)

Proof state:
case h
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
b : β
x y : α
h : ∀ a ∈ s(x, y), P a
⊢ b ∈ pmap f s(x, y) h ↔ ∃ a, ∃ (ha : a ∈ s(x, y)), b = f a ⋯

Tactic:
rw [pmap_pair f x y h]

Result:
case h
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
b : β
x y : α
h : ∀ a ∈ s(x, y), P a
⊢ b ∈ s(f x ⋯, f y ⋯) ↔ ∃ a, ∃ (ha : a ∈ s(x, y)), b = f a ⋯

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
z : Sym2 α
h : ∀ a ∈ z, P a
b : β
⊢ b ∈ pmap f z h ↔ ∃ a, ∃ (ha : a ∈ z), b = f a ⋯

Tactic:
induction' z with x y

Result:
case h
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
b : β
x y : α
h : ∀ a ∈ s(x, y), P a
⊢ b ∈ pmap f s(x, y) h ↔ ∃ a, ∃ (ha : a ∈ s(x, y)), b = f a ⋯

Proof state:
case h
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
b : β
x y : α
h : ∀ a ∈ s(x, y), P a
⊢ b ∈ s(f x ⋯, f y ⋯) ↔ ∃ a, ∃ (ha : a ∈ s(x, y)), b = f a ⋯

Tactic:
aesop

Result:
no goals
-- Mathlib/CategoryTheory/LiftingProperties/Basic.lean
theorem unop {A B X Y : Cᵒᵖ} {i : A ⟶ B} {p : X ⟶ Y} (h : HasLiftingProperty i p) :
    HasLiftingProperty p.unop i.unop :=
  ⟨fun {f} {g} sq => by
    rw [CommSq.HasLift.iff_op]
    simp only [Quiver.Hom.op_unop]
    infer_instance⟩

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Opposite.unop Y ⟶ Opposite.unop B
g : Opposite.unop X ⟶ Opposite.unop A
sq : CommSq f p.unop i.unop g
⊢ ⋯.HasLift

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Opposite.unop Y ⟶ Opposite.unop B
g : Opposite.unop X ⟶ Opposite.unop A
sq : CommSq f p.unop i.unop g
⊢ sq.HasLift

Tactic:
rw [CommSq.HasLift.iff_op]

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Opposite.unop Y ⟶ Opposite.unop B
g : Opposite.unop X ⟶ Opposite.unop A
sq : CommSq f p.unop i.unop g
⊢ ⋯.HasLift
-- Mathlib/GroupTheory/Sylow.lean
theorem IsPGroup.sylow_mem_fixedPoints_iff {P : Subgroup G} (hP : IsPGroup p P) {Q : Sylow p G} :
    Q ∈ fixedPoints P (Sylow p G) ↔ P ≤ Q

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
P : Subgroup G
hP : IsPGroup p ↥P
Q : Sylow p G
⊢ Q ∈ fixedPoints (↥P) (Sylow p G) ↔ P ≤ ↑Q

Tactic:
rw [P.sylow_mem_fixedPoints_iff, ← inf_eq_left, hP.inf_normalizer_sylow, inf_eq_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem elem_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : List α} (h : a ∈ as) : elem a as = true

Proof state:
case tail
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : elem a as✝ = true
⊢ elem a (b✝ :: as✝) = true

Tactic:
simp [elem]

Result:
case tail
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : elem a as✝ = true
⊢ (match a == b✝ with
    | true => true
    | false => elem a as✝) =
    true

Proof state:
case tail.h_1
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : elem a as✝ = true
x✝ : Bool
heq✝ : (a == b✝) = true
⊢ true = true

case tail.h_2
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : elem a as✝ = true
x✝ : Bool
heq✝ : (a == b✝) = false
⊢ elem a as✝ = true

Tactic:
rfl

Result:
case tail.h_2
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : elem a as✝ = true
x✝ : Bool
heq✝ : (a == b✝) = false
⊢ elem a as✝ = true

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : List α
h : a ∈ as
⊢ elem a as = true

Tactic:
induction h with
| head _ => simp [elem]
| tail _ _ ih => simp [elem]; split; rfl; assumption

Result:
no goals

Proof state:
case tail
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : elem a as✝ = true
⊢ (match a == b✝ with
    | true => true
    | false => elem a as✝) =
    true

Tactic:
split

Result:
case tail.h_1
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : elem a as✝ = true
x✝ : Bool
heq✝ : (a == b✝) = true
⊢ true = true

case tail.h_2
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : elem a as✝ = true
x✝ : Bool
heq✝ : (a == b✝) = false
⊢ elem a as✝ = true

Proof state:
case tail.h_2
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : elem a as✝ = true
x✝ : Bool
heq✝ : (a == b✝) = false
⊢ elem a as✝ = true

Tactic:
assumption

Result:
no goals

Proof state:
case head
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as as✝ : List α
⊢ elem a (a :: as✝) = true

Tactic:
simp [elem]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem nfpBFamily_fp {i hi} (H : IsNormal (f i hi)) (a) :
    f i hi (nfpBFamily.{u, v} o f a) = nfpBFamily.{u, v} o f a

Proof state:
case H
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ IsNormal (o.familyOfBFamily f ((enum fun x1 x2 => x1 < x2) ⟨i, ⋯⟩))

Tactic:
rw [familyOfBFamily_enum]

Result:
case H
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ IsNormal (f i ?H.hi)

case H.hi
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ i < o

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ o.familyOfBFamily f ((enum fun x1 x2 => x1 < x2) ⟨i, ⋯⟩) (o.nfpBFamily f a) = o.nfpBFamily f a

Tactic:
apply nfpFamily_fp

Result:
case H
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ IsNormal (o.familyOfBFamily f ((enum fun x1 x2 => x1 < x2) ⟨i, ⋯⟩))

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ f i hi (o.nfpBFamily f a) = o.nfpBFamily f a

Tactic:
rw [← familyOfBFamily_enum o f]

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ o.familyOfBFamily f ((enum fun x1 x2 => x1 < x2) ⟨i, ⋯⟩) (o.nfpBFamily f a) = o.nfpBFamily f a

Proof state:
case H
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ IsNormal (f i ?H.hi)

case H.hi
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
H : IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ i < o

Tactic:
exact H

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ushiftRight_or_distrib (x y : BitVec w)  (n : Nat) :
    (x ||| y) >>> n = (x >>> n) ||| (y >>> n)

Proof state:
case pred
w : Nat
x y : BitVec w
n i✝ : Nat
a✝ : i✝ < w
⊢ ((x ||| y) >>> n).getLsbD i✝ = (x >>> n ||| y >>> n).getLsbD i✝

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
n : Nat
⊢ (x ||| y) >>> n = x >>> n ||| y >>> n

Tactic:
ext

Result:
case pred
w : Nat
x y : BitVec w
n i✝ : Nat
a✝ : i✝ < w
⊢ ((x ||| y) >>> n).getLsbD i✝ = (x >>> n ||| y >>> n).getLsbD i✝
-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem Ideal.toIdeal_homogeneousHull_eq_iSup :
    (I.homogeneousHull 𝒜).toIdeal = ⨆ i, Ideal.span (GradedRing.proj 𝒜 i '' I)

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ (homogeneousHull 𝒜 I).toIdeal = span (⋃ i, ⇑(GradedRing.proj 𝒜 i) '' ↑I)

Tactic:
apply congr_arg Ideal.span _

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r} = ⋃ i, ⇑(GradedRing.proj 𝒜 i) '' ↑I

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ (homogeneousHull 𝒜 I).toIdeal = ⨆ i, span (⇑(GradedRing.proj 𝒜 i) '' ↑I)

Tactic:
rw [← Ideal.span_iUnion]

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ (homogeneousHull 𝒜 I).toIdeal = span (⋃ i, ⇑(GradedRing.proj 𝒜 i) '' ↑I)

Proof state:
case h
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
x✝ : A
⊢ x✝ ∈ {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r} ↔ x✝ ∈ ⋃ i, ⇑(GradedRing.proj 𝒜 i) '' ↑I

Tactic:
simp only [Set.mem_iUnion, Set.mem_image, mem_setOf_eq, GradedRing.proj_apply, SetLike.exists,
  exists_prop, Subtype.coe_mk, SetLike.mem_coe]

Result:
no goals

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r} = ⋃ i, ⇑(GradedRing.proj 𝒜 i) '' ↑I

Tactic:
ext1

Result:
case h
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
x✝ : A
⊢ x✝ ∈ {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r} ↔ x✝ ∈ ⋃ i, ⇑(GradedRing.proj 𝒜 i) '' ↑I
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem cos_oangle_left_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) :
    Real.Angle.cos (∡ p₃ p₁ p₂) = dist p₁ p₂ / dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ (∡ p₃ p₁ p₂).cos = dist p₁ p₂ / dist p₁ p₃

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe,
  cos_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h),
  dist_comm p₁ p₃]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₃ p₁ p₂).sign = 1

Tactic:
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₃ p₁ p₂).cos = dist p₁ p₂ / dist p₁ p₃

Tactic:
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ (∡ p₃ p₁ p₂).cos = dist p₁ p₂ / dist p₁ p₃
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem mk_eq_one_iff {p : E} : mk p = 1 ↔ ‖p‖ = 0

Proof state:
E : Type u_2
inst✝ : SeminormedCommGroup E
p : E
⊢ mk p = 1 ↔ ‖p‖ = 0

Tactic:
rw [← norm_mk', norm_eq_zero']

Result:
no goals