harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem ι_comp_lift (φ : NormedAddGroupHom V₁ V) (h : f.comp φ = g.comp φ) :
    (ι _ _).comp (lift φ h) = φ

Proof state:
V : Type u_1
W : Type u_2
V₁ : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : SeminormedAddCommGroup W
inst✝ : SeminormedAddCommGroup V₁
f g : NormedAddGroupHom V W
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
⊢ (ι f g).comp (lift φ h) = φ

Tactic:
ext

Result:
case H
V : Type u_1
W : Type u_2
V₁ : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : SeminormedAddCommGroup W
inst✝ : SeminormedAddCommGroup V₁
f g : NormedAddGroupHom V W
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
x✝ : V₁
⊢ ((ι f g).comp (lift φ h)) x✝ = φ x✝

Proof state:
case H
V : Type u_1
W : Type u_2
V₁ : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : SeminormedAddCommGroup W
inst✝ : SeminormedAddCommGroup V₁
f g : NormedAddGroupHom V W
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
x✝ : V₁
⊢ ((ι f g).comp (lift φ h)) x✝ = φ x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Order/ScottTopology.lean
@[simp] lemma dirSupClosed_compl : DirSupClosed sᶜ ↔ DirSupInacc s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ DirSupClosed sᶜ ↔ DirSupInacc s

Tactic:
rw [← dirSupInacc_compl, compl_compl]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem UniformEquicontinuous.closure' {A : Set Y} {u : Y → β → α}
    (hA : UniformEquicontinuous (u ∘ (↑) : A → β → α)) (hu : Continuous u) :
    UniformEquicontinuous (u ∘ (↑) : closure A → β → α)

Proof state:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
hA : UniformEquicontinuousOn (u ∘ Subtype.val) univ
hu : Continuous u
⊢ UniformEquicontinuousOn (u ∘ Subtype.val) univ

Tactic:
exact hA.closure' (Pi.continuous_restrict _ |>.comp hu)

Result:
no goals

Proof state:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
hA : UniformEquicontinuous (u ∘ Subtype.val)
hu : Continuous u
⊢ UniformEquicontinuous (u ∘ Subtype.val)

Tactic:
rw [← uniformEquicontinuousOn_univ] at hA ⊢

Result:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
hA : UniformEquicontinuousOn (u ∘ Subtype.val) univ
hu : Continuous u
⊢ UniformEquicontinuousOn (u ∘ Subtype.val) univ
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem enum_zero_le' {o : Ordinal} (h0 : 0 < o) (a : o.toType) :
    enum (α := o.toType) (· < ·) ⟨0, type_toType _ ▸ h0⟩ ≤ a

Proof state:
o : Ordinal.{u_1}
h0 : 0 < o
a : o.toType
⊢ ¬a < (enum fun x1 x2 => x1 < x2) ⟨0, ⋯⟩

Tactic:
apply enum_zero_le

Result:
no goals

Proof state:
o : Ordinal.{u_1}
h0 : 0 < o
a : o.toType
⊢ (enum fun x1 x2 => x1 < x2) ⟨0, ⋯⟩ ≤ a

Tactic:
rw [← not_lt]

Result:
o : Ordinal.{u_1}
h0 : 0 < o
a : o.toType
⊢ ¬a < (enum fun x1 x2 => x1 < x2) ⟨0, ⋯⟩
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem Bool.or_eq_of_eq_false_right {a b : Bool} (h : b = false) : (a || b) = a

Proof state:
a b : Bool
h : b = false
⊢ (a || b) = a

Tactic:
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem append_ne_nil_of_ne_nil_right (s : List α) : t ≠ [] → s ++ t ≠ []

Proof state:
α : Type u_1
t s : List α
⊢ t ≠ [] → s ++ t ≠ []

Tactic:
simp_all

Result:
no goals
-- Mathlib/Analysis/Polynomial/Basic.lean
theorem tendsto_atBot_iff_leadingCoeff_nonpos :
    Tendsto (fun x => eval x P) atTop atBot ↔ 0 < P.degree ∧ P.leadingCoeff ≤ 0

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ Tendsto (fun x => eval x P) atTop atBot ↔ 0 < P.degree ∧ P.leadingCoeff ≤ 0

Tactic:
simp only [← tendsto_neg_atTop_iff, ← eval_neg, tendsto_atTop_iff_leadingCoeff_nonneg,
  degree_neg, leadingCoeff_neg, neg_nonneg]

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropOn_univ : LiftPropOn P g univ ↔ LiftProp P g

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
⊢ LiftPropOn P g univ ↔ LiftProp P g

Tactic:
simp [LiftPropOn, LiftProp, LiftPropAt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/DecidableEq.lean
theorem isEqvAux_self (r : α → α → Bool) (hr : ∀ a, r a a) (a : Array α) (i : Nat) (h : i ≤ a.size) :
    Array.isEqvAux a a rfl r i h = true

Proof state:
case zero
α : Type u_1
r : α → α → Bool
hr : ∀ (a : α), r a a = true
a : Array α
h : 0 ≤ a.size
⊢ a.isEqvAux a ⋯ r 0 h = true

Tactic:
simp [Array.isEqvAux]

Result:
no goals

Proof state:
case succ
α : Type u_1
r : α → α → Bool
hr : ∀ (a : α), r a a = true
a : Array α
i : Nat
ih : ∀ (h : i ≤ a.size), a.isEqvAux a ⋯ r i h = true
h : i + 1 ≤ a.size
⊢ a.isEqvAux a ⋯ r (i + 1) h = true

Tactic:
simp_all only [isEqvAux, Bool.and_self]

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Bool
hr : ∀ (a : α), r a a = true
a : Array α
i : Nat
h : i ≤ a.size
⊢ a.isEqvAux a ⋯ r i h = true

Tactic:
induction i with
| zero => simp [Array.isEqvAux]
| succ i ih =>
  simp_all only [isEqvAux, Bool.and_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_alter_of_beq [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} (h : k == k') :
    k' ∈ m.alter k f ↔ (f (m.get? k)).isSome

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
h : (k == k') = true
⊢ k' ∈ m.alter k f ↔ (f (m.get? k)).isSome = true

Tactic:
rw [mem_alter, if_pos h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ofInt_toInt {x : BitVec w} : BitVec.ofInt w x.toInt = x

Proof state:
w : Nat
x : BitVec w
⊢ BitVec.ofInt w x.toInt = x

Tactic:
by_cases h : 2 * x.toNat < 2^w <;> ext <;> simp [getLsbD, h, BitVec.toInt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_zero : (0#w).msb = false

Proof state:
w : Nat
⊢ (0#w).msb = false

Tactic:
simp [BitVec.msb, getMsbD]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem erase_add (i : ι) (f₁ f₂ : Π₀ i, β i) : erase i (f₁ + f₂) = erase i f₁ + erase i f₂ :=
  ext fun _ => by simp [ite_zero_add]

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
f₁ f₂ : Π₀ (i : ι), β i
x✝ : ι
⊢ (erase i (f₁ + f₂)) x✝ = (erase i f₁ + erase i f₂) x✝

Tactic:
simp [ite_zero_add]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem abs_arg_le_pi_div_two_iff {z : ℂ} : |arg z| ≤ π / 2 ↔ 0 ≤ re z

Proof state:
z : ℂ
⊢ |z.arg| ≤ π / 2 ↔ 0 ≤ z.re

Tactic:
rw [abs_le, arg_le_pi_div_two_iff, neg_pi_div_two_le_arg_iff, ← or_and_left, ← not_le,
  and_not_self_iff, or_false]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Block.lean
lemma BlockTriangular.comp [Zero R] {M : Matrix m m (Matrix n n R)} (h : BlockTriangular M b) :
    BlockTriangular (M.comp m m n n R) fun i ↦ b i.1 :=
  fun i j lt ↦ by simp [h lt]

Proof state:
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
b : m → α
inst✝¹ : LT α
inst✝ : Zero R
M : Matrix m m (Matrix n n R)
h : M.BlockTriangular b
i j : m × n
lt : (fun i => b i.1) j < (fun i => b i.1) i
⊢ (Matrix.comp m m n n R) M i j = 0

Tactic:
simp [h lt]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem differentiableWithinAt_comp_add_left (a : E) :
    DifferentiableWithinAt 𝕜 (fun x ↦ f (a + x)) s x ↔
      DifferentiableWithinAt 𝕜 f (a +ᵥ s) (a + x)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
a : E
⊢ DifferentiableWithinAt 𝕜 (fun x => f (a + x)) s x ↔ DifferentiableWithinAt 𝕜 f (a +ᵥ s) (a + x)

Tactic:
simp [DifferentiableWithinAt, hasFDerivWithinAt_comp_add_left]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem le_trailingDegree_X_pow (n : ℕ) : (n : ℕ∞) ≤ trailingDegree (X ^ n : R[X])

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ ↑n ≤ (X ^ n).trailingDegree

Tactic:
simpa only [C_1, one_mul] using le_trailingDegree_C_mul_X_pow n (1 : R)

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem map_comp
    {M'' : Type*} [AddCommGroup M''] [Module R M''] [LieRingModule L M''] {g : M' →ₗ⁅R,L⁆ M''} :
    N.map (g.comp f) = (N.map f).map g :=
  SetLike.coe_injective <| by
    simp only [← Set.image_comp, coe_map, LinearMap.coe_comp, LieModuleHom.coe_comp]

Proof state:
R : Type u
L : Type v
M : Type w
M' : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N : LieSubmodule R L M
M'' : Type u_1
inst✝² : AddCommGroup M''
inst✝¹ : Module R M''
inst✝ : LieRingModule L M''
g : M' →ₗ⁅R,L⁆ M''
⊢ ↑(map (g.comp f) N) = ↑(map g (map f N))

Tactic:
simp only [← Set.image_comp, coe_map, LinearMap.coe_comp, LieModuleHom.coe_comp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem getRight?_swap (x : α ⊕ β) : x.swap.getRight? = x.getLeft?

Proof state:
α : Type u_1
β : Type u_2
x : α ⊕ β
⊢ x.swap.getRight? = x.getLeft?

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem a_is_soln (ha : F.eval a = 0) :
    F.eval a = 0 ∧
      ‖a - a‖ < ‖F.derivative.eval a‖ ∧
        ‖F.derivative.eval a‖ = ‖F.derivative.eval a‖ ∧
          ∀ z', F.eval z' = 0 → ‖z' - a‖ < ‖F.derivative.eval a‖ → z' = a :=
  ⟨ha, by simp [deriv_ne_zero hnorm], rfl, a_soln_is_unique ha⟩

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
ha : Polynomial.eval a F = 0
⊢ ‖a - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖

Tactic:
simp [deriv_ne_zero hnorm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ofBool_xor_ofBool : ofBool b ^^^ ofBool b' = ofBool (b ^^ b')

Proof state:
b b' : Bool
⊢ ofBool b ^^^ ofBool b' = ofBool (b ^^ b')

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

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
lemma map_normEDS (n : ℤ) : f (normEDS b c d n) = normEDS (f b) (f c) (f d) n

Proof state:
R : Type u
inst✝¹ : CommRing R
b c d : R
S : Type v
inst✝ : CommRing S
f : R →+* S
n : ℤ
⊢ f (normEDS b c d n) = normEDS (f b) (f c) (f d) n

Tactic:
rw [normEDS, map_mul, map_preNormEDS, map_pow, apply_ite f, map_one, normEDS]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem ball_div_one : ball 1 δ / s = thickening δ s⁻¹

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ ball 1 δ / s = thickening δ s⁻¹

Tactic:
simp [div_eq_mul_inv, ball_mul_one]

Result:
no goals
-- Mathlib/Analysis/Calculus/LocalExtr/Polynomial.lean
theorem card_rootSet_le_derivative {F : Type*} [CommRing F] [Algebra F ℝ] (p : F[X]) :
    Fintype.card (p.rootSet ℝ) ≤ Fintype.card (p.derivative.rootSet ℝ) + 1

Proof state:
F : Type u_1
inst✝¹ : CommRing F
inst✝ : Algebra F ℝ
p : F[X]
⊢ Fintype.card ↑(p.rootSet ℝ) ≤ Fintype.card ↑((derivative p).rootSet ℝ) + 1

Tactic:
simpa only [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe, derivative_map] using
  card_roots_toFinset_le_derivative (p.map (algebraMap F ℝ))

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma even_iff_exists_two_mul : Even a ↔ ∃ b, a = 2 * b

Proof state:
α : Type u_2
inst✝ : Semiring α
a : α
⊢ Even a ↔ ∃ b, a = 2 * b

Tactic:
simp [even_iff_exists_two_nsmul]

Result:
no goals
-- Mathlib/Logic/IsEmpty.lean
theorem nonempty_fun : Nonempty (α → β) ↔ IsEmpty α ∨ Nonempty β :=
  not_iff_not.mp <| by rw [not_or, not_nonempty_iff, not_nonempty_iff, isEmpty_fun, not_isEmpty_iff]

Proof state:
α : Sort u_1
β : Sort u_2
⊢ ¬Nonempty (α → β) ↔ ¬(IsEmpty α ∨ Nonempty β)

Tactic:
rw [not_or, not_nonempty_iff, not_nonempty_iff, isEmpty_fun, not_isEmpty_iff]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem ciInf_eq_of_forall_ge_of_forall_gt_exists_lt [Nonempty ι] {f : ι → α} (h₁ : ∀ i, b ≤ f i)
    (h₂ : ∀ w, b < w → ∃ i, f i < w) : ⨅ i : ι, f i = b

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
b : α
inst✝ : Nonempty ι
f : ι → α
h₁ : ∀ (i : ι), b ≤ f i
h₂ : ∀ (w : α), b < w → ∃ i, f i < w
⊢ ⨅ i, f i = b

Tactic:
exact ciSup_eq_of_forall_le_of_forall_lt_exists_gt (α := αᵒᵈ) (f := ‹_›) ‹_› ‹_›

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem mapEquiv_trans [CommSemiring S₁] [CommSemiring S₂] [CommSemiring S₃] (e : S₁ ≃+* S₂)
    (f : S₂ ≃+* S₃) : (mapEquiv σ e).trans (mapEquiv σ f) = mapEquiv σ (e.trans f) :=
  RingEquiv.ext fun p => by
    simp only [RingEquiv.coe_trans, comp_apply, mapEquiv_apply, RingEquiv.coe_ringHom_trans,
      map_map]

Proof state:
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
inst✝² : CommSemiring S₁
inst✝¹ : CommSemiring S₂
inst✝ : CommSemiring S₃
e : S₁ ≃+* S₂
f : S₂ ≃+* S₃
p : MvPolynomial σ S₁
⊢ ((mapEquiv σ e).trans (mapEquiv σ f)) p = (mapEquiv σ (e.trans f)) p

Tactic:
simp only [RingEquiv.coe_trans, comp_apply, mapEquiv_apply, RingEquiv.coe_ringHom_trans,
  map_map]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem cos_coe_pi : cos (π : Angle) = -1

Proof state:
⊢ (↑π).cos = -1

Tactic:
rw [cos_coe, Real.cos_pi]

Result:
no goals
-- Mathlib/Order/SuccPred/Tree.lean
lemma RootedTree.subtreeOf_mem_subtrees [DecidableEq t] {v : t} (hr : v ≠ ⊥) :
    t.subtreeOf v ∈ t.subtrees

Proof state:
t : RootedTree
inst✝ : DecidableEq ↑t
v : ↑t
hr : v ≠ ⊥
⊢ t.subtreeOf v ∈ t.subtrees

Tactic:
simpa [RootedTree.subtrees, RootedTree.subtreeOf]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Expand.lean
theorem map_expand (f : R →+* S) (p : ℕ) (φ : MvPolynomial σ R) :
    map f (expand p φ) = expand p (map f φ)

Proof state:
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
p : ℕ
φ : MvPolynomial σ R
⊢ (map f) ((expand p) φ) = (expand p) ((map f) φ)

Tactic:
simp [expand, map_bind₁]

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem disjoint_iSup_iff {f : ι → α} : Disjoint a (⨆ i, f i) ↔ ∀ i, Disjoint a (f i)

Proof state:
α : Type u
ι : Sort w
inst✝ : Frame α
a : α
f : ι → α
⊢ Disjoint a (⨆ i, f i) ↔ ∀ (i : ι), Disjoint a (f i)

Tactic:
simpa only [disjoint_comm] using @iSup_disjoint_iff

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean
@[reassoc (attr := simp)]
lemma biprod_lift_snd_f (α : M ⟶ K) (β : M ⟶ L) (i : ι) :
    (biprod.lift α β).f i ≫ (biprod.snd : K ⊞ L ⟶ L).f i = β.f i

Proof state:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
M : HomologicalComplex C c
α : M ⟶ K
β : M ⟶ L
i : ι
⊢ (biprod.lift α β).f i ≫ biprod.snd.f i = β.f i

Tactic:
rw [← comp_f, biprod.lift_snd]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem div_lt_iff_lt_mul : a / c < b ↔ a < b * c

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a / c < b ↔ a < b * c

Tactic:
rw [← mul_lt_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean
protected lemma map_det (g : GL n R) : Matrix.GeneralLinearGroup.det (map f g) =
    Units.map f (Matrix.GeneralLinearGroup.det g)

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ det ((map f) g) = (Units.map ↑f) (det g)

Tactic:
ext

Result:
case a
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ ↑(det ((map f) g)) = ↑((Units.map ↑f) (det g))

Proof state:
case a
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ ↑(det ((map f) g)) = ↑((Units.map ↑f) (det g))

Tactic:
simp only [map, RingHom.mapMatrix_apply, Units.inv_eq_val_inv, Matrix.coe_units_inv,
  Matrix.GeneralLinearGroup.val_det_apply, Units.coe_map, MonoidHom.coe_coe]

Result:
case a
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ (↑f.mapMatrix ↑g).det = f (↑g).det

Proof state:
case a
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ (↑f.mapMatrix ↑g).det = f (↑g).det

Tactic:
exact Eq.symm (RingHom.map_det f g.1)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_biUnion_eq_iSup {s : ι → Set α} {t : Set ι} (ht : t.Countable)
    (hd : DirectedOn ((· ⊆ ·) on s) t) : μ (⋃ i ∈ t, s i) = ⨆ i ∈ t, μ (s i)

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
hd : DirectedOn ((fun x1 x2 => x1 ⊆ x2) on s) t
this : Countable ↑t
⊢ μ (⋃ i ∈ t, s i) = ⨆ i ∈ t, μ (s i)

Tactic:
rw [biUnion_eq_iUnion, hd.directed_val.measure_iUnion, ← iSup_subtype'']

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
hd : DirectedOn ((fun x1 x2 => x1 ⊆ x2) on s) t
⊢ μ (⋃ i ∈ t, s i) = ⨆ i ∈ t, μ (s i)

Tactic:
haveI := ht.to_subtype

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
hd : DirectedOn ((fun x1 x2 => x1 ⊆ x2) on s) t
this : Countable ↑t
⊢ μ (⋃ i ∈ t, s i) = ⨆ i ∈ t, μ (s i)
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem one_le_div' : 1 ≤ a / b ↔ b ≤ a

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ 1 ≤ a / b ↔ b ≤ a

Tactic:
rw [← mul_le_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem limit.π_comp_eqToHom (F : J ⥤ C) [HasLimit F] {j j' : J} (hj : j = j') :
    limit.π F j ≫ eqToHom (by subst hj; rfl) = limit.π F j'

Proof state:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasLimit F
j j' : J
hj : j = j'
⊢ F.obj j = F.obj j'

Tactic:
subst hj

Result:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasLimit F
j : J
⊢ F.obj j = F.obj j

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
j j' : J
hj : j = j'
⊢ π F j ≫ eqToHom ⋯ = π F j'

Tactic:
subst hj

Result:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
j : J
⊢ π F j ≫ eqToHom ⋯ = π F j

Proof state:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasLimit F
j : J
⊢ F.obj j = F.obj j

Tactic:
rfl

Result:
no goals

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
j : J
⊢ π F j ≫ eqToHom ⋯ = π F j

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean
lemma triangleRemovalBound_nonpos (hε : ε ≤ 0) : triangleRemovalBound ε ≤ 0

Proof state:
ε : ℝ
hε : ε ≤ 0
⊢ triangleRemovalBound ε ≤ 0

Tactic:
rw [triangleRemovalBound, ceil_eq_zero.2 (div_nonpos_of_nonneg_of_nonpos _ hε)] <;> simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Defs.lean
theorem mul_inv_cancel_right₀ (h : b ≠ 0) (a : G₀) : a * b * b⁻¹ = a :=
  calc
    a * b * b⁻¹ = a * (b * b⁻¹) := mul_assoc _ _ _
    _ = a

Proof state:
G₀ : Type u
inst✝ : GroupWithZero G₀
b : G₀
h : b ≠ 0
a : G₀
⊢ a * (b * b⁻¹) = a

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Combinatorics/Additive/CauchyDavenport.lean
@[to_additive]
private lemma wellFoundedOn_devosMulRel :
    {x : Finset α × Finset α | x.1.Nonempty ∧ x.2.Nonempty}.WellFoundedOn
      (DevosMulRel : Finset α × Finset α → Finset α × Finset α → Prop)

Proof state:
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
n : ℕ
⊢ ({x | x.1.Nonempty ∧ x.2.Nonempty} ∩ (fun x => #(x.1 * x.2)) ⁻¹' {n}).WellFoundedOn
    ((fun x1 x2 => x1 > x2) on fun x => #x.1 + #x.2)

Tactic:
exact wellFounded_lt.onFun.wellFoundedOn.mono' fun x hx y _ ↦ tsub_lt_tsub_left_of_le <|
  add_le_add ((card_le_card_mul_right hx.1.2).trans_eq hx.2) <|
    (card_le_card_mul_left hx.1.1).trans_eq hx.2

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
⊢ {x | x.1.Nonempty ∧ x.2.Nonempty}.WellFoundedOn DevosMulRel

Tactic:
refine wellFounded_lt.onFun.wellFoundedOn.prod_lex_of_wellFoundedOn_fiber fun n ↦
  Set.WellFoundedOn.prod_lex_of_wellFoundedOn_fiber ?_ fun n ↦
    wellFounded_lt.onFun.wellFoundedOn

Result:
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
n : ℕ
⊢ ({x | x.1.Nonempty ∧ x.2.Nonempty} ∩ (fun x => #(x.1 * x.2)) ⁻¹' {n}).WellFoundedOn
    ((fun x1 x2 => x1 > x2) on fun x => #x.1 + #x.2)
-- Mathlib/Computability/Halting.lean
theorem comp₁ {n} (f : ℕ →. ℕ) {g : List.Vector ℕ n → ℕ} (hf : @Partrec' 1 fun v => f v.head)
    (hg : @Partrec' n g) : @Partrec' n fun v => f (g v)

Proof state:
n : ℕ
f : ℕ →. ℕ
g : List.Vector ℕ n → ℕ
hf : Partrec' fun v => f v.head
hg : Partrec' ↑g
⊢ Partrec' fun v => f (g v)

Tactic:
simpa using hf.comp' (Partrec'.cons hg Partrec'.nil)

Result:
no goals
-- Mathlib/Data/List/FinRange.lean
theorem map_coe_finRange (n : ℕ) : ((finRange n) : List (Fin n)).map (Fin.val) = List.range n

Proof state:
n : ℕ
⊢ map Fin.val (finRange n) = range n

Tactic:
apply List.ext_getElem <;> simp

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem filter_eq_zero_iff : f.filter p = 0 ↔ ∀ x, p x → f x = 0

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
⊢ filter p f = 0 ↔ ∀ (x : α), p x → f x = 0

Tactic:
simp only [DFunLike.ext_iff, filter_eq_indicator, zero_apply, Set.indicator_apply_eq_zero,
  Set.mem_setOf_eq]

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Basic.lean
lemma ne_one_iff {χ : MulChar R R'} : χ ≠ 1 ↔ ∃ a : Rˣ, χ a ≠ 1

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
⊢ χ ≠ 1 ↔ ∃ a, χ ↑a ≠ 1

Tactic:
simp only [Ne, eq_one_iff, not_forall]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrixAlgEquiv_mul (f g : M₁ →ₗ[R] M₁) :
    LinearMap.toMatrixAlgEquiv v₁ (f * g) =
      LinearMap.toMatrixAlgEquiv v₁ f * LinearMap.toMatrixAlgEquiv v₁ g

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f g : M₁ →ₗ[R] M₁
⊢ (toMatrixAlgEquiv v₁) (f * g) = (toMatrixAlgEquiv v₁) f * (toMatrixAlgEquiv v₁) g

Tactic:
rw [LinearMap.mul_eq_comp, LinearMap.toMatrixAlgEquiv_comp v₁ f g]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem multipliable_iff_of_multipliable_div (hfg : Multipliable fun b ↦ f b / g b) :
    Multipliable f ↔ Multipliable g :=
  ⟨fun hf ↦ hf.trans_div <| by simpa only [inv_div] using hfg.inv, fun hg ↦ hg.trans_div hfg⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
hfg : Multipliable fun b => f b / g b
hf : Multipliable f
⊢ Multipliable fun b => g b / f b

Tactic:
simpa only [inv_div] using hfg.inv

Result:
no goals