harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftProp_inclusion {Q : (H → H) → Set H → H → Prop} (hG : LocalInvariantProp G G Q)
    (hQ : ∀ y, Q id univ y) {U V : Opens M} (hUV : U ≤ V) :
    LiftProp Q (Opens.inclusion hUV : U → V)

Proof state:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U V : Opens M
hUV : U ≤ V
x : ↥U
⊢ LiftPropAt Q (Opens.inclusion hUV) x

Tactic:
show LiftPropAt Q (id ∘ Opens.inclusion hUV) x

Result:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U V : Opens M
hUV : U ≤ V
x : ↥U
⊢ LiftPropAt Q (id ∘ Opens.inclusion hUV) x

Proof state:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U V : Opens M
hUV : U ≤ V
⊢ LiftProp Q (Opens.inclusion hUV)

Tactic:
intro x

Result:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U V : Opens M
hUV : U ≤ V
x : ↥U
⊢ LiftPropAt Q (Opens.inclusion hUV) x

Proof state:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U V : Opens M
hUV : U ≤ V
x : ↥U
⊢ LiftPropAt Q (id ∘ Opens.inclusion hUV) x

Tactic:
rw [← hG.liftPropAt_iff_comp_inclusion hUV]

Result:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U V : Opens M
hUV : U ≤ V
x : ↥U
⊢ LiftPropAt Q id (inclusion hUV x)

Proof state:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U V : Opens M
hUV : U ≤ V
x : ↥U
⊢ LiftPropAt Q id (inclusion hUV x)

Tactic:
apply hG.liftProp_id hQ

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Strong.lean
theorem whiskerRight_naturality_id (f : G.obj a ⟶ a') :
    (η.naturality (𝟙 a)).hom ▷ f ≫ (α_ _ _ _).hom ≫ η.app a ◁ G.mapId a ▷ f =
    F.mapId a ▷ η.app a ▷ f ≫ (λ_ (η.app a)).hom ▷ f ≫ (ρ_ (η.app a)).inv ▷ f ≫
    (α_ _ _ _).hom

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
η : StrongOplaxNatTrans F G
a : B
a' : C
f : G.obj a ⟶ a'
⊢ (η.naturality (𝟙 a)).hom ▷ f ≫ (α_ (η.app a) (G.map (𝟙 a)) f).hom ≫ η.app a ◁ G.mapId a ▷ f =
    F.mapId a ▷ η.app a ▷ f ≫ (λ_ (η.app a)).hom ▷ f ≫ (ρ_ (η.app a)).inv ▷ f ≫ (α_ (η.app a) (𝟙 (G.obj a)) f).hom

Tactic:
apply η.toOplax.whiskerRight_naturality_id

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
lemma shift_v' (a : ℤ) (p q : ℤ) (hpq : p + n = q) :
    (γ.shift a).v p q hpq = γ.v (p + a) (q + a) (by omega)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a p q : ℤ
hpq : p + n = q
⊢ (γ.shift a).v p q hpq = γ.v (p + a) (q + a) ⋯

Tactic:
simp only [shift_v γ a p q hpq _ _ rfl rfl, shiftFunctor_obj_X, shiftFunctorObjXIso,
  HomologicalComplex.XIsoOfEq_rfl, Iso.refl_hom, Iso.refl_inv, comp_id, id_comp]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a p q : ℤ
hpq : p + n = q
⊢ p + a + n = q + a

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftSequence.lean
lemma shiftIso_add' (n m mn : M) (hnm : m + n = mn) (a a' a'' : M)
    (ha' : n + a = a') (ha'' : m + a' = a'') :
    F.shiftIso mn a a'' (by rw [← hnm, ← ha'', ← ha', add_assoc]) =
      isoWhiskerRight (shiftFunctorAdd' C m n _ hnm) _ ≪≫ Functor.associator _ _ _ ≪≫
        isoWhiskerLeft _ (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''

Proof state:
C : Type u_1
A : Type u_2
inst✝⁴ : Category.{u_6, u_1} C
inst✝³ : Category.{u_5, u_2} A
F : C ⥤ A
M : Type u_3
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ F.shiftIso mn a a'' ⋯ =
    isoWhiskerRight (shiftFunctorAdd' C m n mn hnm) (F.shift a) ≪≫
      (shiftFunctor C m).associator (shiftFunctor C n) (F.shift a) ≪≫
        isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''

Tactic:
subst hnm

Result:
C : Type u_1
A : Type u_2
inst✝⁴ : Category.{u_6, u_1} C
inst✝³ : Category.{u_5, u_2} A
F : C ⥤ A
M : Type u_3
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ F.shiftIso (m + n) a a'' ⋯ =
    isoWhiskerRight (shiftFunctorAdd' C m n (m + n) ⋯) (F.shift a) ≪≫
      (shiftFunctor C m).associator (shiftFunctor C n) (F.shift a) ≪≫
        isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''

Proof state:
C : Type u_1
A : Type u_2
inst✝⁴ : Category.{u_6, u_1} C
inst✝³ : Category.{u_5, u_2} A
F : C ⥤ A
M : Type u_3
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ F.shiftIso (m + n) a a'' ⋯ =
    isoWhiskerRight (shiftFunctorAdd' C m n (m + n) ⋯) (F.shift a) ≪≫
      (shiftFunctor C m).associator (shiftFunctor C n) (F.shift a) ≪≫
        isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''

Tactic:
rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftIso_add]

Result:
no goals

Proof state:
C : Type u_1
A : Type u_2
inst✝⁶ : Category.{?u.53004, u_1} C
inst✝⁵ : Category.{?u.53008, u_2} A
F : C ⥤ A
M : Type u_3
inst✝⁴ : AddMonoid M
inst✝³ : HasShift C M
G : Type u_4
inst✝² : AddGroup G
inst✝¹ : HasShift C G
inst✝ : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ mn + a = a''

Tactic:
rw [← hnm, ← ha'', ← ha', add_assoc]

Result:
no goals
-- Mathlib/Probability/Distributions/Gaussian.lean
lemma gaussianPDFReal_mul {μ : ℝ} {v : ℝ≥0} {c : ℝ} (hc : c ≠ 0) (x : ℝ) :
    gaussianPDFReal μ v (c * x)
      = |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (⟨(c^2)⁻¹, inv_nonneg.mpr (sq_nonneg _)⟩ * v) x

Proof state:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ gaussianPDFReal μ v (c * x) = |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (⟨(c ^ 2)⁻¹, ⋯⟩ * v) x

Tactic:
conv_lhs => rw [← inv_inv c, gaussianPDFReal_inv_mul (inv_ne_zero hc)]

Result:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (⟨c⁻¹ ^ 2, ⋯⟩ * v) x = |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (⟨(c ^ 2)⁻¹, ⋯⟩ * v) x

Proof state:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (⟨c⁻¹ ^ 2, ⋯⟩ * v) x = |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (⟨(c ^ 2)⁻¹, ⋯⟩ * v) x

Tactic:
simp

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma ge_of_forall_gt_iff_ge : (∀ a : α, a < x → a ≤ y) ↔ x ≤ y

Proof state:
α : Type u_1
inst✝² : LinearOrder α
x y : WithTop α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
⊢ (∀ (a : α), ↑a < x → ↑a ≤ y) ↔ x ≤ y

Tactic:
cases x <;> cases y <;> simp [exists_gt, forall_lt_imp_le_iff_le_of_dense]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_of_isEmpty [LawfulBEq α] (h : m.1.WF) {a : α} {fallback : β a} :
    m.1.isEmpty = true → m.getD a fallback = fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
a : α
fallback : β a
⊢ (toListModel m.val.buckets).isEmpty = true → getValueCastD a (toListModel m.val.buckets) fallback = fallback

Tactic:
empty

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
a : α
fallback : β a
⊢ m.val.isEmpty = true → m.getD a fallback = fallback

Tactic:
simp_to_model

Result:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
a : α
fallback : β a
⊢ (toListModel m.val.buckets).isEmpty = true → getValueCastD a (toListModel m.val.buckets) fallback = fallback
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem eq_of_mem_uIcc_of_mem_uIcc : a ∈ [[b, c]] → b ∈ [[a, c]] → a = b

Proof state:
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ a ∈ [[b, c]] → b ∈ [[a, c]] → a = b

Tactic:
simp_rw [mem_uIcc]

Result:
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ b ⊓ c ≤ a ∧ a ≤ b ⊔ c → a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a = b

Proof state:
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ b ⊓ c ≤ a ∧ a ≤ b ⊔ c → a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a = b

Tactic:
exact Set.eq_of_mem_uIcc_of_mem_uIcc

Result:
no goals
-- Mathlib/Topology/Maps/Proper/Basic.lean
/-- Any product of proper maps is proper. -/
lemma IsProperMap.pi_map {X Y : ι → Type*} [∀ i, TopologicalSpace (X i)]
    [∀ i, TopologicalSpace (Y i)] {f : (i : ι) → X i → Y i} (h : ∀ i, IsProperMap (f i)) :
    IsProperMap (fun (x : ∀ i, X i) i ↦ f i (x i))

Proof state:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h : ∀ (i : ι), IsProperMap (f i)
⊢ IsProperMap fun x i => f i (x i)

Tactic:
simp_rw [isProperMap_iff_ultrafilter] at h ⊢

Result:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ (Continuous fun x i => f i (x i)) ∧
    ∀ ⦃𝒰 : Ultrafilter ((i : ι) → X i)⦄ ⦃y : (i : ι) → Y i⦄,
      Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y) → ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem tmul_pow (a : A) (b : B) (k : ℕ) : a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[R] (b ^ k)

Proof state:
case succ
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : A
b : B
k : ℕ
ih : a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[R] (b ^ k)
⊢ a ⊗ₜ[R] b ^ (k + 1) = (a ^ (k + 1)) ⊗ₜ[R] (b ^ (k + 1))

Tactic:
simp [pow_succ, ih]

Result:
no goals

Proof state:
case zero
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : A
b : B
⊢ a ⊗ₜ[R] b ^ 0 = (a ^ 0) ⊗ₜ[R] (b ^ 0)

Tactic:
simp [one_def]

Result:
no goals

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : A
b : B
k : ℕ
⊢ a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[R] (b ^ k)

Tactic:
induction' k with k ih

Result:
case zero
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : A
b : B
⊢ a ⊗ₜ[R] b ^ 0 = (a ^ 0) ⊗ₜ[R] (b ^ 0)

case succ
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : A
b : B
k : ℕ
ih : a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[R] (b ^ k)
⊢ a ⊗ₜ[R] b ^ (k + 1) = (a ^ (k + 1)) ⊗ₜ[R] (b ^ (k + 1))
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_le_div_iff : 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b

Proof state:
case inl
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : b < 0
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b

Tactic:
simp [hb, hb.not_lt, one_le_div_of_neg]

Result:
no goals

Proof state:
case inr.inl
α : Type u_2
inst✝ : LinearOrderedField α
a : α
⊢ 1 ≤ a / 0 ↔ 0 < 0 ∧ 0 ≤ a ∨ 0 < 0 ∧ a ≤ 0

Tactic:
simp [lt_irrefl, zero_lt_one.not_le, zero_lt_one]

Result:
no goals

Proof state:
case inr.inr
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : 0 < b
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b

Tactic:
simp [hb, hb.not_lt, one_le_div]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b

Tactic:
rcases lt_trichotomy b 0 with (hb | rfl | hb)

Result:
case inl
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : b < 0
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b

case inr.inl
α : Type u_2
inst✝ : LinearOrderedField α
a : α
⊢ 1 ≤ a / 0 ↔ 0 < 0 ∧ 0 ≤ a ∨ 0 < 0 ∧ a ≤ 0

case inr.inr
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : 0 < b
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
-- Mathlib/Data/NNRat/Floor.lean
theorem ceil_cast (x : ℚ≥0) : ⌈(x : K)⌉₊ = ⌈x⌉₊

Proof state:
case inl
K : Type u_1
inst✝¹ : LinearOrderedSemifield K
inst✝ : FloorSemiring K
⊢ ⌈↑0⌉₊ = ⌈0⌉₊

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedSemifield K
inst✝ : FloorSemiring K
x : ℚ≥0
⊢ ⌈↑x⌉₊ = ⌈x⌉₊

Tactic:
obtain rfl | hx := eq_or_ne x 0

Result:
case inl
K : Type u_1
inst✝¹ : LinearOrderedSemifield K
inst✝ : FloorSemiring K
⊢ ⌈↑0⌉₊ = ⌈0⌉₊

case inr
K : Type u_1
inst✝¹ : LinearOrderedSemifield K
inst✝ : FloorSemiring K
x : ℚ≥0
hx : x ≠ 0
⊢ ⌈↑x⌉₊ = ⌈x⌉₊

Proof state:
case inr
K : Type u_1
inst✝¹ : LinearOrderedSemifield K
inst✝ : FloorSemiring K
x : ℚ≥0
hx : x ≠ 0
⊢ ⌈↑x⌉₊ = ⌈x⌉₊

Tactic:
refine (Nat.ceil_eq_iff ?_).2 (mod_cast (Nat.ceil_eq_iff ?_).1 (Eq.refl ⌈x⌉₊)) <;> simpa

Result:
no goals
-- Mathlib/RingTheory/OreLocalization/Ring.lean
theorem nontrivial_iff :
    Nontrivial R[S⁻¹] ↔ 0 ∉ S

Proof state:
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
⊢ Nontrivial (OreLocalization S R) ↔ 0 ∉ S

Tactic:
rw [← not_subsingleton_iff_nontrivial, subsingleton_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrix_smulBasis_right {G} [Group G] [DistribMulAction G M₂]
    [SMulCommClass G R M₂] (g : G) (f : M₁ →ₗ[R] M₂) :
    LinearMap.toMatrix v₁ (g • v₂) f =
      LinearMap.toMatrix v₁ v₂ (DistribMulAction.toLinearMap _ _ g⁻¹ ∘ₗ f)

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : Finite m
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
G : Type u_7
inst✝² : Group G
inst✝¹ : DistribMulAction G M₂
inst✝ : SMulCommClass G R M₂
g : G
f : M₁ →ₗ[R] M₂
⊢ (toMatrix v₁ (g • v₂)) f = (toMatrix v₁ v₂) (DistribMulAction.toLinearMap R M₂ g⁻¹ ∘ₗ f)

Tactic:
ext

Result:
case a
R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : Finite m
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
G : Type u_7
inst✝² : Group G
inst✝¹ : DistribMulAction G M₂
inst✝ : SMulCommClass G R M₂
g : G
f : M₁ →ₗ[R] M₂
i✝ : m
j✝ : n
⊢ (toMatrix v₁ (g • v₂)) f i✝ j✝ = (toMatrix v₁ v₂) (DistribMulAction.toLinearMap R M₂ g⁻¹ ∘ₗ f) i✝ j✝

Proof state:
case a
R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : Finite m
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
G : Type u_7
inst✝² : Group G
inst✝¹ : DistribMulAction G M₂
inst✝ : SMulCommClass G R M₂
g : G
f : M₁ →ₗ[R] M₂
i✝ : m
j✝ : n
⊢ (toMatrix v₁ (g • v₂)) f i✝ j✝ = (toMatrix v₁ v₂) (DistribMulAction.toLinearMap R M₂ g⁻¹ ∘ₗ f) i✝ j✝

Tactic:
rw [LinearMap.toMatrix_apply, LinearMap.toMatrix_apply]

Result:
case a
R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : Finite m
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
G : Type u_7
inst✝² : Group G
inst✝¹ : DistribMulAction G M₂
inst✝ : SMulCommClass G R M₂
g : G
f : M₁ →ₗ[R] M₂
i✝ : m
j✝ : n
⊢ ((g • v₂).repr (f (v₁ j✝))) i✝ = (v₂.repr ((DistribMulAction.toLinearMap R M₂ g⁻¹ ∘ₗ f) (v₁ j✝))) i✝

Proof state:
case a
R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : Finite m
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
G : Type u_7
inst✝² : Group G
inst✝¹ : DistribMulAction G M₂
inst✝ : SMulCommClass G R M₂
g : G
f : M₁ →ₗ[R] M₂
i✝ : m
j✝ : n
⊢ ((g • v₂).repr (f (v₁ j✝))) i✝ = (v₂.repr ((DistribMulAction.toLinearMap R M₂ g⁻¹ ∘ₗ f) (v₁ j✝))) i✝

Tactic:
dsimp

Result:
no goals
-- Mathlib/Algebra/CharP/Basic.lean
/-- If two integers from `{0, 1, -1}` result in equal elements in a ring `R`
that is nontrivial and of characteristic not `2`, then they are equal. -/
lemma Int.cast_injOn_of_ringChar_ne_two {R : Type*} [NonAssocRing R] [Nontrivial R]
    (hR : ringChar R ≠ 2) : ({0, 1, -1} : Set ℤ).InjOn ((↑) : ℤ → R)

Proof state:
case inr.inl.inr.inr
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : 1 = -1
⊢ 1 = -1

Tactic:
exact ((Ring.neg_one_ne_one_of_char_ne_two hR).symm h).elim

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ InjOn Int.cast {0, 1, -1}

Tactic:
rintro _ (rfl | rfl | rfl) _ (rfl | rfl | rfl) h <;>
simp only
  [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢

Result:
case inr.inl.inr.inr
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : 1 = -1
⊢ 1 = -1

case inr.inr.inr.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : -1 = 1
⊢ -1 = 1

Proof state:
case inr.inr.inr.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : -1 = 1
⊢ -1 = 1

Tactic:
exact ((Ring.neg_one_ne_one_of_char_ne_two hR) h).elim

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma toRatCDF_unit_prod (a : α) :
    toRatCDF (fun (p : Unit × α) ↦ f p.2) ((), a) = toRatCDF f a

Proof state:
α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ toRatCDF (fun p => f p.2) ((), a) = toRatCDF f a

Tactic:
unfold toRatCDF

Result:
α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ (if IsRatStieltjesPoint (fun p => f p.2) ((), a) then (fun p => f p.2) ((), a) else defaultRatCDF) =
    if IsRatStieltjesPoint f a then f a else defaultRatCDF

Proof state:
α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ (if IsRatStieltjesPoint (fun p => f p.2) ((), a) then (fun p => f p.2) ((), a) else defaultRatCDF) =
    if IsRatStieltjesPoint f a then f a else defaultRatCDF

Tactic:
rw [isRatStieltjesPoint_unit_prod_iff]

Result:
no goals
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem isubtree_cons [DecidableEq F.A] [Inhabited (M F)] (ps : Path F) {a} (f : F.B a → M F)
    {i : F.B a} : isubtree (⟨_, i⟩ :: ps) (M.mk ⟨a, f⟩) = isubtree ps (f i)

Proof state:
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps : Path F
a : F.A
f : F.B a → F.M
i : F.B a
⊢ isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = isubtree ps (f i)

Tactic:
simp only [isubtree, ichildren_mk, PFunctor.Obj.iget, dif_pos, isubtree, M.casesOn_mk']

Result:
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps : Path F
a : F.A
f : F.B a → F.M
i : F.B a
⊢ isubtree ps (f (cast ⋯ i)) = isubtree ps (f i)

Proof state:
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps : Path F
a : F.A
f : F.B a → F.M
i : F.B a
⊢ isubtree ps (f (cast ⋯ i)) = isubtree ps (f i)

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/ClassEquation.lean
theorem Group.sum_card_conj_classes_eq_card [Finite G] :
    ∑ᶠ x : ConjClasses G, x.carrier.ncard = Nat.card G

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G

Tactic:
cases nonempty_fintype G

Result:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G

Proof state:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ i : ConjClasses G, i.carrier.ncard = ∑ x : ConjClasses G, x.carrier.toFinset.card

Tactic:
simp [Set.ncard_eq_toFinset_card']

Result:
no goals

Proof state:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G

Tactic:
rw [Nat.card_eq_fintype_card, ← sum_conjClasses_card_eq_card, finsum_eq_sum_of_fintype]

Result:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ i : ConjClasses G, i.carrier.ncard = ∑ x : ConjClasses G, x.carrier.toFinset.card

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G

Tactic:
classical
cases nonempty_fintype G
rw [Nat.card_eq_fintype_card, ← sum_conjClasses_card_eq_card, finsum_eq_sum_of_fintype]
simp [Set.ncard_eq_toFinset_card']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem fold_cons {l : Raw α β} {acc : List ((a : α) × β a)} :
    l.fold (fun acc k v => ⟨k, v⟩ :: acc) acc = (toListModel l.buckets).reverse ++ acc

Proof state:
α : Type u
β : α → Type v
l : Raw α β
acc : List ((a : α) × β a)
⊢ Raw.fold (fun acc k v => ⟨k, v⟩ :: acc) acc l = (toListModel l.buckets).reverse ++ acc

Tactic:
simp [fold_cons_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem get_attachWith {p : α → Prop} {o : Option α} (H : ∀ a ∈ o, p a) (h : (o.attachWith p H).isSome) :
    (o.attachWith p H).get h = ⟨o.get (by simpa using h), H _ (by simp)⟩

Proof state:
case none
α : Type u_1
p : α → Prop
H : ∀ (a : α), a ∈ none → p a
h : (none.attachWith p H).isSome = true
⊢ (none.attachWith p H).get h = ⟨none.get ⋯, ⋯⟩

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
o : Option α
H : ∀ (a : α), a ∈ o → p a
h : (o.attachWith p H).isSome = true
⊢ (o.attachWith p H).get h = ⟨o.get ⋯, ⋯⟩

Tactic:
cases o

Result:
case none
α : Type u_1
p : α → Prop
H : ∀ (a : α), a ∈ none → p a
h : (none.attachWith p H).isSome = true
⊢ (none.attachWith p H).get h = ⟨none.get ⋯, ⋯⟩

case some
α : Type u_1
p : α → Prop
val✝ : α
H : ∀ (a : α), a ∈ some val✝ → p a
h : ((some val✝).attachWith p H).isSome = true
⊢ ((some val✝).attachWith p H).get h = ⟨(some val✝).get ⋯, ⋯⟩

Proof state:
case some
α : Type u_1
p : α → Prop
val✝ : α
H : ∀ (a : α), a ∈ some val✝ → p a
h : ((some val✝).attachWith p H).isSome = true
⊢ ((some val✝).attachWith p H).get h = ⟨(some val✝).get ⋯, ⋯⟩

Tactic:
simp [get_some]

Result:
no goals

Proof state:
α : Type ?u.7032
p : α → Prop
o : Option α
H : ∀ (a : α), a ∈ o → p a
h : (o.attachWith p H).isSome = true
⊢ o.get ⋯ ∈ o

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.7032
p : α → Prop
o : Option α
H : ∀ (a : α), a ∈ o → p a
h : (o.attachWith p H).isSome = true
⊢ o.isSome = true

Tactic:
simpa using h

Result:
no goals