harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_mul_dvd_lcm (h : Commute x y) :
    orderOf (x * y) ∣ Nat.lcm (orderOf x) (orderOf y)

Proof state:
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
⊢ orderOf (x * y) ∣ (orderOf x).lcm (orderOf y)

Tactic:
rw [orderOf, ← comp_mul_left]

Result:
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
⊢ minimalPeriod ((fun x_1 => x * x_1) ∘ fun x => y * x) 1 ∣ (orderOf x).lcm (orderOf y)

Proof state:
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
⊢ minimalPeriod ((fun x_1 => x * x_1) ∘ fun x => y * x) 1 ∣ (orderOf x).lcm (orderOf y)

Tactic:
exact Function.Commute.minimalPeriod_of_comp_dvd_lcm h.function_commute_mul_left

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem ult_eq_msb_of_msb_neq {x y : BitVec w} (h : x.msb ≠ y.msb) :
    x.ult y = y.msb

Proof state:
w : Nat
x y : BitVec w
h : x.msb ≠ y.msb
⊢ x.ult y = y.msb

Tactic:
simp only [BitVec.ult, msb_eq_decide, ne_eq, decide_eq_decide] at *

Result:
w : Nat
x y : BitVec w
h : ¬(2 ^ (w - 1) ≤ x.toNat ↔ 2 ^ (w - 1) ≤ y.toNat)
⊢ x.toNat < y.toNat ↔ 2 ^ (w - 1) ≤ y.toNat

Proof state:
w : Nat
x y : BitVec w
h : ¬(2 ^ (w - 1) ≤ x.toNat ↔ 2 ^ (w - 1) ≤ y.toNat)
⊢ x.toNat < y.toNat ↔ 2 ^ (w - 1) ≤ y.toNat

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem sub_inv_antitoneOn_Icc_right (ha : c < a) :
    AntitoneOn (fun x ↦ (x-c)⁻¹) (Set.Icc a b)

Proof state:
case neg
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : c < a
hab : ¬a ≤ b
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)

Tactic:
simp [hab, Set.Subsingleton.antitoneOn]

Result:
no goals

Proof state:
case pos
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : c < a
hab : a ≤ b
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)

Tactic:
exact sub_inv_antitoneOn_Ioi.mono <| (Set.Icc_subset_Ioi_iff hab).mpr ha

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : c < a
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)

Tactic:
by_cases hab : a ≤ b

Result:
case pos
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : c < a
hab : a ≤ b
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)

case neg
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : c < a
hab : ¬a ≤ b
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)
-- Mathlib/Data/DFinsupp/Defs.lean
theorem subtypeDomain_def (f : Π₀ i, β i) :
    f.subtypeDomain p = mk (f.support.subtype p) fun i => f i

Proof state:
case neg
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : Subtype p
h2 : f ↑i = 0
⊢ f ↑i = if i ∈ Finset.subtype p f.support then f ↑i else 0

Tactic:
simp [h2]

Result:
no goals

Proof state:
case neg
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : Subtype p
h2 : f ↑i = 0
⊢ (subtypeDomain p f) i = (mk (Finset.subtype p f.support) fun i => f ↑↑i) i

Tactic:
dsimp

Result:
case neg
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : Subtype p
h2 : f ↑i = 0
⊢ f ↑i = if i ∈ Finset.subtype p f.support then f ↑i else 0

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : Subtype p
⊢ (subtypeDomain p f) i = (mk (Finset.subtype p f.support) fun i => f ↑↑i) i

Tactic:
by_cases h2 : f i ≠ 0 <;> try simp at h2; dsimp; simp [h2]

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
⊢ subtypeDomain p f = mk (Finset.subtype p f.support) fun i => f ↑↑i

Tactic:
ext i

Result:
case h
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : Subtype p
⊢ (subtypeDomain p f) i = (mk (Finset.subtype p f.support) fun i => f ↑↑i) i

Proof state:
case neg
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : Subtype p
h2 : ¬f ↑i ≠ 0
⊢ (subtypeDomain p f) i = (mk (Finset.subtype p f.support) fun i => f ↑↑i) i

Tactic:
simp at h2

Result:
case neg
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : Subtype p
h2 : f ↑i = 0
⊢ (subtypeDomain p f) i = (mk (Finset.subtype p f.support) fun i => f ↑↑i) i
-- Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean
theorem isUnit_exp (A : Matrix m m 𝔸) : IsUnit (exp 𝕂 A)

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
this✝¹ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this✝ : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
this : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra
⊢ IsUnit (exp 𝕂 A)

Tactic:
exact isUnit_exp _ A

Result:
no goals

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
this : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
⊢ IsUnit (exp 𝕂 A)

Tactic:
letI : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing

Result:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
this✝ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
⊢ IsUnit (exp 𝕂 A)

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
⊢ IsUnit (exp 𝕂 A)

Tactic:
letI : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing

Result:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
this : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
⊢ IsUnit (exp 𝕂 A)

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
this✝ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
⊢ IsUnit (exp 𝕂 A)

Tactic:
letI : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra

Result:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
this✝¹ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this✝ : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
this : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra
⊢ IsUnit (exp 𝕂 A)
-- Mathlib/Combinatorics/SetFamily/Shatter.lean
protected lemma Shatters.subset_iff (h : 𝒜.Shatters s) : t ⊆ s ↔ ∃ u ∈ 𝒜, s ∩ u = t :=
  ⟨fun ht ↦ h ht, by rintro ⟨u, _, rfl⟩; exact inter_subset_left⟩

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
u : Finset α
left✝ : u ∈ 𝒜
⊢ s ∩ u ⊆ s

Tactic:
exact inter_subset_left

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
h : 𝒜.Shatters s
⊢ (∃ u ∈ 𝒜, s ∩ u = t) → t ⊆ s

Tactic:
rintro ⟨u, _, rfl⟩

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
u : Finset α
left✝ : u ∈ 𝒜
⊢ s ∩ u ⊆ s
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma map_ofHom :
    (Cochain.ofHom f).map Φ = Cochain.ofHom ((Φ.mapHomologicalComplex _).map f)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
f : K ⟶ L
Φ : C ⥤ D
inst✝ : Φ.Additive
⊢ (ofHom f).map Φ = ofHom ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).map f)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem div_zero (n : Num) : n / 0 = 0 :=
  show n.div 0 = 0 by
    cases n
    · rfl
    · simp [Num.div]

Proof state:
n : Num
⊢ n.div 0 = 0

Tactic:
cases n

Result:
case zero

⊢ zero.div 0 = 0

case pos
a✝ : PosNum
⊢ (pos a✝).div 0 = 0

Proof state:
case zero

⊢ zero.div 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case pos
a✝ : PosNum
⊢ (pos a✝).div 0 = 0

Tactic:
simp [Num.div]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem mul_neg_geom_series (x : R) (h : ‖x‖ < 1) : (1 - x) * ∑' i : ℕ, x ^ i = 1

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ (1 - x) * ∑' (i : ℕ), x ^ i = 1

Tactic:
have := (summable_geometric_of_norm_lt_one h).hasSum.mul_left (1 - x)

Result:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => (1 - x) * x ^ i) ((1 - x) * ∑' (b : ℕ), x ^ b)
⊢ (1 - x) * ∑' (i : ℕ), x ^ i = 1

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => (1 - x) * x ^ i) ((1 - x) * ∑' (b : ℕ), x ^ b)
⊢ Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)

Tactic:
simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_norm_lt_one h)

Result:
no goals

Proof state:
case h.e'_3.h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
this✝ : HasSum (fun i => (1 - x) * x ^ i) ((1 - x) * ∑' (b : ℕ), x ^ b)
this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
x✝ : ℕ
⊢ 1 - x ^ x✝ = ∑ i ∈ Finset.range x✝, (1 - x) * x ^ i

Tactic:
rw [← mul_neg_geom_sum, Finset.mul_sum]

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => (1 - x) * x ^ i) ((1 - x) * ∑' (b : ℕ), x ^ b)
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, (1 - x) * x ^ i) atTop (𝓝 1)

Tactic:
have : Tendsto (fun n : ℕ ↦ 1 - x ^ n) atTop (𝓝 1) := by
  simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_norm_lt_one h)

Result:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
this✝ : HasSum (fun i => (1 - x) * x ^ i) ((1 - x) * ∑' (b : ℕ), x ^ b)
this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, (1 - x) * x ^ i) atTop (𝓝 1)

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => (1 - x) * x ^ i) ((1 - x) * ∑' (b : ℕ), x ^ b)
⊢ (1 - x) * ∑' (i : ℕ), x ^ i = 1

Tactic:
refine tendsto_nhds_unique this.tendsto_sum_nat ?_

Result:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => (1 - x) * x ^ i) ((1 - x) * ∑' (b : ℕ), x ^ b)
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, (1 - x) * x ^ i) atTop (𝓝 1)

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
this✝ : HasSum (fun i => (1 - x) * x ^ i) ((1 - x) * ∑' (b : ℕ), x ^ b)
this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, (1 - x) * x ^ i) atTop (𝓝 1)

Tactic:
convert← this

Result:
case h.e'_3.h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
this✝ : HasSum (fun i => (1 - x) * x ^ i) ((1 - x) * ∑' (b : ℕ), x ^ b)
this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
x✝ : ℕ
⊢ 1 - x ^ x✝ = ∑ i ∈ Finset.range x✝, (1 - x) * x ^ i
-- Mathlib/Order/Monotone/Basic.lean
theorem Nat.rel_of_forall_rel_succ_of_le_of_lt (r : β → β → Prop) [IsTrans β r] {f : ℕ → β} {a : ℕ}
    (h : ∀ n, a ≤ n → r (f n) (f (n + 1))) ⦃b c : ℕ⦄ (hab : a ≤ b) (hbc : b < c) :
    r (f b) (f c)

Proof state:
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℕ → β
a : ℕ
h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))
b c : ℕ
hab : a ≤ b
hbc : b < c
⊢ r (f b) (f c)

Tactic:
induction hbc with
| refl => exact h _ hab
| step b_lt_k r_b_k => exact _root_.trans r_b_k (h _ (hab.trans_lt b_lt_k).le)

Result:
no goals

Proof state:
case step
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℕ → β
a : ℕ
h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))
b c : ℕ
hab : a ≤ b
m✝ : ℕ
b_lt_k : b.succ.le m✝
r_b_k : r (f b) (f m✝)
⊢ r (f b) (f m✝.succ)

Tactic:
exact _root_.trans r_b_k (h _ (hab.trans_lt b_lt_k).le)

Result:
no goals

Proof state:
case refl
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℕ → β
a : ℕ
h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))
b c : ℕ
hab : a ≤ b
⊢ r (f b) (f b.succ)

Tactic:
exact h _ hab

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/RCLike.lean
theorem RCLike.tendsto_inverse_atTop_nhds_zero_nat :
    Tendsto (fun n : ℕ => (n : 𝕜)⁻¹) atTop (𝓝 0)

Proof state:
case h.e'_3.h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
x✝ : ℕ
⊢ (↑x✝)⁻¹ = (⇑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) x✝

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)

Tactic:
convert tendsto_algebraMap_inverse_atTop_nhds_zero_nat 𝕜

Result:
case h.e'_3.h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
x✝ : ℕ
⊢ (↑x✝)⁻¹ = (⇑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) x✝
-- Mathlib/Topology/Bornology/Basic.lean
theorem comap_cobounded_le_iff [Bornology β] {f : α → β} :
    (cobounded β).comap f ≤ cobounded α ↔ ∀ ⦃s⦄, IsBounded s → IsBounded (f '' s)

Proof state:
case intro.intro
α : Type u_2
β : Type u_3
x✝ : Bornology α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : s ⊆ f ⁻¹' tᶜ
⊢ IsBounded (f '' s)

Tactic:
exact (IsCobounded.compl ht).subset ((image_subset f hts).trans <| image_preimage_subset _ _)

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
x✝ : Bornology α
inst✝ : Bornology β
f : α → β
⊢ comap f (cobounded β) ≤ cobounded α ↔ ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)

Tactic:
refine
  ⟨fun h s hs => ?_, fun h t ht =>
    ⟨(f '' tᶜ)ᶜ, h <| IsCobounded.compl ht, compl_subset_comm.1 <| subset_preimage_image _ _⟩⟩

Result:
α : Type u_2
β : Type u_3
x✝ : Bornology α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
⊢ IsBounded (f '' s)

Proof state:
α : Type u_2
β : Type u_3
x✝ : Bornology α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
⊢ IsBounded (f '' s)

Tactic:
obtain ⟨t, ht, hts⟩ := h hs.compl

Result:
case intro.intro
α : Type u_2
β : Type u_3
x✝ : Bornology α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : f ⁻¹' t ⊆ sᶜ
⊢ IsBounded (f '' s)

Proof state:
case intro.intro
α : Type u_2
β : Type u_3
x✝ : Bornology α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : f ⁻¹' t ⊆ sᶜ
⊢ IsBounded (f '' s)

Tactic:
rw [subset_compl_comm, ← preimage_compl] at hts

Result:
case intro.intro
α : Type u_2
β : Type u_3
x✝ : Bornology α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : s ⊆ f ⁻¹' tᶜ
⊢ IsBounded (f '' s)
-- Mathlib/Order/SuccPred/Basic.lean
theorem Ico_subset_Ioo_pred_left_of_not_isMin (ha : ¬IsMin a) : Ico a b ⊆ Ioo (pred a) b

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ Ici a ∩ Iio b ⊆ Ioi (pred a) ∩ Iio b

Tactic:
gcongr

Result:
case H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ Ici a ⊆ Ioi (pred a)

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ Ico a b ⊆ Ioo (pred a) b

Tactic:
rw [← Ioi_inter_Iio, ← Ici_inter_Iio]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ Ici a ∩ Iio b ⊆ Ioi (pred a) ∩ Iio b

Proof state:
case H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ Ici a ⊆ Ioi (pred a)

Tactic:
apply Ici_subset_Ioi_pred_of_not_isMin ha

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem setIfInBounds_mkVector_self : (mkVector n a).setIfInBounds i a = mkVector n a

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
⊢ (mkVector n a).setIfInBounds i a = mkVector n a

Tactic:
rw [← toArray_inj]

Result:
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
⊢ ((mkVector n a).setIfInBounds i a).toArray = (mkVector n a).toArray

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
⊢ ((mkVector n a).setIfInBounds i a).toArray = (mkVector n a).toArray

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fintype/Prod.lean
@[simp] lemma product_eq_univ [Nonempty α] [Nonempty β] : s ×ˢ t = univ ↔ s = univ ∧ t = univ

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
s : Finset α
t : Finset β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
⊢ s ×ˢ t = univ ↔ s = univ ∧ t = univ

Tactic:
simp [eq_univ_iff_forall, forall_and]

Result:
no goals
-- Mathlib/Probability/IdentDistrib.lean
theorem comp_of_aemeasurable {u : γ → δ} (h : IdentDistrib f g μ ν)
    (hu : AEMeasurable u (Measure.map f μ)) : IdentDistrib (u ∘ f) (u ∘ g) μ ν :=
  { aemeasurable_fst := hu.comp_aemeasurable h.aemeasurable_fst
    aemeasurable_snd

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g μ ν
hu : AEMeasurable u (Measure.map f μ)
⊢ Measure.map (u ∘ f) μ = Measure.map (u ∘ g) ν

Tactic:
rw [← AEMeasurable.map_map_of_aemeasurable hu h.aemeasurable_fst, ←
  AEMeasurable.map_map_of_aemeasurable _ h.aemeasurable_snd, h.map_eq]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g μ ν
hu : AEMeasurable u (Measure.map f μ)
⊢ AEMeasurable u (Measure.map g ν)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g μ ν
hu : AEMeasurable u (Measure.map g ν)
⊢ AEMeasurable (u ∘ g) ν

Tactic:
exact hu.comp_aemeasurable h.aemeasurable_snd

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g μ ν
hu : AEMeasurable u (Measure.map f μ)
⊢ AEMeasurable (u ∘ g) ν

Tactic:
rw [h.map_eq] at hu

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g μ ν
hu : AEMeasurable u (Measure.map g ν)
⊢ AEMeasurable (u ∘ g) ν

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g μ ν
hu : AEMeasurable u (Measure.map f μ)
⊢ AEMeasurable u (Measure.map g ν)

Tactic:
rwa [← h.map_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_replicate [LawfulBEq α] (n : Nat) (a b : α) :
    (replicate n a).erase b = if b == a then replicate (n - 1) a else replicate n a

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a b : α
⊢ eraseP (fun x => b == x) (replicate n a) = if (b == a) = true then replicate (n - 1) a else replicate n a

Tactic:
simp [eraseP_replicate]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a b : α
⊢ (replicate n a).erase b = if (b == a) = true then replicate (n - 1) a else replicate n a

Tactic:
rw [erase_eq_eraseP]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a b : α
⊢ eraseP (fun x => b == x) (replicate n a) = if (b == a) = true then replicate (n - 1) a else replicate n a
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem Module.finrank_zero_iff [NoZeroSMulDivisors R M] :
    finrank R M = 0 ↔ Subsingleton M

Proof state:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Module.Finite R M
inst✝ : NoZeroSMulDivisors R M
⊢ finrank R M = 0 ↔ ↑(finrank R M) = 0

Tactic:
norm_cast

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Module.Finite R M
inst✝ : NoZeroSMulDivisors R M
⊢ finrank R M = 0 ↔ Subsingleton M

Tactic:
rw [← rank_zero_iff (R := R), ← finrank_eq_rank]

Result:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Module.Finite R M
inst✝ : NoZeroSMulDivisors R M
⊢ finrank R M = 0 ↔ ↑(finrank R M) = 0
-- Mathlib/NumberTheory/FLT/Basic.lean
lemma not_fermatLastTheoremFor_two : ¬ FermatLastTheoremFor 2 :=
  fun h ↦ h 3 4 5 (by norm_num) (by norm_num) (by norm_num) (by norm_num)

Proof state:
h : FermatLastTheoremFor 2
⊢ 4 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
h : FermatLastTheoremFor 2
⊢ 5 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
h : FermatLastTheoremFor 2
⊢ 3 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
h : FermatLastTheoremFor 2
⊢ 3 ^ 2 + 4 ^ 2 = 5 ^ 2

Tactic:
norm_num

Result:
no goals