harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/Primrec.lean
theorem nat_iff {f : α → β → σ} : Primrec₂ f ↔ Nat.Primrec
    (.unpaired fun m n => encode <| (@decode α _ m).bind fun a => (@decode β _ n).map (f a))

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
a : Option α
b : Option β
⊢ Option.map (fun p => f p.1 p.2) (a.bind fun a => Option.map (Prod.mk a) b) = a.bind fun a => Option.map (f a) b

Tactic:
cases a <;> cases b <;> rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
this :
  ∀ (a : Option α) (b : Option β),
    Option.map (fun p => f p.1 p.2) (a.bind fun a => Option.map (Prod.mk a) b) = a.bind fun a => Option.map (f a) b
⊢ Primrec₂ f ↔ Nat.Primrec (Nat.unpaired fun m n => encode ((decode m).bind fun a => Option.map (f a) (decode n)))

Tactic:
simp [Primrec₂, Primrec, this]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ Primrec₂ f ↔ Nat.Primrec (Nat.unpaired fun m n => encode ((decode m).bind fun a => Option.map (f a) (decode n)))

Tactic:
have :
  ∀ (a : Option α) (b : Option β),
    Option.map (fun p : α × β => f p.1 p.2)
        (Option.bind a fun a : α => Option.map (Prod.mk a) b) =
      Option.bind a fun a => Option.map (f a) b := fun a b => by
        cases a <;> cases b <;> rfl

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
this :
  ∀ (a : Option α) (b : Option β),
    Option.map (fun p => f p.1 p.2) (a.bind fun a => Option.map (Prod.mk a) b) = a.bind fun a => Option.map (f a) b
⊢ Primrec₂ f ↔ Nat.Primrec (Nat.unpaired fun m n => encode ((decode m).bind fun a => Option.map (f a) (decode n)))
-- Mathlib/RingTheory/Radical.lean
theorem disjoint_primeFactors {a b : R} (hc : IsCoprime a b) :
    Disjoint (primeFactors a) (primeFactors b)

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
⊢ Disjoint (primeFactors a) (primeFactors b)

Tactic:
exact Multiset.disjoint_toFinset.mpr (disjoint_normalizedFactors hc)

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
⊢ Disjoint (primeFactors a) (primeFactors b)

Tactic:
classical
exact Multiset.disjoint_toFinset.mpr (disjoint_normalizedFactors hc)

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Continuity.lean
/-- A version of `comap_norm_nhdsGT_zero` for a multiplicative normed group. -/
@[to_additive comap_norm_nhdsGT_zero]
lemma comap_norm_nhdsGT_zero' : comap norm (𝓝[>] 0) = 𝓝[≠] (1 : E)

Proof state:
E : Type u_5
inst✝ : NormedGroup E
⊢ comap norm (𝓝[>] 0) = 𝓝[≠] 1

Tactic:
simp [nhdsWithin, comap_norm_nhds_one, Set.preimage, Set.compl_def]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
theorem posLog_nat_mul {n : ℕ} {a : ℝ} :
    log⁺ (n * a) ≤ log n + log⁺ a

Proof state:
n : ℕ
a : ℝ
⊢ log⁺ (↑n * a) ≤ log⁺ ↑n + log⁺ a

Tactic:
exact posLog_mul

Result:
no goals

Proof state:
n : ℕ
a : ℝ
⊢ log⁺ (↑n * a) ≤ log ↑n + log⁺ a

Tactic:
rw [← log_of_nat_eq_posLog]

Result:
n : ℕ
a : ℝ
⊢ log⁺ (↑n * a) ≤ log⁺ ↑n + log⁺ a
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem familyOfBFamily'_enum {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o}
    (ho : type r = o) (f : ∀ a < o, α) (i hi) :
    familyOfBFamily' r ho f (enum r ⟨i, by rwa [ho]⟩) = f i hi

Proof state:
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : Ordinal.{u}
hi : i < o
⊢ familyOfBFamily' r ho f ((enum r) ⟨i, ⋯⟩) = f i hi

Tactic:
simp only [familyOfBFamily', typein_enum]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : Ordinal.{u}
hi : i < o
⊢ i ∈ Iio (type r)

Tactic:
rwa [ho]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Cast.lean
theorem Path.cast_heq {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Path u v) :
    HEq (p.cast hu hv) p

Proof state:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ HEq (cast hu hv p) p

Tactic:
rw [Path.cast_eq_cast]

Result:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ HEq (_root_.cast ⋯ p) p

Proof state:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ HEq (_root_.cast ⋯ p) p

Tactic:
exact _root_.cast_heq _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)} :
    (ofList l).isEmpty = l.isEmpty

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
⊢ (ofList l).isEmpty = l.isEmpty

Tactic:
simp_to_raw using Raw₀.isEmpty_insertMany_empty_list

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Erase.lean
theorem eraseIdx_set_gt {l : Vector α n} {i : Nat} {j : Nat} {a : α} (h : i < j) {w : j < n} :
    (l.set i a).eraseIdx j = (l.eraseIdx j).set i a

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i j : Nat
a : α
h : i < j
w : j < n
⊢ (l.set i a ⋯).eraseIdx j w = (l.eraseIdx j w).set i a ⋯

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
i j : Nat
a : α
h : i < j
l : Array α
w : j < l.size
⊢ ({ toArray := l, size_toArray := ⋯ }.set i a ⋯).eraseIdx j w =
    ({ toArray := l, size_toArray := ⋯ }.eraseIdx j w).set i a ⋯

Proof state:
case mk
α : Type u_1
i j : Nat
a : α
h : i < j
l : Array α
w : j < l.size
⊢ ({ toArray := l, size_toArray := ⋯ }.set i a ⋯).eraseIdx j w =
    ({ toArray := l, size_toArray := ⋯ }.eraseIdx j w).set i a ⋯

Tactic:
simp [Array.eraseIdx_set_gt, *]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem angle_add_angle_eq_pi_of_angle_eq_pi (p₁ : P) {p₂ p₃ p₄ : P} (h : ∠ p₂ p₃ p₄ = π) :
    ∠ p₁ p₃ p₂ + ∠ p₁ p₃ p₄ = π

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
⊢ ∠ p₂ p₃ p₁ + ∠ p₄ p₃ p₁ = π

Tactic:
unfold angle

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) + InnerProductGeometry.angle (p₄ -ᵥ p₃) (p₁ -ᵥ p₃) = π

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
h : ∠ p₂ p₃ p₄ = π
⊢ ∠ p₁ p₃ p₂ + ∠ p₁ p₃ p₄ = π

Tactic:
unfold angle at h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
⊢ ∠ p₁ p₃ p₂ + ∠ p₁ p₃ p₄ = π

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) + InnerProductGeometry.angle (p₄ -ᵥ p₃) (p₁ -ᵥ p₃) = π

Tactic:
exact angle_add_angle_eq_pi_of_angle_eq_pi _ h

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
⊢ ∠ p₁ p₃ p₂ + ∠ p₁ p₃ p₄ = π

Tactic:
rw [angle_comm p₁ p₃ p₂, angle_comm p₁ p₃ p₄]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
⊢ ∠ p₂ p₃ p₁ + ∠ p₄ p₃ p₁ = π
-- Mathlib/Data/Multiset/Bind.lean
theorem card_join (S) : card (@join α S) = sum (map card S) :=
  Multiset.induction_on S (by simp) (by simp)

Proof state:
α : Type u_1
S : Multiset (Multiset α)
⊢ (join 0).card = (map card 0).sum

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
S : Multiset (Multiset α)
⊢ ∀ (a : Multiset α) (s : Multiset (Multiset α)),
    s.join.card = (map card s).sum → (a ::ₘ s).join.card = (map card (a ::ₘ s)).sum

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
lemma intCast_div_eq_divInt (n d : ℤ) : (n : ℚ) / (d) = n /. d

Proof state:
n d : ℤ
⊢ ↑n / ↑d = n /. d

Tactic:
rw [divInt_eq_div]

Result:
no goals
-- Mathlib/Order/Irreducible.lean
theorem SupIrred.ne_bot (ha : SupIrred a) : a ≠ ⊥

Proof state:
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
ha : SupIrred a
⊢ a ≠ ⊥

Tactic:
rintro rfl

Result:
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
ha : SupIrred ⊥
⊢ False

Proof state:
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
ha : SupIrred ⊥
⊢ False

Tactic:
exact not_supIrred_bot ha

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem tendsto_nhds_infty {α : Type*} {f : OnePoint X → α} {l : Filter α} :
    Tendsto f (𝓝 ∞) l ↔
      ∀ s ∈ l, f ∞ ∈ s ∧ ∃ t : Set X, IsClosed t ∧ IsCompact t ∧ MapsTo (f ∘ (↑)) tᶜ s :=
  tendsto_nhds_infty'.trans <| by
    simp only [tendsto_pure_left, hasBasis_coclosedCompact.tendsto_left_iff, forall_and,
      and_assoc, exists_prop]

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
α : Type u_3
f : OnePoint X → α
l : Filter α
⊢ Tendsto f (pure ∞) l ∧ Tendsto (f ∘ some) (coclosedCompact X) l ↔
    ∀ s ∈ l, f ∞ ∈ s ∧ ∃ t, IsClosed t ∧ IsCompact t ∧ MapsTo (f ∘ some) tᶜ s

Tactic:
simp only [tendsto_pure_left, hasBasis_coclosedCompact.tendsto_left_iff, forall_and,
  and_assoc, exists_prop]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem multiset_prod_span_singleton (m : Multiset R) :
    (m.map fun x => Ideal.span {x}).prod = Ideal.span ({Multiset.prod m} : Set R) :=
  Multiset.induction_on m (by simp) fun a m ih => by
    simp only [Multiset.map_cons, Multiset.prod_cons, ih, ← Ideal.span_singleton_mul_span_singleton]

Proof state:
R : Type u
inst✝ : CommSemiring R
m✝ : Multiset R
a : R
m : Multiset R
ih : (Multiset.map (fun x => span {x}) m).prod = span {m.prod}
⊢ (Multiset.map (fun x => span {x}) (a ::ₘ m)).prod = span {(a ::ₘ m).prod}

Tactic:
simp only [Multiset.map_cons, Multiset.prod_cons, ih, ← Ideal.span_singleton_mul_span_singleton]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
m : Multiset R
⊢ (Multiset.map (fun x => span {x}) 0).prod = span {Multiset.prod 0}

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addY_of_Z_eq_zero_right [NoZeroDivisors R] {P Q : Fin 3 → R} (hQ : W'.Equation Q)
    (hQz : Q z = 0) : W'.addY P Q = -(Q y ^ 2 * P z) * P y

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ W'.addY P Q = -(Q y ^ 2 * P z) * P y

Tactic:
rw [addY, negY_eq, negAddY_of_Z_eq_zero_right hQ hQz, negY, addX_of_Z_eq_zero_right hQ hQz,
  addZ_of_Z_eq_zero_right hQ hQz]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -(-(Q y ^ 2 * P z) * (-P y - W'.a₁ * P x - W'.a₃ * P z)) - W'.a₁ * (-(Q y ^ 2 * P z) * P x) -
      W'.a₃ * (-(Q y ^ 2 * P z) * P z) =
    -(Q y ^ 2 * P z) * P y

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -(-(Q y ^ 2 * P z) * (-P y - W'.a₁ * P x - W'.a₃ * P z)) - W'.a₁ * (-(Q y ^ 2 * P z) * P x) -
      W'.a₃ * (-(Q y ^ 2 * P z) * P z) =
    -(Q y ^ 2 * P z) * P y

Tactic:
ring1

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem ppow_succ {f : ArithmeticFunction R} {k : ℕ} {kpos : 0 < k} :
    f.ppow (k + 1) = (f.ppow k).pmul f

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
⊢ f x ^ k * f x = ((f.ppow k).pmul f) x

Tactic:
induction k <;> simp

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
⊢ (f.ppow (k + 1)) x = ((f.ppow k).pmul f) x

Tactic:
rw [ppow_apply (Nat.succ_pos k), _root_.pow_succ]

Result:
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
⊢ f x ^ k * f x = ((f.ppow k).pmul f) x

Proof state:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
⊢ f.ppow (k + 1) = (f.ppow k).pmul f

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
⊢ (f.ppow (k + 1)) x = ((f.ppow k).pmul f) x
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma nnrpow_eq_rpow {a : A} {x : ℝ≥0} (hx : 0 < x) : a ^ x = a ^ (x : ℝ)

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
hx : 0 < x
⊢ a ^ x = a ^ ↑x

Tactic:
rw [nnrpow_def (A := A), rpow_def, cfcₙ_eq_cfc]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma LeftFraction.op_map
    {X Y : C} (φ : W.LeftFraction X Y) (L : C ⥤ D) (hL : W.IsInvertedBy L) :
    (φ.map L hL).op = φ.op.map L.op hL.op

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
φ : W.LeftFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
⊢ (inv (L.map φ.s)).op ≫ (L.map φ.f).op = inv (L.map φ.s).op ≫ (L.map φ.f).op

Tactic:
rw [op_inv]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
φ : W.LeftFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
⊢ (φ.map L hL).op = φ.op.map L.op ⋯

Tactic:
dsimp [map, RightFraction.map]

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
φ : W.LeftFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
⊢ (inv (L.map φ.s)).op ≫ (L.map φ.f).op = inv (L.map φ.s).op ≫ (L.map φ.f).op
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/DecidableEq.lean
theorem beq_toList [BEq α] (a b : Array α) : (a.toList == b.toList) = (a == b)

Proof state:
α : Type u_1
inst✝ : BEq α
a b : Array α
⊢ (a.toList == b.toList) = (a == b)

Tactic:
simp [beq_eq_decide, List.beq_eq_decide]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_le_toIocMod (a b : α) : toIcoMod hp a b ≤ toIocMod hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b • p ≤ toIcoDiv hp a b • p

Tactic:
exact zsmul_left_mono hp.le (toIocDiv_wcovBy_toIcoDiv _ _ _).le

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b ≤ toIocMod hp a b

Tactic:
rw [toIcoMod, toIocMod, sub_le_sub_iff_left]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b • p ≤ toIcoDiv hp a b • p
-- Mathlib/Algebra/Lie/Submodule.lean
theorem idealRange_eq_map : f.idealRange = LieIdeal.map f ⊤

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'
⊢ f.idealRange = LieIdeal.map f ⊤

Tactic:
ext

Result:
case h
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'
m✝ : L'
⊢ m✝ ∈ f.idealRange ↔ m✝ ∈ LieIdeal.map f ⊤

Proof state:
case h
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'
m✝ : L'
⊢ m✝ ∈ f.idealRange ↔ m✝ ∈ LieIdeal.map f ⊤

Tactic:
simp only [idealRange, range_eq_map]

Result:
case h
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'
m✝ : L'
⊢ m✝ ∈ LieSubmodule.lieSpan R L' ↑(LieSubalgebra.map f ⊤) ↔ m✝ ∈ LieIdeal.map f ⊤

Proof state:
case h
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'
m✝ : L'
⊢ m✝ ∈ LieSubmodule.lieSpan R L' ↑(LieSubalgebra.map f ⊤) ↔ m✝ ∈ LieIdeal.map f ⊤

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Bounds/Image.lean
theorem BddBelow.image2 :
    BddBelow s → BddBelow t → BddBelow (image2 f s t)

Proof state:
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddBelow (image2 f s t)

Tactic:
exact ⟨f a b, mem_lowerBounds_image2 h₀ h₁ ha hb⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ BddBelow s → BddBelow t → BddBelow (image2 f s t)

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Result:
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddBelow (image2 f s t)
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled/Lemmas.lean
lemma mulRight₀_symm (a : G₀) (ha : 0 < a) :
    (mulRight₀ a ha).symm = mulRight₀ a⁻¹ (inv_pos.2 ha)

Proof state:
G₀ : Type u_1
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : PartialOrder G₀
inst✝³ : MulPosMono G₀
inst✝² : MulPosReflectLE G₀
inst✝¹ : ZeroLEOneClass G₀
inst✝ : PosMulReflectLT G₀
a : G₀
ha : 0 < a
⊢ (mulRight₀ a ha).symm = mulRight₀ a⁻¹ ⋯

Tactic:
ext

Result:
case h.h
G₀ : Type u_1
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : PartialOrder G₀
inst✝³ : MulPosMono G₀
inst✝² : MulPosReflectLE G₀
inst✝¹ : ZeroLEOneClass G₀
inst✝ : PosMulReflectLT G₀
a : G₀
ha : 0 < a
x✝ : G₀
⊢ (mulRight₀ a ha).symm x✝ = (mulRight₀ a⁻¹ ⋯) x✝

Proof state:
case h.h
G₀ : Type u_1
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : PartialOrder G₀
inst✝³ : MulPosMono G₀
inst✝² : MulPosReflectLE G₀
inst✝¹ : ZeroLEOneClass G₀
inst✝ : PosMulReflectLT G₀
a : G₀
ha : 0 < a
x✝ : G₀
⊢ (mulRight₀ a ha).symm x✝ = (mulRight₀ a⁻¹ ⋯) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Filter/Subsingleton.lean
theorem subsingleton_iff_exists_singleton_mem [Nonempty α] : l.Subsingleton ↔ ∃ a, {a} ∈ l

Proof state:
α : Type u_1
l : Filter α
inst✝ : Nonempty α
⊢ l.Subsingleton ↔ ∃ a, {a} ∈ l

Tactic:
simp only [subsingleton_iff_exists_le_pure, le_pure_iff]

Result:
no goals
-- Mathlib/Data/List/AList.lean
theorem mem_erase {a a' : α} {s : AList β} : a' ∈ erase a s ↔ a' ≠ a ∧ a' ∈ s

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
s : AList β
⊢ a' ∈ erase a s ↔ a' ≠ a ∧ a' ∈ s

Tactic:
rw [mem_keys, keys_erase, s.keys_nodup.mem_erase_iff, ← mem_keys]

Result:
no goals
-- Mathlib/GroupTheory/Transfer.lean
theorem transfer_def [FiniteIndex H] (g : G) : transfer ϕ g = diff ϕ T (g • T)

Proof state:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
T : H.LeftTransversal
inst✝ : H.FiniteIndex
g : G
⊢ ϕ.transfer g = diff ϕ T (g • T)

Tactic:
rw [transfer, ← diff_mul_diff, ← smul_diff_smul, mul_comm, diff_mul_diff] <;> rfl

Result:
no goals
-- Mathlib/Data/List/Lookmap.lean
theorem lookmap.go_append (l : List α) (acc : Array α) :
    lookmap.go f l acc = acc.toListAppend (lookmap f l)

Proof state:
case cons
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ (match f hd with
    | some b => acc.toListAppend (b :: tl)
    | none => go f tl (acc.push hd)) =
    acc.toListAppend
      (match f hd with
      | some b => #[].toListAppend (b :: tl)
      | none => go f tl (#[].push hd))

Tactic:
cases f hd with
| none =>
  simp only [go_append tl _, Array.toListAppend_eq, append_assoc, Array.push_toList]
  rfl
| some a => rfl

Result:
no goals

Proof state:
α : Type u_1
f : α → Option α
l : List α
acc : Array α
⊢ go f l acc = acc.toListAppend (lookmap f l)

Tactic:
cases l with
| nil => simp [go, lookmap]
| cons hd tl =>
  rw [lookmap, go, go]
  cases f hd with
  | none =>
    simp only [go_append tl _, Array.toListAppend_eq, append_assoc, Array.push_toList]
    rfl
  | some a => rfl

Result:
no goals

Proof state:
case cons.some
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
a : α
⊢ (match some a with
    | some b => acc.toListAppend (b :: tl)
    | none => go f tl (acc.push hd)) =
    acc.toListAppend
      (match some a with
      | some b => #[].toListAppend (b :: tl)
      | none => go f tl (#[].push hd))

Tactic:
rfl

Result:
no goals

Proof state:
case cons.none
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ (match none with
    | some b => acc.toListAppend (b :: tl)
    | none => go f tl (acc.push hd)) =
    acc.toListAppend
      (match none with
      | some b => #[].toListAppend (b :: tl)
      | none => go f tl (#[].push hd))

Tactic:
simp only [go_append tl _, Array.toListAppend_eq, append_assoc, Array.push_toList]

Result:
case cons.none
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ acc.toList ++ ([hd] ++ lookmap f tl) = acc.toList ++ ([] ++ ([hd] ++ lookmap f tl))

Proof state:
case cons
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ go f (hd :: tl) acc = acc.toListAppend (lookmap f (hd :: tl))

Tactic:
rw [lookmap, go, go]

Result:
case cons
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ (match f hd with
    | some b => acc.toListAppend (b :: tl)
    | none => go f tl (acc.push hd)) =
    acc.toListAppend
      (match f hd with
      | some b => #[].toListAppend (b :: tl)
      | none => go f tl (#[].push hd))

Proof state:
case nil
α : Type u_1
f : α → Option α
acc : Array α
⊢ go f [] acc = acc.toListAppend (lookmap f [])

Tactic:
simp [go, lookmap]

Result:
no goals

Proof state:
case cons.none
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ acc.toList ++ ([hd] ++ lookmap f tl) = acc.toList ++ ([] ++ ([hd] ++ lookmap f tl))

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Partition/Finpartition.lean
theorem part_surjOn : Set.SurjOn P.part s P.parts := fun p hp ↦ by
  obtain ⟨x, hx⟩ := P.nonempty_of_mem_parts hp
  have hx' := mem_of_subset (P.le hp) hx
  use x, hx', (P.existsUnique_mem hx').unique ⟨P.part_mem hx', P.mem_part hx'⟩ ⟨hp, hx⟩

Proof state:
case intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ ↑P.parts
x : α
hx : x ∈ p
hx' : x ∈ s
⊢ p ∈ P.part '' ↑s

Tactic:
use x, hx', (P.existsUnique_mem hx').unique ⟨P.part_mem hx', P.mem_part hx'⟩ ⟨hp, hx⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ ↑P.parts
⊢ p ∈ P.part '' ↑s

Tactic:
obtain ⟨x, hx⟩ := P.nonempty_of_mem_parts hp

Result:
case intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ ↑P.parts
x : α
hx : x ∈ p
⊢ p ∈ P.part '' ↑s

Proof state:
case intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ ↑P.parts
x : α
hx : x ∈ p
⊢ p ∈ P.part '' ↑s

Tactic:
have hx' := mem_of_subset (P.le hp) hx

Result:
case intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ ↑P.parts
x : α
hx : x ∈ p
hx' : x ∈ s
⊢ p ∈ P.part '' ↑s