harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem integrable_withDensity_iff {f : α → ℝ≥0∞} (hf : Measurable f) (hflt : ∀ᵐ x ∂μ, f x < ∞)
    {g : α → ℝ} : Integrable g (μ.withDensity f) ↔ Integrable (fun x => g x * (f x).toReal) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ
⊢ (fun x => g x * (f x).toReal) = fun x => (f x).toReal • g x

Tactic:
simp [mul_comm]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ
⊢ Integrable g (μ.withDensity f) ↔ Integrable (fun x => g x * (f x).toReal) μ

Tactic:
have : (fun x => g x * (f x).toReal) = fun x => (f x).toReal • g x := by simp [mul_comm]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ
this : (fun x => g x * (f x).toReal) = fun x => (f x).toReal • g x
⊢ Integrable g (μ.withDensity f) ↔ Integrable (fun x => g x * (f x).toReal) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ
this : (fun x => g x * (f x).toReal) = fun x => (f x).toReal • g x
⊢ Integrable g (μ.withDensity f) ↔ Integrable (fun x => g x * (f x).toReal) μ

Tactic:
rw [this]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ
this : (fun x => g x * (f x).toReal) = fun x => (f x).toReal • g x
⊢ Integrable g (μ.withDensity f) ↔ Integrable (fun x => (f x).toReal • g x) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ
this : (fun x => g x * (f x).toReal) = fun x => (f x).toReal • g x
⊢ Integrable g (μ.withDensity f) ↔ Integrable (fun x => (f x).toReal • g x) μ

Tactic:
exact integrable_withDensity_iff_integrable_smul' hf hflt

Result:
no goals
-- Mathlib/Algebra/CharP/Defs.lean
lemma exists' (R : Type*) [NonAssocRing R] [NoZeroDivisors R] [Nontrivial R] :
    CharZero R ∨ ∃ p : ℕ, Fact p.Prime ∧ CharP R p

Proof state:
case intro
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
p : ℕ
hchar : CharP R p
⊢ CharZero R ∨ ∃ p, Fact (Nat.Prime p) ∧ CharP R p

Tactic:
rcases char_is_prime_or_zero R p with h | rfl

Result:
case intro.inl
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
p : ℕ
hchar : CharP R p
h : Nat.Prime p
⊢ CharZero R ∨ ∃ p, Fact (Nat.Prime p) ∧ CharP R p

case intro.inr
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hchar : CharP R 0
⊢ CharZero R ∨ ∃ p, Fact (Nat.Prime p) ∧ CharP R p

Proof state:
case intro.inl
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
p : ℕ
hchar : CharP R p
h : Nat.Prime p
⊢ CharZero R ∨ ∃ p, Fact (Nat.Prime p) ∧ CharP R p

case intro.inr
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hchar : CharP R 0
⊢ CharZero R ∨ ∃ p, Fact (Nat.Prime p) ∧ CharP R p

Tactic:
exacts [Or.inr ⟨p, Fact.mk h, hchar⟩, Or.inl (charP_to_charZero R)]

Result:
no goals

Proof state:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ CharZero R ∨ ∃ p, Fact (Nat.Prime p) ∧ CharP R p

Tactic:
obtain ⟨p, hchar⟩ := CharP.exists R

Result:
case intro
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
p : ℕ
hchar : CharP R p
⊢ CharZero R ∨ ∃ p, Fact (Nat.Prime p) ∧ CharP R p
-- Mathlib/Algebra/Regular/Basic.lean
theorem IsRightRegular.left_of_commute {a : R}
    (ca : ∀ b, Commute a b) (h : IsRightRegular a) : IsLeftRegular a

Proof state:
R : Type u_1
inst✝ : Mul R
a : R
ca : ∀ (b : R), Commute a b
h : IsRightRegular a
⊢ IsLeftRegular a

Tactic:
simp_rw [@Commute.symm_iff R _ a] at ca

Result:
R : Type u_1
inst✝ : Mul R
a : R
h : IsRightRegular a
ca : ∀ (b : R), Commute b a
⊢ IsLeftRegular a

Proof state:
R : Type u_1
inst✝ : Mul R
a : R
h : IsRightRegular a
ca : ∀ (b : R), Commute b a
⊢ IsLeftRegular a

Tactic:
exact fun x y xy => h <| (ca x).trans <| xy.trans <| (ca y).symm

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem length_reverseAux {u v w : V} (p : G.Walk u v) (q : G.Walk u w) :
    (p.reverseAux q).length = p.length + q.length

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
⊢ (nil.reverseAux q).length = nil.length + q.length

Tactic:
simp!

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk u w
⊢ (p.reverseAux q).length = p.length + q.length

Tactic:
induction p with
| nil => simp!
| cons _ _ ih => simp [ih, Nat.succ_add, Nat.add_assoc]

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ (q : G.Walk v✝ w), (p✝.reverseAux q).length = p✝.length + q.length
q : G.Walk u✝ w
⊢ ((cons h✝ p✝).reverseAux q).length = (cons h✝ p✝).length + q.length

Tactic:
simp [ih, Nat.succ_add, Nat.add_assoc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma eval_polynomialX (P : Fin 3 → R) : eval P W'.polynomialX =
    W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P) (C W'.a₁ * X y * X z - (C 3 * X x ^ 2 + C (2 * W'.a₂) * X x * X z + C W'.a₄ * X z ^ 2)) =
    W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2)

Tactic:
eval_simp

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P) W'.polynomialX = W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2)

Tactic:
rw [polynomialX_eq]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P) (C W'.a₁ * X y * X z - (C 3 * X x ^ 2 + C (2 * W'.a₂) * X x * X z + C W'.a₄ * X z ^ 2)) =
    W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2)
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem stalkSpecializes_stalk_to_fiber {R : Type*} [CommRing R] {x y : PrimeSpectrum R}
    (h : x ⤳ y) :
    (structureSheaf R).presheaf.stalkSpecializes h ≫ StructureSheaf.stalkToFiberRingHom R x =
      StructureSheaf.stalkToFiberRingHom R y ≫
      (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h))

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (stalkIso R y).inv ≫ (structureSheaf R).presheaf.stalkSpecializes h =
    CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h) ≫ (stalkIso R x).inv

Tactic:
exact localizationToStalk_stalkSpecializes h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (structureSheaf R).presheaf.stalkSpecializes h ≫ stalkToFiberRingHom R x =
    stalkToFiberRingHom R y ≫ CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h)

Tactic:
change _ ≫ (StructureSheaf.stalkIso R x).hom = (StructureSheaf.stalkIso R y).hom ≫ _

Result:
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (structureSheaf R).presheaf.stalkSpecializes h ≫ (stalkIso R x).hom =
    (stalkIso R y).hom ≫ CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h)

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (structureSheaf R).presheaf.stalkSpecializes h ≫ (stalkIso R x).hom =
    (stalkIso R y).hom ≫ CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h)

Tactic:
rw [← Iso.eq_comp_inv, Category.assoc, ← Iso.inv_comp_eq]

Result:
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (stalkIso R y).inv ≫ (structureSheaf R).presheaf.stalkSpecializes h =
    CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h) ≫ (stalkIso R x).inv
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_smul_left_of_tower (a : S) (x y : M) : polar Q (a • x) y = a • polar Q x y

Proof state:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
Q : QuadraticMap R M N
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
a : S
x y : M
⊢ polar (⇑Q) (a • x) y = a • polar (⇑Q) x y

Tactic:
rw [← IsScalarTower.algebraMap_smul R a x, polar_smul_left, algebraMap_smul]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem mem_rightTransversals_iff_existsUnique_mul_inv_mem :
    S ∈ rightTransversals T ↔ ∀ g : G, ∃! s : S, g * (s : G)⁻¹ ∈ T

Proof state:
case refine_2.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
h : ∀ (g : G), ∃! s, g * (↑s)⁻¹ ∈ T
g : G
x : ↑S
h1 : g * (↑x)⁻¹ ∈ T
h2 : ∀ (y : ↑S), (fun s => g * (↑s)⁻¹ ∈ T) y → y = x
⊢ ∃! x, ↑x.1 * ↑x.2 = g

Tactic:
refine ⟨⟨⟨g * (↑x)⁻¹, h1⟩, x⟩, inv_mul_cancel_right g x, fun y hy => ?_⟩

Result:
case refine_2.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
h : ∀ (g : G), ∃! s, g * (↑s)⁻¹ ∈ T
g : G
x : ↑S
h1 : g * (↑x)⁻¹ ∈ T
h2 : ∀ (y : ↑S), (fun s => g * (↑s)⁻¹ ∈ T) y → y = x
y : ↑T × ↑S
hy : (fun x => ↑x.1 * ↑x.2 = g) y
⊢ y = (⟨g * (↑x)⁻¹, h1⟩, x)

Proof state:
case refine_2.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
h : ∀ (g : G), ∃! s, g * (↑s)⁻¹ ∈ T
g : G
x : ↑S
h1 : g * (↑x)⁻¹ ∈ T
h2 : ∀ (y : ↑S), (fun s => g * (↑s)⁻¹ ∈ T) y → y = x
y : ↑T × ↑S
hy : (fun x => ↑x.1 * ↑x.2 = g) y
hf : y.2 = x
⊢ y = (⟨g * (↑x)⁻¹, h1⟩, x)

Tactic:
exact Prod.ext (Subtype.ext (eq_mul_inv_of_mul_eq (hf ▸ hy))) hf

Result:
no goals

Proof state:
case refine_1
G : Type u_1
inst✝ : Group G
S T : Set G
h : ∀ (g : G), ∃! x, ↑x.1 * ↑x.2 = g
g : G
⊢ ∃! s, g * (↑s)⁻¹ ∈ T

Tactic:
obtain ⟨x, h1, h2⟩ := h g

Result:
case refine_1.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
h : ∀ (g : G), ∃! x, ↑x.1 * ↑x.2 = g
g : G
x : ↑T × ↑S
h1 : ↑x.1 * ↑x.2 = g
h2 : ∀ (y : ↑T × ↑S), (fun x => ↑x.1 * ↑x.2 = g) y → y = x
⊢ ∃! s, g * (↑s)⁻¹ ∈ T

Proof state:
case refine_2
G : Type u_1
inst✝ : Group G
S T : Set G
h : ∀ (g : G), ∃! s, g * (↑s)⁻¹ ∈ T
g : G
⊢ ∃! x, ↑x.1 * ↑x.2 = g

Tactic:
obtain ⟨x, h1, h2⟩ := h g

Result:
case refine_2.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
h : ∀ (g : G), ∃! s, g * (↑s)⁻¹ ∈ T
g : G
x : ↑S
h1 : g * (↑x)⁻¹ ∈ T
h2 : ∀ (y : ↑S), (fun s => g * (↑s)⁻¹ ∈ T) y → y = x
⊢ ∃! x, ↑x.1 * ↑x.2 = g

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
⊢ (∀ (g : G), ∃! x, ↑x.1 * ↑x.2 = g) ↔ ∀ (g : G), ∃! s, g * (↑s)⁻¹ ∈ T

Tactic:
refine ⟨fun h g => ?_, fun h g => ?_⟩

Result:
case refine_1
G : Type u_1
inst✝ : Group G
S T : Set G
h : ∀ (g : G), ∃! x, ↑x.1 * ↑x.2 = g
g : G
⊢ ∃! s, g * (↑s)⁻¹ ∈ T

case refine_2
G : Type u_1
inst✝ : Group G
S T : Set G
h : ∀ (g : G), ∃! s, g * (↑s)⁻¹ ∈ T
g : G
⊢ ∃! x, ↑x.1 * ↑x.2 = g

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
⊢ S ∈ rightTransversals T ↔ ∀ (g : G), ∃! s, g * (↑s)⁻¹ ∈ T

Tactic:
rw [rightTransversals, Set.mem_setOf_eq, isComplement_iff_existsUnique]

Result:
G : Type u_1
inst✝ : Group G
S T : Set G
⊢ (∀ (g : G), ∃! x, ↑x.1 * ↑x.2 = g) ↔ ∀ (g : G), ∃! s, g * (↑s)⁻¹ ∈ T
-- Mathlib/Algebra/Order/AddGroupWithTop.lean
@[simp]
lemma top_ne_zero :
    (⊤ : α) ≠ 0

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
nh : ⊤ = 0
a b : α
h : a ≠ b
this : a + ⊤ ≠ b + ⊤
⊢ False

Tactic:
simp at this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
⊢ ⊤ ≠ 0

Tactic:
intro nh

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
nh : ⊤ = 0
⊢ False

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
nh : ⊤ = 0
a b : α
h : a ≠ b
⊢ False

Tactic:
have : a + 0 ≠ b + 0 := by simpa

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
nh : ⊤ = 0
a b : α
h : a ≠ b
this : a + 0 ≠ b + 0
⊢ False

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
nh : ⊤ = 0
a b : α
h : a ≠ b
⊢ a + 0 ≠ b + 0

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
nh : ⊤ = 0
a b : α
h : a ≠ b
this : a + 0 ≠ b + 0
⊢ False

Tactic:
rw [← nh] at this

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
nh : ⊤ = 0
a b : α
h : a ≠ b
this : a + ⊤ ≠ b + ⊤
⊢ False

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
nh : ⊤ = 0
⊢ False

Tactic:
have ⟨a, b, h⟩ := Nontrivial.exists_pair_ne (α := α)

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
nh : ⊤ = 0
a b : α
h : a ≠ b
⊢ False
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem nullHomotopicMap_f_of_not_rel_right {k₁ k₀ : ι} (r₁₀ : c.Rel k₁ k₀)
    (hk₁ : ∀ l : ι, ¬c.Rel l k₁) (hom : ∀ i j, C.X i ⟶ D.X j) :
    (nullHomotopicMap hom).f k₁ = C.d k₁ k₀ ≫ hom k₀ k₁

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (nullHomotopicMap hom).f k₁ = C.d k₁ k₀ ≫ hom k₀ k₁

Tactic:
dsimp only [nullHomotopicMap]

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (dNext k₁) hom + (prevD k₁) hom = C.d k₁ k₀ ≫ hom k₀ k₁

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (dNext k₁) hom + (prevD k₁) hom = C.d k₁ k₀ ≫ hom k₀ k₁

Tactic:
rw [dNext_eq hom r₁₀, prevD, AddMonoidHom.mk'_apply, D.shape, comp_zero, add_zero]

Result:
case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel (c.prev k₁) k₁

Proof state:
case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel (c.prev k₁) k₁

Tactic:
exact hk₁ _

Result:
no goals
-- Mathlib/Order/Filter/Pointwise.lean
theorem one_le_div_iff : 1 ≤ f / g ↔ ¬Disjoint f g

Proof state:
case refine_2.intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
f g : Filter α
h : ¬Disjoint f g
s t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
hs : t₁ / t₂ ⊆ s
⊢ s ∈ 1

Tactic:
exact hs (Set.one_mem_div_iff.2 fun ht => h <| disjoint_of_disjoint_of_mem ht h₁ h₂)

Result:
no goals

Proof state:
case refine_2
α : Type u_2
inst✝ : Group α
f g : Filter α
⊢ ¬Disjoint f g → 1 ≤ f / g

Tactic:
rintro h s ⟨t₁, h₁, t₂, h₂, hs⟩

Result:
case refine_2.intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
f g : Filter α
h : ¬Disjoint f g
s t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
hs : t₁ / t₂ ⊆ s
⊢ s ∈ 1

Proof state:
case refine_1
α : Type u_2
inst✝ : Group α
f g : Filter α
h : 1 ≤ f / g
hfg : Disjoint f g
⊢ False

Tactic:
obtain ⟨s, hs, t, ht, hst⟩ := hfg.le_bot (mem_bot : ∅ ∈ ⊥)

Result:
case refine_1.intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
f g : Filter α
h : 1 ≤ f / g
hfg : Disjoint f g
s : Set α
hs : s ∈ f
t : Set α
ht : t ∈ g
hst : ∅ = s ∩ t
⊢ False

Proof state:
α : Type u_2
inst✝ : Group α
f g : Filter α
⊢ 1 ≤ f / g ↔ ¬Disjoint f g

Tactic:
refine ⟨fun h hfg => ?_, ?_⟩

Result:
case refine_1
α : Type u_2
inst✝ : Group α
f g : Filter α
h : 1 ≤ f / g
hfg : Disjoint f g
⊢ False

case refine_2
α : Type u_2
inst✝ : Group α
f g : Filter α
⊢ ¬Disjoint f g → 1 ≤ f / g

Proof state:
case refine_1.intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
f g : Filter α
h : 1 ≤ f / g
hfg : Disjoint f g
s : Set α
hs : s ∈ f
t : Set α
ht : t ∈ g
hst : ∅ = s ∩ t
⊢ False

Tactic:
exact Set.one_mem_div_iff.1 (h <| div_mem_div hs ht) (disjoint_iff.2 hst.symm)

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem contractLeft_mul_algebraMap (a : CliffordAlgebra Q) (r : R) :
    d⌋(a * algebraMap _ _ r) = d⌋a * algebraMap _ _ r

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
a : CliffordAlgebra Q
r : R
⊢ (contractLeft d) (a * (algebraMap R (CliffordAlgebra Q)) r) =
    (contractLeft d) a * (algebraMap R (CliffordAlgebra Q)) r

Tactic:
rw [← Algebra.commutes, contractLeft_algebraMap_mul, Algebra.commutes]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Tower.lean
@[simp]
lemma baseChange_span (s : Set M) :
    (span R s).baseChange A = span A (TensorProduct.mk R A M 1 '' s)

Proof state:
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ ⇑((TensorProduct.mk R A M) 1) '' ↑(span R s) ⊆ ↑(span A (⇑((TensorProduct.mk R A M) 1) '' s))

Tactic:
rintro - ⟨m : M, hm : m ∈ span R s, rfl⟩

Result:
case intro.intro
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
hm : m ∈ span R s
⊢ ((TensorProduct.mk R A M) 1) m ∈ ↑(span A (⇑((TensorProduct.mk R A M) 1) '' s))

Proof state:
case intro.intro.add
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
hm : m ∈ span R s
m₁ m₂ : M
hx✝ : m₁ ∈ span R s
hy✝ : m₂ ∈ span R s
hm₁ : 1 ⊗ₜ[R] m₁ ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)
hm₂ : 1 ⊗ₜ[R] m₂ ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)
⊢ 1 ⊗ₜ[R] (m₁ + m₂) ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)

Tactic:
rw [tmul_add]

Result:
case intro.intro.add
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
hm : m ∈ span R s
m₁ m₂ : M
hx✝ : m₁ ∈ span R s
hy✝ : m₂ ∈ span R s
hm₁ : 1 ⊗ₜ[R] m₁ ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)
hm₂ : 1 ⊗ₜ[R] m₂ ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)
⊢ 1 ⊗ₜ[R] m₁ + 1 ⊗ₜ[R] m₂ ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)

Proof state:
case intro.intro.mem
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m✝ : M
hm✝ : m✝ ∈ span R s
m : M
hm : m ∈ s
⊢ 1 ⊗ₜ[R] m ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)

Tactic:
exact subset_span ⟨m, hm, rfl⟩

Result:
no goals

Proof state:
case intro.intro.smul
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
hm : m ∈ span R s
r : R
m' : M
hx✝ : m' ∈ span R s
hm' : 1 ⊗ₜ[R] m' ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)
⊢ (r • 1) • 1 ⊗ₜ[R] m' ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)

Tactic:
exact smul_mem _ (r • 1) hm'

Result:
no goals
-- Mathlib/RingTheory/Regular/RegularSequence.lean
lemma isRegular_cons_iff' (r : R) (rs : List R) :
    IsRegular M (r :: rs) ↔
      IsSMulRegular M r ∧ IsRegular (QuotSMulTop r M)
          (rs.map (Ideal.Quotient.mk (Ideal.span {r})))

Proof state:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
⊢ IsWeaklyRegular M (r :: rs) ∧ ¬⊤ = Ideal.ofList (r :: rs) • ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) ∧
        ¬⊤ = Ideal.ofList (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) • ⊤

Tactic:
rw [isWeaklyRegular_cons_iff', ← restrictScalars_inj R (R ⧸ _),
  ← Ideal.map_ofList, ← Ideal.Quotient.algebraMap_eq, Ideal.smul_restrictScalars,
  restrictScalars_top, top_eq_ofList_cons_smul_iff, and_assoc]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
⊢ IsRegular M (r :: rs) ↔
    IsSMulRegular M r ∧ IsRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)

Tactic:
conv => congr <;> rw [isRegular_iff, ne_eq]

Result:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
⊢ IsWeaklyRegular M (r :: rs) ∧ ¬⊤ = Ideal.ofList (r :: rs) • ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) ∧
        ¬⊤ = Ideal.ofList (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) • ⊤
-- Mathlib/Topology/Bases.lean
theorem IsTopologicalBasis.sigma {s : ∀ i : ι, Set (Set (E i))}
    (hs : ∀ i, IsTopologicalBasis (s i)) :
    IsTopologicalBasis (⋃ i : ι, (fun u => (Sigma.mk i '' u : Set (Σi, E i))) '' s i)

Proof state:
case h.e'_4.h.a
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
a : (i : ι) × E i
x✝ : Set ((i : ι) × E i)
⊢ x✝ ∈ ⋃ i, (fun u => Sigma.mk i '' u) '' s i ∧ a ∈ x✝ ↔
    x✝ ∈ (fun i => Sigma.mk a.fst '' i) '' {i | i ∈ s a.fst ∧ a.snd ∈ i}

Tactic:
aesop

Result:
no goals

Proof state:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
a : (i : ι) × E i
⊢ (𝓝 a).HasBasis (fun t => t ∈ ⋃ i, (fun u => Sigma.mk i '' u) '' s i ∧ a ∈ t) id

Tactic:
rw [Sigma.nhds_eq]

Result:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
a : (i : ι) × E i
⊢ (map (Sigma.mk a.fst) (𝓝 a.snd)).HasBasis (fun t => t ∈ ⋃ i, (fun u => Sigma.mk i '' u) '' s i ∧ a ∈ t) id

Proof state:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
a : (i : ι) × E i
⊢ (map (Sigma.mk a.fst) (𝓝 a.snd)).HasBasis (fun t => t ∈ ⋃ i, (fun u => Sigma.mk i '' u) '' s i ∧ a ∈ t) id

Tactic:
convert (((hs a.1).nhds_hasBasis).map _).to_image_id

Result:
case h.e'_4.h.a
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
a : (i : ι) × E i
x✝ : Set ((i : ι) × E i)
⊢ x✝ ∈ ⋃ i, (fun u => Sigma.mk i '' u) '' s i ∧ a ∈ x✝ ↔
    x✝ ∈ (fun i => Sigma.mk a.fst '' i) '' {i | i ∈ s a.fst ∧ a.snd ∈ i}

Proof state:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
⊢ IsTopologicalBasis (⋃ i, (fun u => Sigma.mk i '' u) '' s i)

Tactic:
refine .of_hasBasis_nhds fun a ↦ ?_

Result:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
a : (i : ι) × E i
⊢ (𝓝 a).HasBasis (fun t => t ∈ ⋃ i, (fun u => Sigma.mk i '' u) '' s i ∧ a ∈ t) id