harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Fintype/Prod.lean
theorem Pi.infinite_of_exists_right {ι : Sort*} {π : ι → Sort*} (i : ι) [Infinite <| π i]
    [∀ i, Nonempty <| π i] : Infinite (∀ i : ι, π i)

Proof state:
ι : Sort u_4
π : ι → Sort u_5
i : ι
inst✝¹ : Infinite (π i)
inst✝ : ∀ (i : ι), Nonempty (π i)
⊢ Infinite ((i : ι) → π i)

Tactic:
let ⟨m⟩ := @Pi.instNonempty ι π _

Result:
ι : Sort u_4
π : ι → Sort u_5
i : ι
inst✝¹ : Infinite (π i)
inst✝ : ∀ (i : ι), Nonempty (π i)
m : (a : ι) → π a
⊢ Infinite ((i : ι) → π i)

Proof state:
ι : Sort u_4
π : ι → Sort u_5
i : ι
inst✝¹ : Infinite (π i)
inst✝ : ∀ (i : ι), Nonempty (π i)
⊢ Infinite ((i : ι) → π i)

Tactic:
classical
let ⟨m⟩ := @Pi.instNonempty ι π _
exact Infinite.of_injective _ (update_injective m i)

Result:
no goals

Proof state:
ι : Sort u_4
π : ι → Sort u_5
i : ι
inst✝¹ : Infinite (π i)
inst✝ : ∀ (i : ι), Nonempty (π i)
m : (a : ι) → π a
⊢ Infinite ((i : ι) → π i)

Tactic:
exact Infinite.of_injective _ (update_injective m i)

Result:
no goals
-- Mathlib/Order/Filter/ZeroAndBoundedAtFilter.lean
theorem BoundedAtFilter.add [SeminormedAddCommGroup β] {l : Filter α} {f g : α → β}
    (hf : BoundedAtFilter l f) (hg : BoundedAtFilter l g) : BoundedAtFilter l (f + g)

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SeminormedAddCommGroup β
l : Filter α
f g : α → β
hf : l.BoundedAtFilter f
hg : l.BoundedAtFilter g
⊢ l.BoundedAtFilter (f + g)

Tactic:
simpa using hf.add hg

Result:
no goals
-- Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
theorem Cofix.dest_corec {α : TypeVec n} {β : Type u} (g : β → F (α.append1 β)) (x : β) :
    Cofix.dest (Cofix.corec g x) = appendFun id (Cofix.corec g) <$$> g x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
⊢ Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ (Quot.mk Mcongr (corecF g x)) =
    (TypeVec.id ::: corec g) <$$> g x

Tactic:
dsimp

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
⊢ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) (corecF g x)) = (TypeVec.id ::: corec g) <$$> g x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
⊢ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) (corecF g x)) = (TypeVec.id ::: corec g) <$$> g x

Tactic:
rw [corecF_eq, abs_map, abs_repr, ← comp_map, ← appendFun_comp]

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
⊢ (TypeVec.id ⊚ TypeVec.id ::: Quot.mk Mcongr ∘ corecF g) <$$> g x = (TypeVec.id ::: corec g) <$$> g x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
⊢ (corec g x).dest = (TypeVec.id ::: corec g) <$$> g x

Tactic:
conv =>
  lhs
  rw [Cofix.dest, Cofix.corec]

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
⊢ Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ (Quot.mk Mcongr (corecF g x)) =
    (TypeVec.id ::: corec g) <$$> g x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
⊢ (TypeVec.id ⊚ TypeVec.id ::: Quot.mk Mcongr ∘ corecF g) <$$> g x = (TypeVec.id ::: corec g) <$$> g x

Tactic:
rfl

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem translationNumber_zpow (f : CircleDeg1Liftˣ) : ∀ n : ℤ, τ (f ^ n : Units _) = n * τ f
  | (n : ℕ) => by simp [translationNumber_pow f n]
  | -[n+1] => by simp; ring

Proof state:
f : CircleDeg1Liftˣ
n : ℕ
⊢ τ ↑(f ^ ↑n) = ↑↑n * τ ↑f

Tactic:
simp [translationNumber_pow f n]

Result:
no goals

Proof state:
f : CircleDeg1Liftˣ
n : ℕ
⊢ -((↑n + 1) * τ ↑f) = (-1 + -↑n) * τ ↑f

Tactic:
ring

Result:
no goals

Proof state:
f : CircleDeg1Liftˣ
n : ℕ
⊢ τ ↑(f ^ -[n+1]) = ↑-[n+1] * τ ↑f

Tactic:
simp

Result:
f : CircleDeg1Liftˣ
n : ℕ
⊢ -((↑n + 1) * τ ↑f) = (-1 + -↑n) * τ ↑f
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem box_zero : box (n + 1) 0 = ∅

Proof state:
n : ℕ
⊢ box (n + 1) 0 = ∅

Tactic:
simp [box]

Result:
no goals
-- Mathlib/FieldTheory/Normal/Closure.lean
lemma normalClosure_def'' : normalClosure F K L = ⨆ f : L ≃ₐ[F] L, K.map f

Proof state:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K : IntermediateField F L
inst✝ : Normal F L
⊢ normalClosure F (↥K) L = ⨆ f, map (↑f) K

Tactic:
refine (normalClosure_def' K).trans (le_antisymm (iSup_le (fun f ↦ ?_)) (iSup_le (fun f ↦ ?_)))

Result:
case refine_1
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K : IntermediateField F L
inst✝ : Normal F L
f : L →ₐ[F] L
⊢ map f K ≤ ⨆ f, map (↑f) K

case refine_2
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K : IntermediateField F L
inst✝ : Normal F L
f : L ≃ₐ[F] L
⊢ map (↑f) K ≤ ⨆ f, map f K

Proof state:
case refine_2
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K : IntermediateField F L
inst✝ : Normal F L
f : L ≃ₐ[F] L
⊢ map (↑f) K ≤ ⨆ f, map f K

Tactic:
exact le_iSup_of_le f le_rfl

Result:
no goals

Proof state:
case refine_1
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K : IntermediateField F L
inst✝ : Normal F L
f : L →ₐ[F] L
⊢ map f K ≤ ⨆ f, map (↑f) K

Tactic:
exact le_iSup_of_le (f.restrictNormal' L)
  (fun b ⟨a, h⟩ ↦ ⟨a, h.1, h.2 ▸ f.restrictNormal_commutes L a⟩)

Result:
no goals
-- Mathlib/Data/Matrix/Defs.lean
theorem map_id (M : Matrix m n α) : M.map id = M

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i✝ : m
j✝ : n
⊢ M.map id i✝ j✝ = M i✝ j✝

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
⊢ M.map id = M

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i✝ : m
j✝ : n
⊢ M.map id i✝ j✝ = M i✝ j✝
-- Mathlib/Data/Multiset/Dedup.lean
theorem count_dedup (m : Multiset α) (a : α) : m.dedup.count a = if a ∈ m then 1 else 0 :=
  Quot.induction_on m fun _ => by
    simp only [quot_mk_to_coe'', coe_dedup, mem_coe, List.mem_dedup, coe_nodup, coe_count]
    apply List.count_dedup _ _

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
a : α
x✝ : List α
⊢ count a (dedup (Quot.mk (⇑(isSetoid α)) x✝)) = if a ∈ Quot.mk (⇑(isSetoid α)) x✝ then 1 else 0

Tactic:
simp only [quot_mk_to_coe'', coe_dedup, mem_coe, List.mem_dedup, coe_nodup, coe_count]

Result:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
a : α
x✝ : List α
⊢ List.count a x✝.dedup = if a ∈ x✝ then 1 else 0

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
a : α
x✝ : List α
⊢ List.count a x✝.dedup = if a ∈ x✝ then 1 else 0

Tactic:
apply List.count_dedup _ _

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem deleteEdges_deleteEdges (s s' : Set (Sym2 V)) :
    (G.deleteEdges s).deleteEdges s' = G.deleteEdges (s ∪ s')

Proof state:
V : Type u
G : SimpleGraph V
s s' : Set (Sym2 V)
⊢ (G.deleteEdges s).deleteEdges s' = G.deleteEdges (s ∪ s')

Tactic:
simp [deleteEdges, sdiff_sdiff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_nonneg_of_nonneg {s : ℝ} (hs : 0 ≤ s) : 0 ≤ Gamma s

Proof state:
case inl
hs : 0 ≤ 0
⊢ 0 ≤ Gamma 0

Tactic:
rw [Gamma_zero]

Result:
no goals

Proof state:
case inr
s : ℝ
hs : 0 ≤ s
h : 0 < s
⊢ 0 ≤ Gamma s

Tactic:
exact (Gamma_pos_of_pos h).le

Result:
no goals

Proof state:
s : ℝ
hs : 0 ≤ s
⊢ 0 ≤ Gamma s

Tactic:
obtain rfl | h := eq_or_lt_of_le hs

Result:
case inl
hs : 0 ≤ 0
⊢ 0 ≤ Gamma 0

case inr
s : ℝ
hs : 0 ≤ s
h : 0 < s
⊢ 0 ≤ Gamma s
-- Mathlib/Data/Nat/MaxPowDiv.lean
theorem le_of_dvd {p n pow : ℕ} (hp : 1 < p) (hn : 0 < n) (h : p ^ pow ∣ n) :
    pow ≤ p.maxPowDiv n

Proof state:
case a
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
⊢ c ≠ 0

Tactic:
intro h'

Result:
case a
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
h' : c = 0
⊢ False

Proof state:
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
this : 0 < c
⊢ pow ≤ p.maxPowDiv n

Tactic:
simp [hc, base_pow_mul hp this]

Result:
no goals

Proof state:
case a
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = 0
h' : c = 0
⊢ False

Tactic:
exact not_eq_zero_of_lt hn hc

Result:
no goals

Proof state:
case a
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
h' : c = 0
⊢ False

Tactic:
rw [h',mul_zero] at hc

Result:
case a
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = 0
h' : c = 0
⊢ False

Proof state:
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
⊢ pow ≤ p.maxPowDiv n

Tactic:
have : 0 < c := by
  apply Nat.pos_of_ne_zero
  intro h'
  rw [h',mul_zero] at hc
  exact not_eq_zero_of_lt hn hc

Result:
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
this : 0 < c
⊢ pow ≤ p.maxPowDiv n

Proof state:
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
⊢ pow ≤ p.maxPowDiv n

Tactic:
have ⟨c, hc⟩ := h

Result:
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
⊢ pow ≤ p.maxPowDiv n

Proof state:
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
⊢ 0 < c

Tactic:
apply Nat.pos_of_ne_zero

Result:
case a
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
⊢ c ≠ 0
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Iic_union_Ioc_eq_Iic (h : a ≤ b) : Iic a ∪ Ioc a b = Iic b

Proof state:
α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
h : a ≤ b
⊢ Set.Iic a ∪ Set.Ioc a b = Set.Iic b

Tactic:
exact Set.Iic_union_Ioc_eq_Iic h

Result:
no goals

Proof state:
α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
h : a ≤ b
⊢ Iic a ∪ Ioc a b = Iic b

Tactic:
rw [← coe_inj]

Result:
α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
h : a ≤ b
⊢ ↑(Iic a ∪ Ioc a b) = ↑(Iic b)

Proof state:
α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
h : a ≤ b
⊢ ↑(Iic a ∪ Ioc a b) = ↑(Iic b)

Tactic:
push_cast

Result:
α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
h : a ≤ b
⊢ Set.Iic a ∪ Set.Ioc a b = Set.Iic b
-- Mathlib/Algebra/Lie/Submodule.lean
theorem map_of_image (h : f '' I = J) : I.map f = J

Proof state:
case a
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ⇑f '' ↑I = ↑J
⊢ ⇑f '' ↑I ⊆ ↑(map f I)

Tactic:
exact LieSubmodule.subset_lieSpan

Result:
no goals

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ⇑f '' ↑I = ↑J
⊢ map f I = J

Tactic:
apply le_antisymm

Result:
case a
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ⇑f '' ↑I = ↑J
⊢ map f I ≤ J

case a
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ⇑f '' ↑I = ↑J
⊢ J ≤ map f I

Proof state:
case a
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ⇑f '' ↑I = ↑J
⊢ ⇑↑f '' ↑(toLieSubalgebra R L I).toSubmodule ⊆ ↑J

Tactic:
erw [h]

Result:
no goals

Proof state:
case a
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ⇑f '' ↑I = ↑J
⊢ map f I ≤ J

Tactic:
rw [map, LieSubmodule.lieSpan_le, Submodule.map_coe]

Result:
case a
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ⇑f '' ↑I = ↑J
⊢ ⇑↑f '' ↑(toLieSubalgebra R L I).toSubmodule ⊆ ↑J

Proof state:
case a
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ⇑f '' ↑I = ↑J
⊢ J ≤ map f I

Tactic:
rw [← SetLike.coe_subset_coe, ← h]

Result:
case a
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ⇑f '' ↑I = ↑J
⊢ ⇑f '' ↑I ⊆ ↑(map f I)
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_bit0 [Semiring α] (n : Num) : (n.bit0 : α) = 2 * (n : α)

Proof state:
α : Type u_1
inst✝ : Semiring α
n : Num
⊢ ↑n.bit0 = 2 * ↑n

Tactic:
rw [← bit0_of_bit0, two_mul, cast_add]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Pointwise.lean
theorem pointwise_smul_eq_comap {a : M} (S : Ideal R) :
    a • S = S.comap (MulSemiringAction.toRingAut _ _ a).symm

Proof state:
case h
M : Type u_1
R : Type u_2
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
x✝ : R
⊢ x✝ ∈ a • S ↔ x✝ ∈ comap (RingEquiv.symm ((MulSemiringAction.toRingAut M R) a)) S

Tactic:
simp [pointwise_smul_def]

Result:
case h
M : Type u_1
R : Type u_2
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
x✝ : R
⊢ x✝ ∈ map (MulSemiringAction.toRingHom M R a) S ↔ x✝ ∈ map (MulSemiringAction.toRingEquiv M R a) S

Proof state:
M : Type u_1
R : Type u_2
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
⊢ a • S = comap (RingEquiv.symm ((MulSemiringAction.toRingAut M R) a)) S

Tactic:
ext

Result:
case h
M : Type u_1
R : Type u_2
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
x✝ : R
⊢ x✝ ∈ a • S ↔ x✝ ∈ comap (RingEquiv.symm ((MulSemiringAction.toRingAut M R) a)) S

Proof state:
case h
M : Type u_1
R : Type u_2
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
x✝ : R
⊢ x✝ ∈ map (MulSemiringAction.toRingHom M R a) S ↔ x✝ ∈ map (MulSemiringAction.toRingEquiv M R a) S

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem one_lt_ncard_iff (hs : s.Finite

Proof state:
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
⊢ (∃ a ∈ s, ∃ b ∈ s, a ≠ b) ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
simp only [exists_prop, exists_and_left]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
⊢ 1 < s.ncard ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
rw [one_lt_ncard hs]

Result:
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
⊢ (∃ a ∈ s, ∃ b ∈ s, a ≠ b) ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_ofList [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)} {k : α} :
    k ∈ ofList l ↔ (l.map Sigma.fst).contains k

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k : α
⊢ k ∈ ofList l ↔ (List.map Sigma.fst l).contains k = true

Tactic:
simp [mem_iff_contains]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem rootD_eq_self {self : UnionFind} {x : Nat} : self.rootD x = x ↔ self.parent x = x

Proof state:
self : UnionFind
x : Nat
h : self.parent x = x
⊢ (if h : x < self.size then ↑(self.root ⟨x, h⟩) else x) = x

Tactic:
split <;> [rw [root, dif_pos (by rwa [parent, parentD_eq ‹_›] at h)]; rfl]

Result:
no goals

Proof state:
self : UnionFind
x : Nat
⊢ self.rootD x = x ↔ self.parent x = x

Tactic:
refine ⟨fun h => by rw [← h, parent_rootD], fun h => ?_⟩

Result:
self : UnionFind
x : Nat
h : self.parent x = x
⊢ self.rootD x = x

Proof state:
self : UnionFind
x : Nat
h : self.rootD x = x
⊢ self.parent x = x

Tactic:
rw [← h, parent_rootD]

Result:
no goals

Proof state:
self : UnionFind
x : Nat
h : self.parent x = x
⊢ self.rootD x = x

Tactic:
rw [rootD]

Result:
self : UnionFind
x : Nat
h : self.parent x = x
⊢ (if h : x < self.size then ↑(self.root ⟨x, h⟩) else x) = x

Proof state:
self : UnionFind
x : Nat
h : self.parent x = x
h✝ : x < self.size
⊢ self.arr[↑⟨x, h✝⟩].parent = ↑⟨x, h✝⟩

Tactic:
rwa [parent, parentD_eq ‹_›] at h

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma preNormEDS_one : preNormEDS b c d 1 = 1

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d 1 = 1

Tactic:
erw [preNormEDS_ofNat, preNormEDS'_one]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem norm_fderiv_le_of_lip' {f : E → F} {x₀ : E}
    {C : ℝ} (hC₀ : 0 ≤ C) (hlip : ∀ᶠ x in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖) :
    ‖fderiv 𝕜 f x₀‖ ≤ C

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ ‖fderiv 𝕜 f x₀‖ ≤ C

Tactic:
by_cases hf : DifferentiableAt 𝕜 f x₀

Result:
case pos
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
hf : DifferentiableAt 𝕜 f x₀
⊢ ‖fderiv 𝕜 f x₀‖ ≤ C

case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
hf : ¬DifferentiableAt 𝕜 f x₀
⊢ ‖fderiv 𝕜 f x₀‖ ≤ C

Proof state:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
hf : ¬DifferentiableAt 𝕜 f x₀
⊢ ‖fderiv 𝕜 f x₀‖ ≤ C

Tactic:
rw [fderiv_zero_of_not_differentiableAt hf]

Result:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
hf : ¬DifferentiableAt 𝕜 f x₀
⊢ ‖0‖ ≤ C

Proof state:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
hf : ¬DifferentiableAt 𝕜 f x₀
⊢ ‖0‖ ≤ C

Tactic:
simp [hC₀]

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
hf : DifferentiableAt 𝕜 f x₀
⊢ ‖fderiv 𝕜 f x₀‖ ≤ C

Tactic:
exact hf.hasFDerivAt.le_of_lip' hC₀ hlip

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem le_of_forall_lt_one_mul_le {x y : ℝ≥0} (h : ∀ a < 1, a * x ≤ y) : x ≤ y :=
  le_of_forall_lt_imp_le_of_dense fun a ha => by
    have hx : x ≠ 0 := pos_iff_ne_zero.1 (lt_of_le_of_lt (zero_le _) ha)
    have hx' : x⁻¹ ≠ 0

Proof state:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this : a * x⁻¹ < 1
⊢ a ≤ y

Tactic:
have : a * x⁻¹ * x ≤ y := h _ this

Result:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this✝ : a * x⁻¹ < 1
this : a * x⁻¹ * x ≤ y
⊢ a ≤ y

Proof state:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ a * x⁻¹ < 1

Tactic:
rwa [← lt_inv_iff_mul_lt hx', inv_inv]

Result:
no goals

Proof state:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ a ≤ y

Tactic:
have : a * x⁻¹ < 1 := by rwa [← lt_inv_iff_mul_lt hx', inv_inv]

Result:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this : a * x⁻¹ < 1
⊢ a ≤ y

Proof state:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this✝ : a * x⁻¹ < 1
this : a * x⁻¹ * x ≤ y
⊢ a ≤ y

Tactic:
rwa [mul_assoc, inv_mul_cancel₀ hx, mul_one] at this

Result:
no goals

Proof state:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
⊢ a ≤ y

Tactic:
have hx' : x⁻¹ ≠ 0 := by rwa [Ne, inv_eq_zero]

Result:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ a ≤ y

Proof state:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
⊢ x⁻¹ ≠ 0

Tactic:
rwa [Ne, inv_eq_zero]

Result:
no goals

Proof state:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
⊢ a ≤ y

Tactic:
have hx : x ≠ 0 := pos_iff_ne_zero.1 (lt_of_le_of_lt (zero_le _) ha)

Result:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
⊢ a ≤ y
-- Mathlib/Data/NNRat/Defs.lean
lemma mul_def (q r : ℚ≥0) : q * r = divNat (q.num * r.num) (q.den * r.den)

Proof state:
q r : ℚ≥0
⊢ q * r = divNat (q.num * r.num) (q.den * r.den)

Tactic:
ext

Result:
case a
q r : ℚ≥0
⊢ ↑(q * r) = ↑(divNat (q.num * r.num) (q.den * r.den))

Proof state:
case a
q r : ℚ≥0
⊢ ↑(q * r) = ↑(divNat (q.num * r.num) (q.den * r.den))

Tactic:
simp [Rat.mul_eq_mkRat, Rat.mkRat_eq_divInt, num_coe, den_coe]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma comap_genWeightSpace_eq_of_injective (hf : Injective f) :
    (genWeightSpace M₂ χ).comap f = genWeightSpace M χ

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective ⇑f
⊢ LieSubmodule.comap f (genWeightSpace M₂ χ) = genWeightSpace M χ

Tactic:
refine le_antisymm (fun m hm ↦ ?_) ?_

Result:
case refine_1
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective ⇑f
m : M
hm : m ∈ LieSubmodule.comap f (genWeightSpace M₂ χ)
⊢ m ∈ genWeightSpace M χ

case refine_2
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective ⇑f
⊢ genWeightSpace M χ ≤ LieSubmodule.comap f (genWeightSpace M₂ χ)

Proof state:
case refine_2
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective ⇑f
⊢ LieSubmodule.map f (genWeightSpace M χ) ≤ genWeightSpace M₂ χ

Tactic:
exact map_genWeightSpace_le f

Result:
no goals