harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/HNNExtension.lean
theorem not_cancels_of_cons_hyp (u : ℤˣ) (w : NormalWord d)
    (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?,
      w.head ∈ toSubgroup A B u → u = u') :
    ¬ Cancels u w

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
hw : w.head ∈ toSubgroup A B u
x : G
hx : w.toList.head? = some (-u, x)
⊢ False

Tactic:
rw [hx] at h2

Result:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hw : w.head ∈ toSubgroup A B u
x : G
h2 : ∀ u' ∈ Option.map Prod.fst (some (-u, x)), w.head ∈ toSubgroup A B u → u = u'
hx : w.toList.head? = some (-u, x)
⊢ False

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
⊢ w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)

Tactic:
intro hw x hx

Result:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
hw : w.head ∈ toSubgroup A B u
x : G
hx : w.toList.head? = some (-u, x)
⊢ False

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hw : w.head ∈ toSubgroup A B u
x : G
h2 : ∀ u' ∈ Option.map Prod.fst (some (-u, x)), w.head ∈ toSubgroup A B u → u = u'
hx : w.toList.head? = some (-u, x)
⊢ False

Tactic:
simpa using h2 (-u) rfl hw

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
⊢ ¬Cancels u w

Tactic:
simp only [Cancels, Option.map_eq_some', Prod.exists,
  exists_and_right, exists_eq_right, not_and, not_exists]

Result:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
⊢ w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
-- Mathlib/Combinatorics/Quiver/Path.lean
lemma heq_of_cons_eq_cons {p : Path a b} {p' : Path a c}
    {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') : HEq p p'

Proof state:
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
p' : Path a c
e : b ⟶ d
e' : c ⟶ d
h : p.cons e = p'.cons e'
⊢ HEq p p'

Tactic:
injection h

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Basic.lean
theorem ext_nonempty {μ₁ μ₂ : OuterMeasure α} (h : ∀ s : Set α, s.Nonempty → μ₁ s = μ₂ s) :
    μ₁ = μ₂ :=
  ext fun s => s.eq_empty_or_nonempty.elim (fun he => by simp [he]) (h s)

Proof state:
α : Type u_1
μ₁ μ₂ : OuterMeasure α
h : ∀ (s : Set α), s.Nonempty → μ₁ s = μ₂ s
s : Set α
he : s = ∅
⊢ μ₁ s = μ₂ s

Tactic:
simp [he]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem casesOn {P : PartENat → Prop} : ∀ a : PartENat, P ⊤ → (∀ n : ℕ, P n) → P a

Proof state:
P : PartENat → Prop
⊢ ∀ (a : PartENat), P ⊤ → (∀ (n : ℕ), P ↑n) → P a

Tactic:
exact PartENat.casesOn'

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_sub_le_norm_mul (a b : E) : ‖a‖ - ‖b‖ ≤ ‖a * b‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a‖ - ‖b‖ ≤ ‖a * b‖

Tactic:
simpa using norm_mul_le' (a * b) (b⁻¹)

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_univ {f : α → β} : f '' univ = range f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ f '' univ = range f

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
x✝ : β
⊢ x✝ ∈ f '' univ ↔ x✝ ∈ range f

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
x✝ : β
⊢ x✝ ∈ f '' univ ↔ x✝ ∈ range f

Tactic:
simp [image, range]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem length_mem_cyclicPermutations (l : List α) (h : l' ∈ cyclicPermutations l) :
    length l' = length l

Proof state:
α : Type u
l' l : List α
h : l' ∈ l.cyclicPermutations
⊢ l'.length = l.length

Tactic:
obtain ⟨k, hk, rfl⟩ := get_of_mem h

Result:
case intro.refl
α : Type u
l : List α
k : Fin l.cyclicPermutations.length
h : l.cyclicPermutations.get k ∈ l.cyclicPermutations
⊢ (l.cyclicPermutations.get k).length = l.length

Proof state:
case intro.refl
α : Type u
l : List α
k : Fin l.cyclicPermutations.length
h : l.cyclicPermutations.get k ∈ l.cyclicPermutations
⊢ (l.cyclicPermutations.get k).length = l.length

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean
theorem map_π_preserves_coequalizer_inv :
    G.map (coequalizer.π f g) ≫ (PreservesCoequalizer.iso G f g).inv =
      coequalizer.π (G.map f) (G.map g)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
⊢ G.map (coequalizer.π f g) ≫ (PreservesCoequalizer.iso G f g).inv = coequalizer.π (G.map f) (G.map g)

Tactic:
rw [← ι_comp_coequalizerComparison_assoc, ← PreservesCoequalizer.iso_hom, Iso.hom_inv_id,
  comp_id]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean
/-- `IsLocalization.mk'` agrees with `IsLocalizedModule.mk'`. -/
lemma IsLocalization.mk'_eq_mk' [IsLocalization S A] (x : R) (s : S) :
    IsLocalization.mk' A x s = IsLocalizedModule.mk' (Algebra.linearMap R A) x s

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
x : R
s : ↥S
⊢ s • mk' A x s = (Algebra.linearMap R A) x

Tactic:
exact IsLocalization.smul_mk'_self

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
x : R
s : ↥S
⊢ mk' A x s = IsLocalizedModule.mk' (Algebra.linearMap R A) x s

Tactic:
rw [← IsLocalizedModule.smul_inj (Algebra.linearMap R A) s, IsLocalizedModule.mk'_cancel']

Result:
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
x : R
s : ↥S
⊢ s • mk' A x s = (Algebra.linearMap R A) x
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
/-- `log x` is bounded above by a multiple of every power of `x` with positive exponent. -/
lemma log_le_rpow_div {x ε : ℝ} (hx : 0 ≤ x) (hε : 0 < ε) : log x ≤ x ^ ε / ε

Proof state:
case inr
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
h : 0 < x
⊢ ε * log x ≤ x ^ ε

Tactic:
exact (log_rpow h ε).symm.trans_le <| (log_le_sub_one_of_pos <| rpow_pos_of_pos h ε).trans
  (sub_one_lt _).le

Result:
no goals

Proof state:
case inl
ε : ℝ
hε : 0 < ε
hx : 0 ≤ 0
⊢ log 0 ≤ 0 ^ ε / ε

Tactic:
rw [log_zero, zero_rpow hε.ne', zero_div]

Result:
no goals

Proof state:
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
⊢ log x ≤ x ^ ε / ε

Tactic:
rcases hx.eq_or_lt with rfl | h

Result:
case inl
ε : ℝ
hε : 0 < ε
hx : 0 ≤ 0
⊢ log 0 ≤ 0 ^ ε / ε

case inr
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
h : 0 < x
⊢ log x ≤ x ^ ε / ε

Proof state:
case inr
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
h : 0 < x
⊢ log x ≤ x ^ ε / ε

Tactic:
rw [le_div_iff₀' hε]

Result:
case inr
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
h : 0 < x
⊢ ε * log x ≤ x ^ ε
-- Mathlib/Algebra/Group/Pi/Lemmas.lean
theorem curry_mulSingle [DecidableEq α] [∀ a, DecidableEq (β a)] [∀ a b, One (γ a b)]
    (i : Σ a, β a) (x : γ i.1 i.2) :
    Sigma.curry (Pi.mulSingle i x) = Pi.mulSingle i.1 (Pi.mulSingle i.2 x)

Proof state:
α : Type u_3
β : α → Type u_4
γ : (a : α) → β a → Type u_5
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (β a)
inst✝ : (a : α) → (b : β a) → One (γ a b)
i : (a : α) × β a
x : γ i.fst i.snd
⊢ curry (Pi.mulSingle i x) = Pi.mulSingle i.fst (Pi.mulSingle i.snd x)

Tactic:
simp only [Pi.mulSingle, Sigma.curry_update, Sigma.curry_one, Pi.one_apply]

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
lemma quasispectrum.mem_of_not_quasiregular (a : A) {r : Rˣ}
    (hr : ¬ IsQuasiregular (-(r⁻¹ • a))) : (r : R) ∈ quasispectrum R a :=
  fun _ ↦ by simpa using hr

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : NonUnitalRing A
inst✝ : Module R A
a : A
r : Rˣ
hr : ¬IsQuasiregular (-(r⁻¹ • a))
x✝ : IsUnit ↑r
⊢ ¬IsQuasiregular (-(x✝.unit⁻¹ • a))

Tactic:
simpa using hr

Result:
no goals
-- Mathlib/GroupTheory/Sylow.lean
theorem exists_subgroup_card_pow_prime [Finite G] (p : ℕ) {n : ℕ} [Fact p.Prime]
    (hdvd : p ^ n ∣ Nat.card G) : ∃ K : Subgroup G, Nat.card K = p ^ n :=
  let ⟨K, hK⟩ := exists_subgroup_card_pow_prime_le p hdvd ⊥
    (by rw [card_bot, pow_zero]) n.zero_le
  ⟨K, hK.1⟩

Proof state:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p n : ℕ
inst✝ : Fact (Nat.Prime p)
hdvd : p ^ n ∣ Nat.card G
⊢ Nat.card ↥⊥ = p ^ 0

Tactic:
rw [card_bot, pow_zero]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean
/-- If a property of maps of topological spaces is satisfied by all homeomorphisms,
every isomorphism of schemes satisfies the induced property. -/
lemma topologically_iso_le
    (hP : ∀ {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β), P f) :
    MorphismProperty.isomorphisms Scheme ≤ (topologically P)

Proof state:
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
hP : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), P ⇑f
⊢ MorphismProperty.isomorphisms Scheme ≤ topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P

Tactic:
intro X Y e (he : IsIso e)

Result:
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
hP : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), P ⇑f
X Y : Scheme
e : X ⟶ Y
he : IsIso e
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) e

Proof state:
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
hP : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), P ⇑f
X Y : Scheme
e : X ⟶ Y
he this : IsIso e
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) e

Tactic:
exact hP (TopCat.homeoOfIso (asIso e.base))

Result:
no goals

Proof state:
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
hP : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), P ⇑f
X Y : Scheme
e : X ⟶ Y
he : IsIso e
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) e

Tactic:
have : IsIso e := he

Result:
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
hP : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), P ⇑f
X Y : Scheme
e : X ⟶ Y
he this : IsIso e
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) e
-- Mathlib/Data/Option/NAry.lean
theorem map₂_coe_right (f : α → β → γ) (a : Option α) (b : β) :
    map₂ f a b = a.map fun a => f a b

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : β
⊢ map₂ f a (some b) = Option.map (fun a => f a b) a

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/Analysis/Analytic/CPolynomialDef.lean
theorem HasFiniteFPowerSeriesOnBall.mk' {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E}
    {n : ℕ} {r : ℝ≥0∞} (finite : ∀ (m : ℕ), n ≤ m → p m = 0) (pos : 0 < r)
    (sum_eq : ∀ y ∈ EMetric.ball 0 r, (∑ i ∈ Finset.range n, p i fun _ ↦ y) = f (x + y)) :
    HasFiniteFPowerSeriesOnBall f p x n r where
  r_le := p.radius_eq_top_of_eventually_eq_zero (Filter.eventually_atTop.mpr ⟨n, finite⟩) ▸ le_top
  r_pos := pos
  hasSum hy := sum_eq _ hy ▸ hasSum_sum_of_ne_finset_zero fun m hm ↦ by
    rw [Finset.mem_range, not_lt] at hm; rw [finite m hm]; rfl
  finite := finite

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
r : ℝ≥0∞
finite : ∀ (m : ℕ), n ≤ m → p m = 0
pos : 0 < r
sum_eq : ∀ y ∈ EMetric.ball 0 r, (∑ i ∈ Finset.range n, (p i) fun x => y) = f (x + y)
y✝ : E
hy : y✝ ∈ EMetric.ball 0 r
m : ℕ
hm : m ∉ Finset.range n
⊢ ((p m) fun x => y✝) = 0

Tactic:
rw [Finset.mem_range, not_lt] at hm

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
r : ℝ≥0∞
finite : ∀ (m : ℕ), n ≤ m → p m = 0
pos : 0 < r
sum_eq : ∀ y ∈ EMetric.ball 0 r, (∑ i ∈ Finset.range n, (p i) fun x => y) = f (x + y)
y✝ : E
hy : y✝ ∈ EMetric.ball 0 r
m : ℕ
hm : n ≤ m
⊢ ((p m) fun x => y✝) = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
r : ℝ≥0∞
finite : ∀ (m : ℕ), n ≤ m → p m = 0
pos : 0 < r
sum_eq : ∀ y ∈ EMetric.ball 0 r, (∑ i ∈ Finset.range n, (p i) fun x => y) = f (x + y)
y✝ : E
hy : y✝ ∈ EMetric.ball 0 r
m : ℕ
hm : n ≤ m
⊢ (0 fun x => y✝) = 0

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
r : ℝ≥0∞
finite : ∀ (m : ℕ), n ≤ m → p m = 0
pos : 0 < r
sum_eq : ∀ y ∈ EMetric.ball 0 r, (∑ i ∈ Finset.range n, (p i) fun x => y) = f (x + y)
y✝ : E
hy : y✝ ∈ EMetric.ball 0 r
m : ℕ
hm : n ≤ m
⊢ ((p m) fun x => y✝) = 0

Tactic:
rw [finite m hm]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
r : ℝ≥0∞
finite : ∀ (m : ℕ), n ≤ m → p m = 0
pos : 0 < r
sum_eq : ∀ y ∈ EMetric.ball 0 r, (∑ i ∈ Finset.range n, (p i) fun x => y) = f (x + y)
y✝ : E
hy : y✝ ∈ EMetric.ball 0 r
m : ℕ
hm : n ≤ m
⊢ (0 fun x => y✝) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
theorem mkBEqCached_le_size (aig : AIG α) {input : BinaryInput aig} :
    aig.decls.size ≤ (aig.mkBEqCached input).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ (aig.mkBEqCached input).aig.decls.size

Tactic:
simp only [mkBEqCached]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤
    (((aig.mkGateCached (input.asGateInput false true)).aig.mkGateCached
                  ((input.asGateInput true false).cast ⋯)).aig.mkGateCached
            { lhs := { ref := (aig.mkGateCached (input.asGateInput false true)).ref.cast ⋯, inv := true },
              rhs :=
                {
                  ref :=
                    ((aig.mkGateCached (input.asGateInput false true)).aig.mkGateCached
                        ((input.asGateInput true false).cast ⋯)).ref,
                  inv := true } }).aig.decls.size

Proof state:
case h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤
    ((aig.mkGateCached (input.asGateInput false true)).aig.mkGateCached
            ((input.asGateInput true false).cast ⋯)).aig.decls.size

Tactic:
apply LawfulOperator.le_size_of_le_aig_size

Result:
case h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ (aig.mkGateCached (input.asGateInput false true)).aig.decls.size

Proof state:
case h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ (aig.mkGateCached (input.asGateInput false true)).aig.decls.size

Tactic:
apply LawfulOperator.le_size_of_le_aig_size

Result:
case h.h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤
    (((aig.mkGateCached (input.asGateInput false true)).aig.mkGateCached
                  ((input.asGateInput true false).cast ⋯)).aig.mkGateCached
            { lhs := { ref := (aig.mkGateCached (input.asGateInput false true)).ref.cast ⋯, inv := true },
              rhs :=
                {
                  ref :=
                    ((aig.mkGateCached (input.asGateInput false true)).aig.mkGateCached
                        ((input.asGateInput true false).cast ⋯)).ref,
                  inv := true } }).aig.decls.size

Tactic:
apply LawfulOperator.le_size_of_le_aig_size

Result:
case h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤
    ((aig.mkGateCached (input.asGateInput false true)).aig.mkGateCached
            ((input.asGateInput true false).cast ⋯)).aig.decls.size

Proof state:
case h.h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ aig.decls.size

Tactic:
omega

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive]
lemma orderOf_pow_of_dvd {x : G} {n : ℕ} (hn : n ≠ 0) (dvd : n ∣ orderOf x) :
    orderOf (x ^ n) = orderOf x / n

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : n ≠ 0
dvd : n ∣ orderOf x
⊢ orderOf (x ^ n) = orderOf x / n

Tactic:
rw [orderOf_pow' _ hn, Nat.gcd_eq_right dvd]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Constraint.lean
theorem neg_sat : {c : Constraint} → {v : Int} → sat c v → sat (c.neg) (-v)

Proof state:
case mk.some.some.intro.left
l u v : Int
w₁ : l ≤ v
w₂ : v ≤ u
⊢ -u ≤ -v

Tactic:
exact Int.neg_le_neg w₂

Result:
no goals

Proof state:
case mk.none.some
u v : Int
w : v ≤ u
⊢ -u ≤ -v

Tactic:
exact Int.neg_le_neg w

Result:
no goals

Proof state:
case mk.some.some.intro.right
l u v : Int
w₁ : l ≤ v
w₂ : v ≤ u
⊢ -v ≤ -l

Tactic:
exact Int.neg_le_neg w₁

Result:
no goals

Proof state:
case mk.some.some.intro
l u v : Int
w₁ : l ≤ v
w₂ : v ≤ u
⊢ -u ≤ -v ∧ -v ≤ -l

Tactic:
constructor

Result:
case mk.some.some.intro.left
l u v : Int
w₁ : l ≤ v
w₂ : v ≤ u
⊢ -u ≤ -v

case mk.some.some.intro.right
l u v : Int
w₁ : l ≤ v
w₂ : v ≤ u
⊢ -v ≤ -l

Proof state:
case mk.some.some
l u v : Int
w : l ≤ v ∧ v ≤ u
⊢ -u ≤ -v ∧ -v ≤ -l

Tactic:
rcases w with ⟨w₁, w₂⟩

Result:
case mk.some.some.intro
l u v : Int
w₁ : l ≤ v
w₂ : v ≤ u
⊢ -u ≤ -v ∧ -v ≤ -l

Proof state:
case mk.some.none
l v : Int
w : l ≤ v
⊢ -v ≤ -l

Tactic:
exact Int.neg_le_neg w

Result:
no goals

Proof state:
⊢ ∀ {c : Constraint} {v : Int}, c.sat v = true → c.neg.sat (-v) = true

Tactic:
rintro ⟨_ | l, _ | u⟩ v w <;> simp_all [sat, neg, flip, map]

Result:
case mk.none.some
u v : Int
w : v ≤ u
⊢ -u ≤ -v

case mk.some.none
l v : Int
w : l ≤ v
⊢ -v ≤ -l

case mk.some.some
l u v : Int
w : l ≤ v ∧ v ≤ u
⊢ -u ≤ -v ∧ -v ≤ -l
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_zero_length (x : BitVec 0) : x.getLsbD i = false

Proof state:
i : Nat
x : BitVec 0
⊢ x.getLsbD i = false

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_length_eq_length {l} : (filter p l).length = l.length ↔ ∀ a ∈ l, p a

Proof state:
case nil
α✝ : Type u_1
p : α✝ → Bool
⊢ (filter p []).length = [].length ↔ ∀ (a : α✝), a ∈ [] → p a = true

Tactic:
simp

Result:
no goals

Proof state:
case cons
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : (filter p l).length = l.length ↔ ∀ (a : α✝), a ∈ l → p a = true
⊢ (filter p (a :: l)).length = (a :: l).length ↔ ∀ (a_1 : α✝), a_1 ∈ a :: l → p a_1 = true

Tactic:
simp only [filter_cons, length_cons, succ_eq_add_one, mem_cons, forall_eq_or_imp]

Result:
case cons
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : (filter p l).length = l.length ↔ ∀ (a : α✝), a ∈ l → p a = true
⊢ (if p a = true then a :: filter p l else filter p l).length = l.length + 1 ↔
    p a = true ∧ ∀ (a : α✝), a ∈ l → p a = true

Proof state:
case cons.isFalse
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : (filter p l).length = l.length ↔ ∀ (a : α✝), a ∈ l → p a = true
h : ¬p a = true
this : (filter p l).length ≠ l.length.succ
⊢ (filter p l).length = l.length + 1 ↔ p a = true ∧ ∀ (a : α✝), a ∈ l → p a = true

Tactic:
simp_all

Result:
no goals

Proof state:
case cons
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : (filter p l).length = l.length ↔ ∀ (a : α✝), a ∈ l → p a = true
⊢ (if p a = true then a :: filter p l else filter p l).length = l.length + 1 ↔
    p a = true ∧ ∀ (a : α✝), a ∈ l → p a = true

Tactic:
split <;> rename_i h

Result:
case cons.isTrue
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : (filter p l).length = l.length ↔ ∀ (a : α✝), a ∈ l → p a = true
h : p a = true
⊢ (a :: filter p l).length = l.length + 1 ↔ p a = true ∧ ∀ (a : α✝), a ∈ l → p a = true

case cons.isFalse
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : (filter p l).length = l.length ↔ ∀ (a : α✝), a ∈ l → p a = true
h : ¬p a = true
⊢ (filter p l).length = l.length + 1 ↔ p a = true ∧ ∀ (a : α✝), a ∈ l → p a = true

Proof state:
case cons.isTrue
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : (filter p l).length = l.length ↔ ∀ (a : α✝), a ∈ l → p a = true
h : p a = true
⊢ (a :: filter p l).length = l.length + 1 ↔ p a = true ∧ ∀ (a : α✝), a ∈ l → p a = true

Tactic:
simp_all [Nat.add_one_inj]

Result:
no goals

Proof state:
case cons.isFalse
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : (filter p l).length = l.length ↔ ∀ (a : α✝), a ∈ l → p a = true
h : ¬p a = true
⊢ (filter p l).length = l.length + 1 ↔ p a = true ∧ ∀ (a : α✝), a ∈ l → p a = true

Tactic:
have := Nat.ne_of_lt (Nat.lt_succ.mpr (length_filter_le p l))

Result:
case cons.isFalse
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : (filter p l).length = l.length ↔ ∀ (a : α✝), a ∈ l → p a = true
h : ¬p a = true
this : (filter p l).length ≠ l.length.succ
⊢ (filter p l).length = l.length + 1 ↔ p a = true ∧ ∀ (a : α✝), a ∈ l → p a = true
-- Mathlib/Data/Set/Lattice.lean
theorem mem_iInter₂ {x : γ} {s : ∀ i, κ i → Set γ} : (x ∈ ⋂ (i) (j), s i j) ↔ ∀ i j, x ∈ s i j

Proof state:
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
x : γ
s : (i : ι) → κ i → Set γ
⊢ x ∈ ⋂ i, ⋂ j, s i j ↔ ∀ (i : ι) (j : κ i), x ∈ s i j

Tactic:
simp_rw [mem_iInter]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem abs_cos_le_one : |cos x| ≤ 1 :=
  abs_le_one_iff_mul_self_le_one.2 <| by simp only [← sq, cos_sq_le_one]

Proof state:
x : ℝ
⊢ cos x * cos x ≤ 1

Tactic:
simp only [← sq, cos_sq_le_one]

Result:
no goals
-- Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
theorem thickenedIndicator_le_one {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) (x : α) :
    thickenedIndicator δ_pos E x ≤ 1

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ (thickenedIndicator δ_pos E) x ≤ 1

Tactic:
rw [thickenedIndicator.coeFn_eq_comp]

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ (ENNReal.toNNReal ∘ thickenedIndicatorAux δ E) x ≤ 1

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ (ENNReal.toNNReal ∘ thickenedIndicatorAux δ E) x ≤ 1

Tactic:
simpa using (toNNReal_le_toNNReal thickenedIndicatorAux_lt_top.ne one_ne_top).mpr
  (thickenedIndicatorAux_le_one δ E x)

Result:
no goals