harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/PEquiv.lean
theorem mem_ofSet_iff {s : Set α} [DecidablePred (· ∈ s)] {a b : α} :
    a ∈ ofSet s b ↔ a = b ∧ a ∈ s

Proof state:
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
⊢ a ∈ (ofSet s) b ↔ a = b ∧ a ∈ s

Tactic:
dsimp [ofSet]

Result:
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
⊢ (a ∈ if b ∈ s then some b else none) ↔ a = b ∧ a ∈ s

Proof state:
case pos
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : b ∈ s
⊢ a ∈ some b ↔ a = b ∧ a ∈ s

Tactic:
simp only [mem_def, eq_comm, some.injEq, iff_self_and]

Result:
case pos
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : b ∈ s
⊢ a = b → a ∈ s

Proof state:
case neg
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : b ∉ s
⊢ a ∈ none ↔ a = b ∧ a ∈ s

Tactic:
simp only [mem_def, false_iff, not_and, reduceCtorEq]

Result:
case neg
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : b ∉ s
⊢ a = b → a ∉ s

Proof state:
case pos
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
h : a ∈ s
⊢ a ∈ s

Tactic:
exact h

Result:
no goals

Proof state:
case pos
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : b ∈ s
⊢ a = b → a ∈ s

Tactic:
rintro rfl

Result:
case pos
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
h : a ∈ s
⊢ a ∈ s

Proof state:
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
⊢ (a ∈ if b ∈ s then some b else none) ↔ a = b ∧ a ∈ s

Tactic:
split_ifs with h

Result:
case pos
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : b ∈ s
⊢ a ∈ some b ↔ a = b ∧ a ∈ s

case neg
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : b ∉ s
⊢ a ∈ none ↔ a = b ∧ a ∈ s

Proof state:
case neg
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
h : a ∉ s
⊢ a ∉ s

Tactic:
exact h

Result:
no goals

Proof state:
case neg
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : b ∉ s
⊢ a = b → a ∉ s

Tactic:
rintro rfl

Result:
case neg
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
h : a ∉ s
⊢ a ∉ s
-- Mathlib/ModelTheory/Algebra/Ring/FreeCommRing.lean
theorem exists_term_realize_eq_freeCommRing (p : FreeCommRing α) :
    ∃ t : Language.ring.Term α,
      (t.realize FreeCommRing.of : FreeCommRing α) = p :=
  FreeCommRing.induction_on p
    ⟨-1, by simp [Term.realize]⟩
    (fun a => ⟨Term.var a, by simp [Term.realize]⟩)
    (fun x y ⟨t₁, ht₁⟩ ⟨t₂, ht₂⟩ =>
      ⟨t₁ + t₂, by simp_all [Term.realize]⟩)
    (fun x y ⟨t₁, ht₁⟩ ⟨t₂, ht₂⟩ =>
      ⟨t₁ * t₂, by simp_all [Term.realize]⟩)

Proof state:
α : Type u_1
p : FreeCommRing α
⊢ Term.realize FreeCommRing.of (-1) = -1

Tactic:
simp [Term.realize]

Result:
no goals

Proof state:
α : Type u_1
p x y : FreeCommRing α
x✝¹ : ∃ t, Term.realize FreeCommRing.of t = x
x✝ : ∃ t, Term.realize FreeCommRing.of t = y
t₁ : ring.Term α
ht₁ : Term.realize FreeCommRing.of t₁ = x
t₂ : ring.Term α
ht₂ : Term.realize FreeCommRing.of t₂ = y
⊢ Term.realize FreeCommRing.of (t₁ + t₂) = x + y

Tactic:
simp_all [Term.realize]

Result:
no goals

Proof state:
α : Type u_1
p x y : FreeCommRing α
x✝¹ : ∃ t, Term.realize FreeCommRing.of t = x
x✝ : ∃ t, Term.realize FreeCommRing.of t = y
t₁ : ring.Term α
ht₁ : Term.realize FreeCommRing.of t₁ = x
t₂ : ring.Term α
ht₂ : Term.realize FreeCommRing.of t₂ = y
⊢ Term.realize FreeCommRing.of (t₁ * t₂) = x * y

Tactic:
simp_all [Term.realize]

Result:
no goals

Proof state:
α : Type u_1
p : FreeCommRing α
a : α
⊢ Term.realize FreeCommRing.of (var a) = FreeCommRing.of a

Tactic:
simp [Term.realize]

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsBasis.transfer (hIX : M.IsBasis I X) (hJX : M.IsBasis J X) (hXY : X ⊆ Y)
    (hJY : M.IsBasis J Y) : M.IsBasis I Y

Proof state:
α : Type u_1
M : Matroid α
I X Y J : Set α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
hXY : X ⊆ Y
hJY : (M ↾ Y).IsBase J
⊢ (M ↾ Y).IsBase I

Tactic:
exact hJY.isBase_of_isBasis_superset hJX.subset (hIX.isBasis_restrict_of_subset hXY)

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I X Y J : Set α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
hXY : X ⊆ Y
hJY : M.IsBasis J Y
⊢ M.IsBasis I Y

Tactic:
rw [← isBase_restrict_iff]

Result:
α : Type u_1
M : Matroid α
I X Y J : Set α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
hXY : X ⊆ Y
hJY : M.IsBasis J Y
⊢ (M ↾ Y).IsBase I

Proof state:
α : Type u_1
M : Matroid α
I X Y J : Set α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
hXY : X ⊆ Y
hJY : M.IsBasis J Y
⊢ (M ↾ Y).IsBase I

Tactic:
rw [← isBase_restrict_iff] at hJY

Result:
α : Type u_1
M : Matroid α
I X Y J : Set α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
hXY : X ⊆ Y
hJY : (M ↾ Y).IsBase J
⊢ (M ↾ Y).IsBase I
-- Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean
theorem PInfty_comp_πSummand_id (n : ℕ) :
    PInfty.f n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = s.πSummand (IndexSet.id (op ⦋n⦌))

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
⊢ 𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = PInfty.f n ≫ s.πSummand (IndexSet.id (op ⦋n⦌))

Tactic:
rw [← sub_eq_zero, ← sub_comp, ← comp_PInfty_eq_zero_iff, sub_comp, id_comp, PInfty_f_idem,
  sub_self]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
⊢ PInfty.f n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = s.πSummand (IndexSet.id (op ⦋n⦌))

Tactic:
conv_rhs => rw [← id_comp (s.πSummand _)]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
⊢ PInfty.f n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌))

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
⊢ PInfty.f n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌))

Tactic:
symm

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
⊢ 𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = PInfty.f n ≫ s.πSummand (IndexSet.id (op ⦋n⦌))
-- Mathlib/Data/Set/Function.lean
lemma BijOn.exists {p : β → Prop} (hf : BijOn f s t) : (∃ b ∈ t, p b) ↔ ∃ a ∈ s, p (f a) where
  mp

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
b : β
hb : b ∈ t
h : p b
⊢ ∃ a ∈ s, p (f a)

Tactic:
obtain ⟨a, ha, rfl⟩ := hf.surjOn hb

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
a : α
ha : a ∈ s
hb : f a ∈ t
h : p (f a)
⊢ ∃ a ∈ s, p (f a)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
a : α
ha : a ∈ s
h : p (f a)
⊢ ∃ b ∈ t, p b

Tactic:
exact ⟨f a, hf.mapsTo ha, h⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
a : α
ha : a ∈ s
hb : f a ∈ t
h : p (f a)
⊢ ∃ a ∈ s, p (f a)

Tactic:
exact ⟨a, ha, h⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
⊢ (∃ b ∈ t, p b) → ∃ a ∈ s, p (f a)

Tactic:
rintro ⟨b, hb, h⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
b : β
hb : b ∈ t
h : p b
⊢ ∃ a ∈ s, p (f a)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
⊢ (∃ a ∈ s, p (f a)) → ∃ b ∈ t, p b

Tactic:
rintro ⟨a, ha, h⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
a : α
ha : a ∈ s
h : p (f a)
⊢ ∃ b ∈ t, p b
-- Mathlib/Data/List/Basic.lean
theorem reverse_cons' (a : α) (l : List α) : reverse (a :: l) = concat (reverse l) a

Proof state:
α : Type u
a : α
l : List α
⊢ (a :: l).reverse = l.reverse.concat a

Tactic:
simp only [reverse_cons, concat_eq_append]

Result:
no goals
-- Mathlib/Order/BooleanSubalgebra.lean
lemma map_top (f : BoundedLatticeHom α β) (h : Surjective f) : BooleanSubalgebra.map f ⊤ = ⊤ :=
  SetLike.coe_injective <| by simp [h.range_eq]

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
f : BoundedLatticeHom α β
h : Surjective ⇑f
⊢ ↑(map f ⊤) = ↑⊤

Tactic:
simp [h.range_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem units_inv_smul (u : Rˣ) (v : Module.Ray R M) : u⁻¹ • v = u • v :=
  have := mul_self_pos.2 u.ne_zero
  calc
    u⁻¹ • v = (u * u) • u⁻¹ • v := Eq.symm <| (u⁻¹ • v).units_smul_of_pos _ (by exact this)
    _ = u • v

Proof state:
R : Type u_1
inst✝² : LinearOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
v : Module.Ray R M
this : 0 < ↑u * ↑u
⊢ (u * u) • u⁻¹ • v = u • v

Tactic:
rw [mul_smul, smul_inv_smul]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : LinearOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
v : Module.Ray R M
this : 0 < ↑u * ↑u
⊢ 0 < ↑(u * u)

Tactic:
exact this

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
@[to_additive (attr := simp)]
lemma index_pi {ι : Type*} [Fintype ι] (H : ι → Subgroup G) :
    (Subgroup.pi Set.univ H).index = ∏ i, (H i).index

Proof state:
G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
H : ι → Subgroup G
x y : ι → G
⊢ (QuotientGroup.leftRel (pi Set.univ H)) x y ↔ piSetoid x y

Tactic:
rw [QuotientGroup.leftRel_pi]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
H : ι → Subgroup G
⊢ Nat.card ((ι → G) ⧸ pi Set.univ H) = Nat.card ((a : ι) → G ⧸ H a)

Tactic:
refine Nat.card_congr
  ((Quotient.congrRight (fun x y ↦ ?_)).trans (Setoid.piQuotientEquiv _).symm)

Result:
G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
H : ι → Subgroup G
x y : ι → G
⊢ (QuotientGroup.leftRel (pi Set.univ H)) x y ↔ piSetoid x y

Proof state:
G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
H : ι → Subgroup G
⊢ (pi Set.univ H).index = ∏ i : ι, (H i).index

Tactic:
simp_rw [index, ← Nat.card_pi]

Result:
G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
H : ι → Subgroup G
⊢ Nat.card ((ι → G) ⧸ pi Set.univ H) = Nat.card ((a : ι) → G ⧸ H a)
-- Mathlib/Data/PNat/Factors.lean
theorem count_factorMultiset (m : ℕ+) (p : Nat.Primes) (k : ℕ) :
    (p : ℕ+) ^ k ∣ m ↔ k ≤ m.factorMultiset.count p

Proof state:
case a.h.e'_3.h
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ Multiset.card (k • PrimeMultiset.ofPrime p) = k ∧ ∀ b ∈ k • PrimeMultiset.ofPrime p, b = p

Tactic:
constructor

Result:
case a.h.e'_3.h.left
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ Multiset.card (k • PrimeMultiset.ofPrime p) = k

case a.h.e'_3.h.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ ∀ b ∈ k • PrimeMultiset.ofPrime p, b = p

Proof state:
m : ℕ+
p : Nat.Primes
k : ℕ
⊢ k • PrimeMultiset.ofPrime p ≤ m.factorMultiset ↔ Multiset.replicate k p ≤ m.factorMultiset

Tactic:
congr! 2

Result:
case a.h.e'_3.h
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ k • PrimeMultiset.ofPrime p = Multiset.replicate k p

Proof state:
case a.h.e'_3.h.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ Multiset.replicate k p
⊢ q = p

Tactic:
exact Multiset.eq_of_mem_replicate h

Result:
no goals

Proof state:
case a.h.e'_3.h.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ k • PrimeMultiset.ofPrime p
⊢ q = p

Tactic:
rw [PrimeMultiset.ofPrime, Multiset.nsmul_singleton _ k] at h

Result:
case a.h.e'_3.h.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ Multiset.replicate k p
⊢ q = p

Proof state:
case a.h.e'_3.h
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ k • PrimeMultiset.ofPrime p = Multiset.replicate k p

Tactic:
apply Multiset.eq_replicate.mpr

Result:
case a.h.e'_3.h
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ Multiset.card (k • PrimeMultiset.ofPrime p) = k ∧ ∀ b ∈ k • PrimeMultiset.ofPrime p, b = p

Proof state:
case a.h.e'_3.h.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ ∀ b ∈ k • PrimeMultiset.ofPrime p, b = p

Tactic:
intro q h

Result:
case a.h.e'_3.h.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ k • PrimeMultiset.ofPrime p
⊢ q = p

Proof state:
m : ℕ+
p : Nat.Primes
k : ℕ
⊢ ↑p ^ k ∣ m ↔ k ≤ Multiset.count p m.factorMultiset

Tactic:
rw [Multiset.le_count_iff_replicate_le, ← factorMultiset_le_iff, factorMultiset_pow,
  factorMultiset_ofPrime]

Result:
m : ℕ+
p : Nat.Primes
k : ℕ
⊢ k • PrimeMultiset.ofPrime p ≤ m.factorMultiset ↔ Multiset.replicate k p ≤ m.factorMultiset

Proof state:
case a.h.e'_3.h.left
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ Multiset.card (k • PrimeMultiset.ofPrime p) = k

Tactic:
rw [Multiset.card_nsmul, PrimeMultiset.card_ofPrime, mul_one]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem continuous_sub_left {a : ℝ≥0∞} (a_ne_top : a ≠ ∞) : Continuous (a - ·)

Proof state:
a : ℝ≥0∞
a_ne_top : a ≠ ⊤
⊢ Continuous (uncurry Sub.sub ∘ fun x => (a, x))

Tactic:
refine continuousOn_sub.comp_continuous (Continuous.Prod.mk a) fun x => ?_

Result:
a : ℝ≥0∞
a_ne_top : a ≠ ⊤
x : ℝ≥0∞
⊢ (a, x) ∈ {p | p ≠ (⊤, ⊤)}

Proof state:
a : ℝ≥0∞
a_ne_top : a ≠ ⊤
x : ℝ≥0∞
⊢ (a, x) ∈ {p | p ≠ (⊤, ⊤)}

Tactic:
simp only [a_ne_top, Ne, mem_setOf_eq, Prod.mk.inj_iff, false_and, not_false_iff]

Result:
no goals
-- Mathlib/Topology/FiberBundle/Basic.lean
theorem continuousOn_of_comp_right {X : Type*} [TopologicalSpace X] {f : TotalSpace F E → X}
    {s : Set B} (hs : IsOpen s) (hf : ∀ b ∈ s,
      ContinuousOn (f ∘ (a.pretrivializationAt b).toPartialEquiv.symm)
        ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ (Set.univ : Set F))) :
    @ContinuousOn _ _ a.totalSpaceTopology _ f (π F E ⁻¹' s)

Proof state:
case refine_3
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen s
hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯
⊢ z.proj ∈ s ∩ (a.pretrivializationAt z.proj).baseSet

Tactic:
exact ⟨hz, a.mem_base_pretrivializationAt z.proj⟩

Result:
no goals
-- Mathlib/RingTheory/Discriminant.lean
theorem discr_reindex (b : Basis ι A B) (f : ι ≃ ι') : discr A (b ∘ ⇑f.symm) = discr A b

Proof state:
A : Type u
B : Type v
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
⊢ discr A (⇑b ∘ ⇑f.symm) = discr A ⇑b

Tactic:
classical rw [← Basis.coe_reindex, discr_def, traceMatrix_reindex, det_reindex_self, ← discr_def]

Result:
no goals

Proof state:
A : Type u
B : Type v
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
⊢ discr A (⇑b ∘ ⇑f.symm) = discr A ⇑b

Tactic:
rw [← Basis.coe_reindex, discr_def, traceMatrix_reindex, det_reindex_self, ← discr_def]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem mem_oneCocycles_def (f : G → A) :
    f ∈ oneCocycles A ↔ ∀ g h : G, A.ρ g (f h) - f (g * h) + f g = 0 :=
  LinearMap.mem_ker.trans <| by
    rw [funext_iff]
    simp only [dOne_apply, Pi.zero_apply, Prod.forall]

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G → ↑A.V
⊢ (∀ (x : G × G), (dOne A) f x = 0 x) ↔ ∀ (g h : G), (A.ρ g) (f h) - f (g * h) + f g = 0

Tactic:
simp only [dOne_apply, Pi.zero_apply, Prod.forall]

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G → ↑A.V
⊢ (dOne A) f = 0 ↔ ∀ (g h : G), (A.ρ g) (f h) - f (g * h) + f g = 0

Tactic:
rw [funext_iff]

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G → ↑A.V
⊢ (∀ (x : G × G), (dOne A) f x = 0 x) ↔ ∀ (g h : G), (A.ρ g) (f h) - f (g * h) + f g = 0
-- Mathlib/Probability/Kernel/Disintegration/StandardBorel.lean
lemma _root_.MeasureTheory.Measure.condKernel_apply (ρ : Measure (α × Ω)) [IsFiniteMeasure ρ]
    (a : α) :
    ρ.condKernel a = condKernelUnitBorel (const Unit ρ) ((), a)

Proof state:
α : Type u_1
Ω : Type u_4
mα : MeasurableSpace α
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
⊢ ρ.condKernel a = (const Unit ρ).condKernelUnitBorel ((), a)

Tactic:
rw [Measure.condKernel]

Result:
α : Type u_1
Ω : Type u_4
mα : MeasurableSpace α
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
⊢ ((const Unit ρ).condKernelUnitBorel.comap (fun a => ((), a)) ⋯) a = (const Unit ρ).condKernelUnitBorel ((), a)

Proof state:
α : Type u_1
Ω : Type u_4
mα : MeasurableSpace α
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
⊢ ((const Unit ρ).condKernelUnitBorel.comap (fun a => ((), a)) ⋯) a = (const Unit ρ).condKernelUnitBorel ((), a)

Tactic:
rfl

Result:
no goals
-- Mathlib/Tactic/LinearCombination'.lean
theorem eq_of_add_pow [Ring α] [NoZeroDivisors α] (n : ℕ) (p : (a:α) = b)
    (H : (a' - b')^n - (a - b) = 0) : a' = b'

Proof state:
α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
n : ℕ
p : a = b
H : (a' - b') ^ n - (a - b) = 0
⊢ a' = b'

Tactic:
rw [← sub_eq_zero] at p ⊢

Result:
α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n - (a - b) = 0
⊢ a' - b' = 0

Proof state:
α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n - (a - b) = 0
⊢ (a' - b') ^ n = 0

Tactic:
rwa [sub_eq_zero, p] at H

Result:
no goals

Proof state:
α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n - (a - b) = 0
⊢ a' - b' = 0

Tactic:
apply pow_eq_zero (n := n)

Result:
α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n - (a - b) = 0
⊢ (a' - b') ^ n = 0
-- Mathlib/Algebra/Ring/Defs.lean
theorem boole_mul {α} [MulZeroOneClass α] (P : Prop) [Decidable P] (a : α) :
    (if P then 1 else 0) * a = if P then a else 0

Proof state:
α : Type u_1
inst✝¹ : MulZeroOneClass α
P : Prop
inst✝ : Decidable P
a : α
⊢ (if P then 1 else 0) * a = if P then a else 0

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Cover.lean
lemma wcovBy_eq_reflGen_covBy [PartialOrder α] : ((· : α) ⩿ ·) = ReflGen (· ⋖ ·)

Proof state:
case h.h.a
α : Type u_1
inst✝ : PartialOrder α
x y : α
⊢ x ⩿ y ↔ ReflGen (fun x1 x2 => x1 ⋖ x2) x y

Tactic:
simp_rw [wcovBy_iff_eq_or_covBy, @eq_comm _ x, reflGen_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
⊢ (fun x1 x2 => x1 ⩿ x2) = ReflGen fun x1 x2 => x1 ⋖ x2

Tactic:
ext x y

Result:
case h.h.a
α : Type u_1
inst✝ : PartialOrder α
x y : α
⊢ x ⩿ y ↔ ReflGen (fun x1 x2 => x1 ⋖ x2) x y
-- Mathlib/MeasureTheory/Function/EssSup.lean
theorem essInf_antitone_measure {f : α → β} (hμν : μ ≪ ν) : essInf f ν ≤ essInf f μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : μ ≪ ν
⊢ essInf f ν ≤ essInf f μ

Tactic:
refine liminf_le_liminf_of_le (Measure.ae_le_iff_absolutelyContinuous.mpr hμν) ?_ ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : μ ≪ ν
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (ae ν) f

case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : μ ≪ ν
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) (ae μ) f

Proof state:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : μ ≪ ν
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (ae ν) f

case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : μ ≪ ν
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) (ae μ) f

Tactic:
all_goals isBoundedDefault

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : μ ≪ ν
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) (ae μ) f

Tactic:
isBoundedDefault

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_ball_mul_of_pos (x : E) {r : ℝ} (hr : 0 < r) (s : ℝ) :
    μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 s)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : 0 < r
s : ℝ
⊢ μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 s)

Tactic:
have : ball (0 : E) (r * s) = r • ball (0 : E) s := by
  simp only [_root_.smul_ball hr.ne' (0 : E) s, Real.norm_eq_abs, abs_of_nonneg hr.le, smul_zero]

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : 0 < r
s : ℝ
this : ball 0 (r * s) = r • ball 0 s
⊢ μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 s)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : 0 < r
s : ℝ
⊢ ball 0 (r * s) = r • ball 0 s

Tactic:
simp only [_root_.smul_ball hr.ne' (0 : E) s, Real.norm_eq_abs, abs_of_nonneg hr.le, smul_zero]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : 0 < r
s : ℝ
this : ball 0 (r * s) = r • ball 0 s
⊢ μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 s)

Tactic:
simp only [this, addHaar_smul, abs_of_nonneg hr.le, addHaar_ball_center, abs_pow]

Result:
no goals