harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma add_smul_equiv (P Q : Fin 3 → R) {u v : R} (hu : IsUnit u) (hv : IsUnit v) :
    W'.add (u • P) (v • Q) ≈ W'.add P Q

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : ¬P ≈ Q
⊢ (fun m => m • W'.add P Q) ((hu.unit * hv.unit) ^ 2) = W'.add (u • P) (v • Q)

Tactic:
convert (add_smul_of_not_equiv h hu hv).symm

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : P ≈ Q
⊢ (fun m => m • W'.add P Q) (hu.unit ^ 4) = W'.add (u • P) (v • Q)

Tactic:
convert (add_smul_of_equiv h hu hv).symm

Result:
no goals

Proof state:
case neg
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : ¬P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

Tactic:
exact ⟨(hu.unit * hv.unit) ^ 2, by convert (add_smul_of_not_equiv h hu hv).symm⟩

Result:
no goals

Proof state:
case pos
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

Tactic:
exact ⟨hu.unit ^ 4, by convert (add_smul_of_equiv h hu hv).symm⟩

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

Tactic:
by_cases h : P ≈ Q

Result:
case pos
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

case neg
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : ¬P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem isBasis_basic_opens : TopologicalSpace.Opens.IsBasis (Set.range (@basicOpen R _))

Proof state:
case h.e'_3
R : Type u
inst✝ : CommSemiring R
⊢ Set.range (SetLike.coe ∘ basicOpen) = Set.range fun r => ↑(basicOpen r)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ TopologicalSpace.IsTopologicalBasis (SetLike.coe '' Set.range basicOpen)

Tactic:
convert isTopologicalBasis_basic_opens (R := R)

Result:
case h.e'_3
R : Type u
inst✝ : CommSemiring R
⊢ SetLike.coe '' Set.range basicOpen = Set.range fun r => ↑(basicOpen r)

Proof state:
case h.e'_3
R : Type u
inst✝ : CommSemiring R
⊢ SetLike.coe '' Set.range basicOpen = Set.range fun r => ↑(basicOpen r)

Tactic:
rw [← Set.range_comp]

Result:
case h.e'_3
R : Type u
inst✝ : CommSemiring R
⊢ Set.range (SetLike.coe ∘ basicOpen) = Set.range fun r => ↑(basicOpen r)

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ TopologicalSpace.Opens.IsBasis (Set.range basicOpen)

Tactic:
unfold TopologicalSpace.Opens.IsBasis

Result:
R : Type u
inst✝ : CommSemiring R
⊢ TopologicalSpace.IsTopologicalBasis (SetLike.coe '' Set.range basicOpen)
-- Mathlib/Topology/LocallyClosed.lean
theorem dense_coborder {s : Set X} :
    Dense (coborder s)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ Dense (coborder s)

Tactic:
rw [dense_iff_closure_eq, coborder_eq_union_closure_compl, closure_union, ← univ_subset_iff]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ univ ⊆ closure s ∪ closure (closure s)ᶜ

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ univ ⊆ closure s ∪ (closure s)ᶜ

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ univ ⊆ closure s ∪ closure (closure s)ᶜ

Tactic:
refine _root_.subset_trans ?_ (union_subset_union_right _ (subset_closure))

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ univ ⊆ closure s ∪ (closure s)ᶜ
-- Mathlib/Data/Fintype/Basic.lean
theorem nonempty_fintype (α : Type*) [Finite α] : Nonempty (Fintype α)

Proof state:
α : Type u_4
inst✝ : Finite α
⊢ Nonempty (Fintype α)

Tactic:
rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩

Result:
case intro.intro
α : Type u_4
inst✝ : Finite α
n : ℕ
e : α ≃ Fin n
⊢ Nonempty (Fintype α)

Proof state:
case intro.intro
α : Type u_4
inst✝ : Finite α
n : ℕ
e : α ≃ Fin n
⊢ Nonempty (Fintype α)

Tactic:
exact ⟨.ofEquiv _ e.symm⟩

Result:
no goals
-- Mathlib/Data/Fintype/List.lean
theorem perm_toList {f₁ f₂ : Finset α} : f₁.toList ~ f₂.toList ↔ f₁ = f₂ :=
  ⟨fun h => Finset.ext_iff.mpr (fun x => by simpa [← Finset.mem_toList] using Perm.mem_iff h),
   fun h ↦ Perm.of_eq <| congrArg Finset.toList h⟩

Proof state:
α : Type u_1
f₁ f₂ : Finset α
h : f₁.toList ~ f₂.toList
x : α
⊢ x ∈ f₁ ↔ x ∈ f₂

Tactic:
simpa [← Finset.mem_toList] using Perm.mem_iff h

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem lt_mul_of_lt_one_right [ExistsAddOfLE α] [PosMulStrictMono α]
    [AddRightStrictMono α] [AddRightReflectLT α]
    (ha : a < 0) (h : b < 1) : a < a * b

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b : α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulStrictMono α
inst✝¹ : AddRightStrictMono α
inst✝ : AddRightReflectLT α
ha : a < 0
h : b < 1
⊢ a < a * b

Tactic:
simpa only [mul_one] using mul_lt_mul_of_neg_left h ha

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatten_filter_not_isEmpty  :
    ∀ {L : List (List α)}, flatten (L.filter fun l => !l.isEmpty) = L.flatten
  | [] => rfl
  | [] :: L
  | (a :: l) :: L => by
      simp [flatten_filter_not_isEmpty (L := L)]

Proof state:
α : Type u_1
a : α
l : List α
L : List (List α)
⊢ (filter (fun l => !l.isEmpty) ((a :: l) :: L)).flatten = ((a :: l) :: L).flatten

Tactic:
simp [flatten_filter_not_isEmpty (L := L)]

Result:
no goals
-- Mathlib/Data/Finset/Disjoint.lean
theorem disjoint_right : Disjoint s t ↔ ∀ ⦃a⦄, a ∈ t → a ∉ s

Proof state:
α : Type u_1
s t : Finset α
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s

Tactic:
rw [_root_.disjoint_comm, disjoint_left]

Result:
no goals
-- Mathlib/Order/SuccPred/CompleteLinearOrder.lean
theorem Order.IsSuccPrelimit.sSup_Iio (h : IsSuccPrelimit x) : sSup (Iio x) = x

Proof state:
case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
hx : ⊥ < x
⊢ sSup (Iio x) = x

Tactic:
exact h.isLUB_Iio.csSup_eq ⟨⊥, hx⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
⊢ sSup (Iio x) = x

Tactic:
obtain rfl | hx := eq_bot_or_bot_lt x

Result:
case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
h : IsSuccPrelimit ⊥
⊢ sSup (Iio ⊥) = ⊥

case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
hx : ⊥ < x
⊢ sSup (Iio x) = x

Proof state:
case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
h : IsSuccPrelimit ⊥
⊢ sSup (Iio ⊥) = ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem union_C0C1_eq : (C0 C ho) ∪ (C1 C ho) = C

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ C0 C ho ∪ C1 C ho = C

Tactic:
ext x

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
⊢ x ∈ C0 C ho ∪ C1 C ho ↔ x ∈ C

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x : I → Bool
⊢ x ∈ C0 C ho ∪ C1 C ho ↔ x ∈ C

Tactic:
simp only [C0, C1, Set.mem_union, Set.mem_inter_iff, Set.mem_setOf_eq,
  ← and_or_left, and_iff_left_iff_imp, Bool.dichotomy (x (term I ho)), implies_true]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_singleton (a : α) (p : α → Bool) :
    #v[a].find? p = if p a then some a else none

Proof state:
α : Type
a : α
p : α → Bool
⊢ find? p { toArray := #[a], size_toArray := ⋯ } = if p a = true then some a else none

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem size_updateBucket [Hashable α] {self : Array (AssocList α β)} {h : 0 < self.size} {k : α}
    {f : AssocList α β → AssocList α β} : (updateBucket self h k f).size = self.size

Proof state:
α : Type u
β : α → Type v
inst✝ : Hashable α
self : Array (AssocList α β)
h : 0 < self.size
k : α
f : AssocList α β → AssocList α β
⊢ (updateBucket self h k f).size = self.size

Tactic:
simp [updateBucket]

Result:
no goals
-- Mathlib/Data/ENat/Basic.lean
theorem toNat_eq_iff {m : ℕ∞} {n : ℕ} (hn : n ≠ 0) : toNat m = n ↔ m = n

Proof state:
m : ℕ∞
n : ℕ
hn : n ≠ 0
⊢ m.toNat = n ↔ m = ↑n

Tactic:
induction m <;> simp [hn.symm]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem nat_mul_aleph0 {n : ℕ} (hn : n ≠ 0) : ↑n * ℵ₀ = ℵ₀ :=
  le_antisymm (lift_mk_fin n ▸ mk_le_aleph0) <|
    le_mul_of_one_le_left (zero_le _) <| by
      rwa [← Nat.cast_one, Nat.cast_le, Nat.one_le_iff_ne_zero]

Proof state:
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ ↑n

Tactic:
rwa [← Nat.cast_one, Nat.cast_le, Nat.one_le_iff_ne_zero]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_intCast (z : ℤ) : ⌊(z : α)⌋ = z :=
  eq_of_forall_le_iff fun a => by rw [le_floor, Int.cast_le]

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z a : ℤ
⊢ a ≤ ⌊↑z⌋ ↔ a ≤ z

Tactic:
rw [le_floor, Int.cast_le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem deleteOne_preserves_assignments_size {n : Nat} (f : DefaultFormula n) (id : Nat) :
    (deleteOne f id).assignments.size = f.assignments.size

Proof state:
n : Nat
f : DefaultFormula n
id : Nat
⊢ (f.deleteOne id).assignments.size = f.assignments.size

Tactic:
simp only [deleteOne]

Result:
n : Nat
f : DefaultFormula n
id : Nat
⊢ (match f.clauses[id]! with
        | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
        | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
          { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
        | some val =>
          { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }).assignments.size =
    f.assignments.size

Proof state:
n : Nat
f : DefaultFormula n
id : Nat
⊢ (match f.clauses[id]! with
        | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
        | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
          { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
        | some val =>
          { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }).assignments.size =
    f.assignments.size

Tactic:
split <;> simp only [Array.size_modify]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) {n : Nat}
    (hn : n < (pmap f l h).length) :
    (pmap f l h)[n] =
      f (l[n]'(@length_pmap _ _ p f l h ▸ hn))
        (h _ (getElem_mem (@length_pmap _ _ p f l h ▸ hn)))

Proof state:
case nil
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ [] → p a
n : Nat
hn : n < 0
⊢ (pmap f [] h)[n] = f [][n] ⋯

Tactic:
exact absurd hn (Nat.not_lt_of_le n.zero_le)

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) {n : Nat} (hn : n < (pmap f tl h).length), (pmap f tl h)[n] = f tl[n] ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
n✝ : Nat
hn : n✝ + 1 < (pmap f (hd :: tl) h).length
⊢ (pmap f (hd :: tl) h)[n✝ + 1] = f (hd :: tl)[n✝ + 1] ⋯

Tactic:
simp [hl]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ [] → p a
n : Nat
hn : n < (pmap f [] h).length
⊢ (pmap f [] h)[n] = f [][n] ⋯

Tactic:
simp only [length, pmap] at hn

Result:
case nil
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ [] → p a
n : Nat
hn : n < 0
⊢ (pmap f [] h)[n] = f [][n] ⋯

Proof state:
case cons
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) {n : Nat} (hn : n < (pmap f tl h).length), (pmap f tl h)[n] = f tl[n] ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
n : Nat
hn : n < (pmap f (hd :: tl) h).length
⊢ (pmap f (hd :: tl) h)[n] = f (hd :: tl)[n] ⋯

Tactic:
cases n

Result:
case cons.zero
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) {n : Nat} (hn : n < (pmap f tl h).length), (pmap f tl h)[n] = f tl[n] ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
hn : 0 < (pmap f (hd :: tl) h).length
⊢ (pmap f (hd :: tl) h)[0] = f (hd :: tl)[0] ⋯

case cons.succ
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) {n : Nat} (hn : n < (pmap f tl h).length), (pmap f tl h)[n] = f tl[n] ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
n✝ : Nat
hn : n✝ + 1 < (pmap f (hd :: tl) h).length
⊢ (pmap f (hd :: tl) h)[n✝ + 1] = f (hd :: tl)[n✝ + 1] ⋯

Proof state:
case cons.zero
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) {n : Nat} (hn : n < (pmap f tl h).length), (pmap f tl h)[n] = f tl[n] ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
hn : 0 < (pmap f (hd :: tl) h).length
⊢ (pmap f (hd :: tl) h)[0] = f (hd :: tl)[0] ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.of_measure_le_smul {μ' : Measure α} {c : ℝ≥0∞} (hc : c ≠ ∞) (hμ'_le : μ' ≤ c • μ)
    {f : α → β} (hf : Integrable f μ) : Integrable f μ'

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → β
hf : MemLp f 1 μ
⊢ MemLp f 1 μ'

Tactic:
exact hf.of_measure_le_smul hc hμ'_le

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → β
hf : Integrable f μ
⊢ Integrable f μ'

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → β
hf : MemLp f 1 μ
⊢ MemLp f 1 μ'
-- Mathlib/MeasureTheory/Group/Prod.lean
theorem measure_mul_right_null (y : G) : μ ((fun x => x * y) ⁻¹' s) = 0 ↔ μ s = 0 :=
  calc
    μ ((fun x => x * y) ⁻¹' s) = 0 ↔ μ ((fun x => y⁻¹ * x) ⁻¹' s⁻¹)⁻¹ = 0

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
y : G
⊢ μ ((fun x => x * y) ⁻¹' s) = 0 ↔ μ ((fun x => y⁻¹ * x) ⁻¹' s⁻¹)⁻¹ = 0

Tactic:
simp_rw [← inv_preimage, preimage_preimage, mul_inv_rev, inv_inv]

Result:
no goals

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
y : G
⊢ μ ((fun x => y⁻¹ * x) ⁻¹' s⁻¹)⁻¹ = 0 ↔ μ s = 0

Tactic:
simp only [measure_inv_null μ, measure_preimage_mul]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem thickening_union (δ : ℝ) (s t : Set α) :
    thickening δ (s ∪ t) = thickening δ s ∪ thickening δ t

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s t : Set α
⊢ thickening δ (s ∪ t) = thickening δ s ∪ thickening δ t

Tactic:
simp_rw [thickening, infEdist_union, min_lt_iff, setOf_or]

Result:
no goals
-- Mathlib/Algebra/Lie/Abelian.lean
lemma isFaithful_iff_ker_eq_bot : IsFaithful R L M ↔ LieModule.ker R L M = ⊥

Proof state:
R : Type u
L : Type v
M : Type w
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
⊢ IsFaithful R L M ↔ LieModule.ker R L M = ⊥

Tactic:
rw [isFaithful_iff', LieSubmodule.ext_iff]

Result:
R : Type u
L : Type v
M : Type w
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
⊢ (∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0) ↔ ∀ (m : L), m ∈ LieModule.ker R L M ↔ m ∈ ⊥

Proof state:
R : Type u
L : Type v
M : Type w
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
⊢ (∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0) ↔ ∀ (m : L), m ∈ LieModule.ker R L M ↔ m ∈ ⊥

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_eq_iff_eq_mul' : a / b = c ↔ a = b * c

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ a / b = c ↔ a = b * c

Tactic:
rw [div_eq_iff_eq_mul, mul_comm]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem mem_closure_iff_nhds_one {x : G} {s : Set G} :
    x ∈ closure s ↔ ∀ U ∈ (𝓝 1 : Filter G), ∃ y ∈ s, y / x ∈ U

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x : G
s : Set G
⊢ x ∈ closure s ↔ ∀ U ∈ 𝓝 1, ∃ y ∈ s, y / x ∈ U

Tactic:
rw [mem_closure_iff_nhds_basis ((𝓝 1 : Filter G).basis_sets.nhds_of_one x)]

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x : G
s : Set G
⊢ (∀ i ∈ 𝓝 1, ∃ y ∈ s, y ∈ {y | y / x ∈ id i}) ↔ ∀ U ∈ 𝓝 1, ∃ y ∈ s, y / x ∈ U

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x : G
s : Set G
⊢ (∀ i ∈ 𝓝 1, ∃ y ∈ s, y ∈ {y | y / x ∈ id i}) ↔ ∀ U ∈ 𝓝 1, ∃ y ∈ s, y / x ∈ U

Tactic:
simp_rw [Set.mem_setOf, id]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_self_rpow_inv {y : ℝ} (hy : y ≠ 0) (x : ℝ≥0) : (x ^ (1 / y)) ^ y = x

Proof state:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ (x ^ (1 / y)) ^ y = x

Tactic:
field_simp [← rpow_mul]

Result:
no goals
-- Mathlib/Analysis/Convex/Jensen.lean
/-- **Maximum principle** for convex functions on an interval. If a function `f` is convex on the
interval `[x, y]`, then the eventual maximum of `f` on `[x, y]` is at `x` or `y`. -/
lemma ConvexOn.le_max_of_mem_Icc {s : Set 𝕜} {f : 𝕜 → β} {x y z : 𝕜} (hf : ConvexOn 𝕜 s f)
    (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ Icc x y) : f z ≤ max (f x) (f y)

Proof state:
𝕜 : Type u_1
β : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set 𝕜
f : 𝕜 → β
x y z : 𝕜
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : z ∈ [x-[𝕜]y]
⊢ f z ≤ f x ⊔ f y

Tactic:
exact hf.le_max_of_mem_segment hx hy hz

Result:
no goals

Proof state:
𝕜 : Type u_1
β : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set 𝕜
f : 𝕜 → β
x y z : 𝕜
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : z ∈ Set.Icc x y
⊢ f z ≤ f x ⊔ f y

Tactic:
rw [← segment_eq_Icc (hz.1.trans hz.2)] at hz

Result:
𝕜 : Type u_1
β : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set 𝕜
f : 𝕜 → β
x y z : 𝕜
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : z ∈ [x-[𝕜]y]
⊢ f z ≤ f x ⊔ f y
-- Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
theorem isIso_of_epi_of_strongMono (f : P ⟶ Q) [Epi f] [StrongMono f] : IsIso f :=
  ⟨⟨(CommSq.mk (show 𝟙 P ≫ f = f ≫ 𝟙 Q by simp)).lift, by simp⟩⟩

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P Q : C
f : P ⟶ Q
inst✝¹ : Epi f
inst✝ : StrongMono f
⊢ 𝟙 P ≫ f = f ≫ 𝟙 Q

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P Q : C
f : P ⟶ Q
inst✝¹ : Epi f
inst✝ : StrongMono f
⊢ f ≫ ⋯.lift = 𝟙 P ∧ ⋯.lift ≫ f = 𝟙 Q

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem average_congr {f g : α → E} (h : f =ᵐ[μ] g) : ⨍ x, f x ∂μ = ⨍ x, g x ∂μ

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f g : α → E
h : f =ᶠ[ae μ] g
⊢ ⨍ (x : α), f x ∂μ = ⨍ (x : α), g x ∂μ

Tactic:
simp only [average_eq, integral_congr_ae h]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalWhiskerRight_cons_of {f f' g h i : C} {α : f' ≅ g} {η : g ⟶ h} {ηs : h ⟶ i}
    {ηs₁ : h ⊗ f ⟶ i ⊗ f} {η₁ : g ⊗ f ⟶ h ⊗ f} {η₂ : g ⊗ f ⟶ i ⊗ f}
    {η₃ : f' ⊗ f ⟶ i ⊗ f}
    (e_ηs₁ : ηs ▷ f = ηs₁) (e_η₁ : η ▷ f = η₁)
    (e_η₂ : η₁ ≫ ηs₁ = η₂) (e_η₃ : (whiskerRightIso α f).hom ≫ η₂ = η₃) :
    (α.hom ≫ η ≫ ηs) ▷ f = η₃

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g h i : C
α : f' ≅ g
η : g ⟶ h
ηs : h ⟶ i
ηs₁ : h ⊗ f ⟶ i ⊗ f
η₁ : g ⊗ f ⟶ h ⊗ f
η₂ : g ⊗ f ⟶ i ⊗ f
η₃ : f' ⊗ f ⟶ i ⊗ f
e_ηs₁ : ηs ▷ f = ηs₁
e_η₁ : η ▷ f = η₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : (whiskerRightIso α f).hom ≫ η₂ = η₃
⊢ (α.hom ≫ η ≫ ηs) ▷ f = η₃

Tactic:
simp_all

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
/-- See `inner_smul_right` for the common special when `𝕜 = 𝕝`. -/
lemma inner_smul_right_eq_smul (x y : E) (r : 𝕝) : ⟪x, r • y⟫ = r • ⟪x, y⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst✝⁵ : CommSemiring 𝕝
inst✝⁴ : StarRing 𝕝
inst✝³ : Algebra 𝕝 𝕜
inst✝² : Module 𝕝 E
inst✝¹ : IsScalarTower 𝕝 𝕜 E
inst✝ : StarModule 𝕝 𝕜
x y : E
r : 𝕝
⊢ ⟪x, r • y⟫_𝕜 = r • ⟪x, y⟫_𝕜

Tactic:
rw [← inner_conj_symm, inner_smul_left_eq_star_smul, starRingEnd_apply, starRingEnd_apply,
  star_smul, star_star, ← starRingEnd_apply, inner_conj_symm]

Result:
no goals
-- Mathlib/Data/Int/Cast/Field.lean
theorem cast_div [DivisionRing α] {m n : ℤ} (n_dvd : n ∣ m) (hn : (n : α) ≠ 0) :
    ((m / n : ℤ) : α) = m / n

Proof state:
case intro
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
hn : ↑n ≠ 0
k : ℤ
⊢ ↑(n * k / n) = ↑(n * k) / ↑n

Tactic:
have : n ≠ 0 := by rintro rfl; simp at hn

Result:
case intro
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
hn : ↑n ≠ 0
k : ℤ
this : n ≠ 0
⊢ ↑(n * k / n) = ↑(n * k) / ↑n

Proof state:
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
hn : ↑n ≠ 0
k : ℤ
⊢ n ≠ 0

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝ : DivisionRing α
k : ℤ
hn : ↑0 ≠ 0
⊢ False

Proof state:
case intro
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
hn : ↑n ≠ 0
k : ℤ
this : n ≠ 0
⊢ ↑(n * k / n) = ↑(n * k) / ↑n

Tactic:
rw [Int.mul_ediv_cancel_left _ this, mul_comm n, Int.cast_mul, mul_div_cancel_right₀ _ hn]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DivisionRing α
k : ℤ
hn : ↑0 ≠ 0
⊢ False

Tactic:
simp at hn

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DivisionRing α
m n : ℤ
n_dvd : n ∣ m
hn : ↑n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
rcases n_dvd with ⟨k, rfl⟩

Result:
case intro
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
hn : ↑n ≠ 0
k : ℤ
⊢ ↑(n * k / n) = ↑(n * k) / ↑n
-- Mathlib/Order/BoundedOrder/Monotone.lean
theorem StrictMono.minimal_preimage_bot [LinearOrder α] [PartialOrder β] [OrderBot β] {f : α → β}
    (H : StrictMono f) {a} (h_bot : f a = ⊥) (x : α) : a ≤ x :=
  H.minimal_of_minimal_image
    (fun p => by
      rw [h_bot]
      exact bot_le)
    x

Proof state:
α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : OrderBot β
f : α → β
H : StrictMono f
a : α
h_bot : f a = ⊥
x : α
p : β
⊢ ⊥ ≤ p

Tactic:
exact bot_le

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : OrderBot β
f : α → β
H : StrictMono f
a : α
h_bot : f a = ⊥
x : α
p : β
⊢ f a ≤ p

Tactic:
rw [h_bot]

Result:
α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : OrderBot β
f : α → β
H : StrictMono f
a : α
h_bot : f a = ⊥
x : α
p : β
⊢ ⊥ ≤ p