harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
lemma two_mul_card_edgeFinset : 2 * #G.edgeFinset = #(univ.filter fun (x, y) ↦ G.Adj x y)

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ 2 * #G.edgeFinset =
    #(filter
        (fun x =>
          match x with
          | (x, y) => G.Adj x y)
        univ)

Tactic:
rw [← dart_card_eq_twice_card_edges, ← card_univ]

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #univ =
    #(filter
        (fun x =>
          match x with
          | (x, y) => G.Adj x y)
        univ)

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #univ =
    #(filter
        (fun x =>
          match x with
          | (x, y) => G.Adj x y)
        univ)

Tactic:
refine card_bij' (fun d _ ↦ (d.fst, d.snd)) (fun xy h ↦ ⟨xy, (mem_filter.1 h).2⟩) ?_ ?_ ?_ ?_
  <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_add_of_nonneg (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) :
    x ^ (y + z) = x ^ y * x ^ z

Proof state:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 ≤ z
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
rcases hy.eq_or_lt with (rfl | hy)

Result:
case inl
x z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hy : 0 ≤ 0
⊢ x ^ (0 + z) = x ^ 0 * x ^ z

case inr
x y z : ℝ
hx : 0 ≤ x
hy✝ : 0 ≤ y
hz : 0 ≤ z
hy : 0 < y
⊢ x ^ (y + z) = x ^ y * x ^ z

Proof state:
case inl
x z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hy : 0 ≤ 0
⊢ x ^ (0 + z) = x ^ 0 * x ^ z

Tactic:
rw [zero_add, rpow_zero, one_mul]

Result:
no goals

Proof state:
case inr
x y z : ℝ
hx : 0 ≤ x
hy✝ : 0 ≤ y
hz : 0 ≤ z
hy : 0 < y
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
exact rpow_add' hx (ne_of_gt <| add_pos_of_pos_of_nonneg hy hz)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_lt_one {x z : ℝ} (hx1 : 0 ≤ x) (hx2 : x < 1) (hz : 0 < z) : x ^ z < 1

Proof state:
x z : ℝ
hx1 : 0 ≤ x
hx2 : x < 1
hz : 0 < z
⊢ x ^ z < 1 ^ z

Tactic:
exact rpow_lt_rpow hx1 hx2 hz

Result:
no goals

Proof state:
x z : ℝ
hx1 : 0 ≤ x
hx2 : x < 1
hz : 0 < z
⊢ x ^ z < 1

Tactic:
rw [← one_rpow z]

Result:
x z : ℝ
hx1 : 0 ≤ x
hx2 : x < 1
hz : 0 < z
⊢ x ^ z < 1 ^ z
-- Mathlib/MeasureTheory/Measure/MutuallySingular.lean
theorem sum_left {ι : Type*} [Countable ι] {μ : ι → Measure α} : sum μ ⟂ₘ ν ↔ ∀ i, μ i ⟂ₘ ν

Proof state:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
⊢ sum μ ⟂ₘ ν ↔ ∀ (i : ι), μ i ⟂ₘ ν

Tactic:
refine ⟨fun h i => h.mono (le_sum _ _) le_rfl, fun H => ?_⟩

Result:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
H : ∀ (i : ι), μ i ⟂ₘ ν
⊢ sum μ ⟂ₘ ν

Proof state:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsν : ∀ (i : ι), ν (s i)ᶜ = 0
⊢ ∀ (i : ι), (μ i) (⋂ b, s b) = 0

Tactic:
exact fun i => measure_mono_null (iInter_subset _ _) (hsμ i)

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsν : ∀ (i : ι), ν (s i)ᶜ = 0
⊢ sum μ ⟂ₘ ν

Tactic:
refine ⟨⋂ i, s i, MeasurableSet.iInter hsm, ?_, ?_⟩

Result:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsν : ∀ (i : ι), ν (s i)ᶜ = 0
⊢ (sum μ) (⋂ i, s i) = 0

case refine_2
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsν : ∀ (i : ι), ν (s i)ᶜ = 0
⊢ ν (⋂ i, s i)ᶜ = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
H : ∀ (i : ι), μ i ⟂ₘ ν
⊢ sum μ ⟂ₘ ν

Tactic:
choose s hsm hsμ hsν using H

Result:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsν : ∀ (i : ι), ν (s i)ᶜ = 0
⊢ sum μ ⟂ₘ ν

Proof state:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsν : ∀ (i : ι), ν (s i)ᶜ = 0
⊢ ν (⋂ i, s i)ᶜ = 0

Tactic:
rwa [compl_iInter, measure_iUnion_null_iff]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsν : ∀ (i : ι), ν (s i)ᶜ = 0
⊢ (sum μ) (⋂ i, s i) = 0

Tactic:
rw [sum_apply _ (MeasurableSet.iInter hsm), ENNReal.tsum_eq_zero]

Result:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsν : ∀ (i : ι), ν (s i)ᶜ = 0
⊢ ∀ (i : ι), (μ i) (⋂ b, s b) = 0
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
@[simp]
lemma hurwitzEvenFEPair_neg (a : UnitAddCircle) : hurwitzEvenFEPair (-a) = hurwitzEvenFEPair a

Proof state:
a : UnitAddCircle
⊢ { f := ofReal ∘ evenKernel (-a), g := ofReal ∘ cosKernel (-a), k := 1 / 2, ε := 1, f₀ := if -a = 0 then 1 else 0,
      g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair.proof_4, hε := hurwitzEvenFEPair.proof_5, h_feq := ⋯,
      hf_top := ⋯, hg_top := ⋯ } =
    { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1, f₀ := if a = 0 then 1 else 0, g₀ := 1,
      hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair.proof_4, hε := hurwitzEvenFEPair.proof_5, h_feq := ⋯,
      hf_top := ⋯, hg_top := ⋯ }

Tactic:
congr 1 <;> simp [Function.comp_def]

Result:
no goals

Proof state:
a : UnitAddCircle
⊢ hurwitzEvenFEPair (-a) = hurwitzEvenFEPair a

Tactic:
unfold hurwitzEvenFEPair

Result:
a : UnitAddCircle
⊢ { f := ofReal ∘ evenKernel (-a), g := ofReal ∘ cosKernel (-a), k := 1 / 2, ε := 1, f₀ := if -a = 0 then 1 else 0,
      g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair.proof_4, hε := hurwitzEvenFEPair.proof_5, h_feq := ⋯,
      hf_top := ⋯, hg_top := ⋯ } =
    { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1, f₀ := if a = 0 then 1 else 0, g₀ := 1,
      hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair.proof_4, hε := hurwitzEvenFEPair.proof_5, h_feq := ⋯,
      hf_top := ⋯, hg_top := ⋯ }
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem inv_Iio₀ {a : α} (ha : a < 0) : (Iio a)⁻¹ = Ioo a⁻¹ 0

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a < 0
⊢ (Iio a)⁻¹ = Ioo a⁻¹ 0

Tactic:
rw [inv_eq_iff_eq_inv, inv_Ioo_0_right (inv_neg''.2 ha), inv_inv]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem lt_tsub_iff_left_of_le (hc : AddLECancellable c) (h : c ≤ b) :
    a < b - c ↔ c + a < b

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ a + c < b

Tactic:
exact hc.lt_tsub_iff_right_of_le h

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ c + a < b

Tactic:
rw [add_comm]

Result:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ a + c < b
-- Mathlib/Algebra/Group/Pi/Basic.lean
theorem elim_div_div [Div γ] : Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
⊢ Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b'

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
x : α ⊕ β
⊢ Sum.elim (a / a') (b / b') x = (Sum.elim a b / Sum.elim a' b') x

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
x : α ⊕ β
⊢ Sum.elim (a / a') (b / b') x = (Sum.elim a b / Sum.elim a' b') x

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
lemma ramificationIdx_map_eq [Algebra R S] {E : Type*} [EquivLike E S S₁] [AlgEquivClass E R S S₁]
    (P : Ideal S) (e : E) :
    ramificationIdx (algebraMap R S₁) p (P.map e) = ramificationIdx (algebraMap R S) p P

Proof state:
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
p : Ideal R
S₁ : Type u_1
inst✝⁴ : CommRing S₁
inst✝³ : Algebra R S₁
inst✝² : Algebra R S
E : Type u_2
inst✝¹ : EquivLike E S S₁
inst✝ : AlgEquivClass E R S S₁
P : Ideal S
e : E
⊢ ramificationIdx (algebraMap R S₁) p (map e P) = ramificationIdx (algebraMap R S) p P

Tactic:
rw [show P.map e = _ from P.map_comap_of_equiv (e : S ≃+* S₁)]

Result:
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
p : Ideal R
S₁ : Type u_1
inst✝⁴ : CommRing S₁
inst✝³ : Algebra R S₁
inst✝² : Algebra R S
E : Type u_2
inst✝¹ : EquivLike E S S₁
inst✝ : AlgEquivClass E R S S₁
P : Ideal S
e : E
⊢ ramificationIdx (algebraMap R S₁) p (comap (↑e).symm P) = ramificationIdx (algebraMap R S) p P

Proof state:
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
p : Ideal R
S₁ : Type u_1
inst✝⁴ : CommRing S₁
inst✝³ : Algebra R S₁
inst✝² : Algebra R S
E : Type u_2
inst✝¹ : EquivLike E S S₁
inst✝ : AlgEquivClass E R S S₁
P : Ideal S
e : E
⊢ ramificationIdx (algebraMap R S₁) p (comap (↑e).symm P) = ramificationIdx (algebraMap R S) p P

Tactic:
exact p.ramificationIdx_comap_eq (e : S ≃ₐ[R] S₁).symm P

Result:
no goals
-- Mathlib/Order/BooleanGenerators.lean
lemma sSup_le_sSup_iff_of_atoms (hS : BooleanGenerators S) (X Y : Set α) (hX : X ⊆ S) (hY : Y ⊆ S) :
    sSup X ≤ sSup Y ↔ X ⊆ Y

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
X Y : Set α
hX : X ⊆ S
hY : Y ⊆ S
h : sSup X ≤ sSup Y
a : α
ha : a ∈ X
⊢ a ∈ Y

Tactic:
apply (hS.mono hY).mem_of_isAtom_of_le_sSup_atoms _ _ ((le_sSup ha).trans h)

Result:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
X Y : Set α
hX : X ⊆ S
hY : Y ⊆ S
h : sSup X ≤ sSup Y
a : α
ha : a ∈ X
⊢ IsAtom a

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
X Y : Set α
hX : X ⊆ S
hY : Y ⊆ S
⊢ sSup X ≤ sSup Y → X ⊆ Y

Tactic:
intro h a ha

Result:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
X Y : Set α
hX : X ⊆ S
hY : Y ⊆ S
h : sSup X ≤ sSup Y
a : α
ha : a ∈ X
⊢ a ∈ Y

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
X Y : Set α
hX : X ⊆ S
hY : Y ⊆ S
⊢ sSup X ≤ sSup Y ↔ X ⊆ Y

Tactic:
refine ⟨?_, sSup_le_sSup⟩

Result:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
X Y : Set α
hX : X ⊆ S
hY : Y ⊆ S
⊢ sSup X ≤ sSup Y → X ⊆ Y

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
X Y : Set α
hX : X ⊆ S
hY : Y ⊆ S
h : sSup X ≤ sSup Y
a : α
ha : a ∈ X
⊢ IsAtom a

Tactic:
exact (hS.mono hX).isAtom a ha

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean
/-- The relation used to construct colimits in types for `J : SingleObj G ⥤ Type u` is
equivalent to the `MulAction.orbitRel` equivalence relation on `J.obj (SingleObj.star G)`. -/
lemma Types.Quot.Rel.iff_orbitRel (x y : J.obj (SingleObj.star G)) :
    Types.Quot.Rel J ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩
    ↔ MulAction.orbitRel G (J.obj (SingleObj.star G)) x y

Proof state:
G : Type v
inst✝ : Group G
J : SingleObj G ⥤ Type u
x y : J.obj (SingleObj.star G)
⊢ Types.Quot.Rel J ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩ ↔ (MulAction.orbitRel G (J.obj (SingleObj.star G))) x y

Tactic:
have h (g : G) : y = g • x ↔ g • x = y := ⟨symm, symm⟩

Result:
G : Type v
inst✝ : Group G
J : SingleObj G ⥤ Type u
x y : J.obj (SingleObj.star G)
h : ∀ (g : G), y = g • x ↔ g • x = y
⊢ Types.Quot.Rel J ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩ ↔ (MulAction.orbitRel G (J.obj (SingleObj.star G))) x y

Proof state:
G : Type v
inst✝ : Group G
J : SingleObj G ⥤ Type u
x y : J.obj (SingleObj.star G)
h : ∀ (g : G), y = g • x ↔ g • x = y
⊢ (∃ g, y = g • x) ↔ ∃ g, g • x = y

Tactic:
conv => lhs; simp only [h]

Result:
no goals

Proof state:
G : Type v
inst✝ : Group G
J : SingleObj G ⥤ Type u
x y : J.obj (SingleObj.star G)
h : ∀ (g : G), y = g • x ↔ g • x = y
⊢ Types.Quot.Rel J ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩ ↔ (MulAction.orbitRel G (J.obj (SingleObj.star G))) y x

Tactic:
show (∃ g : G, y = g • x) ↔ (∃ g : G, g • x = y)

Result:
G : Type v
inst✝ : Group G
J : SingleObj G ⥤ Type u
x y : J.obj (SingleObj.star G)
h : ∀ (g : G), y = g • x ↔ g • x = y
⊢ (∃ g, y = g • x) ↔ ∃ g, g • x = y

Proof state:
G : Type v
inst✝ : Group G
J : SingleObj G ⥤ Type u
x y : J.obj (SingleObj.star G)
h : ∀ (g : G), y = g • x ↔ g • x = y
⊢ Types.Quot.Rel J ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩ ↔ (MulAction.orbitRel G (J.obj (SingleObj.star G))) x y

Tactic:
conv => rhs; rw [Setoid.comm']

Result:
G : Type v
inst✝ : Group G
J : SingleObj G ⥤ Type u
x y : J.obj (SingleObj.star G)
h : ∀ (g : G), y = g • x ↔ g • x = y
⊢ Types.Quot.Rel J ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩ ↔ (MulAction.orbitRel G (J.obj (SingleObj.star G))) y x
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem gcd_mul_left [NormalizedGCDMonoid α] (a b c : α) :
    gcd (a * b) (a * c) = normalize a * gcd b c :=
  (by_cases (by rintro rfl; simp only [zero_mul, gcd_zero_left, normalize_zero]))
    fun ha : a ≠ 0 =>
    suffices gcd (a * b) (a * c) = normalize (a * gcd b c) by simpa
    let ⟨d, eq⟩ := dvd_gcd (dvd_mul_right a b) (dvd_mul_right a c)
    gcd_eq_normalize
      (eq.symm ▸ mul_dvd_mul_left a
        (show d ∣ gcd b c from
          dvd_gcd ((mul_dvd_mul_iff_left ha).1 <| eq ▸ gcd_dvd_left _ _)
            ((mul_dvd_mul_iff_left ha).1 <| eq ▸ gcd_dvd_right _ _)))
      (dvd_gcd (mul_dvd_mul_left a <| gcd_dvd_left _ _) (mul_dvd_mul_left a <| gcd_dvd_right _ _))

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
b c : α
⊢ gcd (0 * b) (0 * c) = normalize 0 * gcd b c

Tactic:
simp only [zero_mul, gcd_zero_left, normalize_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b c : α
ha : a ≠ 0
this : gcd (a * b) (a * c) = normalize (a * gcd b c)
⊢ gcd (a * b) (a * c) = normalize a * gcd b c

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b c : α
⊢ a = 0 → gcd (a * b) (a * c) = normalize a * gcd b c

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
b c : α
⊢ gcd (0 * b) (0 * c) = normalize 0 * gcd b c
-- Mathlib/Analysis/Convex/Cone/Proper.lean
theorem hyperplane_separation_of_nmem (K : ProperCone ℝ E) {f : E →L[ℝ] F} {b : F}
    (disj : b ∉ K.map f) : ∃ y : F, adjoint f y ∈ K.dual ∧ ⟪y, b⟫_ℝ < 0

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
disj : ∀ (y : F), (adjoint f) y ∈ K.dual → 0 ≤ ⟪y, b⟫_ℝ
⊢ b ∈ map f K

Tactic:
rwa [K.hyperplane_separation]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
disj : b ∉ map f K
⊢ ∃ y, (adjoint f) y ∈ K.dual ∧ ⟪y, b⟫_ℝ < 0

Tactic:
contrapose! disj

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
disj : ∀ (y : F), (adjoint f) y ∈ K.dual → 0 ≤ ⟪y, b⟫_ℝ
⊢ b ∈ map f K
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_sub_int' [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b]
    (f : F) (x : G) (n : ℤ) : f (x - n) = f x - n • b

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
x : G
n : ℤ
⊢ f (x - ↑n) = f x - n • b

Tactic:
rw [← map_sub_zsmul, zsmul_one]

Result:
no goals
-- Mathlib/Analysis/Matrix.lean
theorem frobenius_nnnorm_map_eq (A : Matrix m n α) (f : α → β) (hf : ∀ a, ‖f a‖₊ = ‖a‖₊) :
    ‖A.map f‖₊ = ‖A‖₊

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
A : Matrix m n α
f : α → β
hf : ∀ (a : α), ‖f a‖₊ = ‖a‖₊
⊢ ‖A.map f‖₊ = ‖A‖₊

Tactic:
simp_rw [frobenius_nnnorm_def, Matrix.map_apply, hf]

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
lemma odd_sub' : Odd (m - n) ↔ (Odd n ↔ Even m)

Proof state:
m n : ℤ
⊢ Odd (m - n) ↔ (Odd n ↔ Even m)

Tactic:
rw [← not_even_iff_odd, even_sub, not_iff, not_iff_comm, ← not_even_iff_odd]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
lemma charmatrix_fromBlocks :
    charmatrix (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂) =
      fromBlocks (charmatrix M₁₁) (- M₁₂.map C) (- M₂₁.map C) (charmatrix M₂₂)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M₁₁ : Matrix m m R
M₁₂ : Matrix m n R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
⊢ (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂).charmatrix = fromBlocks M₁₁.charmatrix (-M₁₂.map ⇑C) (-M₂₁.map ⇑C) M₂₂.charmatrix

Tactic:
simp only [charmatrix]

Result:
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M₁₁ : Matrix m m R
M₁₂ : Matrix m n R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
⊢ (scalar (m ⊕ n)) X - C.mapMatrix (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂) =
    fromBlocks ((scalar m) X - C.mapMatrix M₁₁) (-M₁₂.map ⇑C) (-M₂₁.map ⇑C) ((scalar n) X - C.mapMatrix M₂₂)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M₁₁ : Matrix m m R
M₁₂ : Matrix m n R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
⊢ (scalar (m ⊕ n)) X - C.mapMatrix (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂) =
    fromBlocks ((scalar m) X - C.mapMatrix M₁₁) (-M₁₂.map ⇑C) (-M₂₁.map ⇑C) ((scalar n) X - C.mapMatrix M₂₂)

Tactic:
ext (i|i) (j|j) : 2 <;> simp [diagonal]

Result:
no goals
-- Mathlib/Algebra/Module/Defs.lean
theorem sub_smul (r s : R) (y : M) : (r - s) • y = r • y - s • y

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r s : R
y : M
⊢ (r - s) • y = r • y - s • y

Tactic:
simp [add_smul, sub_eq_add_neg]

Result:
no goals
-- Mathlib/RingTheory/Finiteness/Basic.lean
theorem fg_top (N : Submodule R M) : (⊤ : Submodule R N).FG ↔ N.FG :=
  ⟨fun h => N.range_subtype ▸ map_top N.subtype ▸ h.map _, fun h =>
    fg_of_fg_map_injective N.subtype Subtype.val_injective <| by rwa [map_top, range_subtype]⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
h : N.FG
⊢ (map N.subtype ⊤).FG

Tactic:
rwa [map_top, range_subtype]

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Basic.lean
lemma quasiIso_eq_subcategoryAcyclic_W :
    quasiIso C (ComplexShape.up ℤ) = (subcategoryAcyclic C).W

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ quasiIso C (ComplexShape.up ℤ) = (subcategoryAcyclic C).W

Tactic:
ext K L f

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
K L : HomotopyCategory C (ComplexShape.up ℤ)
f : K ⟶ L
⊢ quasiIso C (ComplexShape.up ℤ) f ↔ (subcategoryAcyclic C).W f

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
K L : HomotopyCategory C (ComplexShape.up ℤ)
f : K ⟶ L
⊢ quasiIso C (ComplexShape.up ℤ) f ↔ (subcategoryAcyclic C).W f

Tactic:
exact ((homologyFunctor C (ComplexShape.up ℤ) 0).mem_homologicalKernel_W_iff f).symm

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem SSameSide.not_wOppSide {s : AffineSubspace R P} {x y : P} (h : s.SSameSide x y) :
    ¬s.WOppSide x y

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
h : s.SSameSide x y
⊢ ¬s.WOppSide x y

Tactic:
intro ho

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
h : s.SSameSide x y
ho : s.WOppSide x y
⊢ False

Proof state:
case inr
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
h : s.SSameSide x y
ho : s.WOppSide x y
hy : y ∈ s
⊢ False

Tactic:
exact h.2.2 hy

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
h : s.SSameSide x y
ho : s.WOppSide x y
hxy : x ∈ s ∨ y ∈ s
⊢ False

Tactic:
rcases hxy with (hx | hy)

Result:
case inl
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
h : s.SSameSide x y
ho : s.WOppSide x y
hx : x ∈ s
⊢ False

case inr
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
h : s.SSameSide x y
ho : s.WOppSide x y
hy : y ∈ s
⊢ False

Proof state:
case inl
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
h : s.SSameSide x y
ho : s.WOppSide x y
hx : x ∈ s
⊢ False

Tactic:
exact h.2.1 hx

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
h : s.SSameSide x y
ho : s.WOppSide x y
⊢ False

Tactic:
have hxy := wSameSide_and_wOppSide_iff.1 ⟨h.1, ho⟩

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
h : s.SSameSide x y
ho : s.WOppSide x y
hxy : x ∈ s ∨ y ∈ s
⊢ False
-- Mathlib/Data/Real/EReal.lean
lemma sub_self_le_zero {x : EReal} : x - x ≤ 0

Proof state:
x : EReal
⊢ x - x ≤ 0

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bmex_monotone {o o' : Ordinal.{u}}
    {f : ∀ a < o, Ordinal.{max u v}} {g : ∀ a < o', Ordinal.{max u v}}
    (h : brange o f ⊆ brange o' g) : bmex.{_, v} o f ≤ bmex.{_, v} o' g :=
  mex_monotone (by rwa [range_familyOfBFamily, range_familyOfBFamily])

Proof state:
o o' : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
g : (a : Ordinal.{u}) → a < o' → Ordinal.{max u v}
h : o.brange f ⊆ o'.brange g
⊢ range (o.familyOfBFamily f) ⊆ range (o'.familyOfBFamily g)

Tactic:
rwa [range_familyOfBFamily, range_familyOfBFamily]

Result:
no goals