harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Algebra/Operations.lean
theorem map_unop_one :
    map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (1 : Submodule R Aᵐᵒᵖ) = 1

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ map (↑(opLinearEquiv R).symm) 1 = 1

Tactic:
rw [← comap_equiv_eq_map_symm, comap_op_one]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem inf_symmDiff_distrib_right : a ∆ b ⊓ c = (a ⊓ c) ∆ (b ⊓ c)

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b ⊓ c = (a ⊓ c) ∆ (b ⊓ c)

Tactic:
simp_rw [inf_comm _ c, inf_symmDiff_distrib_left]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
@[reassoc]
lemma whiskerLeft_app_tensor_app {X' Y' : J} (f : X' ⟶ Y') (X : J) :
    F.obj X ◁ G.map f ≫ (α.app X ⊗ β.app Y') =
      (α.app X ⊗ β.app X') ≫ F'.obj X ◁ G'.map f

Proof state:
J : Type u_1
inst✝² : Category.{u_3, u_1} J
C : Type u_2
inst✝¹ : Category.{u_4, u_2} C
inst✝ : MonoidalCategory C
F G F' G' : J ⥤ C
α : F ⟶ F'
β : G ⟶ G'
X' Y' : J
f : X' ⟶ Y'
X : J
⊢ F.obj X ◁ G.map f ≫ (α.app X ⊗ β.app Y') = (α.app X ⊗ β.app X') ≫ F'.obj X ◁ G'.map f

Tactic:
simpa using tensor_naturality α β (𝟙 X) f

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive two_nsmul_inf_eq_add_sub_abs_sub]
lemma inf_sq_eq_mul_div_mabs_div (a b : α) : (a ⊓ b) ^ 2 = a * b / |b / a|ₘ

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) ^ 2 = a * b / mabs (b / a)

Tactic:
rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev,
  inv_inv, mul_assoc, mul_inv_cancel_comm_assoc, ← pow_two]

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem PredOrder.nhdsLE [PredOrder α] : 𝓝[≤] b = pure b

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
b : α
inst✝ : PredOrder α
⊢ 𝓝[≤] b = pure b

Tactic:
rw [← Iio_insert, nhdsWithin_insert, PredOrder.nhdsLT, sup_bot_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem add_left_eq_self  {a b : Nat} : a + b = b ↔ a = 0

Proof state:
a b : Nat
⊢ a + b = b ↔ a = 0

Tactic:
omega

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffDist_empty' : hausdorffDist ∅ s = 0

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ hausdorffDist ∅ s = 0

Tactic:
simp [hausdorffDist_comm]

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma ext₀ {F G : ComposableArrows C 0} (h : F.obj' 0 = G.obj 0) : F = G :=
  ext (fun i => match i with
    | ⟨0, _⟩ => h) (fun i hi => by simp at hi)

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : ComposableArrows C 0
h : F.obj' 0 ⋯ = G.obj 0
i : ℕ
hi : i < 0
⊢ F.map' i (i + 1) ⋯ hi = eqToHom ⋯ ≫ G.map' i (i + 1) ⋯ hi ≫ eqToHom ⋯

Tactic:
simp at hi

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem smul_vec3 {R : Type*} [SMul R α] (x : R) (a₀ a₁ a₂ : α) :
    x • ![a₀, a₁, a₂] = ![x • a₀, x • a₁, x • a₂]

Proof state:
α : Type u
R : Type u_1
inst✝ : SMul R α
x : R
a₀ a₁ a₂ : α
⊢ x • ![a₀, a₁, a₂] = ![x • a₀, x • a₁, x • a₂]

Tactic:
rw [smul_cons, smul_cons, smul_cons, smul_empty]

Result:
no goals
-- Mathlib/GroupTheory/HNNExtension.lean
theorem prod_empty : (empty : NormalWord d).prod φ = 1

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
⊢ ReducedWord.prod φ empty.toReducedWord = 1

Tactic:
simp [ReducedWord.prod]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_le_logb_of_le (h : 0 < x) (hxy : x ≤ y) : logb b x ≤ logb b y :=
  (logb_le_logb hb h (by linarith)).mpr hxy

Proof state:
b x y : ℝ
hb : 1 < b
h : 0 < x
hxy : x ≤ y
⊢ 0 < y

Tactic:
linarith

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma Affine.CoordinateRing.mk_ψ₂_sq : mk W W.ψ₂ ^ 2 = mk W (C W.Ψ₂Sq)

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (mk W) W.ψ₂ ^ 2 = (mk W) (C W.Ψ₂Sq)

Tactic:
rw [C_Ψ₂Sq, map_sub, map_mul, AdjoinRoot.mk_self, mul_zero, sub_zero, map_pow]

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem trans_transEquiv (e : PartialEquiv α β) (e' : PartialEquiv β γ) (f'' : γ ≃ δ) :
    (e.trans e').transEquiv f'' = e.trans (e'.transEquiv f'')

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
f'' : γ ≃ δ
⊢ (e.trans e').transEquiv f'' = e.trans (e'.transEquiv f'')

Tactic:
simp only [transEquiv_eq_trans, trans_assoc, Equiv.trans_toPartialEquiv]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Field.lean
theorem degree_le_of_ne_zero {p : A[X]} (pnz : p ≠ 0) (hp : Polynomial.aeval x p = 0) :
    degree (minpoly A x) ≤ degree p :=
  calc
    degree (minpoly A x) ≤ degree (p * C (leadingCoeff p)⁻¹) :=
      min A x (monic_mul_leadingCoeff_inv pnz) (by simp [hp])
    _ = degree p := degree_mul_leadingCoeff_inv p pnz

Proof state:
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pnz : p ≠ 0
hp : (Polynomial.aeval x) p = 0
⊢ (Polynomial.aeval x) (p * C p.leadingCoeff⁻¹) = 0

Tactic:
simp [hp]

Result:
no goals
-- Mathlib/Data/Fintype/BigOperators.lean
theorem prod_eq_mul {f : α → M} (a b : α) (h₁ : a ≠ b) (h₂ : ∀ x, x ≠ a ∧ x ≠ b → f x = 1) :
    ∏ x, f x = f a * f b

Proof state:
α : Type u_1
M : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ ∏ x : α, f x = f a * f b

Tactic:
apply Finset.prod_eq_mul a b h₁ fun x _ hx => h₂ x hx <;>
  exact fun hc => (hc (Finset.mem_univ _)).elim

Result:
no goals
-- Mathlib/RingTheory/DividedPowers/Basic.lean
theorem dpow_smul_right {n : ℕ} (ha : a ∈ I) :
    hI.dpow n (a • b) = hI.dpow n a • b ^ n

Proof state:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
⊢ hI.dpow n (a • b) = hI.dpow n a • b ^ n

Tactic:
rw [smul_eq_mul, hI.dpow_mul_right ha, smul_eq_mul]

Result:
no goals
-- Mathlib/SetTheory/Game/Ordinal.lean
theorem one_toPGame_moveLeft (x) : (toPGame 1).moveLeft x = toPGame 0

Proof state:
x : (toPGame 1).LeftMoves
⊢ (toPGame 1).moveLeft x = toPGame 0

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finsupp.lean
theorem mk_finsupp_nat (α : Type u) [Nonempty α] : #(α →₀ ℕ) = max #α ℵ₀

Proof state:
α : Type u
inst✝ : Nonempty α
⊢ #(α →₀ ℕ) = #α ⊔ ℵ₀

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem isGE_iff_eq_gt_or_eq_eq {o : Ordering} : o.isGE ↔ o = .gt ∨ o = .eq

Proof state:
o : Ordering
⊢ o.isGE = true ↔ o = gt ∨ o = eq

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_one : ⌈(1 : α)⌉ = 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
⊢ ⌈1⌉ = 1

Tactic:
rw [← cast_one, ceil_intCast]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_ne_empty_iff {xs : Array (Array α)} : xs.flatten ≠ #[] ↔ ∃ x, x ∈ xs ∧ x ≠ #[]

Proof state:
α : Type u_1
xs : Array (Array α)
⊢ xs.flatten ≠ #[] ↔ ∃ x, x ∈ xs ∧ x ≠ #[]

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
theorem mul_inv_cancel_right (a b : G) : a * b * b⁻¹ = a

Proof state:
G : Type u_1
inst✝ : Group G
a b : G
⊢ a * b * b⁻¹ = a

Tactic:
rw [mul_assoc, mul_inv_cancel, mul_one]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem iterate_derivative_natCast_mul {n k : ℕ} {f : R[X]} :
    derivative^[k] ((n : R[X]) * f) = n * derivative^[k] f

Proof state:
R : Type u
inst✝ : Semiring R
n k : ℕ
f : R[X]
⊢ (⇑derivative)^[k] (↑n * f) = ↑n * (⇑derivative)^[k] f

Tactic:
induction' k with k ih generalizing f <;> simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean
lemma epi_f₂₄ [Epi sq.f₁₃] : Epi sq.f₂₄ :=
  (MorphismProperty.epimorphisms C).of_isPushout h (by assumption)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPushout
inst✝ : Epi sq.f₁₃
⊢ MorphismProperty.epimorphisms C sq.f₁₃

Tactic:
assumption

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem isConnected_preimage {s : Set Y} (h : X ≃ₜ Y) :
    IsConnected (h ⁻¹' s) ↔ IsConnected s

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsConnected (⇑h ⁻¹' s) ↔ IsConnected s

Tactic:
rw [← image_symm, isConnected_image]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Classes/Order.lean
theorem cmp_congr_right (yz : cmp y z = .eq) : cmp x y = cmp x z

Proof state:
cmp✝ : ?m.4441 → ?m.4441 → Ordering
inst✝¹ : TransCmp cmp✝
x✝ : Sort ?u.4439
cmp : x✝ → x✝ → Ordering
inst✝ : TransCmp cmp
y z x : x✝
yz : cmp y z = Ordering.eq
⊢ cmp x y = cmp x z

Tactic:
rw [← Ordering.swap_inj, symm, symm, cmp_congr_left yz]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem add_le_add_left {a b : Int} (h : a ≤ b) (c : Int) : c + a ≤ c + b :=
  let ⟨n, hn⟩ := le.dest h; le.intro n <| by rw [Int.add_assoc, hn]

Proof state:
a b : Int
h : a ≤ b
c : Int
n : Nat
hn : a + ↑n = b
⊢ c + a + ↑n = c + b

Tactic:
rw [Int.add_assoc, hn]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem C_mul_X_pow_eq_monomial {s : σ} {a : R} {n : ℕ} :
    C a * X s ^ n = monomial (Finsupp.single s n) a

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
a : R
n : ℕ
⊢ C a * X s ^ n = (monomial (Finsupp.single s n)) a

Tactic:
rw [← zero_add (Finsupp.single s n), monomial_add_single, C_apply]

Result:
no goals
-- Mathlib/Logic/Equiv/Fin.lean
theorem finAddFlip_apply_natAdd (k : Fin n) (m : ℕ) :
    finAddFlip (Fin.natAdd m k) = Fin.castAdd m k

Proof state:
n : ℕ
k : Fin n
m : ℕ
⊢ finAddFlip (Fin.natAdd m k) = Fin.castAdd m k

Tactic:
simp [finAddFlip]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem all_flatten {l : List (List α)} : l.flatten.all f = l.all (all · f)

Proof state:
α : Type u_1
f : α → Bool
l : List (List α)
⊢ l.flatten.all f = l.all fun x => x.all f

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/Data/Nat/Prime/Basic.lean
theorem Prime.even_iff {p : ℕ} (hp : Prime p) : Even p ↔ p = 2

Proof state:
p : ℕ
hp : Prime p
⊢ Even p ↔ p = 2

Tactic:
rw [even_iff_two_dvd, prime_dvd_prime_iff_eq prime_two hp, eq_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Galois/GaloisObjects.lean
@[simp]
lemma comp_autMap_apply (F : C ⥤ FintypeCat.{w}) {A B : C} [IsConnected A] [IsGalois B]
    (f : A ⟶ B) (σ : Aut A) (a : F.obj A) :
    F.map (autMap f σ).hom (F.map f a) = F.map f (F.map σ.hom a)

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
A B : C
inst✝¹ : IsConnected A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut A
a : (F.obj A).carrier
⊢ F.map (autMap f σ).hom (F.map f a) = F.map f (F.map σ.hom a)

Tactic:
simpa [-comp_autMap] using congrFun (F.congr_map (comp_autMap f σ)) a

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsPath.of_cons {u v w : V} {h : G.Adj u v} {p : G.Walk v w} :
    (cons h p).IsPath → p.IsPath

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).IsPath → p.IsPath

Tactic:
simp [isPath_def]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem algebraicIndependent_empty_iff :
    AlgebraicIndependent R ((↑) : (∅ : Set A) → A) ↔ Injective (algebraMap R A)

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ AlgebraicIndependent R Subtype.val ↔ Injective ⇑(algebraMap R A)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.swap_right_iff [NoZeroSMulDivisors R V] {x y z : P} (h : Wbtw R x y z) :
    Wbtw R x z y ↔ y = z

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y z : P
h : Wbtw R x y z
⊢ Wbtw R x z y ↔ y = z

Tactic:
rw [← wbtw_swap_right_iff R x, and_iff_right h]

Result:
no goals
-- Mathlib/ModelTheory/ElementarySubstructures.lean
theorem theory_model_iff (S : L.ElementarySubstructure M) (T : L.Theory) : S ⊨ T ↔ M ⊨ T

Proof state:
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.ElementarySubstructure M
T : L.Theory
⊢ ↥S ⊨ T ↔ M ⊨ T

Tactic:
simp only [Theory.model_iff, realize_sentence]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem self (hp : 1 < p) : padicValInt p p = 1

Proof state:
p : ℕ
hp : 1 < p
⊢ padicValInt p ↑p = 1

Tactic:
simp [padicValNat.self hp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem?_setWidth (m : Nat) (x : BitVec n) (i : Nat) :
    (x.setWidth m)[i]? = if i < m then some (x.getLsbD i) else none

Proof state:
n m : Nat
x : BitVec n
i : Nat
⊢ (setWidth m x)[i]? = if i < m then some (x.getLsbD i) else none

Tactic:
simp [getElem?_eq, getElem_setWidth]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Basic.lean
theorem image_ι_comp_eq_zero {R : C} {g : Q ⟶ R} (h : f ≫ g = 0) : Abelian.image.ι f ≫ g = 0 :=
  zero_of_epi_comp (Abelian.factorThruImage f) <| by simp [h]

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
R : C
g : Q ⟶ R
h : f ≫ g = 0
⊢ Abelian.factorThruImage f ≫ image.ι f ≫ g = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem lintegral_prod_mul {f : α → ℝ≥0∞} {g : β → ℝ≥0∞} (hf : AEMeasurable f μ)
    (hg : AEMeasurable g ν) : ∫⁻ z, f z.1 * g z.2 ∂μ.prod ν = (∫⁻ x, f x ∂μ) * ∫⁻ y, g y ∂ν

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ ∫⁻ (z : α × β), f z.1 * g z.2 ∂μ.prod ν = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν

Tactic:
simp [lintegral_prod _ (hf.fst.mul hg.snd), lintegral_lintegral_mul hf hg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isInfix_map_iff {β} {f : α → β} {l₁ : List α} {l₂ : List β} :
    l₂ <:+: l₁.map f ↔ ∃ l, l <:+: l₁ ∧ l₂ = l.map f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l₁ : List α
l₂ : List β
⊢ l₂ <:+: map f l₁ ↔ ∃ l, l <:+: l₁ ∧ l₂ = map f l

Tactic:
rw [← filterMap_eq_map, isInfix_filterMap_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
theorem homEquiv_naturality_right_square_iff (f : X' ⟶ X) (g : X ⟶ G.obj Y')
    (h : X' ⟶ G.obj Y) (k : Y ⟶ Y') :
    (F.map f ≫ (adj.homEquiv X Y').symm g = (adj.homEquiv X' Y).symm h ≫ k) ↔
      (f ≫ g = h ≫ G.map k) :=
  ⟨fun w ↦ by simpa only [Equiv.apply_symm_apply]
      using homEquiv_naturality_left_square adj _ _ _ _ w,
    homEquiv_naturality_right_square adj f g h k⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : X ⟶ G.obj Y'
h : X' ⟶ G.obj Y
k : Y ⟶ Y'
w : F.map f ≫ (adj.homEquiv X Y').symm g = (adj.homEquiv X' Y).symm h ≫ k
⊢ f ≫ g = h ≫ G.map k

Tactic:
simpa only [Equiv.apply_symm_apply]
using homEquiv_naturality_left_square adj _ _ _ _ w

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem nrComplexPlaces_eq_zero_of_finrank_eq_one (h : finrank ℚ K = 1) :
    nrComplexPlaces K = 0

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
h : finrank ℚ K = 1
⊢ nrComplexPlaces K = 0

Tactic:
linarith [card_add_two_mul_card_eq_rank K]

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem frontier_Ici' {a : α} (ha : (Iio a).Nonempty) : frontier (Ici a) = {a}

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
ha : (Iio a).Nonempty
⊢ frontier (Ici a) = {a}

Tactic:
simp [frontier, ha]

Result:
no goals
-- Mathlib/Probability/Independence/Basic.lean
theorem iIndepSet_iff_meas_biInter {f : ι → Set Ω} (hf : ∀ i, MeasurableSet (f i)) :
    iIndepSet f μ ↔ ∀ s, μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)

Proof state:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : ι → Set Ω
hf : ∀ (i : ι), MeasurableSet (f i)
⊢ iIndepSet f μ ↔ ∀ (s : Finset ι), μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)

Tactic:
simp_rw [iIndepSet, Kernel.iIndepSet_iff_meas_biInter hf, ae_dirac_eq, Filter.eventually_pure,
  Kernel.const_apply]

Result:
no goals
-- Mathlib/Data/Multiset/Count.lean
theorem le_iff_count {s t : Multiset α} : s ≤ t ↔ ∀ a, count a s ≤ count a t :=
  Quotient.inductionOn₂ s t fun _ _ ↦ by simp [subperm_iff_count]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
x✝¹ x✝ : List α
⊢ ⟦x✝¹⟧ ≤ ⟦x✝⟧ ↔ ∀ (a : α), count a ⟦x✝¹⟧ ≤ count a ⟦x✝⟧

Tactic:
simp [subperm_iff_count]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Category.lean
theorem exchange {I J K : D ⥤ E} (α : F ⟶ G) (β : G ⟶ H) (γ : I ⟶ J) (δ : J ⟶ K) :
    (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ β ◫ δ

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G H : C ⥤ D
I J K : D ⥤ E
α : F ⟶ G
β : G ⟶ H
γ : I ⟶ J
δ : J ⟶ K
⊢ (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ β ◫ δ

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive two_zsmul] lemma zpow_two (a : G) : a ^ (2 : ℤ) = a * a

Proof state:
G : Type u_1
inst✝ : DivInvMonoid G
a : G
⊢ a ^ 2 = a * a

Tactic:
rw [zpow_ofNat, pow_two]

Result:
no goals
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
@[simp]
lemma Spec.preimage_id {R : CommRingCat} : Spec.preimage (𝟙 (Spec R)) = 𝟙 R :=
  Spec.map_injective (by simp)

Proof state:
R : CommRingCat
⊢ map (preimage (𝟙 (Spec R))) = map (𝟙 R)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
@[simp] lemma Commute.smul_left_iff : Commute (g • a) b ↔ Commute a b

Proof state:
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
g : G
inst✝³ : Mul H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
a b : H
⊢ Commute (g • a) b ↔ Commute a b

Tactic:
rw [Commute.symm_iff, Commute.smul_right_iff, Commute.symm_iff]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma ofENat_eq_nat {m : ℕ∞} {n : ℕ} : (m : Cardinal) = n ↔ m = n

Proof state:
m : ℕ∞
n : ℕ
⊢ ↑m = ↑n ↔ m = ↑n

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tan_neg : tan (-x) = -tan x

Proof state:
x : ℂ
⊢ tan (-x) = -tan x

Tactic:
simp [tan, neg_div]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem arctan_neg (x : ℝ) : arctan (-x) = -arctan x

Proof state:
x : ℝ
⊢ arctan (-x) = -arctan x

Tactic:
simp [arctan_eq_arcsin, neg_div]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
lemma mono_homologyMap_of_mono_of_not_rel (φ : K ⟶ L) (j : ι)
    [K.HasHomology j] [L.HasHomology j] [Mono (φ.f j)] (hj : ∀ i, ¬ c.Rel i j) :
    Mono (homologyMap φ j) :=
  ((MorphismProperty.monomorphisms C).arrow_mk_iso_iff
    (Arrow.isoMk (K.isoHomologyπ _ j rfl (shape _ _ _ (by tauto)))
      (L.isoHomologyπ _ j rfl (shape _ _ _ (by tauto))))).1
      (MorphismProperty.monomorphisms.infer_property (cyclesMap φ j))

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex C c
φ : K ⟶ L
j : ι
inst✝² : K.HasHomology j
inst✝¹ : L.HasHomology j
inst✝ : Mono (φ.f j)
hj : ∀ (i : ι), ¬c.Rel i j
⊢ ¬c.Rel (c.prev j) j

Tactic:
tauto

Result:
no goals
-- Mathlib/RingTheory/Localization/FractionRing.lean
theorem lift_mk' (hg : Injective g) (x) (y : nonZeroDivisors A) :
    lift hg (mk' K x y) = g x / g y

Proof state:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
hg : Injective ⇑g
x : A
y : ↥(nonZeroDivisors A)
⊢ (lift hg) (mk' K x y) = g x / g ↑y

Tactic:
simp only [mk'_eq_div, map_div₀, lift_algebraMap]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem diam_Ioo {a b : ℝ} (h : a ≤ b) : Metric.diam (Ioo a b) = b - a

Proof state:
a b : ℝ
h : a ≤ b
⊢ Metric.diam (Ioo a b) = b - a

Tactic:
simp [Metric.diam, ENNReal.toReal_ofReal (sub_nonneg.2 h)]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem subtype_coe_map_comap (s : Set α) (f : Filter α) :
    map ((↑) : s → α) (comap ((↑) : s → α) f) = f ⊓ 𝓟 s

Proof state:
α : Type u_1
s : Set α
f : Filter α
⊢ map Subtype.val (comap Subtype.val f) = f ⊓ 𝓟 s

Tactic:
rw [map_comap, Subtype.range_coe]

Result:
no goals
-- Mathlib/FieldTheory/AbelRuffini.lean
theorem gal_X_sub_C_isSolvable (x : F) : IsSolvable (X - C x).Gal

Proof state:
F : Type u_1
inst✝ : Field F
x : F
⊢ IsSolvable (X - C x).Gal

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem terminatedAt_iff_partDen_none : g.TerminatedAt n ↔ g.partDens.get? n = none

Proof state:
α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.TerminatedAt n ↔ g.partDens.get? n = none

Tactic:
rw [terminatedAt_iff_s_none, partDen_none_iff_s_none]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem reverse_inj {xs ys : List α} : xs.reverse = ys.reverse ↔ xs = ys

Proof state:
α : Type u_1
xs ys : List α
⊢ xs.reverse = ys.reverse ↔ xs = ys

Tactic:
simp [reverse_eq_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem compMeasurable_toGerm [MeasurableSpace β] [BorelSpace β] [PseudoMetrizableSpace β]
    [PseudoMetrizableSpace γ] [SecondCountableTopology γ] [MeasurableSpace γ]
    [OpensMeasurableSpace γ] (g : β → γ) (hg : Measurable g) (f : α →ₘ[μ] β) :
    (compMeasurable g hg f).toGerm = f.toGerm.map g :=
  induction_on f fun f _ => by simp

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁹ : MeasurableSpace α
μ : Measure α
inst✝⁸ : TopologicalSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace β
inst✝⁵ : BorelSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : PseudoMetrizableSpace γ
inst✝² : SecondCountableTopology γ
inst✝¹ : MeasurableSpace γ
inst✝ : OpensMeasurableSpace γ
g : β → γ
hg : Measurable g
f✝ : α →ₘ[μ] β
f : α → β
x✝ : AEStronglyMeasurable f μ
⊢ (compMeasurable g hg (mk f x✝)).toGerm = Germ.map g (mk f x✝).toGerm

Tactic:
simp

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem not_isPredLimit_iff : ¬ IsPredLimit a ↔ IsMax a ∨ ¬ IsPredPrelimit a

Proof state:
α : Type u_1
a : α
inst✝ : Preorder α
⊢ ¬IsPredLimit a ↔ IsMax a ∨ ¬IsPredPrelimit a

Tactic:
rw [IsPredLimit, not_and_or, not_not]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
theorem Bool.bne_to_beq (a b : Bool) : (a != b) = (!(a == b))

Proof state:
a b : Bool
⊢ (a != b) = !a == b

Tactic:
simp [bne]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
theorem mul_div_cancel_right (a b : G) : a * b / b = a

Proof state:
G : Type u_1
inst✝ : Group G
a b : G
⊢ a * b / b = a

Tactic:
rw [div_eq_mul_inv, mul_inv_cancel_right a b]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Cast.lean
@[simp, norm_cast] lemma cast_le : (m : R) ≤ n ↔ m ≤ n

Proof state:
R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
m n : ℤ
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
rw [← sub_nonneg, ← cast_sub, cast_nonneg, sub_nonneg]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem leadingCoeff_C_mul_X_pow (a : R) (n : ℕ) : leadingCoeff (C a * X ^ n) = a

Proof state:
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (C a * X ^ n).leadingCoeff = a

Tactic:
rw [C_mul_X_pow_eq_monomial, leadingCoeff_monomial]

Result:
no goals