harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem factorial_mul_ascFactorial (n : ℕ) : ∀ k, n ! * (n + 1).ascFactorial k = (n + k)!
  | 0 => by rw [ascFactorial_zero, Nat.add_zero, Nat.mul_one]
  | k + 1 => by
    rw [ascFactorial_succ, ← Nat.add_assoc, factorial_succ, Nat.mul_comm (n + 1 + k),
      ← Nat.mul_assoc, factorial_mul_ascFactorial n k, Nat.mul_comm, Nat.add_right_comm]

Proof state:
n : ℕ
⊢ n ! * (n + 1).ascFactorial 0 = (n + 0)!

Tactic:
rw [ascFactorial_zero, Nat.add_zero, Nat.mul_one]

Result:
no goals

Proof state:
n k : ℕ
⊢ n ! * (n + 1).ascFactorial (k + 1) = (n + (k + 1))!

Tactic:
rw [ascFactorial_succ, ← Nat.add_assoc, factorial_succ, Nat.mul_comm (n + 1 + k),
  ← Nat.mul_assoc, factorial_mul_ascFactorial n k, Nat.mul_comm, Nat.add_right_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
lemma continuous_integral_boundedContinuousFunction
    {α : Type*} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] (f : α →ᵇ ℝ) :
    Continuous fun μ : FiniteMeasure α ↦ ∫ x, f x ∂μ

Proof state:
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : FiniteMeasure α
⊢ ContinuousAt (fun μ => ∫ (x : α), f x ∂↑μ) μ

Tactic:
exact continuousAt_of_tendsto_nhds
  (FiniteMeasure.tendsto_iff_forall_integral_tendsto.mp tendsto_id f)

Result:
no goals

Proof state:
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
⊢ Continuous fun μ => ∫ (x : α), f x ∂↑μ

Tactic:
rw [continuous_iff_continuousAt]

Result:
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
⊢ ∀ (x : FiniteMeasure α), ContinuousAt (fun μ => ∫ (x : α), f x ∂↑μ) x

Proof state:
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
⊢ ∀ (x : FiniteMeasure α), ContinuousAt (fun μ => ∫ (x : α), f x ∂↑μ) x

Tactic:
intro μ

Result:
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : FiniteMeasure α
⊢ ContinuousAt (fun μ => ∫ (x : α), f x ∂↑μ) μ
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem face_eq_mkOfPoint {n : ℕ} (s : Simplex k P n) (i : Fin (n + 1)) :
    s.face (Finset.card_singleton i) = mkOfPoint k (s.points i)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s : Simplex k P n
i : Fin (n + 1)
⊢ s.face ⋯ = mkOfPoint k (s.points i)

Tactic:
ext

Result:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s : Simplex k P n
i : Fin (n + 1)
i✝ : Fin (0 + 1)
⊢ (s.face ⋯).points i✝ = (mkOfPoint k (s.points i)).points i✝

Proof state:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s : Simplex k P n
i : Fin (n + 1)
i✝ : Fin (0 + 1)
⊢ (s.face ⋯).points i✝ = (mkOfPoint k (s.points i)).points i✝

Tactic:
simp [Affine.Simplex.mkOfPoint_points, Affine.Simplex.face_points, Finset.orderEmbOfFin_singleton]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
lemma length_le_coheight {x : α} {p : LTSeries α} (hhead : x ≤ p.head) :
    p.length ≤ coheight x :=
  length_le_height (α := αᵒᵈ) (p := p.reverse) (by simpa)

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hhead : x ≤ RelSeries.head p
⊢ (RelSeries.reverse p).last ≤ x

Tactic:
simpa

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem aleph_isNormal : IsNormal (ord ∘ aleph)

Proof state:
case h.e'_1

⊢ ord ∘ ⇑ℵ_ = ⇑ω_

Tactic:
exact funext ord_aleph

Result:
no goals

Proof state:
⊢ IsNormal (ord ∘ ⇑ℵ_ )

Tactic:
convert isNormal_omega

Result:
case h.e'_1

⊢ ord ∘ ⇑ℵ_ = ⇑ω_
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem leftUnitor_tensor (X Y : C) :
    (λ_ (X ⊗ Y)).hom = (α_ (𝟙_ C) X Y).inv ≫ (λ_ X).hom ▷ Y

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ (X ⊗ Y)).hom = (α_ (𝟙_ C) X Y).inv ≫ (λ_ X).hom ▷ Y

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Center.lean
theorem invOf_mem_center {a : M} [Invertible a] (ha : a ∈ Set.center M) : ⅟a ∈ Set.center M

Proof state:
M : Type u_1
inst✝¹ : Monoid M
a : M
inst✝ : Invertible a
ha : a ∈ center M
⊢ ⅟a ∈ center M

Tactic:
rw [Semigroup.mem_center_iff] at *

Result:
M : Type u_1
inst✝¹ : Monoid M
a : M
inst✝ : Invertible a
ha : ∀ (g : M), g * a = a * g
⊢ ∀ (g : M), g * ⅟a = ⅟a * g
-- Mathlib/NumberTheory/ModularForms/Identities.lean
theorem vAdd_width_periodic (N : ℕ) (k n : ℤ) (f : SlashInvariantForm (Gamma N) k) (z : ℍ) :
    f (((N * n) : ℝ) +ᵥ z) = f z

Proof state:
N : ℕ
k n : ℤ
f : SlashInvariantForm Γ(N) k
z : ℍ
⊢ f (↑(↑N * n) +ᵥ z) = f z

Tactic:
rw [← modular_T_zpow_smul z (N * n)]

Result:
N : ℕ
k n : ℤ
f : SlashInvariantForm Γ(N) k
z : ℍ
⊢ f (ModularGroup.T ^ (↑N * n) • z) = f z

Proof state:
case h.e'_3
N : ℕ
k n : ℤ
f : SlashInvariantForm Γ(N) k
z : ℍ
⊢ f z = (↑(↑(ModularGroup.T ^ (↑N * n)) 1 0) * ↑z + ↑(↑(ModularGroup.T ^ (↑N * n)) 1 1)) ^ k * f z

Tactic:
simp only [Fin.isValue, ModularGroup.coe_T_zpow (N * n), of_apply, cons_val', cons_val_zero,
  empty_val', cons_val_fin_one, cons_val_one, head_fin_const, Int.cast_zero, zero_mul, head_cons,
  Int.cast_one, zero_add, one_zpow, one_mul]

Result:
no goals

Proof state:
N : ℕ
k n : ℤ
f : SlashInvariantForm Γ(N) k
z : ℍ
⊢ f (ModularGroup.T ^ (↑N * n) • z) = f z

Tactic:
convert slash_action_eqn' f (ModularGroup_T_pow_mem_Gamma N (N * n) (Int.dvd_mul_right N n)) z

Result:
case h.e'_3
N : ℕ
k n : ℤ
f : SlashInvariantForm Γ(N) k
z : ℍ
⊢ f z = (↑(↑(ModularGroup.T ^ (↑N * n)) 1 0) * ↑z + ↑(↑(ModularGroup.T ^ (↑N * n)) 1 1)) ^ k * f z

Proof state:
N : ℕ
k n : ℤ
f : SlashInvariantForm Γ(N) k
z : ℍ
⊢ f (↑N * ↑n +ᵥ z) = f z

Tactic:
norm_cast

Result:
N : ℕ
k n : ℤ
f : SlashInvariantForm Γ(N) k
z : ℍ
⊢ f (↑(↑N * n) +ᵥ z) = f z
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma Walk.connected_induce_support {u v : V} (p : G.Walk u v) :
    (G.induce {v | v ∈ p.support}).Connected

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ (induce p.toSubgraph.verts G).Connected

Tactic:
exact p.toSubgraph_connected.induce_verts

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ (induce {v_1 | v_1 ∈ p.support} G).Connected

Tactic:
rw [← p.verts_toSubgraph]

Result:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ (induce p.toSubgraph.verts G).Connected
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem normalize_eq_zero {x : α} : normalize x = 0 ↔ x = 0 :=
  ⟨fun hx => (associated_zero_iff_eq_zero x).1 <| hx ▸ associated_normalize _, by
    rintro rfl; exact normalize_zero⟩

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
x : α
⊢ x = 0 → normalize x = 0

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
⊢ normalize 0 = 0

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
⊢ normalize 0 = 0

Tactic:
exact normalize_zero

Result:
no goals
-- Mathlib/Topology/Semicontinuous.lean
theorem LowerSemicontinuousAt.comp_continuousAt_of_eq {f : α → β} {g : ι → α} {y : α} {x : ι}
    (hf : LowerSemicontinuousAt f y) (hg : ContinuousAt g x) (hy : g x = y) :
    LowerSemicontinuousAt (fun x ↦ f (g x)) x

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
ι : Type u_5
inst✝ : TopologicalSpace ι
f : α → β
g : ι → α
y : α
x : ι
hf : LowerSemicontinuousAt f y
hg : ContinuousAt g x
hy : g x = y
⊢ LowerSemicontinuousAt (fun x => f (g x)) x

Tactic:
rw [← hy] at hf

Result:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
ι : Type u_5
inst✝ : TopologicalSpace ι
f : α → β
g : ι → α
y : α
x : ι
hf : LowerSemicontinuousAt f (g x)
hg : ContinuousAt g x
hy : g x = y
⊢ LowerSemicontinuousAt (fun x => f (g x)) x

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
ι : Type u_5
inst✝ : TopologicalSpace ι
f : α → β
g : ι → α
y : α
x : ι
hf : LowerSemicontinuousAt f (g x)
hg : ContinuousAt g x
hy : g x = y
⊢ LowerSemicontinuousAt (fun x => f (g x)) x

Tactic:
exact comp_continuousAt hf hg

Result:
no goals
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If 0 belongs to the interior of the interval `integrableExpSet X μ`,
then `X ^ n` is integrable for all nonnegative `p : ℝ`. -/
lemma integrable_rpow_of_mem_interior_integrableExpSet
    (h : 0 ∈ interior (integrableExpSet X μ)) {p : ℝ} (hp : 0 ≤ p) :
    Integrable (fun ω ↦ X ω ^ p) μ

Proof state:
case h.e'_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ (fun ω => X ω ^ p) = fun ω => X ω ^ p * rexp (0 * X ω)

Tactic:
simp

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω => X ω ^ p) μ

Tactic:
convert integrable_rpow_mul_exp_of_mem_interior_integrableExpSet h hp using 1

Result:
case h.e'_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ (fun ω => X ω ^ p) = fun ω => X ω ^ p * rexp (0 * X ω)
-- Mathlib/Analysis/Convex/Side.lean
theorem wSameSide_iff_exists_right {s : AffineSubspace R P} {x y p₂ : P} (h : p₂ ∈ s) :
    s.WSameSide x y ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
⊢ (y ∈ s ∨ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
simp_rw [SameRay.sameRay_comm]

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
⊢ s.WSameSide x y ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
rw [wSameSide_comm, wSameSide_iff_exists_left h]

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
⊢ (y ∈ s ∨ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
-- Mathlib/RingTheory/LinearDisjoint.lean
theorem of_basis_right {ι : Type*} (b : Basis ι R B)
    (H : LinearIndependent A (B.val ∘ b)) : A.LinearDisjoint B

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : Basis ι R ↥B
H : LinearMap.ker ((toSubmodule A).mulRightMap ⇑b) = ⊥
⊢ A.LinearDisjoint B

Tactic:
exact Submodule.LinearDisjoint.of_basis_right _ _ b H

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : Basis ι R ↥B
H : LinearIndependent (↥A) (⇑B.val ∘ ⇑b)
⊢ A.LinearDisjoint B

Tactic:
rw [← mulRightMap_ker_eq_bot_iff_linearIndependent] at H

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : Basis ι R ↥B
H : LinearMap.ker ((toSubmodule A).mulRightMap ⇑b) = ⊥
⊢ A.LinearDisjoint B
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_mul_eq_zero_of_left (q : R[X]) (hp : p.eval₂ f x = 0) : (p * q).eval₂ f x = 0

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
q : R[X]
hp : eval₂ f x p = 0
⊢ eval₂ f x (p * q) = 0

Tactic:
rw [eval₂_mul f x]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
q : R[X]
hp : eval₂ f x p = 0
⊢ eval₂ f x p * eval₂ f x q = 0

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
q : R[X]
hp : eval₂ f x p = 0
⊢ eval₂ f x p * eval₂ f x q = 0

Tactic:
exact mul_eq_zero_of_left hp (q.eval₂ f x)

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_surjective : Surjective (image f) ↔ Surjective f

Proof state:
α : Type u
β : Type v
f : α → β
⊢ Surjective (image f) ↔ Surjective f

Tactic:
refine ⟨fun h y => ?_, Surjective.image_surjective⟩

Result:
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
⊢ ∃ a, f a = y

Proof state:
case intro.intro.intro
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
x : α
left✝ : x ∈ s
hx : f x = y
⊢ ∃ a, f a = y

Tactic:
exact ⟨x, hx⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
⊢ ∃ a, f a = y

Tactic:
rcases h {y} with ⟨s, hs⟩

Result:
case intro
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
⊢ ∃ a, f a = y

Proof state:
case intro
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
this : y ∈ {y}
⊢ ∃ a, f a = y

Tactic:
rw [← hs] at this

Result:
case intro
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
this : y ∈ f '' s
⊢ ∃ a, f a = y

Proof state:
case intro
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
this : y ∈ f '' s
⊢ ∃ a, f a = y

Tactic:
rcases this with ⟨x, _, hx⟩

Result:
case intro.intro.intro
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
x : α
left✝ : x ∈ s
hx : f x = y
⊢ ∃ a, f a = y

Proof state:
case intro
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
⊢ ∃ a, f a = y

Tactic:
have := mem_singleton y

Result:
case intro
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
this : y ∈ {y}
⊢ ∃ a, f a = y
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
lemma HasFTaylorSeriesUpToOn.analyticOn
    (hf : HasFTaylorSeriesUpToOn ω f p s) (h : AnalyticOn 𝕜 (fun x ↦ p x 0) s) :
    AnalyticOn 𝕜 f s

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn ω f p s
h : AnalyticOn 𝕜 (fun x => p x 0) s
⊢ AnalyticOn 𝕜 f s

Tactic:
have : AnalyticOn 𝕜 (fun x ↦ (continuousMultilinearCurryFin0 𝕜 E F) (p x 0)) s :=
  (LinearIsometryEquiv.analyticOnNhd _ _ ).comp_analyticOn
    h (Set.mapsTo_univ _ _)

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn ω f p s
h : AnalyticOn 𝕜 (fun x => p x 0) s
this : AnalyticOn 𝕜 (fun x => (continuousMultilinearCurryFin0 𝕜 E F) (p x 0)) s
⊢ AnalyticOn 𝕜 f s

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn ω f p s
h : AnalyticOn 𝕜 (fun x => p x 0) s
this : AnalyticOn 𝕜 (fun x => (continuousMultilinearCurryFin0 𝕜 E F) (p x 0)) s
⊢ AnalyticOn 𝕜 f s

Tactic:
exact this.congr (fun y hy ↦ (hf.zero_eq _ hy).symm)

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_union_of_not_mem_inter (h : a ∉ s ∩ t) (f : α → M) :
    mulIndicator (s ∪ t) f a = mulIndicator s f a * mulIndicator t f a

Proof state:
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
s t : Set α
a : α
h : a ∉ s ∩ t
f : α → M
⊢ (s ∪ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Tactic:
rw [← mulIndicator_union_mul_inter_apply f s t, mulIndicator_of_not_mem h, mul_one]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
theorem of_h_eq_floor : (of v).h = ⌊v⌋

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ (of v).h = ↑⌊v⌋

Tactic:
simp [of_h_eq_intFractPair_seq1_fst_b, IntFractPair.of]

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

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

Tactic:
rw [symmDiff_eq_sup_sdiff_inf, inf_sdiff_distrib_left, inf_sup_left, inf_inf_distrib_left,
  symmDiff_eq_sup_sdiff_inf]

Result:
no goals
-- Mathlib/Data/List/Infix.lean
theorem IsInfix.flatten {l₁ l₂ : List (List α)} (h : l₁ <:+: l₂) :
    l₁.flatten <:+: l₂.flatten

Proof state:
case intro.intro
α : Type u_1
l₁ l l' : List (List α)
⊢ l₁.flatten <:+: (l ++ l₁ ++ l').flatten

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <:+: l₂
⊢ l₁.flatten <:+: l₂.flatten

Tactic:
rcases h with ⟨l, l', rfl⟩

Result:
case intro.intro
α : Type u_1
l₁ l l' : List (List α)
⊢ l₁.flatten <:+: (l ++ l₁ ++ l').flatten
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
lemma isLocalizedModule_id (R') [CommSemiring R'] [Algebra R R'] [IsLocalization S R'] [Module R' M]
    [IsScalarTower R R' M] : IsLocalizedModule S (.id : M →ₗ[R] M) where
  map_units s

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
R' : Type u_6
inst✝⁴ : CommSemiring R'
inst✝³ : Algebra R R'
inst✝² : IsLocalization S R'
inst✝¹ : Module R' M
inst✝ : IsScalarTower R R' M
s : ↥S
⊢ IsUnit ((algebraMap R (Module.End R M)) ↑s)

Tactic:
rw [← (Algebra.lsmul R (A := R') R M).commutes]

Result:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
R' : Type u_6
inst✝⁴ : CommSemiring R'
inst✝³ : Algebra R R'
inst✝² : IsLocalization S R'
inst✝¹ : Module R' M
inst✝ : IsScalarTower R R' M
s : ↥S
⊢ IsUnit ((Algebra.lsmul R R M) ((algebraMap R R') ↑s))

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
R' : Type u_6
inst✝⁴ : CommSemiring R'
inst✝³ : Algebra R R'
inst✝² : IsLocalization S R'
inst✝¹ : Module R' M
inst✝ : IsScalarTower R R' M
s : ↥S
⊢ IsUnit ((Algebra.lsmul R R M) ((algebraMap R R') ↑s))

Tactic:
exact (IsLocalization.map_units R' s).map _

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Linear.lean
lemma zero_lt_finrank_genWeightSpace {χ : L → R} (hχ : genWeightSpace M χ ≠ ⊥) :
    0 < finrank R (genWeightSpace M χ)

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : LieRing.IsNilpotent L
χ : L → R
hχ : genWeightSpace M χ ≠ ⊥
⊢ 0 < finrank R ↥(genWeightSpace M χ)

Tactic:
rwa [← LieSubmodule.nontrivial_iff_ne_bot, ← rank_pos_iff_nontrivial (R := R), ← finrank_eq_rank,
  Nat.cast_pos] at hχ

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma add_of_Z_eq_zero_left [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P)
    (hPz : P z = 0) (hQz : Q z ≠ 0) : W'.add P Q = (P y ^ 2 * Q z) • Q

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
hQz : Q z ≠ 0
⊢ W'.add P Q = (P y ^ 2 * Q z) • Q

Tactic:
rw [add, if_neg <| not_equiv_of_Z_eq_zero_left hPz hQz, addXYZ_of_Z_eq_zero_left hP hPz]

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem ComplementedLattice.isStronglyAtomic' [h : IsAtomic α] : IsStronglyCoatomic α

Proof state:
α : Type u_2
inst✝³ : Lattice α
inst✝² : BoundedOrder α
inst✝¹ : IsModularLattice α
inst✝ : ComplementedLattice α
h : IsAtomic α
⊢ IsStronglyCoatomic α

Tactic:
rw [isAtomic_iff_isCoatomic] at h

Result:
α : Type u_2
inst✝³ : Lattice α
inst✝² : BoundedOrder α
inst✝¹ : IsModularLattice α
inst✝ : ComplementedLattice α
h : IsCoatomic α
⊢ IsStronglyCoatomic α

Proof state:
α : Type u_2
inst✝³ : Lattice α
inst✝² : BoundedOrder α
inst✝¹ : IsModularLattice α
inst✝ : ComplementedLattice α
h : IsCoatomic α
⊢ IsStronglyCoatomic α

Tactic:
exact isStronglyCoatomic

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See also `inv_lt_of_inv_lt₀` for a one-sided implication with one fewer assumption. -/
lemma inv_lt_comm₀ (ha : 0 < a) (hb : 0 < b) : a⁻¹ < b ↔ b⁻¹ < a

Proof state:
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : PartialOrder G₀
inst✝³ : ZeroLEOneClass G₀
inst✝² : PosMulReflectLT G₀
a b : G₀
inst✝¹ : MulPosStrictMono G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
hb : 0 < b
⊢ a⁻¹ < b ↔ b⁻¹ < a

Tactic:
rw [← inv_lt_inv₀ hb (inv_pos.2 ha), inv_inv]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
@[simp] lemma locallyLinear_comap {G : SimpleGraph β} {e : α ≃ β} :
    (G.comap e).LocallyLinear ↔ G.LocallyLinear

Proof state:
case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
h : (SimpleGraph.comap (⇑e) G).LocallyLinear
⊢ G.LocallyLinear

Tactic:
rw [← comap_map_eq e.symm.toEmbedding G, comap_symm, map_symm]

Result:
case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
h : (SimpleGraph.comap (⇑e) G).LocallyLinear
⊢ (SimpleGraph.map e.toEmbedding (SimpleGraph.comap (⇑e.toEmbedding) G)).LocallyLinear

Proof state:
case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
h : (SimpleGraph.comap (⇑e) G).LocallyLinear
⊢ (SimpleGraph.map e.toEmbedding (SimpleGraph.comap (⇑e.toEmbedding) G)).LocallyLinear

Tactic:
exact h.map _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ (SimpleGraph.comap (⇑e) G).LocallyLinear ↔ G.LocallyLinear

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
h : (SimpleGraph.comap (⇑e) G).LocallyLinear
⊢ G.LocallyLinear

case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ G.LocallyLinear → (SimpleGraph.comap (⇑e) G).LocallyLinear

Proof state:
case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ G.LocallyLinear → (SimpleGraph.map e.symm.toEmbedding G).LocallyLinear

Tactic:
exact LocallyLinear.map _

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ G.LocallyLinear → (SimpleGraph.comap (⇑e) G).LocallyLinear

Tactic:
rw [← Equiv.coe_toEmbedding, ← map_symm]

Result:
case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ G.LocallyLinear → (SimpleGraph.map e.symm.toEmbedding G).LocallyLinear
-- Mathlib/Probability/Independence/Kernel.lean
theorem iIndepSet.indep_generateFrom_lt [Preorder ι] {s : ι → Set Ω}
    (hsm : ∀ n, MeasurableSet (s n)) (hs : iIndepSet s κ μ) (i : ι) :
    Indep (generateFrom {s i}) (generateFrom { t | ∃ j < i, s j = t }) κ μ

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : Preorder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
i : ι
⊢ Indep (generateFrom {s i}) (generateFrom {t | ∃ j < i, s j = t}) κ μ

Tactic:
convert iIndepSet.indep_generateFrom_of_disjoint hsm hs {i} { j | j < i }
  (Set.disjoint_singleton_left.mpr (lt_irrefl _)) using 1

Result:
case h.e'_4
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : Preorder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
i : ι
⊢ generateFrom {s i} = generateFrom {t | ∃ n ∈ {i}, s n = t}

Proof state:
case h.e'_4
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : Preorder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
i : ι
⊢ generateFrom {s i} = generateFrom {t | ∃ n ∈ {i}, s n = t}

Tactic:
simp only [Set.mem_singleton_iff, exists_prop, exists_eq_left, Set.setOf_eq_eq_singleton']

Result:
no goals