harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem zpow_ne_zero_of_isUnit_det [Nonempty n'] [Nontrivial R] {A : M} (ha : IsUnit A.det)
    (z : ℤ) : A ^ z ≠ 0

Proof state:
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit A.det
z : ℤ
this : IsUnit (A ^ z).det
⊢ A ^ z ≠ 0

Tactic:
contrapose! this

Result:
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit A.det
z : ℤ
this : A ^ z = 0
⊢ ¬IsUnit (A ^ z).det

Proof state:
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit A.det
z : ℤ
this : A ^ z = 0
⊢ ¬IsUnit 0

Tactic:
exact not_isUnit_zero

Result:
no goals

Proof state:
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit A.det
z : ℤ
⊢ A ^ z ≠ 0

Tactic:
have := ha.det_zpow z

Result:
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit A.det
z : ℤ
this : IsUnit (A ^ z).det
⊢ A ^ z ≠ 0

Proof state:
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit A.det
z : ℤ
this : A ^ z = 0
⊢ ¬IsUnit (A ^ z).det

Tactic:
rw [this, det_zero ‹_›]

Result:
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit A.det
z : ℤ
this : A ^ z = 0
⊢ ¬IsUnit 0
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc]
lemma RightHomologyData.rightHomologyIso_inv_naturality
    (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
      h₁.homologyIso.inv ≫ homologyMap φ =
        rightHomologyMap' φ h₁ h₂ ≫ h₂.homologyIso.inv

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ h₁.homologyIso.inv ≫ homologyMap φ = rightHomologyMap' φ h₁ h₂ ≫ h₂.homologyIso.inv

Tactic:
simp only [← cancel_mono h₂.homologyIso.hom, assoc, Iso.inv_hom_id_assoc, comp_id,
  ← RightHomologyData.rightHomologyIso_hom_naturality φ h₁ h₂, Iso.inv_hom_id]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem zero_smul_aux (p : LocalizedModule S M) : (0 : T) • p = 0

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ 0 = IsLocalization.mk' T 0 1

Tactic:
rw [IsLocalization.mk'_zero]

Result:
no goals

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
p : LocalizedModule S M
⊢ 0 • p = 0

Tactic:
induction' p with m s

Result:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ 0 • mk m s = 0

Proof state:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ 0 • mk m s = 0

Tactic:
rw [show (0 : T) = IsLocalization.mk' T (0 : R) (1 : S) by rw [IsLocalization.mk'_zero],
  mk'_smul_mk, zero_smul, zero_mk]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma sub_self {x : EReal} (h_top : x ≠ ⊤) (h_bot : x ≠ ⊥) : x - x = 0

Proof state:
x : EReal
h_top : x ≠ ⊤
h_bot : x ≠ ⊥
⊢ x - x = 0

Tactic:
cases x <;> simp_all [← coe_sub]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem real_inner_smul_self_right (x : F) (r : ℝ) : ⟪x, r • x⟫_ℝ = r * (‖x‖ * ‖x‖)

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
r : ℝ
⊢ ⟪x, r • x⟫_ℝ = r * (‖x‖ * ‖x‖)

Tactic:
rw [inner_smul_right, ← real_inner_self_eq_norm_mul_norm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_eq_filter (p : α → Bool) :
    filterMap (Option.guard (p ·)) = filter p

Proof state:
case h
α : Type u_1
p : α → Bool
l : Array α
⊢ filterMap (Option.guard fun x => p x = true) l = filter p l

Tactic:
cases l

Result:
case h.mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ filterMap (Option.guard fun x => p x = true) { toList := toList✝ } = filter p { toList := toList✝ }

Proof state:
case h.mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ filterMap (Option.guard fun x => p x = true) { toList := toList✝ } = filter p { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
⊢ (fun as => filterMap (Option.guard fun x => p x = true) as) = fun as => filter p as

Tactic:
funext l

Result:
case h
α : Type u_1
p : α → Bool
l : Array α
⊢ filterMap (Option.guard fun x => p x = true) l = filter p l
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem length_filterMap_eq_countP (f : α → Option β) (l : List α) :
    (filterMap f l).length = countP (fun a => (f a).isSome) l

Proof state:
case nil
α : Type u_2
β : Type u_1
f : α → Option β
⊢ (filterMap f []).length = countP (fun a => (f a).isSome) []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_2
β : Type u_1
f : α → Option β
x : α
l : List α
ih : (filterMap f l).length = countP (fun a => (f a).isSome) l
⊢ (filterMap f (x :: l)).length = countP (fun a => (f a).isSome) (x :: l)

Tactic:
simp only [filterMap_cons, countP_cons]

Result:
case cons
α : Type u_2
β : Type u_1
f : α → Option β
x : α
l : List α
ih : (filterMap f l).length = countP (fun a => (f a).isSome) l
⊢ (match f x with
      | none => filterMap f l
      | some b => b :: filterMap f l).length =
    countP (fun a => (f a).isSome) l + if (f x).isSome = true then 1 else 0

Proof state:
case cons
α : Type u_2
β : Type u_1
f : α → Option β
x : α
l : List α
ih : (filterMap f l).length = countP (fun a => (f a).isSome) l
⊢ (match f x with
      | none => filterMap f l
      | some b => b :: filterMap f l).length =
    countP (fun a => (f a).isSome) l + if (f x).isSome = true then 1 else 0

Tactic:
split <;> simp [ih, *]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_1
f : α → Option β
l : List α
⊢ (filterMap f l).length = countP (fun a => (f a).isSome) l

Tactic:
induction l with
| nil => rfl
| cons x l ih =>
  simp only [filterMap_cons, countP_cons]
  split <;> simp [ih, *]

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem le_grundyValue_of_Iio_subset_moveLeft {G : PGame} {o : Nimber}
    (h : Set.Iio o ⊆ Set.range (grundyValue ∘ G.moveLeft)) : o ≤ grundyValue G

Proof state:
case intro
G : PGame
o : Nimber
h : Set.Iio o ⊆ Set.range (grundyValue ∘ G.moveLeft)
ho : G.grundyValue < o
i : G.LeftMoves
hi : (grundyValue ∘ G.moveLeft) i = G.grundyValue
⊢ False

Tactic:
exact grundyValue_ne_moveLeft i hi

Result:
no goals

Proof state:
G : PGame
o : Nimber
h : Set.Iio o ⊆ Set.range (grundyValue ∘ G.moveLeft)
⊢ o ≤ G.grundyValue

Tactic:
by_contra! ho

Result:
G : PGame
o : Nimber
h : Set.Iio o ⊆ Set.range (grundyValue ∘ G.moveLeft)
ho : G.grundyValue < o
⊢ False

Proof state:
G : PGame
o : Nimber
h : Set.Iio o ⊆ Set.range (grundyValue ∘ G.moveLeft)
ho : G.grundyValue < o
⊢ False

Tactic:
obtain ⟨i, hi⟩ := h ho

Result:
case intro
G : PGame
o : Nimber
h : Set.Iio o ⊆ Set.range (grundyValue ∘ G.moveLeft)
ho : G.grundyValue < o
i : G.LeftMoves
hi : (grundyValue ∘ G.moveLeft) i = G.grundyValue
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem zipWithAll_toArray (f : Option α → Option β → γ) (as : List α) (bs : List β) :
    Array.zipWithAll f as.toArray bs.toArray = (List.zipWithAll f as bs).toArray

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Option α → Option β → γ
as : List α
bs : List β
⊢ Array.zipWithAll f as.toArray bs.toArray = (zipWithAll f as bs).toArray

Tactic:
simp [Array.zipWithAll, zipWithAll_go_toArray]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_eq_some_getKey!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF)
    {a : α} :
    m.contains a = true → m.getKey? a = some (m.getKey! a)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
a : α
⊢ m.contains a = true → m.getKey? a = some (m.getKey! a)

Tactic:
simp_to_raw using Raw₀.getKey?_eq_some_getKey!

Result:
no goals
-- Mathlib/GroupTheory/Abelianization.lean
theorem image_commutatorSet_closureCommutatorRepresentatives :
    (closureCommutatorRepresentatives G).subtype ''
        commutatorSet (closureCommutatorRepresentatives G) =
      commutatorSet G

Proof state:
case h₂
G : Type u
inst✝ : Group G
⊢ commutatorSet G ⊆ ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G)

Tactic:
exact fun g hg =>
  ⟨_,
    ⟨⟨_, subset_closure (Or.inl ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩)⟩,
      ⟨_, subset_closure (Or.inr ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩)⟩, rfl⟩,
    hg.choose_spec.choose_spec⟩

Result:
no goals

Proof state:
G : Type u
inst✝ : Group G
⊢ ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G) = commutatorSet G

Tactic:
apply Set.Subset.antisymm

Result:
case h₁
G : Type u
inst✝ : Group G
⊢ ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G) ⊆ commutatorSet G

case h₂
G : Type u
inst✝ : Group G
⊢ commutatorSet G ⊆ ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G)

Proof state:
case h₁
G : Type u
inst✝ : Group G
⊢ ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G) ⊆ commutatorSet G

Tactic:
rintro - ⟨-, ⟨g₁, g₂, rfl⟩, rfl⟩

Result:
case h₁.intro.intro.intro.intro
G : Type u
inst✝ : Group G
g₁ g₂ : ↥(closureCommutatorRepresentatives G)
⊢ (closureCommutatorRepresentatives G).subtype ⁅g₁, g₂⁆ ∈ commutatorSet G

Proof state:
case h₁.intro.intro.intro.intro
G : Type u
inst✝ : Group G
g₁ g₂ : ↥(closureCommutatorRepresentatives G)
⊢ (closureCommutatorRepresentatives G).subtype ⁅g₁, g₂⁆ ∈ commutatorSet G

Tactic:
exact ⟨g₁, g₂, rfl⟩

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem angle_zero_left (x : V) : angle 0 x = π / 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
⊢ angle 0 x = π / 2

Tactic:
unfold angle

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
⊢ arccos (inner 0 x / (‖0‖ * ‖x‖)) = π / 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
⊢ arccos (inner 0 x / (‖0‖ * ‖x‖)) = π / 2

Tactic:
rw [inner_zero_left, zero_div, Real.arccos_zero]

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
@[simp]
lemma coverMincard_empty {T : X → X} {U : Set (X × X)} {n : ℕ} : coverMincard T ∅ U n = 0 :=
  (sInf_le (by simp [IsDynCoverOf])).antisymm (zero_le (coverMincard T ∅ U n))

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
n : ℕ
⊢ 0 ∈ range fun s => ⨅ (_ : IsDynCoverOf T ∅ U n ↑s), ↑s.card

Tactic:
simp [IsDynCoverOf]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem Right.mul_pos [MulPosStrictMono α] (ha : 0 < a) (hb : 0 < b) : 0 < a * b

Proof state:
α : Type u_3
a b : α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b

Tactic:
simpa only [zero_mul] using mul_lt_mul_of_pos_right ha hb

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem lieSpan_mono {t : Set M} (h : s ⊆ t) : lieSpan R L s ≤ lieSpan R L t

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s t : Set M
h : s ⊆ t
⊢ lieSpan R L s ≤ lieSpan R L t

Tactic:
rw [lieSpan_le]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s t : Set M
h : s ⊆ t
⊢ s ⊆ ↑(lieSpan R L t)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s t : Set M
h : s ⊆ t
⊢ s ⊆ ↑(lieSpan R L t)

Tactic:
exact Subset.trans h subset_lieSpan

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
lemma id_comp (C : VariableChange R) : comp id C = C

Proof state:
R : Type u
inst✝ : CommRing R
C : VariableChange R
⊢ id.comp C = C

Tactic:
simp only [comp, id, zero_add, zero_mul, mul_zero, one_mul]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem pow_mem_closedBall {n : ℕ} (h : a ∈ closedBall b r) :
    a ^ n ∈ closedBall (b ^ n) (n • r)

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : a ∈ closedBall b r
⊢ a ^ n ∈ closedBall (b ^ n) (n • r)

Tactic:
simp only [mem_closedBall, dist_eq_norm_div, ← div_pow] at h ⊢

Result:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a / b‖ ≤ r
⊢ ‖(a / b) ^ n‖ ≤ n • r

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a / b‖ ≤ r
⊢ ↑n * ‖a / b‖ ≤ n • r

Tactic:
simpa only [nsmul_eq_mul] using mul_le_mul_of_nonneg_left h n.cast_nonneg

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a / b‖ ≤ r
⊢ ‖(a / b) ^ n‖ ≤ n • r

Tactic:
refine norm_pow_le_mul_norm.trans ?_

Result:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a / b‖ ≤ r
⊢ ↑n * ‖a / b‖ ≤ n • r
-- Mathlib/Tactic/Ring/Basic.lean
theorem mul_pp_pf_overlap {ea eb e : ℕ} (x : R) (_ : ea + eb = e) (_ : a₂ * b₂ = c) :
    (x ^ ea * a₂ : R) * (x ^ eb * b₂) = x ^ e * c

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a₂ b₂ c : R
ea eb e : ℕ
x : R
x✝¹ : ea + eb = e
x✝ : a₂ * b₂ = c
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * c

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a₂ b₂ : R
ea eb : ℕ
x : R
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a₂ b₂ : R
ea eb : ℕ
x : R
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂)

Tactic:
simp [pow_add, mul_mul_mul_comm]

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem toFinsupp_eq_single_one_one_iff {a : SkewMonoidAlgebra k G} :
    a.toFinsupp = Finsupp.single 1 1 ↔ a = 1

Proof state:
k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
inst✝¹ : One G
inst✝ : One k
a : SkewMonoidAlgebra k G
⊢ a.toFinsupp = Finsupp.single 1 1 ↔ a = 1

Tactic:
rw [← toFinsupp_one, toFinsupp_inj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_cons_eq_some : (a :: xs).find? p = some b ↔ (p a ∧ a = b) ∨ (!p a ∧ xs.find? p = some b)

Proof state:
α✝ : Type u_1
a : α✝
xs : List α✝
p : α✝ → Bool
b : α✝
⊢ find? p (a :: xs) = some b ↔ p a = true ∧ a = b ∨ (!p a) = true ∧ find? p xs = some b

Tactic:
rw [find?_cons]

Result:
α✝ : Type u_1
a : α✝
xs : List α✝
p : α✝ → Bool
b : α✝
⊢ (match p a with
      | true => some a
      | false => find? p xs) =
      some b ↔
    p a = true ∧ a = b ∨ (!p a) = true ∧ find? p xs = some b

Proof state:
α✝ : Type u_1
a : α✝
xs : List α✝
p : α✝ → Bool
b : α✝
⊢ (match p a with
      | true => some a
      | false => find? p xs) =
      some b ↔
    p a = true ∧ a = b ∨ (!p a) = true ∧ find? p xs = some b

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Data/Part.lean
theorem div_get_eq [Div α] (a b : Part α) (hab : Dom (a / b)) :
    (a / b).get hab = a.get (left_dom_of_div_dom hab) / b.get (right_dom_of_div_dom hab)

Proof state:
α : Type u_1
inst✝ : Div α
a b : Part α
hab : (a / b).Dom
⊢ (a / b).get hab = a.get ⋯ / b.get ⋯

Tactic:
simp [div_def]

Result:
α : Type u_1
inst✝ : Div α
a b : Part α
hab : (a / b).Dom
⊢ (a.bind fun y => map (fun x => y / x) b).get ⋯ = a.get ⋯ / b.get ⋯

Proof state:
α : Type u_1
inst✝ : Div α
a b : Part α
hab : (a / b).Dom
⊢ (a.bind fun y => map (fun x => y / x) b).get ⋯ = a.get ⋯ / b.get ⋯

Tactic:
aesop

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
lemma Nat.tendsto_div_const_atTop {n : ℕ} (hn : n ≠ 0) : Tendsto (· / n) atTop atTop

Proof state:
n : ℕ
hn : n ≠ 0
⊢ Tendsto (fun x => x / n) atTop atTop

Tactic:
rw [Tendsto, map_div_atTop_eq_nat n hn.bot_lt]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem infinite_of_forall_exists_gt (h : ∀ a, ∃ b ∈ s, a < b) : s.Infinite

Proof state:
α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n => Nat.recOn n ⋯.choose fun x a => ⋯.choose
⊢ ∀ (n : ℕ), f n ∈ s

Tactic:
rintro (_ | _) <;> exact (h _).choose_spec.1

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n => Nat.recOn n ⋯.choose fun x a => ⋯.choose
⊢ s.Infinite

Tactic:
have hf : ∀ n, f n ∈ s := by rintro (_ | _) <;> exact (h _).choose_spec.1

Result:
α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n => Nat.recOn n ⋯.choose fun x a => ⋯.choose
hf : ∀ (n : ℕ), f n ∈ s
⊢ s.Infinite

Proof state:
α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b ∈ s, a < b
⊢ s.Infinite

Tactic:
inhabit α

Result:
α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
⊢ s.Infinite

Proof state:
α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
⊢ s.Infinite

Tactic:
set f : ℕ → α := fun n => Nat.recOn n (h default).choose fun _ a => (h a).choose

Result:
α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n => Nat.recOn n ⋯.choose fun x a => ⋯.choose
⊢ s.Infinite

Proof state:
α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n => Nat.recOn n ⋯.choose fun x a => ⋯.choose
hf : ∀ (n : ℕ), f n ∈ s
⊢ s.Infinite

Tactic:
exact infinite_of_injective_forall_mem
  (strictMono_nat_of_lt_succ fun n => (h _).choose_spec.2).injective hf

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive (attr := simp)]
lemma prod_mul_prod_comm [Mul β] (s₁ s₂: Set α) (t₁ t₂ : Set β) :
   (s₁ ×ˢ t₁) * (s₂ ×ˢ t₂) = (s₁ * s₂) ×ˢ (t₁ * t₂)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Mul α
inst✝ : Mul β
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ s₁ ×ˢ t₁ * s₂ ×ˢ t₂ = (s₁ * s₂) ×ˢ (t₁ * t₂)

Tactic:
ext

Result:
case h
α : Type u_2
β : Type u_3
inst✝¹ : Mul α
inst✝ : Mul β
s₁ s₂ : Set α
t₁ t₂ : Set β
x✝ : α × β
⊢ x✝ ∈ s₁ ×ˢ t₁ * s₂ ×ˢ t₂ ↔ x✝ ∈ (s₁ * s₂) ×ˢ (t₁ * t₂)

Proof state:
case h
α : Type u_2
β : Type u_3
inst✝¹ : Mul α
inst✝ : Mul β
s₁ s₂ : Set α
t₁ t₂ : Set β
x✝ : α × β
⊢ (∃ a b, (a ∈ s₁ ∧ b ∈ t₁) ∧ ∃ a_1 b_1, (a_1 ∈ s₂ ∧ b_1 ∈ t₂) ∧ (a * a_1, b * b_1) = x✝) ↔
    (∃ x ∈ s₁, ∃ y ∈ s₂, x * y = x✝.1) ∧ ∃ x ∈ t₁, ∃ y ∈ t₂, x * y = x✝.2

Tactic:
aesop

Result:
no goals

Proof state:
case h
α : Type u_2
β : Type u_3
inst✝¹ : Mul α
inst✝ : Mul β
s₁ s₂ : Set α
t₁ t₂ : Set β
x✝ : α × β
⊢ x✝ ∈ s₁ ×ˢ t₁ * s₂ ×ˢ t₂ ↔ x✝ ∈ (s₁ * s₂) ×ˢ (t₁ * t₂)

Tactic:
simp [mem_mul]

Result:
case h
α : Type u_2
β : Type u_3
inst✝¹ : Mul α
inst✝ : Mul β
s₁ s₂ : Set α
t₁ t₂ : Set β
x✝ : α × β
⊢ (∃ a b, (a ∈ s₁ ∧ b ∈ t₁) ∧ ∃ a_1 b_1, (a_1 ∈ s₂ ∧ b_1 ∈ t₂) ∧ (a * a_1, b * b_1) = x✝) ↔
    (∃ x ∈ s₁, ∃ y ∈ s₂, x * y = x✝.1) ∧ ∃ x ∈ t₁, ∃ y ∈ t₂, x * y = x✝.2
-- Mathlib/Data/NNReal/Defs.lean
theorem _root_.Real.toNNReal_of_nonneg {r : ℝ} (hr : 0 ≤ r) : r.toNNReal = ⟨r, hr⟩

Proof state:
r : ℝ
hr : 0 ≤ r
⊢ r.toNNReal = ⟨r, hr⟩

Tactic:
simp_rw [Real.toNNReal, max_eq_left hr]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem submonoidMap_surjective (f : M →* N) (M' : Submonoid M) :
    Function.Surjective (f.submonoidMap M')

Proof state:
case mk.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
M' : Submonoid M
x : M
hx : x ∈ ↑M'
⊢ ∃ a, (f.submonoidMap M') a = ⟨f x, ⋯⟩

Tactic:
exact ⟨⟨x, hx⟩, rfl⟩

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
M' : Submonoid M
⊢ Surjective ⇑(f.submonoidMap M')

Tactic:
rintro ⟨_, x, hx, rfl⟩

Result:
case mk.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
M' : Submonoid M
x : M
hx : x ∈ ↑M'
⊢ ∃ a, (f.submonoidMap M') a = ⟨f x, ⋯⟩
-- Mathlib/Data/Set/NAry.lean
theorem image2_distrib_subset_left {f : α → δ → ε} {g : β → γ → δ} {f₁ : α → β → β'}
    {f₂ : α → γ → γ'} {g' : β' → γ' → ε} (h_distrib : ∀ a b c, f a (g b c) = g' (f₁ a b) (f₂ a c)) :
    image2 f s (image2 g t u) ⊆ image2 g' (image2 f₁ s t) (image2 f₂ s u)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : α → δ → ε
g : β → γ → δ
f₁ : α → β → β'
f₂ : α → γ → γ'
g' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)
a : α
ha : a ∈ s
b : β
hb : b ∈ t
c : γ
hc : c ∈ u
⊢ f a (g b c) ∈ image2 g' (image2 f₁ s t) (image2 f₂ s u)

Tactic:
rw [h_distrib]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : α → δ → ε
g : β → γ → δ
f₁ : α → β → β'
f₂ : α → γ → γ'
g' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)
a : α
ha : a ∈ s
b : β
hb : b ∈ t
c : γ
hc : c ∈ u
⊢ g' (f₁ a b) (f₂ a c) ∈ image2 g' (image2 f₁ s t) (image2 f₂ s u)

Proof state:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : α → δ → ε
g : β → γ → δ
f₁ : α → β → β'
f₂ : α → γ → γ'
g' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)
⊢ image2 f s (image2 g t u) ⊆ image2 g' (image2 f₁ s t) (image2 f₂ s u)

Tactic:
rintro _ ⟨a, ha, _, ⟨b, hb, c, hc, rfl⟩, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : α → δ → ε
g : β → γ → δ
f₁ : α → β → β'
f₂ : α → γ → γ'
g' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)
a : α
ha : a ∈ s
b : β
hb : b ∈ t
c : γ
hc : c ∈ u
⊢ f a (g b c) ∈ image2 g' (image2 f₁ s t) (image2 f₂ s u)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : α → δ → ε
g : β → γ → δ
f₁ : α → β → β'
f₂ : α → γ → γ'
g' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)
a : α
ha : a ∈ s
b : β
hb : b ∈ t
c : γ
hc : c ∈ u
⊢ g' (f₁ a b) (f₂ a c) ∈ image2 g' (image2 f₁ s t) (image2 f₂ s u)

Tactic:
exact mem_image2_of_mem (mem_image2_of_mem ha hb) (mem_image2_of_mem ha hc)

Result:
no goals